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 |
---------- 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 |
In reply to this post by Conor McBride
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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 |
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 |
Aha, of course, Sorry, I misunderstood you.
P. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Conor McBride
Hi Bruno
This looks like the stuff! > Lets also have naturals reflected at the value level: > > > data Nat :: * -> * where > > Zero :: Nat Z > > Succ :: Nat n -> Nat (S n) Good plan. Of course, if you combine this method with Pablo's suggestion, you can make the class RepNat n whose method is repNat :: Nat n and then wrap your explicit versions in implicit versions. Implicit information inferred from type information but passed at run time: it's something we need to get used to. I'm glad we only need three definitions of the natural numbers, none of which is data Nat = Zero | Succ Nat > 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. That's a relief. Of course, in Epigram, you get that n is a successor for free, the moment you look at an element of Fin n. > 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. I thought that might work. Your solution is quite close to the Epigram version of the program, but you haven't covered the Zero (Fs i) (Fs j) case, which is impossible anyway. I suggest the following minor modification, whose significance is purely documentary. > 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) j = undefined {- i stinks -} > thicken (Succ _) (Fs i) Fz = Just Fz > thicken (Succ n) (Fs i) (Fs j) = fmap Fs (thicken n i j) The Epigram version explicitly refutes i in the case where it inhabits Fin Z. I thought of this example because of the other thread about empty cases. > Let me know if that helps. It certainly delivers the necessary explanation. What has happened here? Somehow, we discovered that we had to shift some data from the static language to the dynamic language so that we could give the compiler enough information to see what was ok about the program we started with. There's something subtle here. If the compiler just magically swallowed my earlier program, I think we'd lose type safety, because it allows us to manufacture a non-_|_ inhabitant of (Fin Z) fromJust (thicken (Fs undefined) Fz) = Fz :: Maybe (Fin Z) So you really need a safety check there. Another way to do it, crudely but avoiding the run time numbers, is this > thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n) > thicken Fz Fz = Nothing > thicken Fz (Fs j) = Just j > thicken (Fs Fz) Fz = Just Fz > thicken (Fs Fz) (Fs j) = fmap Fs (thicken Fz j) > thicken (Fs (Fs i)) Fz = Just Fz > thicken (Fs (Fs i)) (Fs j) = fmap Fs (thicken (Fs i) j) That's just another way to get the strictness you need. Although it's ugly. Perhaps it's possible to pack up the explanation "every element of a finite set is an element of a nonempty finite set" as some sort of view, although not the sort of view currently being proposed, I guess. Exactly what information is needed in which phase and how totality or its absence affects what's possible are interesting and subtle questions. We live in interesting times. All the best Conor _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Conor McBride
Hi Connor,
> 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) To me, this looks more like ordinal numbers than like general finite sets: For each type-level natural number n, the set Fin n contains all object-level natural numbers k < n, where k = Fs^k Fz . > 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) So ``thin Fz i'' is defined for i = undefined :: Fin Z. If you don't want this kind of effect, you might consider to keep the empty type away from your calculations: > {-# OPTIONS -fglasgow-exts #-} > data Z = Z > data S x = S x > data Fin :: * -> * where > Fz :: Fin (S n) > Fs :: Fin (S n) -> Fin (S (S n)) > thin :: Fin (S (S n)) -> Fin (S n) -> Fin (S (S n)) > thin Fz i = Fs i > thin (Fs i) Fz = Fz > thin (Fs i) (Fs j) = Fs (thin i j) This gets me one line farther into thicken. But what is possible now: Add a lifting (or embedding) function: > lift :: forall n . Fin n -> Fin (S n) > lift Fz = Fz > lift (Fs i) = Fs (lift i) > thicken0 :: forall n . Fin n -> Fin n -> Maybe (Fin n) > thicken0 Fz Fz = Nothing > thicken0 Fz (Fs j) = Just (lift j) > thicken0 (Fs i) Fz = Just Fz > thicken0 (Fs i) (Fs j) = case (thicken0 i j) of > Nothing -> Nothing > Just k -> Just (Fs k) I think that one ley to your trouble is the fact that there is, as far as I can see, no direct way to define a predicate determining whether an Fin (S n) element is the largest of its type: > isMax :: forall n . Fin (S n) -> Bool > isMax = undefined This would need a type case on Fz :: Fin (S Z) --- I'd dig through Oleg's posts about type equality checking. If you can make this possible, cou can also define > unlift :: forall n . Fin (S n) -> Maybe (Fin n) > unlift = undefined and get your original thicken from that. Wolfram _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Conor McBride
> 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) > [...] > So you really need a safety check there. Another way to do it, crudely > but avoiding the run time numbers, is this > >> thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n) >> thicken Fz Fz = Nothing >> thicken Fz (Fs j) = Just j >> thicken (Fs Fz) Fz = Just Fz >> thicken (Fs Fz) (Fs j) = fmap Fs (thicken Fz j) >> thicken (Fs (Fs i)) Fz = Just Fz >> thicken (Fs (Fs i)) (Fs j) = fmap Fs (thicken (Fs i) j) Isn't the problem simply that in the former 'thicken', the compiler can not guarantee that the case thicken (Fs i) Fz = Just Fz does never show up when we have 'thicken :: Fin (S Z) -> ...'? I mean the subtle point about Fin is that 'Fz' is the "only" inhabitant of 'Fin (S Z)'. At least, this is what Epigram can deduce. But due to _|_, every constructor that is declared may appear in the form of Fs _|_ That's why only the latter 'thicken' can be correct. Regards, apfelmus _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |