Lambda over types.

[oleg@pobox.com]

> Well, I tried to fix the problems you mention.  Results attached.

I'm sorry I can't get it to work.
The simplest example passes:

Lambda> :t eval (A (L x0 x0) x1)
eval (A (L x0 x0) x1) :: Next X 

but even anything more complex seems to fail:

Lambda> :t eval (A (L x0 x0) (A x0 x0))
eval (A (L x0 x0) (A x0 x0)) :: Eval (A (L X X) (A X X)) a => a

The reduce functions seems to do better:

Lambda> :t reduce (A (L x0 x0) (L x1 x1))
reduce (A (L x0 x0) (L x1 x1)) :: (L (Next X) (Next X),T) 

but fails on more complex examples:
Lambda> :t reduce (A (L x0 (L x1 (A x0 x1))) x2)
reduce (A (L x0 (L x1 (A x0 x1))) x2) :: Reduce (A (L X (L (Next X) (A
X (Next X)))) (Next (Next X))) (L a (A b c)) d => (L a (A b c),d)

> I have managed to do without de Brujin  notation.
It seems that you've implemented something like the calculus of
explicit substitutions. The latter has a 'shift' operation to shift
up all the variables: s0 -> s1, s1 -> s2, etc.

> I'll try to come up with a regression test suite
You may want to try evaluating the following terms:

((lambda (x) (x x)) (lambda (y) (y z)))
==> (z z)

(lambda (a) ((lambda (x) (lambda (a) (x a))) a))
==> (lambda (a) (lambda (a-new) (a a-new)))

; compute a*(a+b) 
(
  (lambda (a) (lambda (b)
     (lambda (f) (a (lambda (x) ((b f) ((a f) x)))))))

  (lambda (f) (lambda (x) (f (f x))))	; Numeral 2
  (lambda (f) (lambda (x) (f x)))	; Numeral 1
  )
==> numeral for 6

These are some of the tests from my meta-lambda calculator.

The normal-order evaluator recipe includes a "repeat until done"
phrase. This is one of the challenging aspects: keeping track when
done. It seems there is a simpler, purely recursive way of performing
the normal reductions. First we need a more general notation for
applications: (A t (C t1 (C t2 CNil))) is the same as ((A t t1) t2).
The algorithm can be expressed as a sequence of the following
re-writing rules, which must be tried in the order given:

	; The top-level is a lambda-term: reduce inside
Eval (L x body) -> (L x (Eval body))
	; The top-most leftmost is a redex
	; Reduce it and retry from the top
Eval ((L x body) term) -> Eval (Beta x body term)
	; The topmost is a nested application
	; Unfold using the associativity rule:
	; If (a b) is not a redex and a is not a pair, we try reducing b
	; If (a b) is not a redex and a is a pair (x y), we unfold this
	; as (x y b) and repeat.
Eval ((x) rest) -> Eval (x rest)  ; (x) is the same as x
Eval ((x y . in-rest) . rest) -> Eval (Append (x y . in-rest) rest)
		; In topmost (x y z ...), x is not an appl and not an abst
		; It is equivalent to ((x y) z ...)
		; Try to reduce y, z, etc. separately
Eval (x y . rest) -> (A x (Map Eval (y . rest)))
		; The topmost is (x) -- remove the extra parens
Eval (term) -> Eval term
Eval var -> var

This algorithm has been literally implemented in 
	http://pobox.com/~oleg/ftp/Computation/rewriting-rule-lambda.txt
(in a continuation-passing-style).