9 messages
Open this post in threaded view
|

 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 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.  > 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) Its partial inverse, "thickening" has the spec thicken i i = Nothing thicken i (thin i j) = Just j  > thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n)  > thicken Fz      Fz      = Nothing  > thicken Fz      (Fs j)  = Just j  > thicken (Fs i)  Fz      = Just Fz  > thicken (Fs i)  (Fs j)  = fmap Fs (thicken i j) The trouble is that whilst thin compiles, thicken does not. GHC rightly complains Thicken.lhs:18:32:     Couldn't match expected type `n' (a rigid variable)        against inferred type `S n1'       `n' is bound by the type signature for `thicken'     at Thicken.lhs:15:19       Expected type: Fin n       Inferred type: Fin (S n1)     In the first argument of `Just', namely `Fz'     In the expression: Just Fz The trouble is that (Fs i) is only known to be of some type Fin (S n), so we need to return the Fz :: Fin n, and there ain't no such beast. The question is how to explain that this program actually does make some sense. One to ponder. Cheers Conor _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Fwd: GADTs: the plot thickens?

 ---------- Forwarded message ---------- From: Pablo Nogueira <[hidden email]> Date: 31-Jan-2007 12:04 Subject: Re: [Haskell-cafe] GADTs: the plot thickens? To: Conor McBride <[hidden email]> I haven't tried this yet, but would declaring the class Nat be a starting point? class Nat n instance Nat Z instance Nat n => Nat (S n) data Fin :: * -> * where    Fz :: Nat n => Fin (S n)    Fs :: Nat n => Fin n -> Fin (S n) thin :: Nat n => Fin (S n) -> Fin n -> Fin (S n) thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n) Btw, apparently we have to use GHC HEAD if we want GADTs to compile properly. The error seems very similar to the one you get when trying to write (++) for dependent lists with length encoded as GADTs. To make sure I understand,  you are asking if there is a hack that will enable us to tell the Haskell type checker that  n = (S n1), right? Regards, P. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: GADTs: the plot thickens?

Open this post in threaded view
|

## Re: GADTs: the plot thickens?

 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: GADTs: the plot thickens?

 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 > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

## Re: GADTs: the plot thickens?

Open this post in threaded view
|