什么是haskell的底部（_|_）？

Question

在 Haskell 文档中，有时我会找到底部 (_|_)一词。难道纠正一个底部（_ | _）是一个value不能被进一步细分？

例子，

非底部：

• aNum不是，因为它是类 Num 的实例。
• 1不是，因为，它是一个Num.
• aString不是，因为，它是一个列表Char
• "aa" 不是，因为它是一个 String
• ...

A-Bottom：以下都是底部，因为无法进一步细分。

• 一种 Char
• 一个 Int
• 1::Int
• 一种 Word
• 1::Word
• Apple并Orange在data Fruit = Apple | Orange
• ...

Answer 1

你的直觉是不正确的。底部是代表非终止程序的虚构值。在 Haskell 中，由于懒惰，这个值存在于任何类型中。

例如：

x1 :: Integer
x1 = 42 -- not a bottom

x2 :: Integer
x2 = sum [1..]  -- bottom, it does not terminate

x3 :: (Integer, String)
x3 = x3   -- bottom, infinite recursion

x4 :: (Integer, String)
x4 = (x2, "hello")   -- not a bottom, but a pair (_|_, "hello")

我们还假装undefined和error ".."是底部，因为这些是表达式的异常值，无法计算为它们类型中的“正确”值。

名称底部来自理论计算机科学，在那里研究计算的数学模型。在实践中，在函数式编程语言中对值进行“排序”是很常见的，以便“非终止”对应于最小的可能值，它位于排序的“底部”，因此称为“底部”。

例如，以下对按递增顺序排列。

p1 :: (Integer, Integer)
p1 = p1   -- bottom, infinite recursion

p2 :: (Integer, Integer)
p2 = (sum [1..], sum [1..])   -- not a bottom, but (_|_, _|_) which is only slightly larger

p3 :: (Integer, Integer)
p3 = (42, sum [1..])   
-- (42, _|_) which is larger since it's more defined
-- (fewer bottoms inside, roughly speaking)

p4 :: (Integer, Integer)
p4 = (42, 23)
-- even larger, no larger values exist from here since it's a completely defined value

您还可以在某些类型中无限增加序列：

l1 :: [Int]
l1 = l1   -- bottom

l2 :: [Int]
l2 = 1 : l1  -- not a bottom, 1 : _|_

l3 :: [Int]
l3 = 1 : 2 : l1  -- more defined, 1 : 2 : _|_


l4 :: [Int]
l4 = 1 : 2 : 432 : l1  -- more defined

-- etc. we can go on forever

这种值的排序在编程语言理论中很重要，因为递归定义总是找到满足递归方程的最小值。

例如，公式x1=x1中Int被满足_|_, 0, 1, -1, ...，但如果我们认为这是一个递归定义，我们必须采取最少的解决方案，即_|_。

类似地，在p :: (Integer, Integer)定义为 中p = (32, snd p)，我们找到了解决方案，(32, _|_), (32, 0), (32, 1), (32, -1), ....但我们需要采取最少的方法，所以我们有(32, _|_)。这模拟了这样一个事实，即当我们评估表达式时，第二个组件从未被定义（因为无限递归）。