## Tuesday, July 24, 2007

### ε0 in an Ord instance

In my last post, I worked rather hard to approach ε0, but there is a much simpler way to form a type with an `Ord` instance that has order type ε0, according to Trees, Ordinals and Termination (mirror)

```import List

data Tree = Node | Tree [Tree]

instance Ord Tree where
compare Node Node = EQ
compare Node (Tree _) = LT
compare (Tree _) Node = GT
compare (Tree x) (Tree y) = compare (sort x) (sort y)

instance Eq Tree where
x == y = compare x y == EQ
```
Or, according to Ordinal Arithmetic with List Structures (mirror)
```data Cons = Nil | Cons Cons Cons

instance Ord Cons where
compare Nil Nil = EQ
compare Nil (Cons _ _) = LT
compare (Cons _ _) Nil = GT
compare a@(Cons x' y') b@(Cons x y) =
case compare x' x of
LT -> compare y' b
EQ -> compare y' y
GT -> compare a y

instance Eq Cons where
x == y = compare x y == EQ
```
These representations do not help in the general problem of representing all ordinals less than some ordinal κ, but they are much simpler than our previous method.

For trees with larger order types, see What's so special about Kruskal's theorem and the ordinal &Gamma0 (mirror)