“未定义”如何在 Haskell 中工作

Question

我对 Haskell 中的“未定义”值很好奇。它很有趣，因为你可以把它放在任何地方，Haskell 会很高兴。以下都是可以的

[1.0, 2.0, 3.0 , undefined]  ::[Float]
[1, 2 ,3 undefined, 102312] :: [Int]
("CATS!", undefined)  :: (String, String)
....and many more

undefined 如何在后台工作？是什么使得拥有每种数据类型的数据成为可能？我是否可以定义一个可以放在任何地方的值，或者这是一些特殊情况？

Answer 1

undefined 并没有什么特别之处。它只是一个特殊值——您可以用无限循环、崩溃或段错误来表示它。写它的一种方法是崩溃：

undefined :: a
undefined | False = undefined

或者循环：

undefined = undefined

这是一个特殊的值，可以是任何类型的元素。

由于 Haskell 是惰性的，您仍然可以在计算中使用这些值。例如

 > length [undefined, undefined]
 2

但除此之外，这只是多态性和非严格性的自然结果。

Answer 2

您正在检查的有趣属性是 undefined 对于我们选择的任何类型 a 具有类型 a，即没有约束的 undefined :: a。正如其他人所指出的，undefined 可能被认为是错误或无限循环。我想争辩说，最好将其视为“空洞的真实陈述”。在任何与停机问题密切相关的类型系统中，这几乎是一个不可避免的漏洞，但从逻辑的角度考虑它很有趣。

---

思考类型编程的一种方式是它是一个谜。有人给了你一个类型，并要求你实现一个该类型的函数。比如

Question:    fn  ::  a -> a
Answer:      fn  =  \x -> x

很简单。我们需要为任何类型的a 生成一个a，但是我们得到了一个作为输入，所以我们可以返回它。

有了undefined，这个游戏总是很简单

Question:    fn  ::  Int -> m (f [a])
Answer:      fn  =  \i   -> undefined    -- backdoor!

所以让我们摆脱它。当你生活在一个没有它的世界里时，理解undefined 是最容易的。现在我们的游戏变得更难了。有时是可能的

Question:    fn  :: (forall r. (a -> r) -> r) -> a
Answer:      fn  =  \f                        -> f id

但突然之间，有时也不可能了！

Question:    fn  ::  a -> b
Answer:      fn  =   ???                  -- this is `unsafeCoerce`, btw.
                                          -- if `undefined` isn't fair game,
                                          -- then `unsafeCoerce` isn't either

是吗？

-- The fixed-point combinator, the genesis of any recursive program

Question:    fix  ::  (a -> a) -> a
Answer:      fix  =   \f       -> let a = f a in a

                                          -- Why does this work?
                                          -- One should be thinking of Russell's 
                                          -- Paradox right about now. This plays
                                          -- the same role as a non-wellfounded set.

这是合法的，因为 Haskell 的 let 绑定是惰性的并且（通常）递归。现在我们是黄金。

Question:    fn   ::  a -> b
Answer:      fn   =  \a -> fix id         -- This seems unfair?

即使没有内置undefined，我们也可以使用任何旧的无限循环在游戏中重建它。类型检查。为了真正防止我们在 Haskell 中使用 undefined，我们需要解决停机问题。

Question:    undefined  ::  a
Answer:      undefined  =   fix id

---

现在，正如您所见，undefined 对于调试很有用，因为它可以作为任何值的占位符。不幸的是，操作很糟糕，因为它要么导致无限循环，要么立即崩溃。这对我们的游戏也很不利，因为它让我们作弊。最后，我希望我已经证明，只要你的语言有（可能是无限的）循环，没有undefined 是相当困难的。

存在像 Agda 和 Coq 这样的语言，它们放弃循环以真正消除 undefined。他们这样做是因为我发明的这款游戏在某些情况下实际上非常有价值。它可以对逻辑语句进行编码，因此可以用来形成非常非常严格的数学证明。你的类型代表定理，你的程序保证了这个定理得到证实。 undefined 的存在意味着所有定理都是可证实的，从而使整个系统不可信。

但在 Haskell 中，我们对循环比校对更感兴趣，所以我们宁愿有 fix 也不愿确定没有 undefined。

Answer 3

undefined 是如何工作的？好吧，恕我直言，最好的答案是 它不起作用。但要理解这个答案，我们必须弄清楚它的后果，这对新手来说并不明显。

基本上，如果我们有undefined :: a，这对类型系统意味着undefined 可以出现在任何地方。为什么？因为在 Haskell 中，每当您看到具有某种类型的表达式时，您都可以特化该类型，方法是始终将其任何类型变量的所有实例替换为任何其他类型。熟悉的例子是这样的：

map :: (a -> b) -> [a] -> [b]

-- Substitute b := b -> x
map :: (a -> b -> c) -> [a] -> [b -> c]

-- Substitute a := Int
map :: (Int -> b -> c) -> [Int] -> [b -> c]

-- etc.

