Subject: Re: eta conversion
From: (Rob Warnock)
Date: 2000/05/29
Newsgroups: comp.lang.lisp
Message-ID: <8gsmve$ga0ke$>
Joe Marshall  <> wrote:
| Fernando <spamers@must.die> writes:
| > What is this eta conversion thing?
| In lambda calculus, the expression (lambda (x) (F x)) is equivalent to F
| That's eta conversion.

Provided that "x" is not a free variable in "F", that is.

| Unfortunately, eta conversion doesn't work in
| a typed lambda calculus (in general, anyway).

Yup. The simplest example[*] I know of is "(lambda (x) (3 x))" versus "3".
The predicate "integer?" (INTEGERP in CL) will give different answers when
applied to those two [and so will "procedure?" (FUNCTIONP)].


[*] Sabry & Felleisen, "Reasoning about Programs in Continuation-Passing
    Style" [1992 Conf. on Lisp and Functional Programming], page 3.

Rob Warnock, 41L-955
Applied Networking
Silicon Graphics, Inc.		Phone: 650-933-1673
1600 Amphitheatre Pkwy.		PP-ASEL-IA
Mountain View, CA  94043