kahl at cas.mcmaster.ca kahl at cas.mcmaster.ca
Wed Jan 31 09:32:36 EST 2007

```Hi Connor,

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

To me, this looks more like ordinal numbers than like general finite sets:
For each type-level natural number n, the set  Fin n  contains
all object-level natural numbers k < n,
where  k = Fs^k Fz .

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

So ``thin Fz i''  is defined for  i = undefined :: Fin Z.

If you don't want this kind of effect, you might consider to keep the empty

> {-# OPTIONS -fglasgow-exts #-}
> data Z = Z
> data S x = S x

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

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

This gets me one line farther into thicken.
But what is possible now:

Add a lifting (or embedding) function:

> lift :: forall n . Fin n -> Fin (S n)
> lift Fz = Fz
> lift (Fs i) = Fs (lift i)

> thicken0 :: forall n . Fin n -> Fin n -> Maybe (Fin n)
> thicken0 Fz      Fz      = Nothing
> thicken0 Fz      (Fs j)  = Just (lift j)
> thicken0 (Fs i)  Fz      = Just Fz
> thicken0 (Fs i)  (Fs j)  = case (thicken0 i j) of
>      Nothing -> Nothing
>      Just k -> Just (Fs k)

I think that one ley to your trouble is the fact that there is,
as far as I can see, no direct way to define
a predicate determining whether an Fin (S n) element
is the largest of its type:

> isMax :: forall n . Fin (S n) -> Bool
> isMax = undefined

This would need a type case on  Fz :: Fin (S Z)  ---
I'd dig through Oleg's posts about type equality checking.

If you can make this possible, cou can also define

> unlift :: forall n . Fin (S n) -> Maybe (Fin n)
> unlift = undefined

and get your original thicken from that.

Wolfram
```