haskelldomain-modelling

Domain construction Haskell


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 :

enter image description here

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.


Solution

  • 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.