# Lambda over types.

**oleg@pobox.com
**
oleg@pobox.com

*Tue, 2 Apr 2002 11:20:42 -0800 (PST)*

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.