Implicit typing à la ML for the join-calculus ^{∗}

Cédric Fournet ^{†} Cosimo Laneve ^{‡} Luc Maranget^{†} Didier Rémy^{†}

Abstract

We adapt the Damas-Milner typing discipline to the join-calculus. The main result is a new generalization criterion that extends the polymorphism of ML to join-definitions. We prove the correctness of our typing rules with regard to a chemical semantics. We also relate typed extensions of the core join-calculus to functional languages.

1 Introduction

The distributed implementation of concurrent calculi with message passing raises the problem of implementing communication channels, which finally reduces to the specification of channel managers. In order to reflect this need in the language itself, a new formalism has been recently introduced : the join-calculus [2]. This calculus is similar to Milner’s asynchronous π-calculus, except that the operations of restriction, reception and replication are all combined into a single receptor definition. Such a combination yields better control over communication. In [2, 3], we relied on this locality property to model realistic distributed systems. In this paper, we propose a type system for the join-calculus whose simplicity owes much to locality.

The join-calculus is quite expressive (a lot of examples may be found in [2, 3]) and has been turned into a programming language. A convenient syntax has been provided for sequential composition, process migration and failure detection. A distributed implementation is under way and would benefit from static analyses of programs. A good static semantics should of course rely on a type system. The types we need should be expressive enough for most useful programs and easy to understand for programmers.

This goal is achieved by adapting the Damas-Milner typing discipline developed for ML [1] to the join calculus. From the typing point of view, definitions in the join-calculus are a generalized form of let expressions in ML and polymorphism can be introduced right after typechecking the clauses of a join-definition.

∗This work is partly supported by the ESPRIT CONFER-2 WG-21836

†INRIA Rocquencourt, BP 105, 78153 Le Chesnay Cedex France.

‡Dipartimento di Scienze dell’Informazione, University of Bologna, Mura Anteo Zamboni 7, 40127 Bologna, Italy

However, synchronization on channels is more demanding than plain function calls, as it interacts with polymorphism. Our main result is a generalization criterion for the join-calculus that addresses this issue. We prove the correctness of the resulting typing rules with regard to our concurrent semantics by adapting standard techniques to the chemical framework. Thus, without any change, the join calculus becomes a typed process calculus with implicit parametric polymorphism.

1.1 Polymorphism in the join-calculus

The join-calculus is essentially a name-passing calculus : port names are defined, then used as addresses in messages that convey other names. These messages are polyadic ; the type of a name carrying n objects of type τ_{1}, …, τ_{n} is written ⟨τ_{1}, …, τ_{n}⟩. Traditional languages come with system-supplied primitives, which can be used in the programming practice. Similarly, we could assume systemsupplied primitive names for a language based on the join-calculus, such as print_int that outputs its integer argument on the console. Then,

    def print_two_ints⟨x,y⟩ ▷ print_int⟨x⟩ | print_int⟨y⟩

defines a new name print_two_ints that prints two integers ; more precisely, when the name print_two_ints receives a couple of arguments ⟨x,y⟩, it activates two processes print_int⟨x⟩ and print_int⟨y⟩ running concurrently. The type of the primitive print_int is ⟨int⟩ (i.e., a name that carries one integer) and the type of the new name print_two_ints is ⟨int, int⟩ (i.e., a name that carries two integers).

In this context, a name with a polymorphic type in the join-calculus is reminiscent of a polymorphic function in ML : both don’t need to perform fully type-specific operations on their arguments. Thus, the types of the arguments are not completely specified and unspecified parts are represented by type variables that stand for just any type. This framework is known as parametric polymorphism. For instance, consider the following definition :

    def apply⟨k,x⟩ ▷ k⟨x⟩

The name apply takes two arguments k and x and activates the process k⟨x⟩. Thus, if x is of type τ, then k must carry names of type τ, i.e. be of type ⟨τ⟩. The name apply can be given type ⟨⟨τ⟩, τ⟩ for any type τ. As in ML, this is emphasized by giving apply the type scheme ∀ α. ⟨⟨α⟩, α⟩. Therefore apply can take arguments as print_int and 4, by the call apply⟨print_int,4⟩, thereby instantiating α with the type int. Given another primitive print_string, another legitimate invocation apply⟨print_string,'foo'⟩ would instantiate α with the type string.

The join-calculus improves on ML by providing synchronization between join patterns (several messages in parallel). Consider, for instance, a variant of apply that receives k and x from different sources.

    def port⟨k⟩ | arg⟨x⟩ ▷ k⟨x⟩

The concurrent activation of the co-defined names port and arg fires k⟨x⟩. The names port and arg can be typed with ⟨⟨α⟩⟩ and ⟨α⟩, respectively. Observe, however, that names port and arg are correlated, which is reflected by the use of the same type variable α in their types. This forbids to give port and arg the type schemes ∀ α. ⟨α⟩ and ∀ α. ⟨⟨α⟩⟩. Otherwise, their types schemes could be instantiated independently, loosing their correlation. Clearly, sending the primitive print_string on port and an integer on arg would result in a run-time type error : attempting to print an integer as a string.

As a consequence, our generalization rule copes with synchronization in an abstract way : a type variable cannot be generalized if it appears free in the type of several co-defined names.

1.2 Overview

