> 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