Haskell 中向其他线程抛出异常的操作语义

Question

我已经阅读了 SPJ 的 "Tackling the Awkward Squad" 论文，其中大部分内容很容易理解，但是我并不完全理解分隔线上方的两个条件到底是什么意思：

在论文中指出，它们在这里是为了确保第二个上下文 (E2) 是最大的，即它包括所有活动的捕获。但是我不完全明白这意味着什么。这是否意味着如果第二个线程中有 catch 则不会抛出异常？但是为什么 bind 也在那里呢？

Answer 1

直觉上，它用于"insert"异常ioError e在正确的地方，以一种确定的方式。

考虑 M = catch (threadDelay 1000000) someHandler。我们都有：

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

如果没有边条件，我们将有两个不同的操作步骤，使语义不确定：

{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 not a catch”，可以再次选择M = Ea[M]，替换所有代码。附带条件反而迫使您选择

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

并将 ioError e 插入 catch 中的正确位置。

Haskell 中向其他线程抛出异常的操作语义

Operational semantics for throwing exceptions to other threads in Haskell

haskell

semantics