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

Question

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



在论文中，他们说他们在这里是为了确保第二个上下文(E2)是最大的，即它包括所有的事件捕获。但是我不完全理解它的含义。是不是表示如果有catch就不会抛出异常？在第二个线程内？但是为什么 bind 也在那里呢？

Answer 1

直观地说，它用于“插入”异常 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

在前一种情况下，错误不会被捕获，在后一种情况下是这样。附带条件确保只有后者是有效步骤。

Bind 也可以避免替换以下内容:

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

在这里，如果您只需要“ M 而不是捕获”，您可以再次选择 M = Ea[M]并替换所有代码。相反，附带条件迫使您选择

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

并插入 ioError e在 catch 内的正确位置.