Hello, > > 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? > I have also wanted more powerful, Prolog-like search for instance selection; it would be particularly convenient to think of type variables as logic variables.
I think the main argument against this is that it fundamentally changes the interpretation of constraints; in particular, if you really used a Prolog-style search, the order in which you place constraints can affect type checking. Is there a sensible way for instance selection to depend on the "body" which doesn't result in this? >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? > Having hereditary Harrop formulas at the type level would be cool. It would also probably require type level lambdas. There was a recent discussion about type level lambdas in Haskell which ended with the observations that 1) it would mess up unification (i.e. make it undecidable and/or too hard) to have explicit type level lambdas; and 2) they are already implicitly there (this was pointed out by Oleg) since one can define a type level application and type level functions. I think 1) is a bit of a cop-out since you could always restrict to pattern unification (L-lamda unification) which is decidable and has MGUs. 2) is true, but these implicit lambdas don't play very well with instance selection and require that all reductions are spelled out via an Apply type class. I think it might be useful/interesting to have type level lambdas, and pattern unification, even without turning instance selection into proof search. >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). > This seems like a slippery slope to me. Although I would like having a full fledged (higher-order) logic programming language in which to write type level programs, I am not sure it's a good idea for Haskell in general. I tend to get concerned when type class constraints get too big/complicated to be obviously correct-- what good is the type checker saying something satisfies a constraint if we're not sure that the specification of the constraint itself is correct? -Jeff _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
