- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Philip Wadler <wadler_at_research.bell-labs.com>

Date: Tue, 04 Feb 1997 11:33:01 -0500

*> On the other side,
*

*> it seems a little bit counter-intuitive to prefer 'call-by-value'
*

*> parameter passing for non-deterministic functions if you are
*

*> interested in a LAZY evaluation strategy.
*

It is not at all counter-intuitive. Below is a recent abstract I

wrote, which summarises the close relationship between call-by-value

and call-by-need. So I think that the so-called `call-by-value'

approach to non-deterministic calls is entirely sensible.

-- P

Some recent developments in lambda calculus.

* Moggi's computational calculus, lambda-c, was first proposed in

his 1988 technical report on monads. It has the following grammar

and laws.

terms L,M,N ::= V | P

values V ::= x | \x.N

non-values P ::= LM | let x=M in N

(beta.v) (\x.N)V --> N[x:=V]

(beta.let) let x=V in N --> N[x:=V]

(eta.v) \x.(Vx) --> V

(eta.l) let x=M in x --> M

(assoc) let y=(let x=L in M) in N --> let x=L in (let y=M in N)

(let.1) PM --> let x=P in xM

(let.2) VP --> let y=P in Vy

This calculus contains Plotkin's call-by-value calculus, lambda-v, which

consists onlyof (beta.v) and (eta.v). It is just large enough to have

as equalities all equations that must hold between any two terms

with side effects (where the general notion of side effect may be

modeled using a monad).

* In particular, lambda-c allows us to strengthen Plotkin's

classic CPS results. We view CPS as a translation from lambda-c

to lambda-cps (the smallest subset of lambda-v that contains

in the image of the CPS translation and is closed under reduction).

Write M* for the CPS translation of a lambda-c term M, and

N# for the inverse CPS translation of a lambda-cps term N. Then

we have

lambda-c |- M -->> N# iff lambda-cps |- M* -->> N.

This is an instance of a Galois connection (or an adjoint).

* A variant of lambda-c provides a better model of space as well

as time. Replace (beta.v) and (beta.let) by the following.

(I) (\x.N)M --> let x=M in N

(V) let x=V in C[x] --> let x=V in C[V]

(G.v) let x=V in N --> N, if x not free in N

* A further variant provides a calculus that models call-by-need

rather than call-by-value. Replace (G.v) by the following.

(G) let x=M in N --> n, if x not free in N

The let terms preserve sharing, while the switch from (G.v) to (G)

means that an unneeded term may be discarded without first being

evaluated.

Further discussion of some of these points can be found in the

following papers:

A reflection on call-by-value. Amr Sabry and Philip Wadler.

International Conference on Functional Programming, ACM Press,

Philadelphia, May 1996.

A call-by-need lambda calculus. Zena Ariola, Matthias Felleisen,

John Maraist, Martin Odersky, and Philip Wadler. 22'nd Symposium on

Principles of Programming Languages, ACM Press, San Francisco,

California, January 1995.

Call-by-name, call-by-value, call-by-need, and the linear lambda

calculus. John Maraist, Martin Odersky, David Turner, and Philip

Wadler. 11'th International Conference on the Mathematical

Foundations of Programming Semantics, New Orleans, Lousiana, April

1995.

Lazy vs. strict. Philip Wadler. ACM Computing Surveys, June 1996.

Pointers to these papers can be found at:

http://cm.bell-labs.com/cm/cs/who/wadler/topics/call-by-need.html

-----------------------------------------------------------------------

Philip Wadler wadler_at_research.bell-labs.com

Bell Laboratories http://cm.bell-labs.com/cm/cs/who/wadler/

Lucent Technologies office: +1 908 582 4004

700 Mountain Ave, Room 2T-304 fax: +1 908 582 5857

Murray Hill, NJ 07974-0636 USA home: +1 908 626 9252

-----------------------------------------------------------------------

Received on Di Feb 04 1997 - 18:34:39 CET

Date: Tue, 04 Feb 1997 11:33:01 -0500

It is not at all counter-intuitive. Below is a recent abstract I

wrote, which summarises the close relationship between call-by-value

and call-by-need. So I think that the so-called `call-by-value'

approach to non-deterministic calls is entirely sensible.

-- P

Some recent developments in lambda calculus.

* Moggi's computational calculus, lambda-c, was first proposed in

his 1988 technical report on monads. It has the following grammar

and laws.

terms L,M,N ::= V | P

values V ::= x | \x.N

non-values P ::= LM | let x=M in N

(beta.v) (\x.N)V --> N[x:=V]

(beta.let) let x=V in N --> N[x:=V]

(eta.v) \x.(Vx) --> V

(eta.l) let x=M in x --> M

(assoc) let y=(let x=L in M) in N --> let x=L in (let y=M in N)

(let.1) PM --> let x=P in xM

(let.2) VP --> let y=P in Vy

This calculus contains Plotkin's call-by-value calculus, lambda-v, which

consists onlyof (beta.v) and (eta.v). It is just large enough to have

as equalities all equations that must hold between any two terms

with side effects (where the general notion of side effect may be

modeled using a monad).

* In particular, lambda-c allows us to strengthen Plotkin's

classic CPS results. We view CPS as a translation from lambda-c

to lambda-cps (the smallest subset of lambda-v that contains

in the image of the CPS translation and is closed under reduction).

Write M* for the CPS translation of a lambda-c term M, and

N# for the inverse CPS translation of a lambda-cps term N. Then

we have

lambda-c |- M -->> N# iff lambda-cps |- M* -->> N.

This is an instance of a Galois connection (or an adjoint).

* A variant of lambda-c provides a better model of space as well

as time. Replace (beta.v) and (beta.let) by the following.

(I) (\x.N)M --> let x=M in N

(V) let x=V in C[x] --> let x=V in C[V]

(G.v) let x=V in N --> N, if x not free in N

* A further variant provides a calculus that models call-by-need

rather than call-by-value. Replace (G.v) by the following.

(G) let x=M in N --> n, if x not free in N

The let terms preserve sharing, while the switch from (G.v) to (G)

means that an unneeded term may be discarded without first being

evaluated.

Further discussion of some of these points can be found in the

following papers:

A reflection on call-by-value. Amr Sabry and Philip Wadler.

International Conference on Functional Programming, ACM Press,

Philadelphia, May 1996.

A call-by-need lambda calculus. Zena Ariola, Matthias Felleisen,

John Maraist, Martin Odersky, and Philip Wadler. 22'nd Symposium on

Principles of Programming Languages, ACM Press, San Francisco,

California, January 1995.

Call-by-name, call-by-value, call-by-need, and the linear lambda

calculus. John Maraist, Martin Odersky, David Turner, and Philip

Wadler. 11'th International Conference on the Mathematical

Foundations of Programming Semantics, New Orleans, Lousiana, April

1995.

Lazy vs. strict. Philip Wadler. ACM Computing Surveys, June 1996.

Pointers to these papers can be found at:

http://cm.bell-labs.com/cm/cs/who/wadler/topics/call-by-need.html

-----------------------------------------------------------------------

Philip Wadler wadler_at_research.bell-labs.com

Bell Laboratories http://cm.bell-labs.com/cm/cs/who/wadler/

Lucent Technologies office: +1 908 582 4004

700 Mountain Ave, Room 2T-304 fax: +1 908 582 5857

Murray Hill, NJ 07974-0636 USA home: +1 908 626 9252

-----------------------------------------------------------------------

Received on Di Feb 04 1997 - 18:34:39 CET

*
This archive was generated by hypermail 2.3.0
: So Sep 25 2022 - 07:15:06 CEST
*