anatoli <anatoli at yahoo> wrote:
This is all, of course, of purely academical interest. The notation is extremely inconvenient to do any real work. I'd rather prefer a real, language-supported lambda over types.
Or... wait a minute! You did find all those problems; does it mean you tried to *use* this stuff for something? Just curious.
I must start with a profuse apology, because what follows is perhaps of little relevance to the list. I also propose to re-direct the follow-ups to the Haskell Cafe. I have examined your code and then tried a few examples, some of which from my code's regression tests. I have implemented a compile-time lambda-calculator, in a different language. I should say, in a meta-language. The output of the evaluator is a term that can then be compiled and evaluated. The lambda-calculator acts as a partial evaluator. The calculator normalizes a term in a pure untyped lambda calculus. The result is compiled and evaluated in a call-by-value lambda-calculus with constants. Haskell typechecker (augmented with multi-parameter classes with functional dependencies and let on loose) may do something similar. BTW, the meta-language lambda-evaluator code (with the regression tests) can be found at http://pobox.com/~oleg/ftp/Computation/rewriting-rule-lambda.txt The calculator is implemented in CPS, in some sort of extended lambda calculus. Therefore, the code has three kinds of lambdas: of the source language, of the transformer meta-language, and of the target language. The first and the third lambdas are spelled the same and are the same.