[Haskell] Quantified class constraints (& back-chaining)

[Conal Elliott]

> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell/attachments/20070802/dda680cf/attachment.htm