From: Fernando
Subject: eta conversion
Date: Sun, 28 May 2000 00:00:00 +0000
Message-ID: <f122jscqa3gbs6kstk1rajev5cgmb3vmv7@4ax.com>

Hi!

	What is this eta conversion thing? O:-)  I found it mentionned
in a Lisp related article, but without any explanation....

TIA




//-----------------------------------------------
//	Fernando Rodriguez Romero
//
//	frr at mindless dot com
//------------------------------------------------

• Re: eta conversion Joe Marshall
  • Re: eta conversion Rob Warnock
  • Re: eta conversion Ivar Rummelhoff

From: Joe Marshall
Subject: Re: eta conversion
Date: Sun, 28 May 2000 00:00:00 +0000
Message-ID: <hfbisjh4.fsf@alum.mit.edu>

Fernando <·······@must.die> writes:

> Hi!
> 
> 	What is this eta conversion thing? O:-)  I found it mentionned
> in a Lisp related article, but without any explanation....
> 
> TIA

In lambda calculus, the expression
   (lambda (x) (F x))

is equivalent to 
   F

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

From: Rob Warnock
Subject: Re: eta conversion
Date: Mon, 29 May 2000 00:00:00 +0000
Message-ID: <8gsmve$ga0ke$1@fido.engr.sgi.com>

Joe Marshall  <·········@alum.mit.edu> wrote:
+---------------
| Fernando <·······@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		····@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

From: Ivar Rummelhoff
Subject: Re: eta conversion
Date: Mon, 29 May 2000 00:00:00 +0000
Message-ID: <b874s7hlrij.fsf@adroa.uio.no>

>>>>> Joe Marshall <·········@alum.mit.edu> :
>
> Unfortunately, eta conversion doesn't work in a typed lambda
> calculus (in general, anyway).

For _strongly_ typed lambda calculi eta conversion makes perfectly
sense.  If F:U->V, then F and (lambda (x:U) (F x)) will normally be
considered equivalent.  (How could you tell the difference?)

For _weakly_ typed lambda calculi such as lisp, however, the eta rule
implies that there is only one type: functions.  Hence, it is false in
lisp.
-- 
Ivar Rummelhoff