[Haskell-cafe] GADTs: the plot thickens?

[Bruno Oliveira]

Hello Pablo,

What I meant was simply that the function thin does not need the  
extra Nat n argument to compile;
Conor's original version was already compiling:

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

The reason why I modified thin was to show the similarity with  
thicken (since thicken is the partial inverse
of thin). When you have the new version of thin:

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

it becomes easier to see how to define the inverse, for example we  
can see that there is not a case for:

 > thin Zero  (Fs i)  (Fz)    = Fz    -- type-error

which hints for the following case in thicken:

 > thicken Zero             (Fs i)  Fz      = Nothing

So, although having the new version of thin helps you with the  
definition of thicken, we do not need it to have
a working thin function. That's all I meant.

Cheers,

Bruno

On 31 Jan 2007, at 12:57, Pablo Nogueira wrote:

> Bruno,
>
>> Now we modify thin to take an extra Nat n (not needed, but just to
>> show the duality with thickening):
>
> I'm puzzled by the "not needed" bit. Isn't the introduction of  Fin's
> indices reflected as values in  the GADT , and the fact that the GADT
> makes that reflection, what makes it work?
>
> P.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe