Philip Wadler: Largely lambda, with a slice of pi

Lambda calculus remains a source of inspiration for work on concurrent calculi, and so the first part of the talk summarised some recent developments in lambda calculus. The second part of the talk reversed the usual idea of embedding lambda calculus within pi calculus, and compared two sets of primitives for embedding pi calculus within lambda calculus.
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 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.

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

Embedding pi in lambda
One way to embed pi calculus in lambda calculus is to augment the lambda calculus with one constant for each construct of the pi calculus, modeling binding with higher-order functions in the way first suggested by Church. SML notation is used for the lambda calculus side, where Ch is the type of channels, and Pr the type of processes.

P,Q ::=
nu x. P new : (Ch -> Pr) -> Pr
!x[y_bar].P send : Ch * Ch list * Pr -> Pr
?x[z_bar].Q recv : Ch * (Ch list -> Pr) -> Pr
P | Q op || : Pr * Pr -> Pr
0 none : Pr

For example, here is a pi calculus term and its encoding.

nu x. nu y. new (fn x => new (fn y =>
!x[y].P send (x,[y],P)
| ?x[z].Q || recv (x,fn [z] => Q)
Here is a second set of constants that may be used to represent concurrency, akin to the monadic style used in Concurrent Haskell. It is also surprisingly close to the style used in Concurrent ML. The type Ev corresponds to events in Concurrent ML, or the monad in Concurrent Haskell. The type unit has one value, written ().

op >>= : 'a Ev * ('a -> 'b Ev) -> 'b Ev
op >> : unit Ev * 'b Ev -> 'b Ev
return : 'a -> 'a Ev
new2 : Ch Ev
send2 : Ch * Ch list -> unit Ev
recv2 : Ch -> (Ch list) Ev
fork2 : unit Ev -> unit Ev

For example, here is the same term as above, encoded in the new style.

new2 >>= (fn x => new2 >>= (fn y =>
fork2 (send2 (x,[y]) >> P) >>
recv2 (x) >>= (fn [z] => Q)))
Here is how constants in the second style may be defined in terms of those in the first style. Those familiar with monads will recognize the monadic encoding of CPS.

type 'a Ev = ('a -> Pr) -> Pr

e >>= f = fn c => e (fn x => f x c)
return(x) = fn c => c x
send2(x,y_bar) = fn c => send(x,y_bar,c())
recv2(x) = fn c => recv(x, fn z_bar => c z_bar)
fork2(e) = fn c => e (fn () => none) || c ()

e >> f = e >>= (fn () => f)
The use of a monadic style in Concurrent ML is at first blush rather a surprise. Monads are typically used to encode a call-by-value style of evaluation with side effects into a pure functional language without side effects, where the side-effecting function of type 'a -> 'b corresponds to a side-effect free function of type 'a -> 'b Ev. (Replace Ev by whatever monad captures the side effects you are interested in.) Under this encoding, the functions

new2 : Ch Ev
send2 : Ch * Ch list -> unit Ev
recv2 : Ch -> (Ch list) Ev

might be rewritten as

new3 : unit -> Ch
send3 : Ch * Ch list -> unit
recv3 : Ch -> Ch list

and so why do we need the monad Ev? The answer becomes clearer when we look at the next combinator,

fork2 : unit Ev -> unit Ev

which would be encoded as

fork3 : (unit -> unit) -> unit

where the argument is made into a function, the usual call-by-value trick for turning computations into values. This is workable, but cumbersome, and the attractions of making the monad explicit become clearer.

John Reppy points out there is a further impetus for representing processes explicitly ith the type ('a Ev) rather than implicitly with a side-effecting function (unit -> 'a). In Concurrent ML there is a choice operator, which is similar to fork except the arguments should all denote guarded processes, rather than arbitrary processes. (Choice also differs from fork in taking a list of arguments rather than two, but that is an orthogonal issue.) It is easy enough to contrive that the type ('a Ev) only denotes processes that are guarded, thereby providing an additional impetus for using the explicit ('a Ev) in preference to the implicit (unit -> 'a).

Dagstuhl Seminar on High-level Concurrent Languages
Martin Müller