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
nis 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)) embedand 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 Γ0 without resorting to embedded functions, which means we can do things like computably compare them.