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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