In section 2, we recall the syntax and semantics of the join-calculus and we present the type system. The original RCHAM used in [3] has a defect as regards typing ; we introduce a variant and we relate it to the original. In section 3, we establish the main result : we prove subject reduction in a chemical setting and we show that well-typed programs cannot go wrong at run-time. In section 4, we briefly discuss type inference, as implemented in our prototype compiler. In section 5, we extend the join-calculus with support for functions and expressions, an useful step towards an effective programming language. We generalize the type system accordingly. This extension provides a good basis for a detailed comparison with type systems for functional languages. In section 6, we compare our work with other type systems that have been proposed for concurrent calculi.

2 The typed join-calculus

2.1 Syntax

While names already provide enough expressiveness [2], it is convenient here to supplement names with constants that represent basic values 1, 2…,'foo'… and primitives add, string_of_int, print, along with their basic types such as

int, string.

For names, we assume given a set of port names x ∈ N and a set of constants k ∈ K. We use u ∈ N ∪ K to denote a name in general. For types, we assume given a set of basic types b ∈ T and a set of type variables α.

\begin{matrix}P ::= & u⟨u_{i} ^{i∈1..p}⟩ \\ | & def D in P \\ | & P | P \\ D ::= & J ▷ P \\ | & D ∧ D \\ J ::= & x⟨x_{i} ^{i∈1..p}⟩ \\ | & J | J \end{matrix}  \begin{matrix}τ ::= & b | α | ⟨τ_{i} ^{i∈1..p}⟩ \\ σ ::= & τ | ∀ α. σ \\ A ::= & ∅ | A + (u : σ) \\ B ::= & ∅ | B + (u : τ) \end{matrix}

A process P is either a message, a defining process, or a parallel composition of processes ; a definition D consists of one or several clauses J ▷ P that associate a guarded process P to a specific message pattern J ; a join-pattern J consists of one or several messages in parallel. We say that the pattern J = … x⟨z_{i} ^{i∈1..p}⟩ … defines the name x. We note dv(D) for the set of all names that are defined in D.

Processes and definitions are known modulo renaming of bound variables, as substitution performs α-conversion to avoid captures.

A type τ is either a basic type, a type variable, or a message type conveying a fixed number of types ; a type scheme σ may quantify over type variables ; a typing environment A associates type schemes to names, while a simple environment B associates types to names. Given an environment A that already associates a type scheme to a name u, the new environment A + (u : σ) is well formed and associates σ to u.

Primitive names K are given with a primitive typing environment A_{K} of domain K.

2.2 Typing rules

There are three kinds of typing judgments :

A ⊢ u : τ the name u has type τ in A;
A ⊢ P  the process P is well-typed in A;
A ⊢ D :: B the definition D is well-typed in A with types B for its defined names.

The following rules describe valid proofs for our judgments. They are much inspired by the typing rules for the (polyadic) λ-calculus plus let rec, the real innovation being the generalization in Def.

\frac{u : ∀ α_{i} ^{i∈1..n}. τ ∈ A}{A ⊢ u : τ[τ_{i}/α_{i} ^{i∈1..n}]}^{(Inst)}  \frac{A ⊢ P  A ⊢ Q}{A ⊢ P | Q}^{(Par)}

\frac{A ⊢ u : ⟨τ_{i} ^{i∈1..n}⟩ (A ⊢ u_{i} : τ_{i}) ^{i∈1..n}}{A ⊢ u⟨u_{i} ^{i∈1..n}⟩}^{(Message)}

\frac{A + u_{ij} : τ_{ij} ^{i∈1..n,j∈1..m_{i}} ⊢ P}{A ⊢ x_{1}⟨u_{1j} ^{j∈1..m_{1}}⟩ | … x_{n}⟨u_{nj} ^{j∈1..m_{n}}⟩ ▷ P :: (x_{i} : ⟨τ_{ij} ^{j∈1..m_{i}}⟩) ^{i∈1..n}}^{(Rule)}

\frac{A ⊢ D_{1} :: B_{1} A ⊢ D_{2} :: B_{2}}{A ⊢ D_{1} ∧ D_{2} :: B_{1} ⊕ B_{2}}^{(And)} (Def)

\frac{A + B ⊢ D :: B A + Gen(B, A) ⊢ P}{A ⊢ def D in P}

The rules use the following definitions :

• B_{1}⊕B_{2} is B_{1}+B_{2}, and requires B_{1} and B_{2} to be equal on dv(B_{1})∩dv(B_{2}).

• Gen(B, A) is the generalization of the simple environment B of the form (x_{i} : τ_{i}) ^{i∈1..n} with respect to A: let fv(A) be the set ⋃_{(x:σ)∈A} fv(σ) where fv(σ) contains the free variables of σ; let B\x be the environment B without the binding for x. Then Gen(B, A) is (x_{i} : ∀ (fv(τ_{i}) − fv(A + B\x_{i})) .τ_{i}) ^{i∈1..n}.

2.3 Chemical Semantics

For our type system to be of some use, we must show its consistency with respect to the semantics of the join-calculus.

This semantics is specified as a reflexive chemical abstract machine (RCHAM), as in [2]. The state of the computation is a chemical soup D ⊢ P that consists of two multisets : active definitions D and running processes P.

The chemical soup evolves according to two families of rules : Structural rules ⇀ ↽ are reversible (⇀ is heating, ↽ is cooling) ; they represent the syntactical rearrangement of terms (heating breaks terms into smaller ones, cooling builds larger terms from their components). Reduction rules ⟶ consume specific processes present in the soup, replacing them by some others ; they are the basic computation steps. In the following, a generic rule will be denoted by the symbol ⇀ ↽ ⟶, and we will write dv(D) for the union ⋃_{D∈D} dv(D).

