Lambda over types.
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

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