GHC的Haskell实现在语义上被打破了吗？

Question

今天早上我注意到一些有趣的东西,我想询问一下它是否有重要意义.

所以在Haskell中,undefined语义包含非终止.所以有一个功能应该是不可能的

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我不是一个曲柄.我只是声明未定义的语义存在相当严重的中断,因为它们声明未定义的值应该在某种意义上与非终止无法区分.这个功能有哪些允许.我只是想检查一下人们是否同意这一点以及人们对此的看法,这是否意味着在Haskell的GHC实现中添加某些不安全功能的方便性副作用是为了方便一步到位？:)

编辑:修改代码进行编译

Answer 1

我想制作三个,啊,不,四个(相互关联的)点.

1. 不,使用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,您可以使用其他任何东西.它与命令式编程中的类型一样糟糕,因此所有类型的安全性都已经消失.

2. 你是catchIOException,而不是纯错误(⊥).

   要使用catch,您已将纯错误undefined转换为IO异常.该IO单子看似简单,和错误处理语义不要求使用⊥的.可以把它想象成monad变换器,包括Either某种程度上的错误处理.

3. 与暂停问题的联系是完全虚假的

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

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

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

   有解决的停机问题会更喜欢具有总功能halts :: (a -> IO ()) -> a -> Bool即总是与输出终止True如果给定的功能与输入终止a,并且False如果它永远不会终止.当你区分undefined和error "user-defined error"你的代码所做的事情时,你是不可能的.

   因此,所有对暂停问题的引用都令人困惑,决定一个程序是否终止并决定是否有任何程序终止.如果你使用non-terminating上面的输入而不是undefined; 它没有得出任何结论; 在语义上已经是一个很大的延伸,可以区分非终止和undefined,并且将其称为停止问题的解决方案是无稽之谈.

4. 问题不是一个巨大的语义问题

   基本上所有代码都能够确定您的错误值是使用undefined产生函数还是其他错误产生的.语义的问题有两个undefined,并error "not defined with undefined"具有语义值⊥,但你可以区分它们.好吧,理论上这不是很干净,但是对于⊥的不同原因有不同的输出对于调试是非常有用的,强制执行对值common的共同响应是疯狂的,因为它必须始终是非终止的完全正确.

   结果是任何带有任何错误的程序在出现错误时都必须进入无限输出循环.这使得理论上的好处达到了深刻无益的程度.更好的是打印*** Exception: Prelude.undefined或Error: ungrokable wibbles其他有用的描述性错误消息.

   为了在危机中有所帮助,任何编程语言都必须牺牲你的愿望,使每个人的行为彼此相同.区分不同的iss在理论上并不可爱,但在实践中不这样做是愚蠢的.

   如果一个编程语言理论家称这是一个严重的语义问题,他们就应该被戏弄,以便生活在一个程序冻结/非终止始终是无效输入的最佳结果的世界.

Answer 2

来自文档:

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

它显然也会破坏引用透明度,从而打破纯粹性,因此您放弃了Haskell语义给您的所有保证.

一旦离开纯净的地形,有很多方法可以在脚下射击自己.您也可以使用OS原语来读取整个进程内存IO,以最糟糕的方式破坏引用透明性.

除此之外,,你的定义isUndefined并没有解决停机问题,因为它不是总,这意味着它不会在所有输入终止.

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

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