Ordinals, part 2

Part 1

Peter G. Hancock reminded us of the obvious way to define uncountable ordinals. A rough translation into a single data type, rather than a family:

data Ordinal n = Zero (Nat n)
               | Succ (Ordinal n)
               | forall t . Limit (Less t n) (Ordinal t -> Ordinal n)

The parameter n is the "class" of the ordinal. We need the helper definitions:

data Nat n where
    Z :: Nat Z
    S :: Nat n -> Nat (S n)
data Z
data S n

data Less a b where
    LessZ :: Nat b -> Less Z (S b)
    LessS :: Less a b -> Less (S a) (S b)

embed :: Ordinal n -> Ordinal (S n)
embed (Zero x) = Zero (S x)
embed (Succ x) = Succ (embed x)
embed (Limit e f) = Limit (onemore e) (embed . f)
    where
      onemore :: Less a b -> Less a (S b)
      onemore (LessZ x) = LessZ (S x)
      onemore (LessS p) = LessS (onemore p)

Then we can define the first uncountable ordinal as

omega_1 = Limit (LessS (LessZ Z)) embed

and the sequence of ωs up to ω_ω as

omega_n :: Nat n -> Ordinal n
omega_n Z = Zero Z
omega_n (S n) = Limit (plusone n) embed
    where
      plusone :: Nat n -> Less n (S n)
      plusone Z = LessZ Z
      plusone (S n) = LessS (plusone n)

Hancock has many other interesting ways to represent ordinals, including as surreal numbers (with code), in which we can provide a more precise answer the the question I was originally responding to, What happens when you divide infinite by two? In the case of surreal numbers, you get, simply, ω/2, just as you do with the hyperreals. Hancock also provides a datatype for the ordinals up to Γ₀ without resorting to embedded functions, which means we can do things like computably compare them.