RE: higher-kind deriving ... or not
| data Wonky f |= Wonky || Manky (f (Wonky f)) |deriving Show | | The trouble is that when I ask either hugs -98 or ghci | -fglasgow-exts to | | show (Wonky :: Wonky Copy) | | the poor compiler's brain explodes. I fixed this a few weeks ago. GHC (5.03) now says: Foo.hs:3: No instance for `Show (f (Wonky f))' When deriving the `Show' instance for type `Wonky' | I tried to guess the type of the show instance derived for | Wonky. Being a naive sort of chap, I thought it might be | | show :: (forall a. Show a = Show (f a)) = Wonky f - String Not naive. That's exactly the right type. See Section 7 of Derivable type classes. http://research.microsoft.com/~simonpj/Papers/derive.htm Havn't implemented this, yet, alas. | It's clear that with typing problems, inference becomes | unsustainable pretty soon after you leave the safe harbours | of the Hindley-Milner system. However, lots of lovely | programs have more interesting types: it would be very | frustrating if Haskell forbade these programs just because | their types were not inferrable---not least since, for these | jobs, we usually do think of the type first and the code | afterwards. Sensibly, Haskell allows us to write these types | down, so the machine's task is merely checking. This hybrid | approach preserves type inference for `old' code, whilst | promoting more adventurous programming by allowing us to say | what we mean when the machine is too dim to guess. I agree wholeheartedly with this; it's exactly the approach I'm trying to take with GHC. One obvious extension is to let the user specify the context for a derived instance decl, but still let the compiler generate the code. Havn't done this either! Simon ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: higher-kind deriving ... or not
Hi On Thu, 28 Feb 2002, Tom Pledger wrote: C T McBride writes: | data Fix f = Fix (f (Fix f)) | | There's no equivalent first-order definition. This is where | higher-kind parameters actually buy us extra stuff, and it's also the | point at which the first-order constraint for show becomes hopeless. Did you see the technique Mark Tullsen posted last year, for making instances in the presence of a fixpoint? I've found it useful. http://haskell.cs.yale.edu/pipermail/haskell/2001-May/003942.html Thanks for the pointer. Yes, that looks like a kind of hard-coding of the lifting to higher kinds that I'm after. If I understand things correctly, it would seem that for every type class C t, indexed by types, one can manufacture the constructor class FC f which asserts that f preserves C-ness. For each C-method m :: blah[t] one gives the FC method fm :: C t = blah[f t] One can lift further, by defining classes for constructors with higher-kind parameters which take FC-ness (or whatever) to C-ness. Requiring FC f (a first-order constraint on a higher-kind thing) is a plausible fake of requiring (forall a. C a = C (f a)) (a higher-order constraint on types). If I read correctly, automating this construction, effectively yielding computation of classes from kinds, is part of Simon PJ and Ralf Hinze's `Deriving Type Classes' proposal. The functionality is clearly desirable. It does, however, come at the cost of introducing a third and still separate programming language as a component of Haskell---the language of programming over kinds. It's no good asking when this will stop, because it doesn't. It is worth asking when the different layers of this hierarchy will acquire a greater uniformity. Cheers Conor ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
higher-kind deriving ... or not
Hi I'm rather fond of fixpoint constructions like this one: newtype Copy a = Copy a deriving Show data Wonky f = Wonky | Manky (f (Wonky f)) deriving Show (Clearly this is an ill-motivated example, but the real example which caused this problem is available on request...) The trouble is that when I ask either hugs -98 or ghci -fglasgow-exts to show (Wonky :: Wonky Copy) the poor compiler's brain explodes. I take it this is a known problem with instance inference, deriving, etc. Of course, it's easy to write my own show for Wonky Copy, but that's a tad annoying. I tried to guess the type of the show instance derived for Wonky. Being a naive sort of chap, I thought it might be show :: (forall a. Show a = Show (f a)) = Wonky f - String but that's a syntax error. A little more tinkering, and it looks like it might be show :: Show (f (Wonky f)) = Wonky f - String Is this really the type of show? If so, no wonder there's a problem. I don't want to start an argument about how to solve this problem. I do want to suggest that, for the time being, it would be better to reject `deriving Show' for type constructors like Wonky (ie those with higher-kind parameters) than to generate instances which break the compiler. Or am I just being a spoilsport? Conor ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
higher-kind deriving ... or not
C T McBride writes: : | A little more tinkering, and it looks like it might be | | show :: Show (f (Wonky f)) = Wonky f - String | | Is this really the type of show? That looks correct to me. | If so, no wonder there's a problem. Yes, there's a vicious circle in context reduction, between Wonky Copy and Copy (Wonky Copy). | I don't want to start an argument about how to solve this problem. I | do want to suggest that, for the time being, it would be better to | reject `deriving Show' for type constructors like Wonky (ie those with | higher-kind parameters) than to generate instances which break the | compiler. | | Or am I just being a spoilsport? It depends on your definition of sport. ;-) data Sport f = Sport | Association (f Bool) deriving Show test = show (Sport :: Sport Maybe) Regards, Tom ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
higher-kind deriving ... or not
Tom Pledger writes: | C T McBride writes: | : | | A little more tinkering, and it looks like it might be | | | | show :: Show (f (Wonky f)) = Wonky f - String | | | | Is this really the type of show? | | That looks correct to me. Well, after the first context reduction, anyway. The type starts as Show a = a - String and after substitution becomes Show (Wonky f) = Wonky f - String and I'm not sure whether the first context reduction happens right after that, or waits until f is substituted by something more concrete. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
