Lambda over types.

[anatoli]

oleg@pobox.com wrote [in part]:
> 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

It evaluates all right to "A X X" in both ghci 5.02.1
and December 2001 Hugs.

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

Same here: evaluates to 
(L (Next (Next (Next X))) (A (Next (Next X)) (Next (Next (Next X)))),T)

You may be using an older version of Hugs that is known to
have problems with fundeps.

> You may want to try evaluating the following terms:
> 
> ((lambda (x) (x x)) (lambda (y) (y z)))
> ==> (z z)

Here is a real bug, even two.

First, two rules for SameVar are wrong; second, a
rule for Apply is missing.

diff lambda.lhs lambda.lhs.buggy
80c80
< > instance SameVar (Next x) (A y z) F
---
> > instance SameVar (Next x) (A x y) F
82c82
< > instance SameVar (Next x) (L y z) F
---
> > instance SameVar (Next x) (L x y) F
150d149
< > instance (Reduce y y' tryAgain) => Apply (Next x) y (A (Next x) y') tryAgain

With these fixes, this one passes:

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

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

but this does not, no matter what I try:

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

Time to try other approaches...
-- 
anatoli

__________________________________________________
Do You Yahoo!?
Yahoo! Tax Center - online filing with TurboTax
http://taxes.yahoo.com/