This post is literate Haskell.

In the comments on my last post about ordinals, sigfpe
suggests the following type constructors:

type One = ()
type Two = Either One One
type N = [One]
type Nplus1 = Either N One
type NplusN = Either N N
type NtimesN = (N,N)
type NpowN = [N]
type NpowNplusN = Either NpowN N

The idea is that each of these has an `Ord`

instance
defined. I think he's suggesting that the `Ord`

instance
for each (ignoring _|_) has an order type that is the same as the
ordinal its name corresponds to. I have some quibbles with his
implementation, but I really like the idea, and so I'll expand on it
below.

I'll start with my disagreements. My first is with the order for
`NpowN`

. In NpowN

[[(),()]] > [[()],[(),()]] > [[()],[()],[(),()]] > . . .

or in simpler form

[2] > [1,2] > [1,1,2] > . . .

Since no ordinal has an infinite decreasing sequence, the order type
of `[N]`

is not that of an ordinal. For now, we'll just
disregard the `[]`

type constructor.

My second quibble is with `Times`

. sigfpe does not make
this explicit, but the inference I drew from his examples was that we
could define `Times`

as

type Times = (,)

That doesn't quite work, though. Ordinal
arithmetic places the least significant part first, but the
`Ord`

instance for `(,)`

places the most
significant part first.

Now that we have these differences out of the way, let's get to the code.

We'll need these options for type class machinery later.

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-incoherent-instances #-}

Ala sigfpe:

> type One = ()
> type Plus = Either
> type Times = Flip Both
>
> data Both a b = Both a b
> newtype Flip f a b = Flip (f b a)

To define `Times`

, we use a pair datatype with the standard
Haskell ordering (see `instance Ordinal2 Both`

below), but
apply the newtype `Flip`

, which warrants its own
definition, as it will be useful elsewhere.

So far, we can only define finite ordinals. In order to represent
larger ordinals, we want to be able to represent an unlimited number
of applications of a type constructor to a type.

> data ApplyN f x = More (ApplyN f (f x))
> | Stop x

`ApplyN`

does this -- after n applications of
`More`

, the type `x`

is wrapped n times in the
type constructor `f`

. Essentially, `ApplyN f x`

is f^{ω}(x).

Our first example of this will be adding one ω times.

> type N = ApplyN (Flip Plus One) One

This should look like (λ x . x + 1)^{ω} (1).

If `ApplyN`

works as advertized, `N`

should have
order type ω under a naive definition of
`Ord`

. Unfortunately, it does not. First of all, we can't
automatically derive `Ord`

for the type
`ApplyN`

, since it uses a type constructor, `f`

,
to build a new parameter. We will need

> class Ordinal1 f where
> comp1 :: Ordinal a => f a -> f a -> Ordering

to describe the contract `f`

must meet to make ```
ApplyN
f x
```

ordered. Note that we use the class `Ordinal`

here, which is used only to avoid messing the with `Eq`

requirement on instances for `Ord`

.

> class Ordinal t where
> comp :: t -> t -> Ordering

The second problem with the naive instance of `Ordinal`

on
`ApplyN`

is that each application of `More`

leads to a new type closer to the type we're really talking
about. What I mean by this is that, for the case of `N`

, we
really want to talk about

