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
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 again On Wed, 27 Feb 2002, Tom Pledger wrote: > 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) Fair point, but this is just a thinly disguised first-order type constructor: type Sport f = Maybe (f Bool) Correspondingly, it's fine just to check Show for the actual instance which is used. In effect, some higher-kind parameters to datatypes are unnecessary because all their usages can abstracted as type parameters, and the corresponding applications of f passed in as arguments, just as above. However, once you introduce a fixpoint, this abstraction is no longer possible: > 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. Perhaps banning such derivings for all higher-kind parametric datatypes is being a bit of a spoilsport: we can allow it exactly where it isn't necessary! Another interesting aspect of Tom's example is that the show instance exists in practice exactly because (i) Show Bool (ii) Show a => Show (f a) -- when f is Maybe These are the properties expressed by the relevant instance declarations. They are strictly stronger than Show (f Bool), but it takes a pretty bizarre f to make the distinction. Unfortunately, although we can express (ii) as a property, we can't demand it as a property, because constraints are first-order. If we could, the problem with fixpoints would go away, but instance inference would get even more complex than it already is in post 98 Haskell. There's a real question here: at what point does a problem become too complex for us to accept automation as the only means of its solution? 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. Could there be a corresponding hybrid approach for instance inference? Conor ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: higher-kind deriving ... or not
Conor writes: > newtype Copy a = Copy a deriving Show > >data Wonky f > = Wonky > | Manky (f (Wonky f)) > deriving Show > show (Wonky :: 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? Rejecting such things might be a bit extreme, for example, you could drop the 'deriving Show' on 'Copy a', define: instance Show (Copy a) where show _ = "whatever" then: show (Wonky :: Wonky Copy) is fine and does not result in an infinite loop of context reduction. Of course this makes the example even wonkier ... (In another post Tom Pledger illustrates another example: data Sport f = Sport | Association (f Bool) deriving Show test = show (Sport :: Sport Maybe) where higher kinded arguments do not cause any trouble). The context reducer could probably do a better job at detecting when it is in an infinite loop: Show (Wonky Copy) --> Show (Copy (Wonky Copy)) --> Show (Wonky Copy) ... Cheers, Bernie. ___ 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
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
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
