ε0 in an Ord instance

In my last post, I worked rather hard to approach ε₀, but there is a much simpler way to form a type with an Ord instance that has order type ε₀, 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 &Gamma₀ (mirror)