[Haskell] Re: type class instance selection & search

[jeff p]

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