Lambda over types.

[oleg@pobox.com]

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.