[Haskell] Re: type class instance selection & search

[Chung-chieh Shan]

If only for those watching from home, here are some references.

jeff p <mutjida at gmail.com> wrote in article <a6403bb90707312018t7ab9409enb0999b043e01f992 at mail.gmail.com> in gmane.comp.lang.haskell.general:
> >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.

On that note:
Trifonov, Valery. 2003. Simulating quantified class constraints. In
Proceedings of the 2003 Haskell workshop, 98-102. New York: ACM Press.
http://flint.cs.yale.edu/trifonov/papers/sqcc.pdf
http://flint.cs.yale.edu/trifonov/papers/sqcc.ps.gz

> 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.

On that note:
Neubauer, Matthias, and Peter Thiemann. 2002. Type classes with
more higher-order polymorphism. In ICFP '02: Proceedings of the ACM
international conference on functional programming. New York: ACM Press.
http://www.informatik.uni-freiburg.de/~neubauer/papers/icfp02.pdf
http://www.informatik.uni-freiburg.de/~neubauer/papers/icfp02.ps.gz

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
"Injustice is happening now; suffering is happening now. We have
choices to make now. To insist on absolute certainty before starting
to apply ethics to life decisions is a way of choosing to be amoral."
-Richard Stallman