Conor McBride ctm at cs.nott.ac.uk
Wed Jan 31 06:46:40 EST 2007

```Hi folks

A puzzle for you (and for me too). I just tried to translate an old
Epigram favourite (which predates Epigram by some time) into GADT-speak.
It went wrong. I had a feeling it might. I wonder how to fix it: I
imagine it's possible to fix it, but that some cunning may be necessary.
Here it is:

Type-level Nat

> data Z = Z
> data S x = S x

Finite sets: Fin Z is empty, Fin (S n) has one more element than Fin n

> data Fin :: * -> * where
>   Fz :: Fin (S n)
>   Fs :: Fin n -> Fin (S n)

The "thinning" function: thin i is the order-preserving embedding from
Fin n to Fin (S n) which never returns i.

> thin :: Fin (S n) -> Fin n -> Fin (S n)
> thin Fz      i       = Fs i
> thin (Fs i)  Fz      = Fz
> thin (Fs i)  (Fs j)  = Fs (thin i j)

Its partial inverse, "thickening" has the spec

thicken i i = Nothing
thicken i (thin i j) = Just j

> thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n)
> thicken Fz      Fz      = Nothing
> thicken Fz      (Fs j)  = Just j
> thicken (Fs i)  Fz      = Just Fz
> thicken (Fs i)  (Fs j)  = fmap Fs (thicken i j)

The trouble is that whilst thin compiles, thicken does not. GHC rightly
complains

Thicken.lhs:18:32:
Couldn't match expected type `n' (a rigid variable)
against inferred type `S n1'
`n' is bound by the type signature for `thicken'
at Thicken.lhs:15:19
Expected type: Fin n
Inferred type: Fin (S n1)
In the first argument of `Just', namely `Fz'
In the expression: Just Fz

The trouble is that (Fs i) is only known to be of some type Fin (S n),
so we need to return the Fz :: Fin n, and there ain't no such beast.

The question is how to explain that this program actually does make some
sense.

One to ponder.

Cheers

Conor

```