On 7/31/07, jeff p <<a href="mailto:mutjida@gmail.com">mutjida@gmail.com</a>> wrote:<br><br>> Hello,<br><br>> > My understanding is that this sort of instance collection doesn't<br>> > work together because instance selection is based only on the
<br>> > matching the head of an instance declaration (part after the<br>> > "=>"). I'm wondering why not use the preconditions as well, via a<br>> > Prolog-like, backward-chaining search for much more flexible
<br>> > instance selection? Going further, has anyone investigated using<br>> > Prolog as a model for instance selection?<br><br>> I have also wanted more powerful, Prolog-like search for instance<br>> selection; it would be particularly convenient to think of type
<br>> variables as logic variables.<br><br>> I think the main argument against this is that it fundamentally<br>> changes the interpretation of constraints; in particular, if you<br>> really used a Prolog-style search, the order in which you place
<br>> constraints can affect type checking. Is there a sensible way for<br>> instance selection to depend on the "body" which doesn't result in<br>> this?<br><br>How could constraint order affect type checking? Via "cut" ("!")? I'd omit cut. I see how order of constraints or instance declarations might determine order of solutions produced (as in Prolog). If the compiler rejects ambiguity (existence of multiple solutions), then I'd wouldn't expect the order to have any visible effect.
<br><br>> > Better yet, how about LambdaProlog (<br>> > <a href="http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog">http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog</a>), which<br>> > generalizes from Horn clauses to (higher-order) hereditary Harrop
<br>> > formulas, including (restricted but powerful) universals,<br>> > implication, and existentials?<br><br>> Having hereditary Harrop formulas at the type level would be<br>> cool. It would also probably require type level lambdas.
<br><br>Type level lambdas may not be necessary for HHFs. For simplicity, LambdaProlog encodes its universals and existentials via lambdas. I think we could use type lambdas if we wanted but wouldn't have to.<br><br>
Personally, I'd like to have type level lambdas, assuming we can implement them soundly.<br><br>> There was a recent discussion about type level lambdas in Haskell<br>> which ended with the observations that 1) it would mess up
<br>> unification (i.e. make it undecidable and/or too hard) to have<br>> explicit type level lambdas; and 2) they are already implicitly<br>> there (this was pointed out by Oleg) since one can define a type<br>> level application and type level functions. I think 1) is a bit of a
<br>> cop-out since you could always restrict to pattern unification<br>> (L-lamda unification) which is decidable and has MGUs. 2) is true,<br>> but these implicit lambdas don't play very well with instance<br>
> selection and require that all reductions are spelled out via an<br>> Apply type class.<br><br>> I think it might be useful/interesting to have type level lambdas,<br>> and pattern unification, even without turning instance selection
<br>> into proof search.<br><br>Agreed. And vice versa.<br><br>> > Once search is in there, ambiguity can arise, but perhaps the<br>> > compiler could signal an error in that case ( i.e., if the<br>> > ambiguity is not eliminated by further search pruning).
<br><br>> This seems like a slippery slope to me.<br><br>> Although I would like having a full fledged (higher-order) logic<br>> programming language in which to write type level programs, I am not<br>> sure it's a good idea for Haskell in general. I tend to get
<br>> concerned when type class constraints get too big/complicated to be<br>> obviously correct-- what good is the type checker saying something<br>> satisfies a constraint if we're not sure that the specification of
<br>> the constraint itself is correct?<br><br>> -Jeff<br><br>I like this goal of and motivation for simplicity in type specifications. My hope is that a Lambda-Prolog (or some such, and minus cut) would provide a simpler (and more expressive) basis than the very tricky encodings available now (type level function application, backtracking with type-level numeral annotations, etc).
<br><br> - Conal