For a while now, I have been very interested in programming language theory and process calculi and have started to study them. To be honest, it something that I wouldn't mind going into for a career. I find the theory to be incredibly fascinating. One constant question I keep running into is if either PL Theory or Process Calculi have any importance at all in modern programming language development. I see so many variants on the Pi-calculus out there and there is a lot of active research, but will they ever be needed or have important applications? The reason why I ask is because I love developing programming languages and the true end goal would be to use the theory to actually build a PL. For the stuff I have written, there really has not been any correlation to theory at all.
5 Answers
My answer is really just an elaboration of Gilles', that I had not read before I wrote mine. Maybe it's nevertheless helpful.
Let me begin my attempt at answering your question with a distinction between two dimensions of programming languages work that relate quite differently to programming language theory in general and process calculus in particular.
Pure research.
Product focused research and development.
The latter typically takes place in industry with the aim of providing programming languages as a product. The teams developing Java at Oracle and C# at Microsoft are examples. In contrast, pure research is not tied to products. Its aim is to understand programming languages as objects of intrinsic interest and to explore the mathematical structures underlying all programming languages.
Because of divergent goals, Different aspects of programming language theory are relevant in pure research and in product focused R&D The picture below may give an indication what's important where.
One may ask at this point why the two dimensions are so seemingly different and how they nevertheless relate.
The key insight is that programming language research and development has multiple dimensions: technical, social and economic. Almost by definition, industry is interested in the economic payoff of programming languages. Microsoft et al don't develop languages out of the goodness of their hearts but because they believe programming languages give them an economic advantage. And they have investigated deeply why some programming languages succeed, and others, seemingly similar or with more advanced features, don't. And they found that there isn't a single reason. Programming languages and their environments are complex, and so are the reasons for adopting or ignoring any specific language. But the single biggest factor for the success of a programming language is the preferential attachment of programmers to languages that are already widely used: the more people use a language, the more libraries, tools, teaching material are available, and the more productive a programmer can be using that language. This is also called the network effect. Another reason is the the high cost switching languages for individuals and organisation: mastering language, especially to a not-so-experienced programmer, and when the semantic distance to familiar languages is large, is a serious, time-consuming effort. Given these facts, one may ask why do new languages get traction at all? Why do companies develop new languages at all? Why don't we just stay with Java or Cobol? I think there are several key reasons for whey a language does succeed, and displaces the originally more popular incumbents.
A new domain of programming opens up that has no incumbents to displace. The primary example is the web with its concomitant rise of Javascript.
Language stickiness. By this I mean the high price of changing language. But sometimes programmers move into different fields, taking a programming language with them, and being successful with the old language in the new field.
A language is pushed by a big company with serious financial firepower. This backing reduces the risk of adoption, because early adopters can be reasonably sure that the language will still be supported in a few years. A good example of this is C#.
A language might come with compelling tools and eco-system. Here too C# and it's .Net and Visual Studio eco-system could be mentioned as an example.
Old languages pick up new features. Java comes to mind, which, in each iteration, picks up more good ideas from the functional programming tradition.
Finally, a new language might have intrinsic technical advantages, e.g. be more expressive, have nicer syntax, typing systems that catch more errors, etc.
Given this background, it should not come as a surprise that there is somewhat of a disconnect between pure programming language research, and commercial programming language development. While both aim to make software construction and evolution more efficient, especially for large-scale software, industrial programming language work must be more interested in facilitating quick adoption to reach a critical mass and get the network effect. This leads to a research focus on things that working programmers care about. And that tends to be things like library availability, compiler speed, quality of compiled code, portability and so on. Process calculus as we practise it today is of little use to programmers working on mainstream projects (although I believe that will change in the future).
Pure programming language research is quite different. It works with simplified models of programming languages: the $\lambda$-calculus is a massive simplification of functional programming. In the same way the $\pi$-calculus is a massive simplification of concurrent programming. These massive simplifications are the key to successful research. They enable us to focus on core computational mechanisms (e.g. $\beta$-reduction for functional programming, resolution/unification for logic-programming, name-passing for concurrent computation). To understand if a language like Scala can have viable full type-inference, we don't need to worry about the JVM. Indeed thinking about the JVM will detract from a better understanding of type-inference. That's why abstraction of computation into tiny core calculi is vital and powerful.
So you can think of programming language research as a massive sandbox where people play with toys, and if they find something interesting when playing with a specific toy, and have investigated the toy thoroughly, then that interesting toy begins its long march towards mainstream industrial acceptance. I say long march because language features first invented by programming language researcher tend to take decades before becoming widely accepted. For example garbage collection was conceived in the 1950s and became widely available with Java in the 1990s. Pattern matching harks back to 1970 and is widely used only since Scala.
Process calculus is an especially interesting toy. But it's too new to be investigated thoroughly. That will take another decade of pure research. What currently going in process theory research is to take the single biggest success story of programming language research, the theory of (sequential) types and develop the theory of types for message passing concurrency. Typing systems of moderate expressivity for sequential programming, say Hindley-Milner, are now well-understood, ubiquitous and accepted by working programmers. We'd like to have moderately expressive types for concurrent programming. Research on this started in the 1980s by pioneers like Milner, Sangiorgi, Turner, Kobayashi, Honda, and others, often based, explicitly or implicitly, on the idea of linearity which comes from linear logic. The last few years have seen a major increase in activity and I expect this upwards trajectory to continue for the foreseeable future. I also expect this work to start leaking into product focused R&D, in parts for the pragmatic reason that young researchers who have been trained in process calculus will go and work in industrial R&D labs, but also because of the evolution of CPU and computer architecture away from sequential forms of computation.
In summary, I would not worry that you don't find cutting edge programming language theory such as process calculus useful in your own work of building languages. That's simply because cutting edge theory does not address the concerns of current programming languages. It is about future languages. It will take a while for the 'real world' to catch up. The knowledge you use to build languages for today is the programming language theory of the past. I encourage you to learn more about process calculus because it's one of the most exiting areas of all of theoretical computer science.
-
1$\begingroup$ Wow! How much time did it take to make that diagram, and can I use it in the future? $\endgroup$– codyJul 27, 2014 at 17:05
-
1$\begingroup$ @cody Took a few seconds with OmniGraffle, and feel free to use it. $\endgroup$ Jul 27, 2014 at 17:26
The science of programming language design is very much in its infancy. Theory (the study of what programs mean and of the expressivity of a language) and empiricism (what programmers manage or don't manage to do) give a lot of qualitative arguments to weigh one way or another when designing a language. But we rarely have any quantitative reason to decide.
There is a delay between the time some theory stabilizes enough for an innovation to be usable in a practical programming language, and the time this innovation begins to appear in “mainstream” languages. For example, automatic memory management with garbage collection can be said to have been mature for industrial use in the mid-1960s, but to have only reached mainstream with Java in 1995. Parametric polymorphism was well-understood in the late 1970s, and made it into Java in the mid-200s. On the scale of a researcher's career, 30 years is a long time.
Wide-scale industrial adoption of a language is a matter for sociologists to study, and that science is even more in its infancy. Market considerations are an important factor — if Sun, Microsoft or Apple pushes a language, this has a lot more impact than any number of POPL and PLDI papers. Even for a programmer who has a choice, library availability is usually far more important than language design. Which is not to say that language design isn't important: having a well-designed language is a relief! It just usually isn't the deciding factor.
Process calculi are still at the stage where the theory hasn't stabilized. We believe that we understand sequential calculations — all the models of things that we like to call sequential calculation are equivalent (that's the Church-Turing thesis). This does not hold for concurrency: different process calculi tend to have subtle differences in expressivity.
Process calculi do have practical implications. A lot of computations out there are distributed — they involve clients talking to servers, servers talking to other servers, etc. Even local computations are very often multithreaded to take advantage of parallelism over multiple processors and to react to environmental concurrency (communication with independent programs and with the user).
Are research advances needed to make better software? After all there's a billion-dollar industry out there that can't tell the pi calculus from a pie in the sky. Then again, that industry spends billions of dollars fixing bugs.
“Will they ever be needed” is never a worthwhile question in research. It is impossible to predict in advance what will have long-term consequences. I would even go further and say that it is a safe assumption that any research will have consequences one day — we just don't know at the time whether that day will come next year or next millennium.
I see so many variants on the Pi-calculus out there and there is a lot of active research, but will they ever be needed or have important applications?
The reason why I ask is because I love developing programming languages and the true end goal would be to use the theory to actually build a PL. For the stuff I have written, there really has not been any correlation to theory at all.
This is a tricky question! I'll tell you my personal opinion, and I emphasize that this is my opinion.
I do not think pi-calculus is directly suitable as a notation for concurrent programming. However, I think you should definitely study it before designing a concurrent programming language. The reason is that pi-calculus gives a low-level --- but importantly, compositional! --- account of concurrency. As a result, it can express everything you want, but not always conveniently.
Explaining this comment requires thinking a bit about types. First, useful programming languages generally need some kind of type discipline in order to build abstractions. In particular, you need some kind of function type to make use of procedural abstractions when building software.
Now, the natural type discipline of pi-calculus is some variant of classical linear logic. See, for instance, Abramsky's paper Process Realizability, which shows how you interpret simple concurrent programs as proofs of propositions from linear logic. (The literature contains a lot of work on session types for typing pi-calculus programs, but session types and linear types are very closely related.)
However, I said that the natural type discipline of pi-calculus is classical linear logic, and this is the source of the difficulty in using it directly as a programming language. In most presentations of classical linear logic, the (linear) function type $A \multimap B$ is not a primitive. Instead, you encode function types using de Morgan duality $A^\bot ⅋ B$.
This is just fine from the POV type theory, but it's awkward when programming. The reason is that programmers end up managing not just their function calls, but also the call stack. (Indeed, encodings of lambda calculus into pi calculus typically end up looking like CPS transforms.) Now, typing ensures that they will never screw this up, but nevertheless it's a lot of bookkeeping foisted onto the programmer.
This is not a problem unique to concurrency theory --- the mu-calculus gives a good proof-theoretic account of sequential control operators like call/cc, but at the price of making the stack explicit, which makes it an awkward programming language.
So when designing a concurrent programming language, my opinion is that you should design your language with higher-level abstractions than the raw pi-calculus, but you should make sure that it cleanly translated into a sensible typed process calculus. (A nice recent example of this is Tonhino, Caires and Pfenning's Higher-Order Processes, Functions and Sessions: A Monadic Integration.)
-
$\begingroup$ In what sense to you need to manage the call stack in $\pi$-calculus? This happens automatically in Milner's encoding of $\lambda$ into $\pi$ and also in the new Van Bakel/Vigliotti encoding. Functions are a perfectly fine form of syntactic sugar in $\pi$-calculus. $\endgroup$ Jun 17, 2014 at 11:04
-
$\begingroup$ Also, the $\lambda\mu$-calculus is a really awkward account of sequential control operators like call/cc. Such operators are much more easily and naturally expressed in the $\pi$-caluclus, because jumping is a clearly a form of message passing. $\lambda$-calculus doesn't have a natural notion of name that you can jump to, so you have to code it up as funciton application, or you have to add additional stuff. $\endgroup$ Jun 17, 2014 at 11:07
-
$\begingroup$ One fruitful way of thinking about functions is that they are client-server interactions, where the return channel is affine and the server channel is replicated. This can be typed easily. Session types don't fully capture this, as they are slightly too weak in the constraints on interaction they enforce. $\endgroup$ Jun 17, 2014 at 11:11
-
$\begingroup$ All that said, of course one doesn't want to program in raw $\pi$-calculus any more than in raw $\lambda$-calculus. Both formalism are simplifications that enable us to focus on some features of computation at the exclusoin of others. $\endgroup$ Jun 17, 2014 at 11:43
-
$\begingroup$ @MartinBerger: I was hoping to convince you to answer! I mean that if you wanted to program in raw $\pi$, and also wanted to use functions, then you'd end up writing terms that are in the image of the Milner translation, and so you'd have to "manage the stack" in the sense that you'd essentially be managing continuations and explicit substitutions. (As an aside, I didn't know about the van Bakel/Vigliotti paper -- thanks!) $\endgroup$ Jun 17, 2014 at 12:39
You say that "the true end goal would be to use the theory to actually build a PL." So, you presumably admit that there are other goals?
From my point of view, the No. 1 purpose of theory is to provide understanding, which can be in reasoning about existing programming languages as well as the programs written in them. In my spare time, I maintain a large piece of software, an email client, written ages ago in Lisp. All the PL theory I know such as Hoare logic, Separation Logic, data abstraction, relational parametricity and contextual equivalence etc. does come in handy in daily work. For instance, if I am extending the software with a new feature, I know that it still has to preserve the original functionality, which means that it should behave the same way under all the old contexts even though it is going to do something new in new contexts. If I didn't know anything about contextual equivalence, I probably wouldn't even be able to frame the issue in that way.
Coming to your question about pi-calculus, I think pi-calculus is still a bit too new to be finding applications in language design. The wikipedia page on pi-calculus does mention BPML and occam-pi as language designs using pi-calculus. But you might also look at the pages of its predecessor CCS, and other process calculi such as CSP, join calculus and others, which have been used in many programming language designs. You might also look at the "Objects and pi-calculus" section of the Sangiorgi and Walker book to see how pi-calculus relates to existing programming languages.
I like to search for practical implementations of process calculi in the wild :) (besides reading about the theory).
- Clojure async channels is based on CSP: http://clojure.com/blog/2013/06/28/clojure-core-async-channels.html
- Golang also has channels based on CSP (this inspired Rich Hickey for clojure I think): http://www.informit.com/articles/printerfriendly/1768317
- There's a guy who made an ACP based extension to scala (Subscript) but I don't have enough reputation to post the link...
etc.
