Операционная семантика для выброса исключений в другие потоки в Haskell - PullRequest
Новая
       27

Операционная семантика для выброса исключений в другие потоки в Haskell

5 голосов
/ 23 апреля 2020

Я прочитал "Борьба с неуклюжим отрядом" от SPJ, и большую часть этого было довольно легко понять, однако я не до конца понимал, что именно означают эти два условия над разделительной линией:

throwTo semantics

В документе указывается, что они здесь для того, чтобы гарантировать, что второй контекст (E2) максимален, то есть включает все активные захваты. Однако я не совсем понимаю, что это значит. Означает ли это, что исключение не будет выдано, если во втором потоке есть catch? Но почему же тогда связывается там?

1 Ответ

4 голосов
/ 23 апреля 2020

Интуитивно, он используется для «вставки» исключения ioError e в нужное место, детерминистически c.

Рассмотрим M = catch (threadDelay 1000000) someHandler. У нас есть оба: 

M = Ea[M]
   where Ea[x] = x
M = Eb[M']
   where Eb[x] = catch x someHandler
         M' = threadDelay 1000000

без побочного условия, у нас было бы два отдельных операционных шага, делая семантику недетерминированной c: 

{throwTo t e}s | {M}t ==> {return ()}s | {Ea[ioError e]}t
                        = {return ()}s | {ioError e}t
{throwTo t e}s | {M}t ==> {return ()}s | {Eb[ioError e]}t
                        = {return ()}s | {catch (ioError e) someHandler}t

В первом случае ошибка не ловится, в последнем она есть. Боковое условие гарантирует, что только последний является допустимым шагом.

Привязка также существует, чтобы избежать замены всего в: 

M = catch (threadDelay 1000000) someHandler >>= something

Здесь, если вам требуется только "M, а не поймать ", вы можете снова выбрать M = Ea[M] и заменить весь код. Вместо этого боковое условие заставляет вас выбрать 

Ec[x] = catch x someHandler >>= something

и вставить ioError e в правильное место внутри catch.

...