catch违反了语义逼近顺序？

Question

语义近似顺序表明,如果函数f是在其参数不是一个函数时定义的,那么f在该参数中它是常量(它不使用它).但考虑这个功能,

import Control.Exception

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

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

f undefinedcaught在GHCi中显示,因此它看起来很明确.但是f在它的论证中并不是恒定的,因为f "test"显示test.

某处有错误吗？

Answer 1

为了对异常进行catch正确建模,你需要一个更丰富的术语指称语义,以区分异常和不终止(并区分不同的异常).请参阅GHC实现的语义的不精确异常(pdf)的语义.

请注意,这对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操作时发生的事情毫无用处.但是如果你想在指称语义中对待它,除了异常之外你还会遇到很多困难.