I have a data type :
data Tree e = Node e (Tree e) (Tree e) | Empty deriving (Show)
type Forest e = [Tree e]
data Animal = Squirrel | None deriving (Show)
and the graphical representation of Forest Int is :
The last element is bottom. Then in second last row, it can be empty. But i didn't understand what ⊥:⊥
mean. Is it the constructor for list? like this 5:[]
? Then in 3rd row, why []
is missing in Empty:⊥
.
Can anyone please explain me what I am understanding wrong here. Thank you.
Yes, _|_ : _|_
is the constructor for lists :
, applies to an undefined list element and undefined list tail. This is the value, for instance, associated to the Haskell program
let list = list
elem = elem
in elem : list
Similarly, Empty : _|_
is the value associated to
let list = list
in Empty : list
There's no []
here because the tail of the list fails to terminate (converge) because of the infinite recursion, so its value is undefined (_|_
).
In the domain ordering, we have the increasing sequence
_|_
Empty : _|_
Empty : Empty : _|_
Empty : Empty : Empty : _|_
...
having limit (AKA lub or supremum) the infinite list repeating Empty
forever.
The value
_|_ : _|_ : _|_
is the one associated to
let list = list
elem = elem
in elem : elem : list
By comparison,
_|_ : _|_ : []
is the value of
let elem = elem
in elem : elem : []
Note that the above allows the length to be computed, since the list has a definite end. Taking its length
will produce 2, since there's no need to evaluate the list elements, so no bottom is forced.