对于map，这是如何工作的？好吧，归根结底，map 的参数提供了产生答案所需的一切，无论我们对其类型变量进行何种替换和特化。如果你有一个列表和一个函数，它使用与列表元素相同类型的值，你可以做 map 做的事，句号。

但是在undefined :: a 的情况下，这个签名意味着无论a 可以专门用于哪种类型，undefined 都能够产生该类型的值。它怎么能做到？嗯，实际上，它不能，所以如果一个程序实际上到达了需要undefined 值的步骤，就没有办法继续了。此时程序唯一能做的就是失败

另一个案例背后的故事相似但不同：

loop :: a
loop = loop

在这里，我们可以通过这个听起来很疯狂的论证证明loop 具有a 类型：假设loop 具有a 类型。它需要产生一个a 类型的值。它怎么能做到？很简单，它只调用loop。快！

这听起来很疯狂，对吧？好吧，问题是它与map 的定义的第二个等式中发生的事情并没有什么不同：

map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = f x : map f xs

在第二个等式中，f x 的类型为 b，(f x:) 的类型为 [b] -> [b]；现在结束我们证明map确实具有我们签名声明的类型，我们需要生成[b]。那么我们是如何做到的呢？通过假设 map 具有我们试图证明的类型！

Haskell 的类型推断算法的工作方式是它首先猜测表达式的类型是a，然后只有在发现与该假设相矛盾的东西时才改变猜测。 undefined 类型检查到 a 因为这是一个彻头彻尾的谎言。 loop 类型检查为 a，因为允许递归，而 loop 所做的一切都是递归的。

---

编辑：什么鬼，我还不如说一个例子。下面是一个关于如何从这个定义中推断出map 类型的非正式演示：

map f [] = []
map f (x:xs) = f x : map f xs

是这样的：

1. 我们首先假设map :: a。
2. 但是 map 有两个参数，所以a 不能是类型。我们将我们的假设修改为：map :: a -> b -> c; f :: a。
3. 但正如我们在第一个等式中看到的，第二个参数是一个列表：map :: a -> [b] -> c; f :: a。
4. 但我们也可以在第一个等式中看到，结果也是一个列表：map :: a -> [b] -> [c]; f :: a。
5. 在第二个等式中，我们将第二个参数与构造函数(:) :: b -> [b] -> [b] 进行模式匹配。这意味着在该等式中，x :: b 和 xs :: [b]。
6. 考虑第二个等式的右侧。由于map f (x:xs) 的结果必须是[c] 类型，这意味着f x : map f xs 也必须是[c] 类型。
7. 给定构造函数(:) :: c -> [c] -> [c]的类型，这意味着f x :: c和map f xs :: [c]。
8. 在 (7) 中，我们得出结论：map f xs :: [c]。我们假设在 (6) 中，如果我们在 (7) 中得出其他结论，这将是一个类型错误。我们现在还可以深入研究这个表达式，看看这需要f 和xs 有哪些类型，但长话短说，一切都会检查出来。
9. 由于f x :: c 和x :: b，我们必须得出结论f :: b -> c。所以现在我们得到map :: (b -> c) -> [b] -> [c]。
10. 我们完成了。

相同的过程，但针对loop = loop：

1. 我们暂时假设loop :: a。
2. loop 不带任何参数，所以它的类型目前与a 一致。
3. loop 的右侧是 loop，我们已将其临时分配类型为 a，以便签出。
4. 没有什么需要考虑的了；我们完成了。 loop 的类型为 a。

Answer 4

嗯，基本上是undefined = undefined——如果你尝试评估它，你会得到一个无限循环。但是 Haskell 是一种非严格语言，因此 head [1.0, 2.0, undefined] 不会评估列表的 所有 元素，因此它会打印 1.0 并终止。但是如果你打印show [1.0, 2.0, undefined]，你会看到[1.0,2.0,*** Exception: Prelude.undefined。

至于它是如何具有所有类型的......好吧，如果表达式是A类型，这意味着评估它要么会产生A类型的值，要么评估会发散，不产生任何价值一点也不。现在，undefined 总是发散的，所以它适合每个可以想象的类型A 的定义。

另外，一篇关于相关主题的好博文：http://james-iry.blogspot.ru/2009/08/getting-to-bottom-of-nothing-at-all.html

Answer 5

关于 undefined 有两点需要注意：

• 您几乎可以将 undefined 放在任何地方，并且类型检查器会很高兴。这是因为 undefined 有类型（forall a.a）。
• 您几乎可以将 undefined 放在任何地方，它在运行时会有一些明确定义的表示。

第二个，GHC commentary 明确表示：

⊥ 的表示形式必须是一个指针：它是一个对象，在评估时会抛出异常或进入无限循环。

有关更多详细信息，您可能需要阅读论文Spinless Tagless G-Machine。

Answer 6

如果我在 GHCi 中尝试 undefined，我会得到一个异常：

Prelude> undefined
*** Exception: Prelude.undefined

因此，我想它只是实现为抛出异常：
http://www.haskell.org/ghc/docs/latest/html/libraries/base/Control-Exception.html#g:2