Flip Plus One (Flip Plus One (Flip Plus One . . . .

Which we can't directly say in Haskell.

We want to be talking about the type that is the limit. Since we can't
do that, to compare two values, we'll compare them at the maximum of
their levels. For instance, if we want to compare the values ```
Stop
()
```

and ```
More $ More $ Stop $ Flip $ Left $ Flip $ Left
()
```

, both of which are of type `N`

, we'll inject the
value `()`

into the higher level. To do this, we also need
`f`

to be have the property that we can inject into it a
value of its type parameter.

> class Container f where
> inject :: x -> f x

To bring this back to the ordinals, we'll be representing
ω^{ω} as either and ordinal less than ω, or an
ordinal less than ω^{2}, or an ordinal less than
ω^{3} or …, and to compare two ordinals, we get a
representation of each in a common level, then compare them using the
comparison for ordinals less than the limiting ordinal of that level.

> instance (Container f, Ordinal1 f) => Ordinal1 (ApplyN f) where
> comp1 (Stop u) (Stop v) = comp u v
> comp1 (Stop u) (More v) = comp (Stop (inject u)) v
> comp1 (More u) (Stop v) = comp u (Stop (inject v))
> comp1 (More u) (More v) = comp1 u v

We've defined the ordering on `ApplyN f`

so that

comp (Stop x) (More (Stop (inject x))) == EQ

which is what the paragraph above says, but more concise. We've
defined an equivalence relation on values of the type ```
ApplyN f
t
```

such that `x == inject x`

, so we're off to a good
start.

We'll also want `inject`

to be monotone, that is

x < y ==> inject x < inject y

and for `inject`

to send the order type of the domain not
just to *some* order in the codomain, but to the initial order
in the codomain. So, it's easy to write

> injectPlusL :: a -> Plus a b
> injectPlusL x = Left x

or

> instance Container (Flip Plus b) where
> inject v = Flip (Left v)

Injecting a into a*b is trickier, since we need the second part of the
pair to be the minimal possible value in order for the injection range
to be the initial part of the order. For this we define

> class Least x where
> least :: x
> instance Least One where
> least = ()
> instance Least a => Least (Plus a b) where
> least = Left least
> instance (Least a, Least b) => Least (Times a b) where
> least = Flip (Both least least)
> instance Least b => Least (Flip Plus a b) where
> least = Flip (Left least)
> instance (Least a, Least b) => Least (Flip Times a b) where
> least = Flip (Flip (Both least least))
> instance Least x => Least (ApplyN f x) where
> least = Stop least

And we can now write the injection from a to a*b:

> instance (Least a) => Container (Flip Times a) where
> inject v = Flip (Flip (Both least v))

We also have the trivial

> instance Container (ApplyN f) where
> inject x = Stop x

Let's write the base instances for Ordinal in as general a way as possible:

> class Ordinal2 f where
> comp2 :: (Ordinal a, Ordinal b) => f a b -> f a b -> Ordering
> instance Ordinal2 Plus where
> comp2 (Left _) (Right _) = LT
> comp2 (Right _) (Left _) = GT
> comp2 (Left x) (Left y) = comp x y
> comp2 (Right x) (Right y) = comp x y
> instance Ordinal2 Both where
> comp2 (Both p q) (Both x y) =
> case comp p x of
> LT -> LT
> GT -> GT
> EQ -> comp q y
> instance Ordinal2 f => Ordinal2 (Flip f) where
> comp2 (Flip x) (Flip y) = comp2 x y
>
> instance Ordinal () where
> comp _ _ = EQ

And the conversion instances between the n-ary Ordinal instances:

> instance (Ordinal1 f, Ordinal a) => Ordinal (f a) where
> comp = comp1
> instance (Ordinal2 f, Ordinal a, Ordinal b) => Ordinal (f a b) where
> comp = comp2
> instance (Ordinal2 f, Ordinal a) => Ordinal1 (f a) where
> comp1 = comp2

Now let's do some examples. First we check that `Ordinal`

is
defined for `N`

:

> n_ok = comp (undefined :: N) (undefined :: N)

ω^{ω}:

> type NpowN = ApplyN (Flip Times N) One
> npowN_ok = comp (undefined :: NpowN) (undefined :: NpowN)

We can now plug in `NpowN`

into its own definition to get
ω^{ω} * ω = ω^{ω + 1}

> type NpowNplusOne = ApplyN (Flip Times N) NpowN
> nPowNplusOne_ok = comp (undefined :: NpowNplusOne) (undefined :: NpowNplusOne)

or ω

^{ω * ω} =
ω

^{ω2}:

> type NpowNpow2 = ApplyN (Flip Times NpowN) One
> npowNpow2_ok = comp (undefined :: NpowNpow2) (undefined :: NpowNpow2)

The second method looks more powerful, but continuing it keeps us
below ω^{ω&omega}, so let's use the
first method of substituting back in to see if we can get further.

ω^{ω + 2}:

> type NpowNplus2 = ApplyN (Flip Times N) NpowNplusOne
> nPowNplus2_ok = comp (undefined :: NpowNplus2) (undefined :: NpowNplus2)

We can now plug `ApplyN`

back into itself, and extend this
to ω^{ω + &omega} = ω^{ω * 2}:

> type NpowNtimes2 = ApplyN (ApplyN (Flip Times N)) One
> npowNtimes2_ok = comp (undefined :: NpowNtimes2) (undefined :: NpowNtimes2)

Similarly, ω^{ω * 3}:

> type NpowNtimes3 = ApplyN (ApplyN (Flip Times N)) NpowNtimes2
> npowNtimes3_ok = comp (undefined :: NpowNtimes3) (undefined :: NpowNtimes3)

ω^{ω * ω} =
ω^{ω2}, which we apready saw before,
can also be written as

> type NpowNpow2' = ApplyN (ApplyN (ApplyN (Flip Times N))) One
> npowNpow2'_ok = comp (undefined :: NpowNpow2') (undefined :: NpowNpow2')

ω^{ω2 * ω} = ω^{ω3} =

> type NpowNpow3 = ApplyN (ApplyN (ApplyN (Flip Times N))) NpowNpow2
> npowNpow3_ok = comp (undefined :: NpowNpow3) (undefined :: NpowNpow3)

ω^{ωω}:

> type NpowNpowN = ApplyN (ApplyN (ApplyN (ApplyN (Flip Times N)))) One
> npowNpowN_ok = comp (undefined :: NpowNpowN) (undefined :: NpowNpowN)

ω^{ωω + 1}:

> type NpowNpowNplusOne = ApplyN (ApplyN (ApplyN (ApplyN (Flip Times N)))) NpowNpowN
> npowNpowNplusOne_ok = comp (undefined :: NpowNpowNplusOne) (undefined :: NpowNpowNplusOne)

We can continue this process up to, but not including,
ε_{0}. We might be able to go further than this, but
I'll save that for later.

Thanks to sigfpe for the idea!