[Haskell-cafe] GADTs: the plot thickens?

[kahl at cas.mcmaster.ca]

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
type away from your calculations:

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