Every rule applies on any matching subpart of the soup. More explicitly, for every rule ⇀ ↽ ⟶, we also have a context rule :

\frac{D_{1} ⊢ P_{1} ⇀ ↽ ⟶ D_{2} ⊢ P_{2} (fv(D) ∪ fv(P)) ∩ dv(D_{1}\D_{2} ∪ D_{2}\D_{1}) = ∅}{D ∪ D_{1} ⊢ P_{1} ∪ P ⇀ ↽ ⟶ D ∪ D_{2} ⊢ P_{2} ∪ P}^{(Context)}

A chemical semantics naturally induces a structural equivalence ≡ on terms, defined as the smallest structural congruence that contains ⇀ ↽; this leads to a more classical presentation of the semantics as term rewriting modulo equivalence.

The original machine

In [2, 3], the chemical rules are :

⊢ P_{1} | P_{2}  ⇀ ↽  ⊢ P_{1}, P_{2}  S-Par
D_{1} ∧ D_{2} ⊢  ⇀ ↽ D_{1}, D_{2} ⊢  S-And
⊢ def D in P ⇀ ↽  D ⊢ P  S-Def
J ▷ P ⊢ φ(J)  ⟶ J ▷ P ⊢ φ(P)  R-β
⊢ k⟨u_{i} ^{i∈1..p}⟩ ⟶  ⊢ P  R-δ

with the side-conditions :

• (S-Def) the names defined in D must not appear anywhere in solution but in the reacting process and definition D and P. This condition is global ; in combination with α-renaming it enforces lexical scoping.

• (R-β) φ(·) substitute actual names for the received variables in J and P.

• (R-δ) (u_{i} ^{i∈1..p}, P) ∈ δ_{k}, where {δ_{k}, k ∈ K} is a family of primitive relations that map names u_{i} ^{i∈1..p} to processes P.

We would expect every typing property to be preserved by the structural equivalence, but this is not the case here. The trouble lies in the grouping of definitions that changes outer bound occurrences into recursive ones. Given two definitions D_{1} and D_{2} such that some names defined by D_{1} occur free in D_{2}, but not the converse, we have

              def D_{1} indef D_{2} in P ≡ def D_{1} ∧ D_{2} in P

Unfortunately, the valid typing judgments for the names defined in D_{1} and used in D_{2} are not the same on each side of the equivalence. Polymorphic typing can be used in the left program and not in the right program. In fact, we run across the classical limitation of typing for mutually-recursive functions.

The restricted machine

To solve this problem, we introduce a variant of the RCHAM that is better suited to our typing purposes. In the new machine, definitions with several clauses are not heated ; more specifically, the structural rule S-And disappears and the reduction rule R-β is generalized :

⊢ P_{1} | P_{2}  ⇀ ↽′  ⊢ P_{1}, P_{2} S-Par
⊢ def D in P ⇀ ↽′  D ⊢ P  S-Def
⋯ ∧ J ▷ P ∧ ⋯ ⊢ φ(J)  ⟶′ ⋯ ∧ J ▷ P ∧ ⋯ ⊢ φ(P) R-β’
⊢ k⟨u ^{i∈1..p}⟩ ⟶′  ⊢ P  R-δ

In the rule R-β’ above, ⋯ ∧ J ▷ P ∧ ⋯ stands for an active definition that contains the clause J ▷ P. This notation now expresses the commutativity and the associativity of ∧, which were conveyed more explicitly by the structural rule S-And.

In addition, and for every chemical soup D ⊢ P, we require every name to be defined in exactly one definition of D:

∀D, D′ ∈ D, dv(D) ∩ dv(D′) = ∅

We now relate this restricted machine to the original one. Let us first consider machines that operate on completely diluted solutions (i.e., heating rules cannot apply anymore). There is a straightforward correspondence between chemical solutions of the two formalisms : processes are the same atoms ; definitions are equivalent to the clauses that enter into it. Given this equivalence, β-reduction is the same relation in both frameworks. In the general case, structural cooling in the first machine may lead to more programs. However, we still have :

(⟶) ⊂ (⟶′) ⊂ ( ⇀^{S-And})^{∗} ∘ (⟶) ∘ ( ↽^{S-And})^{∗}

In the following, we use the restricted chemical machine without further discussion. We drop the ′ notation and write ⟶ and ⇀ ↽ for the restricted chemical rules.

2.4 Type-checking solutions

Typing of programs easily extends to chemical solutions. First, we introduce a judgment A ⊢ D to state that the assumptions made in A on the names defined in D are the same as if those names had been added in A after typing the definition D. Precisely, we type D in the environment A extended (actually overridden) with new assumptions B that must be exactly the typing environment produced by D as in rule Def ; then, we check that the generalization of B in A is equal to A restricted to dv(B), i.e. Gen(B, A) is a subset of A. Observe that A + B is also (A \ dv(B)) + B.

We introduce a new typing judgment A ⊢ D ⊢ P to state that the chemical solution D ⊢ P is well-typed in environment A. This happens when all definitions and all processes are independently well typed in the same environment A:

(Multi)

\frac{A + B ⊢ D :: B Gen(B, A) ⊂ A}{A ⊢ D}

\frac{∀P ∈ P, A ⊢ P ∀D ∈ D, A ⊢ D}{A ⊢ D ⊢ P}^{(Soup)}

