Lambda over types.

[oleg@pobox.com]

anatoli <anatoli at yahoo> wrote:
> Attached are two interpreters: one for untyped lambda calculus,

I'm afraid the attached interpreter can't be an implementation of the
lambda calculus. For one thing, it lacks the hygiene of substitutions:

   Lambda> :t lambdaEval (A (L X (L Y (A X Y))) T)
   lambdaEval (A (L X (L Y (A X Y))) T) :: L Y (A T Y)   

That's OK. However,

   Lambda> :t lambdaEval (A (L X (L Y (A X Y))) Y)
   lambdaEval (A (L X (L Y (A X Y))) Y) :: L Y (A Y Y) 

That is wrong! The correct answer is: L Yfresh (A Y Yfresh)

The interpreter in question doesn't appear to be able to manufacture
fresh identifiers (i.e., fresh types). Without an ability to expand
the set of available identifiers, the capture-free substitution is
impossible.

Furthermore, some terms fail to evaluate:

   Lambda> :t lambdaEval (A (L X (A X X)) T)
   lambdaEval (A (L X (A X X)) T) :: Eval (A (L X (A X X)) T) a => a 

   Lambda> :t lambdaEval (A (A (L X X) T) Y)
   lambdaEval (A (A (L X X) T) Y) :: Eval (A (A (L X X) T) Y) a => a 

which is not the result one would've expected.

Finally, the interpreter doesn't actually find the normal form. The
rule 
   > instance Eval (L v e) (L v e)

prevents any reductions under lambda. True, call-by-name or
call-by-value interpreters stop short of reducing the body of a lambda
form. Normal or applicative order interpreters however -- in order to
find the beta-eta-normal form -- should seek and attempt any
reduction.

The hygienic substitution (with alpha-conversion if necessary) and the
repeated identification of the leftmost outermost redex are actually
quite challenging.

We can guarantee the hygienic substitution if we implement the de
Bruijin notation for lambda terms. Another, related technique is
coloring of existing identifiers. A macro-expander of R5RS Scheme
macros implements the coloring to ensure the hygiene of macro
expansions. The macro-expander can be cajoled into painting
identifiers on our demand, which has been used in a macro-expand-time
lambda calculator. In Haskell, we have to paint manually. A variable
in a typechecker-time lambda-calculator has to be represented by a
type like Vr (Succ (Succ (Succ Zero))) X. The latter component is the
"name" and the former is the color. The Eval and Subst relations
should be extended with color_in and color_out type parameters
(perhaps with a dependency: term color_in -> color_out). The only
non-trivial use of colors is in doing a substitution (L var
body)[exp/var']. The bound variable has to be repainted before the
substitution in the body. The beta-substitutor itself can do the
repainting.