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@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of Ken | Shan | Sent: 13 November 2003 05:40 | To: haskell-cafe@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.