higher-kind deriving ... or not

[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