-1

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.

mb21
  • 34,845
  • 8
  • 116
  • 142
Waqar Ahmed
  • 5,005
  • 2
  • 23
  • 45

1 Answers1

1

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.

joranvar
  • 490
  • 5
  • 9
chi
  • 111,837
  • 3
  • 133
  • 218