higher-kind deriving ... or not
C T McBride
Wed, 27 Feb 2002 20:52:47 +0000 (GMT)
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.
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