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: Conor.lhs:28:21: 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. Cheers, Bruno
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.
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
Aha, of course, Sorry, I misunderstood you. P.
participants (2)
-
Bruno Oliveira -
Pablo Nogueira