Subject: Re: eta conversion
From: rpw3@rigden.engr.sgi.com (Rob Warnock)
Date: 2000/05/29
Newsgroups: comp.lang.lisp
Message-ID: <8gsmve$ga0ke$1@fido.engr.sgi.com>
Joe Marshall  <jmarshall@alum.mit.edu> 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)].


-Rob

[*] Sabry & Felleisen, "Reasoning about Programs in Continuation-Passing
    Style" [1992 Conf. on Lisp and Functional Programming], page 3.
    <URL:http://www.cs.rice.edu/CS/PLT/Publications/lfp92-sf.ps.gz>

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