Typing chemical solutions simplifies our proofs by avoiding some of the technicalities introduced by the more common formalism of term-rewriting modulo structural equivalence. In particular, the chemistry treats structural rearrangements and proper reductions in the same way. This simplification has already been profitably used in untyped concurrency theory.

3 Correctness of the evaluation

From a quite abstract point of view, let us assume that some evaluation steps of a program P yields a new program P′. Typing and evaluation agree when two facts hold : first, a typing derivation of P′ can be constructed from a typing derivation of P. Second, messages present in P′ cannot cause “run-time type errors” such as the addition of a string or sending one argument only on a binary name (no type mismatch for primitives, no wrong arity for defined names).

3.1 Assumptions on primitives

For the reduction to be sound, we assume that the primitive reduction relations are consistent with the primitive typing environment A_{K} introduced in section 2.1. That is, for every typing environment A and for every k ∈ K, we have :

A + A_{K} ⊢ k⟨u_{i} ^{i∈1..p}⟩ and (u_{i} ^{i∈1..p}, P) ∈ δ_{k} ⇒ A + A_{K} ⊢ P

In particular, the free names of P are either primitives or among the u_{i}.

3.2 Basic properties for the typing

Lemma 1 (Useless variable) Let u be a name that is not free in P or D, nor defined in D. Then we have :

\begin{matrix}A ⊢ P ⇔ & A + (u : σ) ⊢ P \\ A ⊢ D :: B ⇔ & A + (u : σ) ⊢ D :: B \end{matrix}

Lemma 2 (Renaming of type variables) Let φ be a substitution on type variables. We have :

\begin{matrix}A ⊢ P ⇒ & φ(A) ⊢ P \\ A ⊢ D :: B ⇒ & φ(A) ⊢ D :: φ(B) \end{matrix}

We say that a type ∀ ᾱ. τ is more general than ∀ ᾱ′. τ′ if τ′ is of the form τ[τ̄′′/ᾱ]. This notion lifts to set of assumptions as follows : A′ is more general than A if A and A′ have the same domain and for each u in their domain, A′(u) is more general than A(u).

Lemma 3 (Generalization) If A ⊢ P and A′ is more general than A, then A′ ⊢ P.

Lemma 4 (Substitution of a name in a term) If A + (u : τ) ⊢ P and A ⊢ v : τ then A ⊢ P [v/u].

3.3 Subject reduction

Two environments A and A′ agree when their restrictions to primitive names are equal. We define the relation ⊂ between RCHAMs as the preservation of typings, that is, D ⊢ P ⊂ D′ ⊢ P′ if for any typing environment A such that A ⊢ D ⊢ P, there exists a typing environment A′ such the A′ ⊢ D′ ⊢ P′ and A and A′ agree.

Theorem 1 (subject-reduction) One-step chemical reductions preserve typings

\underline{Proof} : In fact, we prove the stronger property that typing environments also agree on variable names, except maybe on variable names that are defined in either chemical soup but not in both.

That is, for every ⇀ ↽ ⟶, let D ⊢ P ⇀ ↽ ⟶ D′ ⊢ P′ and A ⊢ D ⊢ P. We show that D′ ⊢ P′ is well-typed in an environment A′ that possibly differ from A only on dv((D \ D′) ∪ (D′ \ D)). We prove this property by induction on the number of applications of rule Context in the derivation of the one-step reduction.

Basic case : We first consider the basic case for every reaction rule.

Subcase S-Par : The reduction is ⊢ P_{1} | P_{2} ⇀ ↽ ⊢ P_{1}, P_{2}. Heating : Clearly, if A ⊢ P_{1} | P_{2} then A ⊢ P_{1}, P_{2} by rules Par and Def. Cooling : is as easy.

Subcase S-Def : The reduction is ⊢ def D in P ⇀ ↽ D ⊢ P. Heating : Let us assume that A ⊢ def D in P, that is, there is a derivation ending with :

A + B ⊢ D :: B A + Gen(B, A) ⊢ P \overline{(Def)}

                          A ⊢ def D in P

Clearly, Def and Soup give A + Gen(B, A) ⊢ D ⊢ P. Cooling : Let A ⊢ D ⊢ P. Then A is of the form A′ + Gen(B, A′) and we have both A′+B ⊢ D :: B and A′+Gen(B, A′) ⊢ P. Thus, by Def, A′ ⊢ def D in P.

In both cases, the two typing environments agree on primitive names and on names defined both in the solution to the left and to the right of the structural rule.

Subcase R-β: We first assume that D is J ▷ Q. Therefore let A ⊢ J ▷ Q ⊢ φ(J), where J is of the form x_{1}⟨ū_{1}⟩ | … x_{n}⟨ū_{n}⟩. By the rules Def, Soup and Rule, the hypothesis A ⊢ J ▷ Q ⊢ φ(J) reduces to assume A = A′+Gen(B, A′) and

A ⊢ φ(J)  (1)
A′ + B + (ū_{i} : τ̄_{i}) ^{i∈1..n} ⊢ P  (2)

where B is (x_{i} : ⟨τ̄_{i}⟩) ^{i∈1..n} and Gen(B, A′) is (x_{i} : ∀ ᾱ_{i}. τ̄_{i}) ^{i∈1..n}, where ᾱ_{i} is equal to fv(τ̄_{i}) \ (fv(A′) ∪ fv(τ̄_{j}) ^{j≠i}).

Observe that the derivation of the judgment (1) must have the shape :

