Conal

It certainly makes sense to do backward chaining, but I don’t know any Haskell implementation that’s tried it.  It’d be more complicated in the presence of functional dependencies, since we must “undo” any unifications done as a result of discarded searches, much like the “trail” in a Prolog implementation.

To be honest I can’t see myself trying this anytime soon.  Because of the unification part, it’d be a significant structural change.  And one would need to dig into the theory to make sure that the algorithm was both sound and complete (finds all solutions).

Simon

From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Conal Elliott
Sent: 31 July 2007 20:09
To: haskell@haskell.org
Subject: [Haskell] type class instance selection & search

I keep running into situations in which I want more powerful search in selecting type class instances.  One example I raised in June, in which all of the following instances are useful.

> instance (Functor g, Functor f) => Functor (O g f) where
>   fmap h (O gf) = O (fmap (fmap h) gf)

> instance (Cofunctor g, Cofunctor f) => Functor (O g f) where
>   fmap h (O gf) = O (cofmap (cofmap h) gf)

> instance (Functor g, Cofunctor f) => Cofunctor (O g f) where
>   cofmap h (O gf) = O (fmap (cofmap h) gf)

> instance (Cofunctor g, Functor f) => Cofunctor (O g f) where
>   cofmap h (O gf) = O (cofmap (fmap h) gf)

My understanding is that this sort of instance collection doesn't work together because instance selection is based only on the matching the head of an instance declaration (part after the "=>").  I'm wondering why not use the preconditions as well, via a Prolog-like, backward-chaining search for much more flexible instance selection?  Going further, has anyone investigated using Prolog as a model for instance selection?  Better yet, how about LambdaProlog ( http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog), which generalizes from Horn clauses to (higher-order) hereditary Harrop formulas, including (restricted but powerful) universals, implication, and existentials?  Once search is in there, ambiguity can arise, but perhaps the compiler could signal an error in that case ( i.e., if the ambiguity is not eliminated by further search pruning).