catch违反了语义逼近顺序？

语义近似顺序规定，如果函数f是在其参数不是其中的一个时定义的，那么f在该参数中是常量（它不使用它）。但考虑这个功能，catch违反了语义逼近顺序？

import Control.Exception 

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

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

f undefined显示在GHCI caught，所以看起来定义。但是f在它的论点中并不是不变的，因为f "test"显示为test。

某处有错吗？

来源

2017-03-04 V. Semeria

没有错误 - 此原则仅适用于纯功能。（注意，即使这是不正确的，由于seq和朋友）。你只能看到区别，因为你正在执行'IO'动作，'技术上'只能在'main'中使用' - 所有其他的'IO'操作只是建立新的术语，或者你不能观察术语输入'IO x'。 – user2407038

'seq'不违反这里讨论的原则。 –

'catch'事实上很难找到正确的答案。实际上，我在过去的一两周内一直在努力修复相关的GHC错误。 – dfeuer

为了正确建模异常和catch，术语需要更丰富的指称语义，区分异常和非定义（并区分不同的异常）。有关GHC实现的语义，请参阅A semantics for imprecise exceptions (pdf)。

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

要澄清我的哈斯克尔的“纯片段”的意思是，想象定义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操作时发生的情况恰好是没用的。但是如果你想用指称语义来对待它，除了例外之外，你会遇到很多困难。

来源

2017-03-04 16:25:51

如果你写的只有一个'IO a'（只有一个构造函数'MkIO'没有参数），编译器会优化'f'，强制它不变，等于这个唯一'IO a'。 GHCi的执行结果表明，这并非如此。我从文章中了解到不准确的例外情况，GHC区分了几种底部：可以捕捉的底部，其他底部，如无限循环，不能。我想知道如何通过库里霍华德翻译，底部与数学错误有关，只有一个。 –

当然，我明确指出，这种指称语义（异常识别为非终止，IO视为单例）并不能帮助您预测执行IO操作时会发生什么情况。 –

catch违反了语义逼近顺序？

回答

相关问题