On Wed, Aug 01, 2007 at 05:29:19PM -0700, Conal Elliott wrote:
Sadly, this solution runs into the problem of instance selection based only on head-matching, not back-chaining into constraints. For instance, I'd like also to use the following "conflicting" declaration.
instance (Applicative f, Monoid a) => Monoid (f a) where mempty = pure mempty mappend = liftA2 mappend
No quotes - [] is both Applicative and Monoid. Should [String] ["ab","cd"] `mappend` ["ef","gh"] give ["ab","cd","ef","gh"] or ["abef","abgh","cdef","cdgh"]?
Sure enough - a genuine conflict. Thanks for the simple counter-example, Stefan.
What's the state of thinking & doing with regard to universally quantified class constraints?
Note that hereditary Harrop formulas do include universally quantified goals. Less ambitiously, I think GHC's type-checker already deals with universally-quantified variables, so perhaps quantified constraints are not a great reach (just guessing).
It's something I've wanted... Got a link for hereditary Harrop formulas so I can add them to my to-implement-when-Qhc-is-good-enough list? Google isn't telling me much about them except how to add support for constaints, which isn't terribly helpful.
In addition to the "uniform proofs" paper Jeff P mentioned, here's a paper that describes a progression of interpreters in ML, including HHFs. The culmination is a somewhat efficient implementation of a language very like LambdaProlog. http://citeseer.ist.psu.edu/elliott90semifunctional.html Cheers, - Conal