28

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

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

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

4

6 回答 6

34

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

undefined :: a
undefined | False = undefined

或循环：

undefined = undefined

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

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

 > length [undefined, undefined]
 2

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

于 2013-05-25T10:41:22.057 回答
29

您正在检查的有趣属性是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内置，我们也可以使用任何旧的无限循环在我们的游戏中重建它。类型检查。为了真正防止自己undefined进入 Haskell，我们需要解决停机问题。

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

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

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

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

于 2013-05-25T15:15:32.633 回答
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

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

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

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

在第二个等式中，f x有 type b，并且(f x:)有 type [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 :: cand 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. loopa不带参数，所以它的类型与目前为止是一致的。
  3. loopis的右侧loop，我们临时指定了 type a，以便签出。
  4. 没有什么需要考虑的了；我们完成了。 loop有类型a。
于 2013-05-26T00:15:49.413 回答
1

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

Prelude> undefined
*** Exception: Prelude.undefined

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

于 2013-05-25T15:01:09.023 回答
1

关于 undefined 有两点需要注意：

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

对于第二个，GHC 的评论清楚地说：

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

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

于 2013-05-25T20:02:18.037 回答
1

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

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

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

于 2013-05-25T10:15:42.940 回答