\begin{aligned}A ⊢ x_{i} : ⟨τ̄′_{i}⟩ A ⊢ φ(ū_{i}) : τ̄′_{i} \\ & (Message) \\ A ⊢ x_{i}⟨φ(ū_{i})⟩ \end{aligned} i ∈ 1..n \overline{(Par)}

A ⊢ φ(J) (3)

where types τ̄′_{i} are type instances θ_{i}(τ̄_{i}) of ∀ ᾱ_{i}. τ_{i}, where θ_{i} ranges in ᾱ_{i}. Since generalizable variables never occur in two different bindings, the domains of θ_{i}’s are disjoint and we can define the sum θ of θ_{i}’s for i in 1..n.

Now, applying the substitution φ, which leaves A′ unchanged, to the judgment (2), we get :

A′ + (x_{i} : ⟨θ(τ̄_{i})⟩) ^{i∈1..n} + (ū_{i} : θ(τ̄_{i})) ^{i∈1..n} ⊢ P

By lemma 3, we can generalize the assumptions of the above judgment as follows :

A + (ū_{i} : θ(τ̄_{j})) ^{i∈1..n} ⊢ P

This judgment and the hypothesis A ⊢ φ(ū_{i}) : τ̄′_{i} of (3) allow to derive, by the name substitution lemma 4, A ⊢ P [φ(ū_{j})/ū_{j}], i.e. A ⊢ φ(P).

We now consider the general case of a definition J ▷ P ∧ D. By the rules Def and Soup, the hypothesis A ⊢ J ▷ P ∧ D ⊢ φ(J) reduces to assuming A = A′ + Gen(B, A′) and

A′ + B ⊢ J ▷ P ∧ D :: B A ⊢ φ(J)

By the leftmost judgment and the rule And it follows that B = B′ ⊕ B′′ and A′ + B′ ⊢ J ▷ P :: B′ and A′ + B′′ ⊢ D :: B′′. By lemma 1 applied to A′ + B′ ⊢ J ▷ P :: B′ it follows A′ + B ⊢ J ▷ P :: B′. We reduce to the basic case above by instantiating Rule with this last judgment.

Subcase R-δ: By hypothesis.

Inductive case : We now prove the inductive step uniformly for the context rules. We assume A ⊢ D ∪ D_{1} ⊢ P ∪ P_{1} and D_{1} ⊢ P_{1} ⇀ ↽ ⟶ D_{2} ⊢ P_{2}. By rule Def and Soup, we know that D, D_{1}, P, and P_{1} are all well-typed in A. In particular, A ⊢ D_{1} ⊢ P_{1}. Therefore, by inductive hypothesis, there exists A′ such that A′ ⊢ D_{2} ⊢ P_{2}, i.e. A′ ⊢ D_{2} and A′ ⊢ P_{2}. By inductive hypothesis A and A′ agrees modulo names that are defined in D_{1} and D_{2} but not in both. Let X be such set of names. Then names defined in D are disjoint from X, by the condition in the premise of the rule (Context). Therefore A′ ⊢ D by lemma 1 applied to A ⊢ D. Furthermore, the side condition of the rule S-Def also forces fv(P) to be disjoint from dv((D_{1} \ D_{2}) ∪ (D_{2} \ D_{2})). Thus, we also have A′ ⊢ P, by lemma 1 applied to A ⊢ P. Finally, A′ ⊢ D ∪ D_{2} ⊢ P ∪ P_{2} follows by Soup.

3.4 No run-time errors

We state the correctness of a computation from what can be observed from running chemical machines. When ill-formed messages are released in a solution with a consistent set of primitives (see 3.1), there is no reduction that would consume them, so they remain visible, exactly as barbs on free names in an untyped setting. In this case the computation has failed.

Definition 1 A chemical solution D ⊢ P has failed when P contains either :

• A message k⟨u_{i} ^{i∈1..n}⟩ when no δ-rule applies ;

• A message x⟨u_{i} ^{i∈1..n}⟩ when x is not defined in D, or defined with arity m≠n.

Theorem 2 (Correct computation) A well-typed chemical machine cannot fail through chemical reduction or equivalence. In particular, a typed program cannot fail.

\underline{Proof} : Neither kind of messages of the previous definition can appear in a welltyped chemical soup ; chemical typing is preserved by chemical rewriting.

4 Type inference

Since types and typing rules are in essence those of ML, our type system also allows for type inference. Precisely, there exists an algorithm that given a soup D ⊢ P and a typing environment A_{0} that binds the free names of D and P with the exception of the active names dv(D), returns a typing environment A of domains dv(D) such that A_{0} ⊕A ⊢ D ⊢ P, or fails if no such typing environment exists. Morever, if the algorithms succeeds, then A is principal, that is, for any other typing environment A′ of domain dv(D) such that A_{0} ⊕ A′ ⊢ D ⊢ P, then A is more general than A′.

The complete formalization is a straightforward adaptation of the one for ML [1].

5 Functional constructs

In this section, we extend the join-calculus with functions and expressions and we refine the type system accordingly. Such extensions turn the join-calculus into a practical core language that can be seen as a concurrent extension of a small call-by-value functional language with concurrent evaluation and join-call synchronization.

5.1 Programming in the join-calculus

