## Tuesday, July 24, 2007

### ε0 in an Ord instance

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

## Monday, July 23, 2007

### Ord, Countable Ordinals, and an Idea of sigfpe

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!

## Friday, July 20, 2007

### 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:

Any other ideas?