3

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

所以在 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 实现中为了方便而添加某些不安全功能的意外副作用是不是已经迈出了一步？:)

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

4

2 回答 2

11

我想说三点，啊，不，四点（相互关联）。

  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. 您正在catch处理 IOException，而不是纯错误 (⊥)。

    要使用 catch，您已将纯错误转换undefined为 IO 异常。monad 看似简单，IO错误处理语义不需要使用⊥。把它想象成一个单子变换器，在某种程度上包括错误处理Either。

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

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

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

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

    停止问题的解决方案更像是拥有一个总函数halts :: (a -> IO ()) -> a -> Bool，如果给定函数以 input 终止，并且它永远不会终止，则该函数始终以 output终止。当你区分and时，你不可能远离那，这就是你的代码所做的。TrueaFalseundefinederror "user-defined error"

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

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

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

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

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

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

于 2013-07-15T14:42:15.710 回答
6

从文档：

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

它显然也破坏了引用透明度，从而破坏了pureness，因此您放弃了 Haskell 语义为您提供的所有保证。

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

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

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

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

于 2013-07-15T12:59:31.393 回答