RE: higher-kind deriving ... or not

2002-02-27 Thread Simon Peyton-Jones

|  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

2002-02-27 Thread C T McBride

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