You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A type system is, roughly, a mechanism for classifying the expressions of a language. Type systems for programming languages, sequential and concurrent, are useful for several reasons, most notably:
(1) to detect programming errors statically
(2) to extract information that is useful for reasoning about the behaviour of programs
(3) to improve the efficiency of code generated by a compiler
(4) to make programs easier to understand.
Types are an important part of the theory and of the pragmatics of the $\pi$-calculus, and they are one of the most important differences between $\pi$-calculus and CCS-like languages. Many of the type systems that have been studied for the $\pi$-calculus were suggested by well-known type systems for sequential languages, especially $\lambda$-calculi. In addition, however, type systems specific to processes have been proposed, for instance for preventing certain forms of interference among processes or certain forms of deadlock.
In the book we will be mainly interested in the purposes (1) and (2) of types; purposes (3) and (4) are more specific to programming languages (as opposed to calculi). In this Part of the book we introduce several important type systems and present their basic properties. In the next Part we study the effect of types on process behaviour and reasoning.
We formalize type systems by means of typing rules. The terms that can be typed using these rules are the well-typed terms. The most fundamental property of a type system is its agreement with the reduction relation of the calculus, the subject reduction property. A consequence of this property is type soundness, asserting that well-typed processes do not give rise to run-time errors under reduction. We use a special term wrong to represent a process inside which such an error has occurred. Therefore, type soundness will mean that a well-typed process cannot reduce to a process containing wrong.
We discussed run-time errors informally in Section 3.1, when we introduced the polyadic $\pi$-calculus. There, we used sorting as a mechanism for avoiding errors. Sorting is an example of a type system where equality between types is by name, as opposed to by structure. In the by-name approach, each type has a name (a sort, in the case of a sorting), and two types are equal if they have the same name. In the by-structure approach, two types are equal if they have the same structure. To illustrate the difference, consider two types $T_1$ and $T_2$ that may be ascribed to links that carry booleans. In a by-structure typing, $T_1$ and $T_2$ would be regarded as equal. In a by-name typing, on the other hand, they may be unequal, simply because the two types might have different names. This happens in a sorting if $T_1$ and $T_2$ are different sorts, for example. By-name type equality may be useful for avoiding confusion between types that are structurally equal but are used for different purposes (see Section 9.3 and Remark 9.4.9). By-structure equality, however, is both mathematically more elegant and more flexible. For instance, the by-structure typing rules have a natural interpretation as a logic, more powerful forms of subtyping are available, and two partners can communicate without first agreeing on a name for the type of the data to be exchanged. The last property is important in distributed systems, where the partners may know very little of each other. In this Part, and thereafter in the book, we follow the by-structure approach.
We present several type systems, beginning with a very simple system and then adding type constructs incrementally. For each new type construct, we discuss the associated rules and productions needed for incorporating it in a calculus.
For describing the evolution of processes, we use labelled transition systems, rather than reduction systems. Although some of the proofs of type soundness would be simpler with a reduction system (on this topic, see Remark 6.1.3 and Exercise 6.4.9), the labelled transition systems force us to present more general subject reduction theorems that will in any case be needed in Part IV to obtain proof techniques for reasoning about the behaviour of well-typed processes.
We concentrate on the type systems and omit type-checking algorithms, that is, algorithms for deciding the validity of type judgments. Further, we do not consider type-inference algorithms, that is, algorithms for finding a type for a term. Type systems are easier to understand if algorithmic concerns are left aside.
Structure of the Part The Part consists of three chapters. Chapter 6 lays the foundations. Section 6.1 collects terminology and notation used for the typed calculi in this and later Parts. In Section 6.2 we present Base-$\pi$, essentially the core of CCS with value-passing. Base-$\pi$ will serve as a basis for the typed $\pi$-calculi as well as for the typed higher-order calculi. In Section 6.3 we establish some fundamental properties of the type system for Base-$\pi$. In Section 6.4 we present the (core) simply-typed $\pi$-calculus -- the analogue of the simply-typed $\lambda$-calculus -- and in Section 6.5 we enrich it with the type constructs for products, tuples, unions, records, and variants. In Section 6.6 we describe some convenient derived process constructs for decomposing composite values. In Section 6.7 we discuss recursive types.
Chapter 7 is about subtyping. In Section 7.1 we explain type systems that separate the input and the output capabilities on names. This gives rise to a natural subtyping relation, whose properties are studied in Section 7.2. In Section 7.3 we extend subtyping to the type constructs of Chapter 6. In Section 7.4 we briefly discuss why types, in particular variants, are handy for the representation of objects in the $\pi$-calculus. Section 7.5 is an intermezzo, or an exercise, in which we examine the relative expressiveness of calculi with products, unions, records and variants, with or without subtyping.
In Chapter 8 we look at more refined type systems. First, linearity (Section 8.1), which allows us to control the number of times a name is used; then uniform receptiveness (Section 8.2), which allows us to describe names that are functional, in the sense that the service they provide is persistent and unchanging; and finally parametric polymorphism (Section 8.3), which allows us to have names that can carry values of different types.
6
Foundations
6.1 Terminology and notation for typed calculi
We introduce some terminology and notation for describing typed calculi. On a first reading, it may be best to skim over this section. The main reason for collecting the material here is to make it easier for the reader to find where certain terminology and notation is introduced, than it would be if it were scattered throughout the text.
Definition 6.1.1 (Type environment) An assignment of a type to a name is of the form $a:T$, where $a$ is a name, called the name of the assignment, and $T$ is a type, called the type of the assignment.
A type environment (or type assumption, or, briefly, typing) is a finite set of assignments of types to names, where the names in the assignments are all different. $\Box$
We use $\Gamma, \Delta$ to range over type environments. We ignore the order of the assignments in a type environment. We sometimes regard a type environment $\Gamma$ as a finite function from names to types. Therefore we write $\Gamma(a)$ for the type assigned to $a$ by $\Gamma$, and say that the names of the assignments in $\Gamma$ are the names on which$\Gamma$ is defined. For now, we also call the names of the assignments in $\Gamma$ the support of $\Gamma$, written $supp(\Gamma)$. When we consider polymorphism, however, a type environment $\Gamma$ will also include a set of type variables, and $supp(\Gamma)$ will also include these variables.
To facilitate reading, we sometimes omit curly brackets outside a type environment. For instance we write $a:T,\ b:S$ for the type environment that assigns $T$ to $a$, $S$ to $b$ and is undefined on the other names. We write $\Gamma, \Delta$ for the type environment that is the union of $\Gamma$ and $\Delta$; often $\Delta$ consists of a single type assignment, as in $\Gamma,\ a:T$. Whenever we extend a type environment, we implicitly assume that the environment was not defined on the added names.
Thus, in writing $\Gamma, \Delta$, we assume that the names on which $\Gamma$ and $\Delta$ are defined are disjoint and, similarly, in $\Gamma, a:T$ we assume that $\Gamma$ is not defined on $a$. We write $\Gamma - x$ for the type environment that is undefined on $x$ and is defined as $\Gamma$ elsewhere.
Type judgments are of the form $\Gamma \vdash E:T$, where $E$ may be a process or a value. If $E$ is a process then $T$ is $\diamond$, the behaviour type. A process type judgment $\Gamma \vdash P:\diamond$ asserts that process $P$ respects the type assumptions in $\Gamma$, and a value type judgment$\Gamma \vdash v:T$ that value $v$ has type $T$ under the type assumptions $\Gamma$. Having $\diamond$ in process judgments gives them the same shape as value judgments, and avoids duplication of notations and results. However, we usually abbreviate a process judgment $\Gamma \vdash P:\diamond$ as $\Gamma \vdash P$. The behaviour type $\diamond$ will have an important role in the higher-order calculi of Chapter 12.
Given a type system, a valid type judgment is one that can be proved from the axioms and inference rules of the type system. A proof of the validity of a type judgment is a typing derivation. A process or value $E$ is well typed in $\Gamma$ if there is $T$ such that $\Gamma \vdash E:T$ is valid; $E$ is well typed if it is well typed in $\Gamma$, for some $\Gamma$. We write $\widetilde{x}:\widetilde{T}$ to mean that each $x_i \in \widetilde{x}$ has type $T_i$, and $\Gamma \vdash E_1, E_2:T$ as a shorthand for $\Gamma \vdash E_1:T$ and $\Gamma \vdash E_2:T$. As we deal with several typed calculi, to avoid ambiguity we sometimes add the name of the calculus to type judgments; thus $\mathcal{L} \triangleright \Gamma \vdash E:T$ indicates the type judgment $\Gamma \vdash E:T$ of the calculus $\mathcal{L}$.
In typed calculi, we annotate restricted names with their types, as in $(\nu a:T)P$. Consequently, we add a type also into the notations for bound-output prefixes and local environments, in which a restricted name occurs, and write them as $\overline{b}(a:T).P$ and $P{a:T=(x).Q}$, respectively. In all these cases, however, the type $T$ will be omitted when not important. By contrast, we do not put a type annotation in the bound name $x$ of an input $\alpha(x).P$, as this type can be directly inferred from the type of $a$ (furthermore the type-annotated input prefix is derivable; see Exercise 7.2.13).
A link is a name that may be used to engage in communications. The values are the objects that can be exchanged along links. The link types are the types that can be ascribed to links. The value types are the types that can be ascribed to values. In the $\pi$-calculus, the link types are usually also value types; in Basic $\pi$ (Section 6.2) and in the Higher-Order $\pi$-calculus (Chapter 12), however, link types are not value types. In every typed calculus the names are included among the values, because names can be used as placeholders for values in input prefixes. (The fact that the grammar of values includes names, but that link types may not be value types, should not confuse. 'Link' is more restrictive than 'name': a name may be used as a link, to exchange values, but also as a placeholder for links; and if link types are not value types, then processes cannot exchange values.)
We write $\pi^{\text{op}_1, \dots, \text{op}_n}$ for the $\pi$-calculus in which the value types are determined by the type constructs ${\text{op}_1, \dots, \text{op}_n}$. If $T$ is a link type, then $\mathcal{O}(T)$ is the type of the values that a name of type $T$ may carry. For instance, $\mathcal{O}(\sharp S)$ is $S$ (where $\sharp S$ is the connection type, that is, the type of a name that carries values of type $S$; see Section 6.2). Link-type constructors have syntactic precedence over value-type constructors; see Notation 6.5.1 for an example.
The closed type environments identify the closed processes, which are the processes that are supposed to be run, or to be tested. For now, the only requirement on closed processes is that all their free names have link types. When we discuss linearity, receptiveness, and polymorphism we will add more requirements (for instance, polymorphism uses type variables, and a closed typing will be required to have no free type variables).
Definition 6.1.2 (Closed type environment) A type environment $\Gamma$ is closed if $\Gamma(a)$ is a link type, for all $a$ on which $\Gamma$ is defined. A process $P$ is closed if $\Gamma \vdash P$ for some closed $\Gamma$. $\Box$
The main subject reduction theorems for typed $\pi$-calculi, the analogues of the subject reduction property of typed $\lambda$-calculi, say that closed typings are preserved by silent transitions: if $\Gamma$ is closed and $\Gamma \vdash P$ and $P \stackrel{\tau}{\longrightarrow} P'$, then $\Gamma \vdash P'$. This property holds in all type systems that we will consider.
Remark 6.1.3 We present only the labelled transitions for the typed calculi. Whenever we introduce a new type construct we give the additional transition rules. These will be rules for inferring $\tau$ transitions, and will be of two kinds: error rules, for inferring transitions of the form $P \stackrel{\tau}{\longrightarrow} \mathbf{wrong}$; and $\beta$-reduction rules, for decomposing a composite value into its components. The same rules, without the $\tau$ label, are precisely also the additional rules that would be needed for defining the reduction relation for the calculus in question. $\Box$
We will be very brief about free names, bound names, and related issues. We simply point out, when introducing a new construct, which occurrences of names are binders. As in the previous chapters, round brackets around a name indicate a binding occurrence.
Table 6.1: Base-π: syntax of types
Types
S, T ::= V (value type)
| L (link type)
| ◇ (behaviour type)
Value types
V ::= B (basic type)
Link types
L ::= #V (connection type)
Type environments
Γ ::= Γ, x : L
| Γ, x : V
| ∅
Table 6.2: Base-π: syntax of processes
Values
v, w ::= x (name)
| basval (basic value)
Processes
P, Q, R ::= (ν x : L) P (restriction)
| ... { the other constructs, as in Definition 1.1.1 }
| wrong (error)
OUTERR (where $v$ is not a name) $\overline{v} w. P \xrightarrow{\tau} \textbf{wrong}$
INERR (where $v$ is not a name) $v(x). P \xrightarrow{\tau} \textbf{wrong}$
MATERR (where $v$ or $w$ is not a name) $\dfrac{}{[v=w]P \xrightarrow{\tau} \textbf{wrong}}$
Table 6.4. The transition rules for Base-$\pi$
6.2 Base-$\pi$
We begin describing a very simple typed calculus, Base-$\pi$, essentially the core of CCS with value-passing. The typing and operational rules, however, are set up in such a way as to facilitate later extensions that allow mobility: typed $\pi$-calculi and typed higher-order $\pi$-calculi. The syntax of Base-$\pi$ is in Tables 6.1 and 6.2, the typing rules in Table 6.3, and the transition rules in Table 6.4. (As usual, the symmetric forms of PAR-L, COMM-L, and SUM-L are omitted from Table 6.4.) We briefly comment on these rules below. In Base-$\pi$ and its extensions, the syntactic distinction between value types and link types is made by the use of $V$ to range over value types and $L$ over link types. However, in typing and operational rules, as well as in discussions and proofs, unless important for the sense we will use only the letters $S, T$, which stand for arbitrary types. Thus, for instance, in rule T-INP of Table 6.3 we write $\Gamma \vdash v : \sharp T$, rather than $\Gamma \vdash v : \sharp V$; the syntax of types guarantees that $T$ is a value type.
In Base-$\pi$ there is only one link-type constructor, the connection type$\sharp T$. A type assignment $a : \sharp T$ means that $a$ can be used as a link to carry values of type $T$. The only value types are the basic types; therefore the values of these types, the basic values, are the only values that are exchanged in a closed process. The set of basic types is left unspecified -- the definition of Base-$\pi$ is parametric with respect to this set. Unless otherwise stated, we will assume that the basic types include at least the unit type unit; the only value of type unit is the unit value *, whose typing rule is
T-UNIT$\Gamma \vdash *$ : unit
Other basic types could be, for instance, the integer and boolean types. Were they to be admitted, we would also need operations that manipulate their values, such as addition and negation; see Remark 6.2.2. We have seen in Section 3.4 that integers and booleans are encodable in $\pi$-calculus. But they occur so often as values that it would be cumbersome to adopt those encodings as a programming style. In Tables 6.1, 6.2 and 6.3, $B$ is a metavariable over basic types, and $basval$ a metavariable over basic values. Moreover, $basval \in B$ means that $basval$ is a basic value of type $B$.
One of the purposes of a type system is to avoid run-time errors. To make the meaning of run-time errors precise and to prove theorems about the absence of run-time errors, we add a new process construct, wrong, to the syntax of processes. It denotes a process in which a run-time error has occurred.
There is one typing rule for each syntactic form except wrong, which is not well typed under any assumptions. The inert process 0 is well typed in any typing. The parallel composition and the sum of two processes are well typed if each is well typed in isolation. Similarly, a replication !$P$ is well typed if $P$, the single copy, is. A process whose outermost constructor is a restriction is well typed if its body observes the constraints imposed both by the type environment and by the declared type of the new name. Note that the type of the restricted name is a link type: restrictions introduce new links, not arbitrary new values. The most interesting cases are the rules for input and output. In an input $\nu(x). P$, the subject $\nu$ should have a link type (which also implies $\nu$ should be a name); moreover, from this type, a type for $x$ is determined and then the body $P$ is required to be well typed under the resulting extension of $\Gamma$. The case for output is similar: the output $\overline{\nu} w. P$ is well typed if $\nu$ has a link type and this type is compatible with that of $w$; moreover $P$ itself must be well typed. The typing rule for matching stipulates that only names of the same connection type can be tested. We cannot therefore use matching to test equality between arbitrary values. The reason for this is that the equality test on connection types, and in general on link types, is a semantically subtle construct (see the discussion on rule T-MAT in Section 7.1). We prefer that the equality test on other types (for instance integers), if needed, is introduced as a separate construct. Note also that, in a type environment, the types assigned to names can be link types or value types, but cannot be the behaviour type.
As in the polyadic $\pi$-calculus of Section 3.1, transitions can be of three forms:
• $\tau$ transitions $P \xrightarrow{\tau} P'$, with the usual meaning
• input transitions $P \xrightarrow{a v} P'$, meaning that $P$ can receive a value $v$ at $a$ and continue as $P'$
• output transitions $P \xrightarrow{(\nu \widetilde{z} : \widetilde{T}) \overline{a} v} P'$, meaning that $P$ can send the value $v$ along $a$ extruding the set of names $\widetilde{z}$ of types $\widetilde{T}$, and then continue as $P'$.
In an output transition $P \xrightarrow{(\nu \widetilde{z} : \widetilde{T}) \overline{a} v} P'$, names $\widetilde{z}$ are free in $v$. If $P$ is a well-typed process of Base-$\pi$, then $\widetilde{z}$ is always empty -- because in Base-$\pi$ links are not values. But when values can include names, as in typed $\pi$-calculi, or processes, as in higher-order $\pi$-calculi, then $\widetilde{z}$ can be non-empty; see Exercises 6.4.3 and 6.5.2 for examples. We maintain the terminology for actions of the previous chapters; thus in actions $a v$ and $(\nu \widetilde{z} : \widetilde{T}) \overline{a} v$ we call $v$ the object and $a$ the subject. Having output actions of the form $(\nu \widetilde{z} : \widetilde{T}) \overline{a} v$, with a special place for the (possibly empty) set $\widetilde{z}$ of extruded names, allows us to accommodate both forms of output actions of the monadic $\pi$-calculus (Definition 1.3.1), namely the free output $\overline{x} y$ and the bound output $\overline{x} (z)$.
The transition rules (Table 6.4) are similar to those of the untyped $\pi$-calculus. The differences are: the two communication rules COMM-L and REP-COMM, in place of the four rules COMM-L, CLOSE-L, REP-COMM, and REP-CLOSE; the more general side condition in rule OPEN; and the presence of rules MATERR, INERR, and OUTERR, for signalling run-time errors. In Base-$\pi$, an error occurs if a value that is not a name ends up as the subject of a prefix or in a matching; extensions of the type systems in later sections will add more rules for errors.
The operational rules are defined on arbitrary processes -- they need not be well typed, let alone closed. Only closed well-typed processes, however, are guaranteed not to produce a run-time error, as will be proved in Section 6.3. As Base-$\pi$ is very simple, we could have prevented run-time errors by syntactic means. This would however be complicated in later extensions of Base-$\pi$. In the grammar of Table 6.2, we cannot use names instead of arbitrary values as subjects of input and output prefixes and as arguments of matches. The operational rules would not be well defined, because the derivative of a process might not be a process, as in
$\overline{a} *. P \mid a(x). \overline{x} c. \mathbf{0} \xrightarrow{\tau} P \mid * c. \mathbf{0}$.
The problem is with substitutions: $P{v/x}$ might not be a process. This problem does not exist with the present syntax, as shown by the following lemma:
Lemma 6.2.1$P{v/x}$ is a process, for every process $P$, name $x$, and value $v$. $\Box$
As a consequence of this lemma, the expression E in a judgment P ⊢ E inferred from the rules of Table 6.4 is a process.
Remark 6.2.2 We might wish to have operations that manipulate values of basic types. For instance, if we have integers, we would probably need addition and multiplication, and, if we have booleans, negation and conjunction. For this, we should add to the syntax of Base-τ the syntactic category of value expressions, that is, expressions that reduce to values. Value expressions would include, but not coincide with, values. For instance, if succ is the successor function on integers, then succ 2 would be a value expression but not a value. We would then need rules for evaluating value expressions, such as
$\dfrac{}{\text{succ } n \stackrel{\tau}{\longrightarrow} n + 1}$
as well as rules for evaluating value expressions in processes, such as, using e for a value expression,
These rules determine a reduction strategy. Different choices of reduction strategies are possible; for instance rule (6.1) is typical of the call-by-value strategy.
We do not introduce value expressions, and hence reduction strategies, into the typed calculi that we present. This addition is an orthogonal issue, and can easily be accomplished by analogy with typed λ-calculi. In examples, however, we occasionally use integer and boolean expressions, assuming standard call-by-value reduction rules for them such as rule (6.1). Reduction strategies are discussed in Chapter 14. ▢
6.3 Properties of typing
We now establish some fundamental properties of the type system for Base-τ. These properties will continue to hold in extensions of Base-τ, unless otherwise stated. To carry out proofs, we have to fix the set of basic types: we take unit as the only such type.
Lemmas 6.3.1–6.3.5 are proved by straightforward induction on the depth of the derivation of the judgment in the hypothesis.
Lemma 6.3.1 If Γ ⊢ E : T and Γ is not defined on x, then x is not free in E. ▢
Lemma 6.3.2 If Γ ⊢ P then P does not have wrong as a subterm. ▢
Lemma 6.3.3 For every typing $\Gamma$ and name $x$ there is at most one type $T$ such that $\Gamma \vdash x : T$.
$\Box$
Lemma 6.3.4 (Strengthening) If $\Gamma, x:S \vdash E:T$ and $x$ is not free in $E$, then also $\Gamma \vdash E:T$.
$\Box$
Lemma 6.3.5 (Weakening) If $\Gamma \vdash E:T$ then $\Gamma, x:S \vdash E:T$ for any type $S$ and any name $x$ on which $\Gamma$ is not defined.
$\Box$
Proof Take the derivation of $\Gamma \vdash E : T$. We obtain one for $\Gamma \vdash E{v/x} : T$ as follows. Consider all leaves that look up the type of $x$. They are of the form
$\dfrac{}{\Delta, x:S \vdash x:S}$
Here the typing $\Delta, x:S$ is an extension of $\Gamma$, in the sense that there is $\Gamma'$ such that $\Delta, x:S = \Gamma, \Gamma'$. Hence, by Weakening, also $\Delta, x:S \vdash v:S$ is valid. Therefore such a leaf may be replaced by a derivation of $\Delta, x:S \vdash v:S$. Replace also all occurrences of $x$ to the right of a turnstile by $v$. The result is a derivation of $\Gamma \vdash E{v/x}:T$, which can be proved by induction on the depth of the derivation of $\Gamma \vdash E:T$.
$\Box$
In the present system, the type of a name is unique (Lemma 6.3.3), and hence in Lemma 6.3.6 the condition Γ(x) = S could be replaced by Γ ⊢ x : S. However, this will not hold in later extensions of the system; see for instance Exercise 7.2.1.
The Subject Reduction Theorem 6.3.7 expresses a consistency between the operational semantics and the typing rules. The theorem shows how the typing of a process evolves under transitions and how the typing can be used to obtain information about the process's possible transitions. For instance, the type of the value sent out by the process in an output must be compatible with the type of the name at which the output takes place. The first clause is the most important one; it shows that a (closed) process maintains its typing as it evolves.
Theorem 6.3.7 (Subject Reduction) Suppose Γ ⊢ P , with Γ closed, and P α→ P'.
