I feel like a bit of a change of pace, and trying a bit of an experiment.
Re-reading Backus’s old FP work reminds me of what I was doing the last time I read it, which
was back in grad school. At the time, I was working on some stuff involving parallel computation,
and I discovered Robin Milner’s π-calculus as a tool for describing parallel computation. You
can think of π-calculus as being a sort of parallel (pun intended) for the λ-calculus: in
sequential, single-threaded computation, λ-calculus can be a great tool for describing what
things mean. But λ-calculus has absolutely no way of describing the concept of multiple
things happening at once. π-calculus is fundamentally built on the concept of multiple threads
which can only share information by passing messages.
There’s a reason that reading Backus made me think of this, beyond just the temporal coincendence of the fact that I was working with π-calculus the last time I read Backus’s
FP paper. One of the major points that Backus made was how poorly the vonNeumann model was
at describing many computations; that has become far more true in recent years. Even my laptop now has multiple processors; computation just isn’t single-threaded anymore. But most programming languages are basically deeply single-threaded. Even Haskell, for all of its functional
purity, isn’t particularly good at multi-threaded execution. But I’ve always thought it would be
a great idea to build a language around π-calculus the way that ML is built around λ-calculus.
So my experiment, such as it is, is to see if I can work through how to create an actual, useful, non-pathological programming language based on the π-calculus; and not just do that,
but do it publicly, here on the blog.
The obvious starting place is with a quick overview of what π-calculus is. Today, I’llgive you a quick overview of it; and then in another post, I’ll dive into a bit of semantics – but only as much semantics as is really relevant to building a language out of it.
π-calculus is really remarkably simple. The idea is that you describe a set of
processes using the syntax of the calculus, and then there are a set of reduction rules
that describe how the computation actually executes. Syntactically, there are really only six
constructs in λ-calculus; and some of those can be viewed as “compounds”. The basic
- Parallel composition: if P and Q are both processes then “
P|Q” is a process which runs “P” and “Q” in parallel.
- Non-deterministic choice: if P and Q are both processes, then “P+Q” is a process
which will be non-deterministically transformed into either “P” or “Q”, but not both.
- Receive a message. If “P” is a process, and “c” is the name of a communication channel, and
“x” is an identifier, then then “
c(x).P” waits for a message to be received
on channel “c”, binds the contents of that message to the identifier “x”,
and then becomes process P. This is very much like the π-calculus version of
- Send a message: If “P” is a process, “x” is a value, and “c” is the name of a communication channel, then “
*c(x).P” sends the value “x” as a message on channel “c” and then proceeds with process “P”. (In standard π-calculus syntax, this would be written a c with an overbar, but that’s very awkward in HTML, so I’m using “*” as an alternative.)
- Replication: If “P” is a process, then “
!P” is a process consisting of an arbitrary
number of copies of P. “
!P” is syntactically equivalent to “
P|!P“. You can think of “!P” as being something like an HTTP service: no matter
how many times you send an HTTP request to a server, there’s always an HTTP listener waiting
to receive your request.
- Channel creation: If “P” is the name of a process, and “x” is an unbound identifier,
then “(νx)P” creates a new communication channel bound to the identifier “x”, and
then proceeds with process P (where the new identifier is in scope.)
- Process termination/null process. “0” is an identifier for a null process. It’s generally
used to describe process termination: when a process P become 0, it halts.
Computations in π-calculus is described in terms of a fundamental reduction rule, →, which is read “reduces in one step” (think of → as the π-calculus version of β-reduction): “
*x(z).P | x(y).Q→P|(Q[z/y])“, where Q[z/y] means “Q with z replacing y”.
To clarify the what this means in the context of the other constructs, we also usually say the following, although strictly speaking, they should be derivable from the syntax and the basic reduction rule:
- If “P→Q” then “P|R→Q|R”
- If “P→Q” then “(νx)P → (νx)Q”.
- If “(P→Q)” then “(P+R)→Q”.
Suppose that “out” is a communication channel that prints to a standard output. Then
the following is a little “program” in π-calculus which prints hello world.
(νin)( (!(in(x).*out(x).0)) | (*in(hello).*in(world).0) )
We can walk through a quick reduction of that:
(νin)( (!(in(x).*out(x).0)) | (*in(hello).*in(world).0) ) = (νin)( (in(x).*out(x).0|!(in(x).*out(x).0)) | (*in(hello).*in(world).0) ) [! expansion] → (νin)( *out(hello).0|!(in(x).*out(x).0)) | (*in(world).0) ) [one → step on channel "in"] → (νin)( !(in(x).*out(x).0)) | (*in(world).0) ) [one → step with the "invisible" standard out process step] = (νin)( (in(x).*out(x).0|!(in(x).*out(x).0)) | (*in(world).0) ) [Another "!" expansion] → (νin)( *out(world).0|!(in(x).*out(x).0)) | (0) ) [→ on "in"] → (νin)(!(in(x).*out(x).0)) [→ with standard out process on "out".]