Hypothetical reasoning in type classes
simonpj at microsoft.com
Thu Nov 13 13:19:28 EST 2003
Yes, absolutely. See
Section 7, and Trifanov's paper at the Haskell Workshop 2003
| -----Original Message-----
| From: haskell-cafe-bounces at haskell.org
[mailto:haskell-cafe-bounces at haskell.org] On Behalf Of Ken
| Sent: 13 November 2003 05:40
| To: haskell-cafe at haskell.org
| Subject: Hypothetical reasoning in type classes
| 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
| 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
| 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
| 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...
| 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
| "Hi, Ken!"
| "Put midgets back in midget porn!" -- Not authorized by Ken Shan.
| the association of midget porn workers, Local 9823.
More information about the Haskell-Cafe