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