域结构的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) 

和森林诠释的图形表示是：

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

任何人都可以请解释我在这里理解错误。 谢谢。

Answer 1

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

let list = list 
    elem = elem 
in elem : list 

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

let list = list 
in Empty : list 

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

在域排序，我们有具有限制（AKA LUB或确界）的无穷列表重复Empty永远增加序列

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

。

值

_|_ : _|_ : _|_ 

是关联到

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

通过比较所述一个，

_|_ : _|_ : [] 

是

let elem = elem 
in elem : elem : [] 

的值

请注意，以上允许计算长度，因为列表有确定的结束。考虑到它的length将产生2，因为不需要评估列表元素，所以不会强制底部。