haskell - catch 违反语义近似顺序？

Question

语义近似顺序表明，如果函数 f当一个参数不是时定义，然后 f在该参数中是常量(它不使用它)。但是考虑这个函数，

import Control.Exception

handleAll :: SomeException -> IO ()
handleAll e = putStrLn "caught"

f :: String -> IO ()
f x = catch (putStrLn x) handleAll

f undefined显示 caught在 GHCi 中，所以它看起来很明确。然而 f它的参数不是常数，因为 f "test"显示 test .

某处有错误吗？

Answer 1

模拟异常和 catch正确地，您需要更丰富的术语指称语义，将异常与非终止区分开来(并将不同的异常区分开来)。见 A semantics for imprecise exceptions (pdf)对于 GHC 实现的语义。

请注意，这对 Haskell 的“纯片段”的指称语义没有影响，因为您无法观察 IO a 之间的区别。纯代码中的值(除了底部与非底部)。

为了澄清我所说的 Haskell 的“纯片段”是什么意思，想象一下定义 IO输入为

data IO a = MkIO

和 catch作为

catch a h = MkIO

现在您的 f 没有问题了, 因为两者都是 f undefined和 f "test"等于 MkIO .从指称语义的角度来看，这对应于解释

[[IO t]] = {⊥ < ⊤}

由于我们可以对 IO 操作进行的唯一操作是 seq将它们合并到其他 IO 操作中，这是一种完全一致的指称语义，不会影响您谈论诸如 length :: [Bool] -> Integer 之类的事物的语义的能力。 .它恰好对理解执行 IO 操作时发生的情况毫无用处。但是，如果您想在指称语义中处理它，除了异常(exception)，您还会遇到许多困难。