haskell - GHC对Haskell的实现在语义上被破坏了吗？

Question

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

因此，在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)

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

朱尔斯

编辑:有些人似乎认为我声称已经解决了Halt问题XD，但我不是一个曲柄。我只是在说undefined语义上有一个相当严重的突破，因为它们指出undefined的值在某种意义上应该与untermination不可区分。该功能允许哪些功能。我只是想检查一下人们是否对此表示赞同，以及人们对此有何看法，为方便起见，在Haskell的GHC实现中增加某些不安全功能的这种意想不到的副作用是到目前为止吗？ :)

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

Answer 1

我想提出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

kes!根据Haskell报告，语义已损坏。哦，不，等等，我使用了unsafe...。我被警告了。

主要问题是使用unsafeCoerce，您可以使用它将任何东西转换成其他东西。它与命令式编程中的类型转换一样糟糕，因此所有类型的安全性都超出了人们的视野。

您正在catch编写IOException，而不是纯错误(t)。

要使用catch，您已将纯错误undefined转换为IO异常。 IO monad从表面上看很简单，并且错误处理语义不需要使用⊥。可以将其视为一个monad转换器，在某种程度上包含一个错误处理Either。

与停止问题相关的链接完全是伪造的

我们不需要任何编程语言的任何不安全功能就可以在非终止和错误之间进行这种区分。

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

kes!我们通过区分未定义和未终止来解决暂停问题。哦，不，等等，不，我们实际上仅区分了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已经是一个很大的难题，称其为停止问题的解决方案是毫无意义的。

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

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

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

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

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