是GHC的Haskell语义破坏的实现？
今天早上我注意到一些有趣的事情，我想问一下看看它是否有意义。
所以在Haskell中，未定义的语义上包含非终止。 所以应该不可能有一个功能
isUndefined :: a -> Bool
因为语义会表明这解决了暂停问题。
不过，我相信GHC的一些内置功能允许这种限制“相当可靠”地被打破。 特别抓住＃。
以下代码允许未定义的值被“相当可靠地”检测到：
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我不是一个曲柄。 我只是简单地指出，在未定义的语义中存在相当严重的中断，因为它们声明未定义的值在某种意义上应该与非终止无法区分。 这个函数允许哪种类型。 我只是想检查一下人们是否同意这一点，以及人们对此的看法，这是在GHC实现Haskell中添加某些不安全函数的非预期副作用，目的是为了方便一步？ :)
编辑：修复代码编译
我想做三个，啊，不，四个（相互关联的）点。
不，使用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..]的输入non_terminating where non_terminating = head.show.length $ [1..]上运行这两个程序，我们发现第二个程序不会终止，因为第一个程序不会终止。 事实上，我们的第二个程序没有解决暂停问题，因为它本身并没有终止。
停止问题的解决方案更像是一个总函数halts :: (a -> IO ()) -> a -> Bool ，如果给定的函数终止于输入a ，则总是终止于输出True ，而False if它永远不会终止。 当你区分undefined和error "user-defined error"时，你无法做到这一点，这就是你的代码所做的。
因此，所有对停止问题的引用都会让人困惑，以决定一个程序是否终止以决定是否有程序终止。 如果使用上面的non-terminating输入而不是undefined的输入，它将不会得出任何结论; 它在语义上已经是一个很大的延伸，可以称之为区分非终止和undefined ，并且将其称为停止问题的解决方案是无稽之谈。
问题不是一个巨大的语义问题
本质上你所有的代码都能够确定你的错误值是否是使用undefined或其他错误产生函数产生的。 这里的语义问题是， undefined和undefined error "not defined with undefined"具有语义值⊥，但是可以区分它们。 好的，理论上这并不是很干净，但是对于不同的原因，对于⊥有不同的输出对于调试非常有用，所以对值⊥执行一个共同的响应会很疯狂，因为它必须始终是非终止的完全正确。
其结果是任何有错误的程序都会被迫在发生错误时进入无限输出循环。 这是理论上的好处，以至于没有帮助的地步。 更好的办法是打印*** Exception: Prelude.undefined或Error: ungrokable wibbles或其他有用的描述性错误消息。
要在危机中有所帮助，任何编程语言都必须牺牲每个⊥彼此相同的愿望。 区分不同的⊥在理论上并不可靠，但在实践中不这样做会很愚蠢。
如果一位程序设计语言理论家认为这是一个严重的语义问题，那么他们应该被戏弄生活在一个世界，在这个世界里，程序冻结/不终止总是无效输入的最好结果。
从文档：
高度不安全的原始unsafeCoerce将来自任何类型的值转换为任何其他类型。 不用说，如果你使用这个函数，你有责任确保旧的和新的类型具有相同的内部表示，以防止运行时间损坏。
它显然也打破了参照透明度，因此纯粹性，所以你放弃了Haskell语义给你的所有保证。
一旦离开纯粹的地形，有很多方法可以在脚下自己拍摄。 你也可以使用OS原语在IO读取你的整个进程内存，以最糟糕的方式破坏参照透明。
除此之外，您定义的isUndefined并不能解决暂停问题，因为它不是全部的，这意味着它不会终止所有的输入。
例如， isUndefined (last [1..])不会终止。
有很多程序可以证明他们是否终止，但这并不意味着我们已经解决了停止问题。
链接地址: http://www.djcxy.com/p/7487.html上一篇: is GHC's implementation of Haskell semantically broken?