域构建 Haskell

Question

我有一个数据类型：

data Tree e = Node e (Tree e) (Tree e) | Empty deriving (Show)

type Forest e = [Tree e]

data Animal = Squirrel | None deriving (Show)

Forest Int 的图形表示是：

最后一个元素是底部。然后在倒数第二行，它可以是空的。但是我不明白 ⊥:⊥ 是什么意思。它是列表的构造函数吗？像这样 5:[]？然后在第 3 行，为什么 Empty:⊥ 中缺少 []。

谁能解释一下我在这里理解错了什么。谢谢。

Answer 1

是的，_|_ : _|_是列表:的构造函数，适用于未定义的列表元素和未定义的列表尾。例如，这是与 Haskell 程序

关联的值

let list = list
    elem = elem
in elem : list

同样，Empty : _|_ 是关联到

的值

let list = list
in Empty : list

这里没有[]，因为链表的尾部因为无限递归而无法终止（收敛），所以它的值是未定义的（_|_）。

在域排序中，我们有递增序列

_|_
Empty : _|_
Empty : Empty : _|_
Empty : Empty : Empty : _|_
...

有限制（AKA lub 或 supremum）无限列表永远重复 Empty。

值

_|_ : _|_ : _|_

是关联到

let list = list
    elem = elem
in elem : elem : list

相比之下，

_|_ : _|_ : []

是

的值

let elem = elem
in elem : elem : []

请注意，上面允许计算长度，因为列表有明确的结尾。取它的 length 会产生 2，因为不需要计算列表元素，所以没有强制底部。

Domain construction Haskell