Hypothetical reasoning in type classes

[Simon Peyton-Jones]

Yes, absolutely.  See
	http://research.microsoft.com/~simonpj/Papers/derive.htm
Section 7, and Trifanov's paper at the Haskell Workshop 2003

Simon

| -----Original Message-----
| From: haskell-cafe-bounces at haskell.org
[mailto:haskell-cafe-bounces at haskell.org] On Behalf Of Ken
| Shan
| Sent: 13 November 2003 05:40
| To: haskell-cafe at haskell.org
| Subject: Hypothetical reasoning in type classes
| 
| 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.