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