- 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
- values V ::= x | \x.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
- (beta.let) let x=V in N --> N[x:=V]
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
- (V) let x=V in C[x] --> let x=V in C[V]
-
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.
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
- nu x. P new : (Ch -> Pr) -> Pr
- 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)
- !x[y].P send (x,[y],P)
For example, here is a pi calculus term and its encoding.
-
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
- op >> : unit Ev * 'b Ev -> 'b Ev
- new2 >>= (fn x => new2 >>= (fn y =>
- fork2 (send2 (x,[y]) >> P) >>
- recv2 (x) >>= (fn [z] => Q)))
- fork2 (send2 (x,[y]) >> P) >>
For example, here is the same term as above, encoded in the new style.
-
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 ()
- return(x) = fn c => c x
- 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
- send2 : Ch * Ch list -> unit Ev
- new3 : unit -> Ch
- send3 : Ch * Ch list -> unit
- recv3 : Ch -> Ch list
- send3 : Ch * Ch list -> unit
- fork2 : unit Ev -> unit Ev
- fork3 : (unit -> unit) -> unit
might be rewritten as
and so why do we need the monad Ev? The answer becomes clearer when we look at the next combinator,
which would be encoded as
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).