In practice, programmers feel uncomfortable with the non-deterministic behavior of the “print two integer” example of the introduction ; they would often prefer to print x, then y. The standard trick for enforcing sequential control is to use continuation passing style. Indeed, our implementation provides a synchronous print_int primitive that takes two arguments : an integer to be output, and a continuation to be triggered thereafter. This continuation is used for synchronization only ; it carries no argument, and has type ⟨⟩. Thus, the type of the synchronous print_int is ⟨int, ⟨⟩⟩. The synchronous version of print_two_ints also takes an extra continuation argument, and has type ⟨int, int, ⟨⟩⟩:

    def print_two_ints⟨x,y,k⟩ ▷
      def ky⟨⟩ ▷ k⟨⟩ in
      def kx⟨⟩ ▷ print_int⟨y,ky⟩ in
      print_int⟨x,kx⟩

The continuation passing style idiom is so common in process calculi that it deserves a convenient syntax that avoids writing explicit continuations (see also [8]). In our setting, continuation arguments are implicit in both primitive names and user-defined names. The synchronous version of “print two integers” becomes :

    def print_two_ints⟨x,y⟩ ▷
      print_int⟨x⟩ ; print_int⟨y⟩ ; reply to print_two_ints

The sequencing operator “;” avoids the definition of explicit continuations inside the body of print_two_ints. The final call to continuation is left explicit. This keeps the introduction of synchronous names simple and general, since a joincalculus definition may introduce several synchronous names (and thus several continuations) simultaneously. We write reply u_{1}, ...u_{p} to x by analogy to the C return instruction. We also provide a sequencing binding let x_{1}, ...x_{p} = e in P, where e is an expression, i.e. some kind of process with a continuation. More generally, we do not refrain from the temptation of using ⟨τ_{1}, …, τ_{q}⟩ → ⟨τ′_{1}, …, τ′_{p}⟩ as a convenient synonym for ⟨τ_{1}, …, τ_{q}, ⟨τ′_{1}, …, τ′_{p}⟩⟩. Hence, the type

of print_two_ints can be written ⟨int,int⟩ → ⟨⟩.

5.2 Functions as names

Port names can now be used in two different manners : either asynchronously or synchronously. The synchronous invocation of a name u is performed by the new let x_{i} ^{i∈1..p} = u⟨u_{j} ^{j∈1..q}⟩ in P construct. The other new construct reply u_{i} ^{i∈1..p} to x is the asynchronous invocation of the continuation of x. At run-time, it will fire the pending P of a matching let x_{i} ^{i∈1..p} = x⟨u_{j} ^{j∈1..q}⟩ in P construct.

P ::= u⟨u_{i} ^{i∈1..p}⟩

     | def D in P

| P | P
| let x_{i} ^{i∈1..p} = u⟨u_{j} ^{j∈1..q}⟩ in P
| reply u_{i} ^{i∈1..p} to x

τ ::= b | α | ⟨τ_{i} ^{i∈1..p}⟩_{| ⟨τ_{j} ^{j∈1..q}⟩ → ⟨τ′_{i} ^{i∈1..p}⟩}_{σ ::= τ | ∀ α. σ}

Patterns, clauses and typing environments are as before. The sequencing operator “ ;” corresponds to the let construct with p = 0. There are two additional typing rules for the new constructs :

(Let-Val)

\frac{A ⊢ u : ⟨τ_{j} ^{j∈1..q}⟩ → ⟨τ′_{i} ^{i∈1..p}⟩  (A ⊢ u_{j} : τ_{j}) ^{j∈1..q}  A + (x_{i} : τ′_{i}) ^{i∈1..p} ⊢ P}{A ⊢ let x_{i} ^{i∈1..p} = u⟨u_{j} ^{j∈1..q}⟩ in P}

(Reply)

\frac{A ⊢ x : ⟨τ_{j} ^{j∈1..q}⟩ → ⟨τ′_{i} ^{i∈1..p}⟩ (A ⊢ u_{i} : τ′_{i}) ^{i∈1..p}}{A ⊢ reply u_{i} ^{i∈1..p} to x}

The typing rules guarantee that synchronous and asynchronous invocations on the same name do not mix. Moreover, an user-defined name x must be invoked synchronously when its definition includes type consistent occurrences of the reply u_{i} ^{i∈1..p} to x construct.

Therefore, we give names an asynchronous or synchronous status. Name status may be determined by typing, provided the following agreement : every name whose synchronous usage is not detected by the type inference system is considered asynchronous. In the following, we simply write f, instead of x, for synchronous names.

5.3 A typed CPS encoding

As usual for process calculi, we translate functional names back to the initial joincalculus. The translation applies to type correct programs and once synchronous names have been identified. Given a synchronous name f, we introduce the fresh name κ_{f} for its continuation ; we also use the reserved name κ for intermediate continuations generated while translating lets. The call-by-value translation is :

f⟨u_{i} ^{i∈1..p}⟩ =^{def} f⟨u_{i} ^{i∈1..p}, κ_{f}⟩  (in join-patterns J)
reply u_{i} ^{i∈1..p} to f =^{def} κ_{f}⟨u_{i} ^{i∈1..p}⟩  (in guarded processes P)
let x_{i} ^{i∈1..p} = f⟨u_{j} ^{j∈1..q}⟩ in P =^{def} def κ⟨x_{i} ^{i∈1..p}⟩ ▷ P in f⟨u_{j} ^{j∈1..q}, κ⟩
⟨τ_{j} ^{j∈1..q}⟩ → ⟨τ′_{i} ^{i∈1..p}⟩ =^{def} ⟨τ_{j} ^{j∈1..q}, ⟨τ′_{i} ^{i∈1..p}⟩⟩

