GHC 的 Haskell 实现是否在语义上被破坏了？答案

【问题标题】：is GHC's implementation of Haskell semantically broken?GHC 的 Haskell 实现是否在语义上被破坏了？
【发布时间】：2013-07-13 07:39:35
【问题描述】：

今天早上我注意到一些有趣的事情，我想问一下它是否重要。

所以在 Haskell 中，未定义语义包含非终止。所以应该是不可能有函数的

isUndefined :: a -> Bool

因为语义表明这解决了停机问题。

但是，我相信 GHC 的一些内置函数可以“相当可靠地”打破这一限制。尤其是catch#。

以下代码允许“相当可靠地”检测未定义的值：

import Control.Exception
import System.IO.Unsafe
import Unsafe.Coerce

isUndefined :: a -> Bool
isUndefined x = unsafePerformIO $ catch ((unsafeCoerce x :: IO ()) >> return False) ((\e -> return $ show e == "Prelude.undefined") :: SomeException -> IO Bool)

另外，这真的算吗，因为您会注意到它使用了几个“不安全”的功能？

朱尔斯

编辑：有些人似乎认为我声称已经解决了停机问题 XD 我不是一个怪人。我只是说 undefined 的语义有一个相当严重的中断，因为他们声明 undefined 的值应该在某种意义上与非终止没有区别。这个功能允许的。我只是想检查一下人们是否同意这一点以及人们对此有何看法，在 Haskell 的 GHC 实现中为了方便而添加某些不安全功能的意外副作用是不是更进一步？ :)

编辑：修复了要编译的代码

【问题讨论】：

当然，当你在代码中输入unsafe这个词时，各种东西都可能会被破坏！
还有一个错误的假设：停止问题确实不说明您无法检测到非终止，它只是说您不能为每个程序。您的 isUndefined 函数绝对不会在 x 的所有可能值上终止
是的，GHC 中的undefined 已“损坏”，但已损坏得很好。在 99% 的情况下，以这种方式实现 undefined 在语义上是等效的，如果你使用 unsafe* 函数，你已经进入了黑魔法
您使用的是哪个版本？这甚至不适合我。
@AndrewC：对不起，这更像是一个理论问题，我在提交之前没有测试代码，这只是一个想法。我已经对其进行了编辑，现在它应该可以在 GHC 7.6.3 上编译。

标签： haskell semantics ghc

【解决方案1】：

来自the docs：

高度不安全的原语unsafeCoerce 将值从任何类型转换为任何其他类型。不用说，如果您使用此功能，您有责任确保新旧类型具有相同的内部表示，以防止运行时损坏。

它显然也破坏了引用透明度，因此纯粹，所以你放弃了 Haskell 语义给你的所有保证。

一旦你离开纯地形，就有很多方法可以让你在脚下开枪。你也可以使用操作系统原语来读取IO 中的整个进程内存，以最糟糕的方式破坏引用透明度。

除此之外，您对isUndefined 的定义没有解决了停止问题，因为它不是total，这意味着它不会全部终止输入。

例如，isUndefined (last [1..]) 不会终止。

有很多程序我们可以证明它们是否终止，但这并不意味着我们已经解决了停止问题。

【讨论】：

别担心，我不是一个怪人，我绝不声称已经解决了停机问题 :) 我完全理解为什么这段代码不能解决停机问题。我的观点是，这是对 Haskell 形式语义的严重突破。其他不安全的函数破坏了引用透明性。哪个是“坏”，但不像这个那么“坏”。
@Julian：那么语义上的中断是什么？我认为你的论点是你可以编写一个检测非终止的函数（你显然不能）。 undefined 只是在IO monad 中很容易检测到的非终止的一个具体例子，如果你想这样解释它
Haskell 的形式语义表明 undefined 包含终止，因此 undefined 的值在某种意义上应该与非终止没有区别。然而，在语言的 GHC 实现的不安全部分中，这是可能的。这是与语义的突破，这可能是其他不安全函数的无意副作用，这些函数本身是为了方便而添加的。
@Julien：你的第一句话是基于什么（“底部包含非终止”）？这是 Haskell 标准的一部分吗？
找到它：haskell.org/onlinereport/haskell2010/… 那么你的问题的正确答案是：unsafeCoerce 不是安全 Haskell 的一部分，所以你只能在 IO 中捕获错误

