If only for those watching from home, here are some references. jeff p <mutjida@gmail.com> wrote in article <a6403bb90707312018t7ab9409enb0999b043e01f992@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