Hypothetical reasoning in type classes

[Ken Shan]

Hello,

Has anyone thought about adding hereditary Harrop formulas, in other
words hypothetical reasoning and universal quantification, to the
instance contexts in the Hsakell type class system?  Just today (and not
only today) I wanted to write instance definitions like

    instance (forall a. C a => D a) => E [a] where ...

This is analogous to wanting to write a rank-2 dictionary constructor

    (forall a. C a -> D a) -> E [a]

at the term level, but with type classes, this dictionary constructor
should be applied automatically, in a type-directed fashion, at compile
time.  The theory behind such instance contexts doesn't seem so
intractable; indeed it looks decidable to my cursory examination.  The
opreational intuition is that we would like the type checker to generate
an eigenvariable "a" and perform hypothetical reasoning.

I would also like to quantify universally over type classes; in other
words, if "?" is the kind of a type class constraint (aka a dictionary
type; perhaps "o" would be a better choice of notation), then I would
like to define not just types of kind "*->*->?" (aka type classes) or
kind "(*->*)->?" (aka constructor classes), but also types of kind
"(*->?)->(*->?)".  But that's for another day...

	Ken

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
"Hi, my name is Kent, and I let people change my .sig on the internet."
"Hi, Ken!"
"Put midgets back in midget porn!" -- Not authorized by Ken Shan. Supported by
the association of midget porn workers, Local 9823.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://haskell.org/pipermail/haskell-cafe/attachments/20031113/20817a3b/attachment.bin