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: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] 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).

_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Reply via email to