【解决方案2】：

我想提出三点，ah, no，四点（相互关联）。

不，使用 unsafe... 不算数：

使用unsafeCoerce 显然是违反规则的举动，因此要回答“这真的算数吗？”的问题：不，不算数。 unsafe 是各种东西都会破坏的警告，包括语义：
```
isGood :: a -> Bool
isGood x = unsafePerformIO . fmap read $ readFile "I_feel_like_it.txt"
```
```
> isGood '4'
True
> isGood '4'
False
```
哎呀！根据 Haskell 报告，语义被破坏。哦，不，等等，我用了unsafe...。我被警告了。

主要问题是使用unsafeCoerce，你可以用它把任何东西变成其他东西。它与命令式编程中的类型转换一样糟糕，因此所有类型安全都已经消失了。
您catch正在处理 IOException，而不是纯错误 (⊥)。

要使用 catch，您已将纯错误 undefined 转换为 IO 异常。 IO monad 看似简单，错误处理语义不需要使用⊥。可以把它想象成一个单子转换器，在某种程度上包括错误处理 Either。
与停机问题的链接完全是虚假的

我们不需要任何编程语言的任何不安全特性来导致这种区分非终止和错误。

想象两个程序。一个程序Char -> IO () 输出字符，另一个程序将第一个输出写入文件，然后将该文件与字符串"*** Exception: Prelude.undefined" 进行比较，并找到它的长度。我们可以使用输入undefined 或输入'c' 运行第一个。第一个是⊥，第二个是正常终止。

哎呀！我们通过区分未定义和非终止来解决了停止问题。哦不，等等，不，我们实际上只区分了undefined 和终止。如果我们在输入non_terminating where non_terminating = head.show.length $ [1..] 上运行这两个程序，我们会发现第二个没有终止，因为第一个没有。事实上，我们的第二个程序未能解决停机问题，因为它本身并没有终止。

停止问题的解决方案更像是有一个 total 函数 halts :: (a -> IO ()) -> a -> Bool，如果给定函数以输入终止，则 always 以输出 True 终止a 和 False 如果它永远不会终止。当您区分 undefined 和 error "user-defined error" 时，您的代码就是这样做的。

因此，您对停止问题的所有引用都混淆了决定 one 程序是否终止与决定 any 程序是否终止。如果使用上面的输入non-terminating而不是undefined，则无法得出任何结论；将其称为区分非终止和undefined 在语义上已经是一个很大的延伸，将其称为停止问题的解决方案是无稽之谈。
问题不是很大的语义问题

基本上，您的代码所能做的就是确定您的错误值是使用undefined 还是其他一些产生错误的函数产生的。语义问题是undefined 和error "not defined with undefined" 都具有语义值⊥，但您可以区分它们。好的，理论上这不是很干净，但是对于 ⊥ 的不同原因有不同的输出 so 对于调试很有用，因此强制对值 ⊥ 的共同响应是疯狂的，因为它必须始终不终止是完全正确的。

结果是任何有任何错误的程序在出现错误时都必须进入一个无限的无输出循环。这将理论上的善意带到了深深的无益的地步。最好打印 *** Exception: Prelude.undefined 或 Error: ungrokable wibbles 或其他有用的描述性错误消息。

为了在危机中提供帮助，任何编程语言都必须牺牲你让每个 ⊥ 行为相同的愿望。区分不同的⊥在理论上并不可爱，但在实践中不这样做会很愚蠢。

如果编程语言理论家称这是一个严重的语义问题，他们应该被嘲笑生活在一个程序冻结/不终止始终是无效输入的最佳结果的世界。

【讨论】：