Hypothetical reasoning in type classes
ken at digitas.harvard.edu
Thu Nov 13 00:40:18 EST 2003
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...
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."
"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
Size: 189 bytes
Desc: Digital signature
Url : http://haskell.org/pipermail/haskell-cafe/attachments/20031113/20817a3b/attachment.bin
More information about the Haskell-Cafe