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

问题描述 投票:0回答:1

我看过 "对付尴尬的小队" SPJ的论文,大部分内容很容易理解,但是我没有完全理解分离线上面的那两个条件到底是什么意思。

throwTo semantics

在论文中说,它们是为了确保第二个上下文(E2)是最大的,也就是说,它包括了所有的主动捕获。然而我并不完全理解它的意思。它是否意味着如果有一个异常,就不会抛出 catch 在第二个线程里面?但是为什么bind也在那里呢?

haskell semantics
1个回答
4
投票

直观地说,它是用来 "插入 "异常的 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.

© www.soinside.com 2019 - 2024. All rights reserved.