The two additional typing rules, once their operands have been translated, are derived from the type system of section 2 :

(translated Let-Val)

\frac{A ⊢ f : ⟨τ_{j} ^{j∈1..q}, ⟨τ′_{i} ^{i∈1..p}⟩⟩  (A ⊢ u_{j} : τ_{j}) ^{j∈1..q}  A + (x_{i} : τ′_{i}) ^{i∈1..p} ⊢ P}{A ⊢ def κ⟨x_{i} ^{i∈1..p}⟩ ▷ P in f⟨u_{j} ^{j∈1..q}, κ⟩}

(translated Reply)

\frac{A ⊢ f : ⟨τ_{j} ^{j∈1..q}, ⟨τ′_{i} ^{i∈1..p}⟩⟩ (A ⊢ u_{i} : τ′_{i}) ^{i∈1..p}}{A ⊢ κ_{f}⟨u_{i} ^{i∈1..p}⟩}

5.4 A join-calculus-based language

A complete syntax for processes and expressions is :

P ::= u⟨E_{i} ^{i∈1..p}⟩

         | def D in P

| P | P
| let x_{i} ^{i∈1..p} = E in P
| reply E_{i} ^{i∈1..p} to x

E ::= u
| u⟨E_{i} ^{i∈1..p}⟩

                                          | def D in E

| let x_{i} ^{i∈1..p} ▷ E in E

Clauses and definitions are as before.

Again, expressions are only a convenient syntactic sugar, which can be removed. This new translation amounts to introducing explicit bindings of the kind of the previous section for all subexpressions, nested calls being translated top-down, left-to-right.

reply E_{i} ^{i∈1..p} to f =^{def} κ_{f}⟨E_{i} ^{i∈1..p}⟩ (in guarded processes P)
u⟨E_{i} ^{i∈1..p}⟩ =^{def} (let x_{i} = E_{i} in) ^{i∈1..p}u⟨x_{i} ^{i∈1..p}⟩
let x = u in P =^{def} P {x/u}
let x_{i} ^{i∈1..p} = f⟨E_{j} ^{j∈1..q}⟩ in P =^{def} def κ⟨x_{i} ^{i∈1..p}⟩ = P in f⟨E_{j} ^{j∈1..q}, κ⟩

In practice, we introduce new typing judgments for expressions (A ⊢ E : τ_{i} ^{i∈1..p}), along with new typing rules. The typing rules for expressions are derived from the previous ones and are omitted.

5.5 A comparison with functional types

If we remove join-composition in patterns and parallel-composition in processes from our language, we get a polyadic functional kernel similar to core-ML : both the reductions and the typing rules do correspond. Let us consider in detail how we would translate the let binder of ML. According to the let-bound expression, there are two cases with distinct typing properties. When the syntax suffices to identify functions either directly or as aliases, we use a generalizing definition :

[[let f(x) = e_{1} in e_{2}]] = def f⟨x⟩ ▷ reply e_{1} to f in e_{2}
[[let g = let f(x) = e_{1} in f in e_{2}]] = def f⟨x⟩ ▷ reply x to f in e_{2}[f/g]

For other values (e.g. function calls), we use a continuation message to convey the result, which forces this result to be monomorphic. This restricts polymorphism to syntactic values and is thus equivalent to Wright’s proposal for ML [13] :

[[let x = f(u) in e_{2}]] = def κ⟨x⟩ ▷ e_{2} in f⟨u, κ⟩

Typing side-effects

The language as a whole is more expressive than ML ; it provides support for general, concurrent programming, including imperative constructs and side-effects as messages. For instance, reference cells need not be taken as primitives ; they are programmable in the join-calculus using the following definition :

    def ref⟨x⟩ ▷
      def get ⟨⟩ | state⟨x⟩ ▷ state⟨x⟩ | reply x to get
      and set⟨y⟩ | state⟨x⟩ ▷ state⟨y⟩ | reply to set
      in  state⟨x⟩ | reply get,set to ref in ...

Here, the state is kept local and, more importantly, both methods get and set are returned in the same message. Since only one name ref has been defined, its type ⟨α → ⟨⟨⟩ → ⟨α⟩, ⟨α⟩ → ⟨⟩⟩⟩, can obviously be generalized. And ref can be used polymorphically :

    let g1,s1 = ref⟨'hello'⟩ in
    let g2,s2 = ref⟨3⟩ in ...

More generally, join-calculus definitions may describe protocols that involve sophisticated synchronization of numerous methods and/or partial states, but this is largely independent of the typing, as long as side-effects are tracked using the sharing of type variables.

This is in contrast with the classical approach in ML, where references are introduced in a “pure” language as dangerous black boxes that cannot be given polymorphic types, and that communicate with a global store by magic. In [14], references are introduced as local stores that can be extruded. This is slightly closer to the join-calculus, but again references are a new special construct. If required, the store can still be identified as some part of the chemical machine, that consists of the instances of cell definitions on the left-hand-side, and of their state messages on the right-hand-side. The approach taken in the joincalculus is uniform and, by the way, it allows to type at least as much as ML with references.

6 Related works for concurrent languages

In the area of name-passing process calculi, the first step was taken by Milner in 1991 [6]. Milner introduced an improvement of the π-calculus, called polyadic π-calculus, where channels are allowed to carry tuples of messages. Polyadicity naturally supports a concept of “sorting”, which is in our view a humble word for typing. In the context of polyadic π-calculus, maintaining the type discipline enforces channels to always carry tuples of the same length and nature.

