我看过 "对付尴尬的小队" SPJ的论文,大部分内容很容易理解,但是我没有完全理解分离线上面的那两个条件到底是什么意思。
在论文中说,它们是为了确保第二个上下文(E2)是最大的,也就是说,它包括了所有的主动捕获。然而我并不完全理解它的意思。它是否意味着如果有一个异常,就不会抛出 catch
在第二个线程里面?但是为什么bind也在那里呢?
直观地说,它是用来 "插入 "异常的 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
.