ε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)

Ord, Countable Ordinals, and an Idea of sigfpe

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 ω², or an ordinal less than ω³ 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, ε₀. We might be able to go further than this, but I'll save that for later.

Thanks to sigfpe for the idea!

Ordinal Notation and Computer Proof

Last ordinal post here

There is an implementation in Coq of the countable ordinals up to Γ₀.

More Proof of Referential Transparency

Previously, I talked about proving referential transparency. The authors of A Persistent Union-Find Data Structure (other version) use Coq to prove imperative functions referentially transparent, and they point out the work of Harold Baker, who designed fast persistent arrays (and here), which they also prove to be referentially transparent. These arrays are even available in Haskell, though wrapped in the IO monad.

The authors of the union-find paper say that their structure is not "purely applicative". I don't actually know what that means, but I suppose it means it's not strictly functional, since it requires in-place modification.

In any case, there are now at least four cases for being able to prove referential transparency so we can use it without wrapping everything in the IO monad:

• Memoization - For memoization in (not just for) Haskell, see this paper by the Simons and Conal Elliott. (mirror 1, mirror 2)
• Diff Arrays
• Splay Trees
• Union-Find

Any other ideas?