The first extension of Milner’s system has been undertaken by Pierce and Sangiorgi. They distinguish between input-only, output-only, and input-output channels. This extension naturally leads to recursive types with subtyping [7]. Since then more and more elaborate extensions have then been proposed and experimented, mostly around the Pict language, a strongly-typed implementation of the π-calculus with support for functions and objects [8, 11]. Recently, a further extension captures linearity information in channel types [4]. This provides a finer account on communication patterns, and static type inference leads to a more efficient compilation.

The type systems of all these authors are usually more sophisticated than ours. Some of this sophistication is due to the complexity of the π-calculus semantics and is thus irrelevant in our case. Nevertheless, sophisticated static analysis such as deadlock or linearity analysis would be useful in an optimizing join-calculus compiler. We chose not to integrate such high-level analyses in the basic type system.

The basic theory of polymorphic extensions of Milner’s sort discipline for π-calculus has been developed by Turner in his PhD thesis [11]. We recall that Turner’s polymorphism is explicit : inputs and outputs are always annotated with sorts. For example, the π-calculus process \overline{x}[y, z] | x[u, w]. \overline{u}[w] is tagged as follows :

\overline{x}[int; y, z] | x[α; u :↑ α, w : α]. \overline{u}[α; w] .

Consequently, explicit abstraction and application of types are interleaved with communication : in the above example the sort α in the output \overline{u}[α; w] depends on the message received on the channel x. This commitment to explicit polymorphism in π-calculus follows from the absence of a place where sort generalization may occur.

Typing à la ML for concurrent languages is not new. Proposals have been defined for languages which combine functional and concurrent primitives (among the others, Concurrent ML [9] and Facile [10]). An analogous approach has recently been taken by Vasconcelos for an extension of π-calculus with agent names [12]. In these languages channels are always monomorphic, and polymorphism is only allowed under functional abstractions. This enables to parameterize processes by arguments of different types. However, two processes can never communicate values of different types on the same channel, which restricts the expressiveness of the language. In particular, it is impossible to implement polymorphic services. As a simplified example, consider a computing server :

    def run⟨f,x,r⟩ ▷ f⟨x,r⟩ in . . .

This defines a channel run of type ⟨⟨α,⟨β⟩⟩,α,⟨β⟩⟩ to which expensive requests can be sent together with a channel to receive the result (in the distributed join calculus, the location of the server would also be passed to f so that f can choose to migrate to the server before intensive computing.)

There is apparently no way to define such a service in CML, Facile, or the language proposed in [12]. In fact, this limitation has been known in CML. The solution would be to use first-order, explicit existential types such as in [5]. Then, the channel run could be given the monomorphic type ∃α,β.⟨⟨α,⟨β⟩⟩,α,⟨β⟩⟩. Unsurprisingly, the translation of the example in PICT would give run a similar type.

7 Conclusion

We have typed the join-calculus using traditional parametric polymorphism. Thereby, we demonstrate that successful concepts and techniques now familiar in functional programming carries over to concurrent programming.

This experience strengthens our confidence both in the join-calculus and in parametric polymorphism. The join-calculus is a practical concurrent programming language because it support a simple, convenient and well established typing paradigm. ML polymorphism is not bound to ML ; it can sustain significant changes in the language semantics, provided lexical scoping is maintained and generalization points are clearly identified.

References

[1] L. Damas and R. Milner. Principal type schemes for functional programs. In Proceedings on Principles of Programmining Languages, pages 207 – 212, 1982.

[2] C. Fournet and G. Gonthier. The reflexive chemical abstract machine and the join-calculus. In 23rd ACM Symposium on Principles of Programming Languages (POPL’96), 1996.

[3] C. Fournet, G. Gonthier, J.-J. Lévy, L. Maranget, and D. Rémy. A calculus of mobile agents. In 7th International Conference on Concurrency Theory (CONCUR’96), 1996. LNCS 1119.

[4] N. Kobayashi, B. C. Pierce, and D. N. Turner. Linear types and picalculus. In 23rd ACM Symposium on Principles of Programming Languages (POPL’96), 1996.

[5] K. Läufer and M. Odersky. An extension of ML with first-class abstract types. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, 1992.

[6] R. Milner. The polyadic π-calculus : a tutorial. In Bauer, Brawer, and Schwichtenberg, editors, Logic and Algebra of Specification. Springer Verlag, 1993.

[7] B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. In Logic in Computer Science, pages 187 – 215, 1993.

[8] B. Pierce and D. Turner. Pict : a programming language based on the pi-calculus, 1995. To appear.

[9] J. H. Reppy. Concurrent ML : Design, application and semantics. In Programming, Concurrency, Simulation and Automated Reasoning, pages 165 – 198, 1992. LNCS 693.

[10] B. Thomsen. Polymorphic sorts and types for concurrent functional programs. Technical Report ECRC-93-10, European Computer-Industry Research Center, Munich, Germany, 1993.

[11] D. N. Turner. The π-calculus : Types, polymorphism and implementation. PhD thesis, LFCS, University of Edinburgh, 1995.

[12] V. T. Vasconcelos. Predicative polymorphism in the π-calculus. In Proceedings of 5th Conference on Parallel Architectures and Languages (PARLE 94), 1994. LNCS.

[13] A. K. Wright. Polymorphism for imperative languages without imperative types. Technical Report 93-200, Rice University, February 1993.

[14] A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1) :38–94, 1994.