[Haskell-cafe] GADTs: the plot thickens?

Bruno Oliveira bruno.oliveira at comlab.ox.ac.uk
Wed Jan 31 07:45:53 EST 2007

Hello Conor,

The following seems to work:

On 31 Jan 2007, at 11:46, Conor McBride wrote:

> 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

Lets also have naturals reflected at the value level:

 > data Nat :: * -> * where
 >    Zero :: Nat Z
 >    Succ :: Nat n -> Nat (S n)

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

Now we modify thin to take an extra Nat n (not needed, but just to  
show the duality with thickening):

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

The thing to note here is that only:

 > thin (Succ n)  (Fs i)  (Fz)    = Fz

is well typed; if you had the case:

 > thin Zero  (Fs i)  (Fz)    = Fz

you get:

     Inaccessible case alternative: Can't match types `S n' and `Z'
     In the pattern: Fz
     In the definition of `thin': thin Zero (Fs i) (Fz) = Fz
Failed, modules loaded: none.

> Its partial inverse, "thickening" has the spec
> thicken i i = Nothing
> thicken i (thin i j) = Just j

Now lets go for the thickening function:

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

Note that this version of thicken is more precise than the version  
you had -- your third case splits into two
different cases now. The problem is that when you had:

 > thicken (Fs i) Fz = ...

you need to account for two possibilities: the first possibility is  
(Fz :: Fin (S Zero)), to which you want to return Nothing
and (Fz :: Fin (S (S n))) for which you can safely return Just Fz.

Let me know if that helps.



More information about the Haskell-Cafe mailing list