GHC对Haskell的实现在语义上是否被破坏了?



今天早上我注意到一些有趣的事情,我想问一下,看看它是否有意义。

因此,在Haskell中,未定义的Semantically包含非终止。所以应该不可能有一个功能

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)

此外,正如你会注意到的那样,这真的算在内吗?它使用了几个"不安全"的函数?

Jules

编辑:有些人似乎认为我声称已经解决了暂停问题XD我不是一个怪人。我只是简单地说,undefined的语义有一个相当严重的突破,因为它们声明undefine的值在某种意义上应该与非终止不可区分。这个功能允许。我只是想看看人们是否同意这一点,以及人们对此的看法,在Haskell的GHC实现中添加某些不安全功能的意外副作用是否是一个进步?:)

EDIT:修复了编译的代码

我想提出三个,啊,不,四个(相互关联的)点。

  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. 您是一个IOException的catch,而不是一个纯粹的错误(Ş)

    要使用catch,您已经将纯错误undefined转换为IO异常。IO monad看似简单,并且错误处理语义不需要使用Ş。把它想象成一个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,如果给定函数以输入a终止,则总是以输出True终止,如果从未终止,则False终止。当您在undefinederror "user-defined error"之间进行区分时,您可能离这很远,这就是您的代码所做的。

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

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

    基本上,您的代码所能做的就是确定您的错误值是使用undefined还是其他产生错误的函数产生的。这里的语义问题是undefinederror "not defined with undefined"都有语义值Ş,但你可以区分它们。好吧,这在理论上不是很清楚,但在不同的原因上有不同的输出是的,所以对调试很有用,强制对值的公共响应是疯狂的,因为它必须始终是非终止的才能完全正确。

    结果是,任何有错误的程序在出现错误时都必须进入无限输出自由循环。这使理论上的细微之处变得毫无帮助。更好的方法是打印*** Exception: Prelude.undefinedError: ungrokable wibbles或其他有用的描述性错误消息。

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

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

来自文档:

高度不安全的基元CCD_ 30将值从任何类型转换为任何其他类型。不用说,如果使用此函数,您有责任确保新旧类型具有相同的内部表示,以防止运行时损坏。

很明显,它还破坏了引用透明性,因此纯粹性,因此您放弃了Haskell语义提供的所有保证。

一旦你离开纯净的地形,有很多方法可以射中自己的脚。您还可以使用操作系统原语来读取IO中的整个进程内存,以最糟糕的方式打破引用透明度。

除此之外,您对isUndefined的定义并不能解决停止问题,因为它不是总数,这意味着它不会在所有输入上终止。

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

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

最新更新