1 Introduction

Recent advances in the theory and practice of programming languages have resulted in modern languages and tools that provide certain correctness guarantees regarding the execution of programs. However, these advances have not been effectively applied to the construction of systems programs, the core components of a computer system. One of the primary causes of this problem is the fact that existing languages do not simultaneously support modern language features — such as static type safety, type inference, higher order functions and polymorphism — as well as features that are critical to the correctness and performance of systems programs such as prescriptive data structure representation and mutability. In this paper, we endeavor to bridge this gap between modern language design and systems programming. We first discuss the support for these features in existing languages, identify the challenges in combining these feature sets and then describe our approach toward solving this problem.

Representation Control    A systems programming language must be expressive enough to specify details of representation including boxed/unboxed data-structure layout and stack/heap allocation. For systems programs, this is both a correctness as well as a performance requirement. Systems programs interact with the hardware through data structures such as page tables whose representation is dictated by the hardware. Conformance to these representation specifications is necessary for correctness. Languages like ML [16] intentionally omit details of representation from the language definition, since this greatly simplifies the mathematical description of the language. Compilers like TIL [23] implement unboxed representation as a discretionary optimization. However, in systems programs, statements about representation are prescriptive, not descriptive. Formal treatment of representation is required in systems programming languages.

Systems programs also rely on representation control for performance since it affects cache locality and paging behavior. This expressiveness is also crucial for interfacing with external C [9] or assembly code and data. For example, a careful implementation of the TCP/IP protocol stack in Standard ML incurred a substantial overhead of up to 10x increase in system load and a 40x slowdown in accessing external memory relative to the equivalent C implementation [ 1 ,3 ]. This shows that representation control is as important as, or even more important than, high level algorithms for the performance of systems tasks.

Complete Mutability    One of the key features essential for systems programming is support for mutability. The support for mutability must be `complete' in the sense that any location — whether on the stack, heap, or within other unboxed structures — can be mutated. Allocation of mutable cells on the stack boosts performance because (1) the top of the stack is typically accessible from the data cache (2) stack locations are directly addressable and therefore do not require the extra dereferencing involved in the case of heap locations (3) stack allocation does not involve garbage collection overhead. This is particularly important for high confidence and/or embedded kernels as they cannot tolerate unpredictable variance in overhead caused by heap allocation and collection. ML-like languages require all mutable (ref) cells to reside on the heap. In pure languages like Haskell [14], the support for mutability is even more restrictive than ML. These restricted models of mutability are insufficiently expressive from a systems programming perspective.

Consistent Mutability    The mutability support in a language is said to be `consistent' if the (im)mutability of every location is invariant across all aliases over program execution. In this model, there is a sound notion of immutability of locations. This benefits tools that perform static analysis or model checking because conclusions drawn about the immutability of a location need never be conservative. It also increases the amount of optimization that a compiler can safely perform without complex alias analysis. Polymorphic type inference systems such as Hindley-Milner algorithm [15] also rely on a sound notion of immutability. ML supports consistent mutability since types are definitive about the (im)mutability of every location. In contrast, C does not support this feature. For example, in C it is legal to write:
      const bool *cp = ...; bool *p = cp; *p = false; // OK!
The alleged ``constness'' of the location pointed to by cp is a local property (only) with respect to the alias cp and not a statement of true immutability of the target location. The analysis and optimization of critical systems programs can be improved by using a language with a consistent mutability model.

Type Inference and Polymorphism    Type inference achieves the advantages of static typing with a lower burden on the programmer, facilitating rapid prototyping and development. Polymorphic type inference (c.f. ML or Haskell) combines the advantages of static type safety with much of the convenience provided by dynamically typed languages like Python [18]. Automatic inference of polymorphism simplifies generic programming, and therefore increases the reuse and reliability of code. Safe languages like Java [17], C# [4], or Vault [2] do not support type inference. Cyclone [10] features partial type inference and supports polymorphism only for functions with explicit type annotations.

The following table summarizes the support available in existing languages for the above features and static type safety:

	C/Asm	Safe-C	CCured	Cyclone	Vault	Java	ML	Haskell
Representation	?Y?			?Y?	?Y?
Complete Mutability	?Y?	?Y?	?Y?	?Y?	?Y?	?Y?
Consistent Mutability							?Y?	?Y?
Static Type Safety				?Y?	?Y?	?Y?	?Y?	?Y?
Poly. Type Inference							?Y?	?Y?

In this paper, we present a new type system and formal foundations for a safe systems programming language that supports all of the above features.

The combination of mutability and unboxed representation presents several challenges for type inference. Mutability is an attribute of the location storing a value and not the value itself. Therefore, two expressions across a copy boundary (ex: arguments copied at a function call) can differ in their mutability. We refer to this notion of mutability compatibility of types as copy compatibility. Copy compatibility creates ramifications for syntax-directed type and mutability inference. Type inference is further complicated due to well known problems with the interaction of mutability and polymorphism [25]. This has forced a second-class treatment of mutability in ML-like languages and a lack of inferred polymorphism in others.

We present a sound and complete polymorphic type inference algorithm for a language that supports consistent and complete mutability. In order to overcome the challenges posed by copy compatibility, the underlying type system uses a system of constrained types that range over mutability and polymorphism. Safety of the type system as well as the soundness and completeness of the type inference algorithm have been proved.

2 Informal Overview

..-2ex

In this section, we give an informal description of our type system and inference algorithm. For purposes of presentation in this paper, we define *B*, a core systems programming language calculus. *B* is a direct expression of lambda calculus with side effects, extended to be able to reflect the semantics of explicit representation.

Identifiers _x_ ::= _y_ | _z_ | ... Booleans ?b? ::= true | false Indices i ::= 1 | 2 | !i Values _v_ ::= () | ?b? | λ_x_._e_ | (_v_, _v_) Left Expr _l_ ::= _x_ | _e_^ | _l_.i | _l_ : τ Expressions _e_ ::= _v_ | _x_ | _e_ _e_ | _l_ := _e_     | if  _e_ then _e_ else _e_ | _e_ : τ     | dup(_e_) | _e_^ | (_e_, _e_) | _e_.i     | let _x_[:τ] = _e_ in _e_

Vars α ::= α | β | γ | δ | ε | ... ς ::= α | Ψα Types ρ ::= α | unit | bool | τ → τ       | τ ✗ τ | ⇑τ | Ψρ ϱ ::= ρ | α⇃ρ τ ::= ϱ | ς↓ρ Scheme σ ::= τ | ∀α*.τ\*D* Ct. Set *D* ::= ∅ | {★ϰ_x_(τ)} | *D* ∪ *D* Kinds ϰ ::= κ | ψ | ∀

The type ⇑τ represents a reference (pointer) type and Ψρ represents a mutable type. The expression dup(_e_), where _e_ has type τ, returns a reference of type ⇑τ to a heap-allocated copy of the value of _e_. The ^ operator is used to dereference heap cells. Pairs (,) are unboxed structures whose constituent elements are contiguously allocated on the stack, or in their containing data-structure. _e_.1 and _e_.2 perform selection from pairs. We define !1 = 2 and !2 = 1. The let construct can be used for allocating (possibly mutable) stack variables and to create let-polymorphic bindings. let _x_[:τ] = _e_ represents optional type qualification of let-bound variables.

The Mutability Model    *B* supports consistent, complete mutability. The mutability support is complete since the := operator mutates both stack locations (let-bound locals, function parameters) and heap locations (dup-ed values). It can also perform in-place updates to individual fields of unboxed pairs. The mutability support is consistent since we impose the ``one location, one type'' rule. For example, in the following expression,
      let _cp_ : ⇑bool = dup(true) in let _p_ : ⇑Ψbool = _cp_    (* Error *)
_cp_ has the type reference to bool (⇑bool), which is incompatible with that of _p_, reference to mutable-bool (⇑Ψbool). Unlike ML, := does not dereference its target. The expressions that can appear on the left of an assignment := are restricted to left expressions (defined by the above grammar). This not only preserves the programmer's mental model of the relationship between locations storage, but also ensures that compiler transformations are semantics preserving.

Copy Compatibility    *B* is a call-by-value language, and supports copy compatibility, which permits locations across a copy boundary to differ in their mutability. For example, in the following expression:
      let _fnxn_ = λ_x_.(_x_ := false) in let _y_ : bool = true in _fnxn_ _y_
the type of _fnxn_ is (Ψbool) → unit, whereas that of the actual argument _y_ is bool. Since _x_ is a copy of _y_ and occupies a different location, this expression is type safe. Thus, we write bool ≅ Ψbool, where ≅ indicates copy compatibility.

Copy compatibility must not extend past a reference boundary in order to ensure that every location has a unique type. We define copy compatibility for *B* as:

τ ≅ τ

τ1 ≅ τ2 τ2 ≅ τ1

τ1 ≅ τ2    τ2 ≅ τ3 τ1 ≅ τ3

τ ≅ ρ τ ≅ Ψρ

τ1 ≅ τ′1    τ2 ≅ τ′2 τ1 ✗ τ2 ≅ τ′1 ✗ τ′2

Copy compatibility is allowed at all positions where a copy is performed: at argument passing, new variable binding, assignment, and basically in all expressions where a left-expression is not expected or returned. For example, the expression (_x_ : τ) : Ψτ is ill typed, but the branches of a conditional can have different but copy compatible types as in if  true then _a_ : τ else _b_ : Ψτ .

..-4pt

3 Formal Description

In order to formalize the semantics of *B*, we extend the calculus with stack and heap locations (Fig. 1). Heap locations are first class values, but stack locations are not. Further, we annotate all let expressions with a kind — let^ψ: monomorphic, possibly mutable definition, and let^∀: polymorphic definitions. The two kinds of let expressions have different execution semantics. We write let^κ to range over the two kinds of let expressions. This distinction is similar to Smith and Volpano's Polymorphic-C [21]. However, unlike Polymorphic-C, let-kind is meta syntax, and is not a part of the input program. The correct kind of let is inferred from the static type information. We do not show the semantics for type-qualified expressions as they are trivial.

Dynamic Semantics    The system state is represented by the triple S; H; _e_ consisting of the stack S, the heap H, and the expression _e_ to be evaluated. Evaluation itself is a two place relation S; H; _e_ ⇒ S^′; H^′; _e_^′ that denotes a single step of execution. Fig. 2 shows the evaluation rules for our core language. We assume that the program is alpha-converted so that there are no name collisions due to inner bindings. Following the theoretical development of [6], we give separate execution semantics for left evaluation (execution of left expressions _l_ on the LHS of an assignment, denoted by ⇛) and right evaluation (⇒) respectively.

Since the E-Dup and E-^ rules work only on the heap, we can only capture references to heap cells. Stack locations cannot escape beyond their scope since E-Rval rule performs implicit value extraction from stack locations in rvalue contexts. State updates can be performed either on the stack or on the heap (E-:=* rules). The stack is modeled as a pseudo-heap. This enables us to abstract away details such as closure-construction and garbage collection while illustrating the core semantics, as they can later be reified independently.

The execution semantics do not perform a copy operation in all cases where copy compatibility is permitted. For example, the E-If rule does not introduce a copy step in the branching expression. Since if-expressions are not lvalues, they cannot be the target of an assignment. Therefore, the value that either branch evaluates to, can itself be used in all cases where a copy of that value can be.

Static Semantics    Fig. 3 defines several operators and predicates on types that we use in this section. The operators ▴ and ▾ respectively increase and decrease the shallow top-level mutability of a type. △ and ▽ maximize / minimize the mutability of a type up to a reference or function boundary. *I* removes all mutability in a type up to a function boundary. We write τ₁ =_▾ τ₂ as shorthand for ▾(τ₁) = ▾(τ₂) and τ₁ =_▽ τ₂ for ▽(τ₁) = ▽(τ₂). In our algebra of types, the mutable type constructor is idempotent (ΨΨτ ≡ Ψτ). We also define the equivalences: α⇃ρ ≡ α⇃ρ^′, where ρ =_▾ ρ^′ and ς⇃ρ ≡ ς⇃ρ^′, where ρ =_▽ ρ^′. The predicates ?Immut? and ?Mut? identify types that are observably immutable and mutable respectively. The □(τ) predicate tests if the type τ is concretizable by fixing variables that range over mutability.

θ〈τ〉 denotes the application of a substitution θ on τ as defined in Fig. 3. θ〈_e_〉 performs substitutions for κ annotations in _e_. {|τ|} denotes the set of all constrained types and unconstrained type variables structurally present in τ. θ〈 〉 and {| |} are extended to σ, Γ, Σ, and {τ^*} in the natural, capture-avoiding manner.

Definition I (Canonical Expressions).    An expression _e_ is said to be canonical if all let expressions in _e_ are annotated with one of the kinds ψ or ∀.

Definition II (Consistency of Constrained types).    Let ?mtv??(?τ^*?)?, ?Mtv??(?τ^*?)?, and ?ntv??(?τ^*?)? be the set of all type variables appearing in {τ^*} constrained by α⇃ρ, by ς↓ρ and unconstrained respectively. We say that the set of types {τ^*} is consistent, written  ⊪ {τ^*}, if: (1) For all {α⇃ρ,  α⇃ρ^′} ⊆ {|τ^*|}, we have ρ =_▾ ρ^′.
(2) For all {ς↓ρ,  ς^′↓ρ^′} ⊆ {|τ^*|} such that ς =_▾ ς^′, we have ρ =_▽ ρ^′.
(3) ?mtv??(?τ^*?)?, ?Mtv??(?τ^*?)?, and ?ntv??(?τ^*?)? are mutually exclusive.

Definition III (Consistency of substitutions).    A substitution θ is said to be consistent over a set of types {τ^*}, written θ ⊪ {τ^*} if: (1)  ⊪ θ{|τ^*|}.
(2) For all α⇃ρ ∊ {|τ^*|}, we have θ〈α〉 = β, or θ〈α〉 = ρ^′ such that ρ^′ =_▾ θ〈ρ〉.
(3) For all ς↓ρ ∊ {|τ^*|}, we have θ〈ς〉 = ς^′, or θ〈ς〉 = ϱ such that ϱ =_▽ θ〈ρ〉.

Definition IV (Consistency of ★ constraints).    A set of ★ constraints *D* is said to be consistent, written  ⊧ *D* if: (1) For all ★∀_x_(τ) ∊ *D*, we have ?Immut??(?τ?)?.
(2) For all ★ψ_x_(τ1) ... ★ψ_x_(τn) ∊ *D*, we have τ1 =  ...  = τn.
(3) For all ★ϰ1_x_(τ1) ∊ *D* and ★ϰ2_y_(τ2) ∊ *D*, ϰ1 ≠ ϰ2 implies _x_ ≠ _y_.

Declarative Type Rules    Fig. 4 presents a declarative definition of the type system of *B*. In this type system, copy compatibility is realized through copy coercion (⊴:) rules that are similar to subtyping rules (S-* rules in Fig. 4). Since reference types ⇑τ are handled only by S-Refl, types cannot coerced beyond a reference boundary. Also, two function types are coercible only if they are structurally identical. Here, the contravariance/covariance of argument/return types is unnecessary as we can follow a standard convention with respect to the mutability of argument/return types at copy positions. The rules for typing expressions (T-* rules) introduce these coercions at all copy-compatible positions.

The type judgment *D*; Γ; Σ ⊢ _e_ : τ is understood as: given a binding environment Γ and store typing Σ, the expression _e_ has type τ subject to the set of ★ constraints *D*. We write _e_ ⊴: τ as a shorthand for _e_ : τ^′ and τ^′ ⊴: τ, for some type τ^′. The rule T-Lambda permits the interface type of a function be different from its internal type, as explained in Sec. 2.1. The rule T-App introduces copy-coercions at argument and return positions of an application. T-Let-M rule types let expressions monomorphically, and thus requires a let^ψ annotation. In this case, the expression _e_₁ is permitted to be expansive (i.e. need not be a syntactic value υ). The T-Let-MP rule types let expressions where the expression being bound is a syntactic value. It assigns _x_ a constrained type scheme along with the constraint ★^ϰ_{_x_}(τ). The T-Id rule instantiates types and constraints. The instantiated constraints are collected over the entire derivation, so that we can enforce instantiation consistency.  ⊧_new α^* identifies fresh type variables.

We prove the soundness of our type system by demonstrating subject reduction. Here, we prove that the type of an expression is preserved exactly by left-execution, which ensures that the type of a location does not change during the execution of a program. We also show that right execution preserves types except for shallow mutability. The result of a right execution can only be used in copy compatible positions, or as the target of a dereference. In the former case, preservation of shallow mutability is unnecessary, and in the later, the type within the reference is preserved exactly.

The interesting case is the safety of polymorphic let expressions. The T-Let-MP rule does not require that the type τ being quantified over be immutable, but adds the ★^ϰ_{_x_}(τ) constraint. Now, if we have a derivation *D*; Γ; Σ ⊢ _e_ : τ such that  ⊧ *D*, then one of the two cases must follow. (1) If any instantiation of τ is mutable, then ϰ = ψ. In this case, execution proceeds through the E-Let-M rule, which create a stack location for _x_. Therefore, _x_ is permitted to be the target of an assignment.  ⊧ *D* guarantees that all instantiations of τ are identical, which ensures that the type of a location cannot change. (2) If τ is instantiated polymorphically, then ϰ = ∀. Execution proceeds through the E-Let-P rule, which performs a value substitution. Here,  ⊧ *D* guarantees that all instantiations are deeply immutable. Therefore, _x_ cannot be directly used (in the forms _x_ or _x_.?p?) as the target of an assignment, which ensures that the value substitution cannot lead to a stuck state.

Definition V (Consistent Type Derivation).    Let {|*D*; Γ; Σ ⊢ _e_ : τ|} denote the extension {| |} function to the set of all types used in the derivation of *D*; Γ; Σ ⊢ _e_ : τ. We say that *D*; Γ; Σ ⊢_* _e_ : τ is a consistent derivation if *D*^′; Γ; Σ ⊢ _e_ : τ for some *D*^′ ⊆ *D*, and  ⊪ {|*D*|} ∪ {|*D*^′; Γ; Σ ⊢ _e_ : τ|}.

Definition VI (Stack and Heap Typing)    A heap H and a stack S are said to be well typed with respect to Γ, Σ and *D*, written *D*; Γ; Σ ⊢_* H + S, if:
(1) dom(Σ) = dom(H) ∪ dom(S)
(2) ∀ℓ ∊ dom(H), *D*; Γ; Σ ⊢_* H(ℓ) : τ such that Σ(ℓ) =_▽ τ
(3) ∀l ∊ dom(S), *D*; Γ; Σ ⊢_* S(l) : τ such that Σ(l) =_▽ τ

Definition VII (Valid Lvalues).    We say that an lvalue £ is valid with respect to a stack S and heap H, written H + S ⊢_v £ if for some ?p?, either (1) £ = l or £ = l.?p? where l ∊ dom(S); or (2) £ = ℓ^ or £ = ℓ^.?p? where ℓ ∊ dom(H).

Lemma I (Progress).    If _e_ is a closed canonical well typed expression, that is, *D*; ∅; Σ ⊢_* _e_ : τ for some τ and Σ, given any heap and stack such that *D*; ∅; Σ ⊢_* H + S,
(1) If _e_ is a left expression (_e_ = _l_), then _e_ is either a valid lvalue (that is, _e_ = £ and
    H + S ⊢_v £) or else ∃ _e_^′, S^′, H^′  such that S; H; _e_ ⇛ S^′; H^′; _e_^′.
(2) _e_ is a value _v_ or else ∃ _e_^′, S^′, H^′  such that S; H; _e_ ⇒ S^′; H^′; _e_^′.

Lemma II (Preservation).    For any canonical expression _e_, if *D*; Γ; Σ ⊢_* _e_ : τ, *D*; Γ; Σ ⊢_* H + S and  ⊧ *D* then,
(1) If S; H; _e_ ⇛ S^′; H^′; _e_^′, then, ∃  Σ^′ ⊇ Σ such that *D*; Γ; Σ^′ ⊢_* _e_^′ : τ
     and *D*; Γ; Σ^′ ⊢_* H^′ + S^′.
(2) If S; H; _e_ ⇒ S^′; H^′; _e_^′, then, ∃  Σ^′ ⊇ Σ such that *D*; Γ; Σ^′ ⊢_* _e_^′ : τ^′,
    *D*; Γ; Σ^′ ⊢_* H^′ + S^′ and τ =_▽ τ^′.

Definition VIII (Stuck State).    A system state S; H; _e_ is said to be stuck if _e_ ≠ _v_ and there are no S^′, H^′, and _e_^′ such that S; H; _e_ ⇒ S^′; H^′; _e_^′.

Theorem I (Type Soundness).    Let ⇒* denote the reflexive-transitive-closure of ⇒. For any canonical expression _e_, if *D*; ∅; Σ ⊢_* _e_ : τ,   *D*; ∅; Σ ⊢_* H + S,    ⊧ *D*, and S; H; _e_ ⇒* S^′; H^′; _e_^′, then S^′; H^′; _e_^′ is not stuck. That is, execution of a closed, canonical, well typed expression cannot lead to a stuck state.

Type Inference Algorithm    Type inference is a program transformation that accepts a program in which let expressions are not annotated with their kinds, and returns the same program with let expressions annotated with their kinds and all expressions annotated with their types. The type inference algorithm is shown in Fig. 5. The inference judgment Γ; Σ ⊢_i _e_ : τ | *C* is understood as: given a binding environment Γ and store typing Σ, the expression _e_ has type τ subject to the constraints *C*.

The inference algorithm introduces constrained types of the form ς↓ρ at all copy compatible positions. For example, the I-App rule introduces copy compatibility for the function type itself, the argument and the return types. The I-Sel rule represents the pair type as ε⇃(α↓β ✗ γ↓δ), which (1) permits top-level mutability of the pair type to be either mutable or immutable (2) ensures that the type of the selection is exactly same as the type of the field being selected (3) propagates full copy compatibility ``one level down.''

The unification algorithm is shown in Fig. 6. The unification of a constraint set *C* either fails with an error ⊥, or produces the pair (*D*, θ). θ is a solution for all equality constraints and some of the ★ constraints in *C*. *D* is the set of ★ constraints in *C* on which θ has been applied. ∪ represents disjoint union of sets.

The U-Ct* rules perform unification of constrained types with other constrained or unconstrained types. First, immutable versions of the two types are unified to establish compatibility (through constraints involving =_▾ and =_▽). Then, the constrained type is made to exactly equal the other type by unifying its variable part with the other type. The key observation here is that the copy compatibility is a special restricted form of subtyping. Since the type of the copy can be anywhere in the lattice of copy compatible types, subtyping requirements are always with respect a local maxima (the most immutable compatible type). We exploit this behavior to design a simple unification algorithm that only uses equality constraints over constrained types.

The U-Om1 ensures that all instantiations of monomorphic kind are the same. U-Op1 rule forces any concretizable instantiation of polymorphic kind to be immutable. The U-Om2 rule infers monomorphic kind based on the mutability of the instantiated type, and U-Op2 infers polymorphic kind if a variable _x_ is instantiated polymorphically to two types that do not inter-unify.

Definition IX (Constraint Satisfaction).    The satisfaction of a constraint set *C* by a substitution θ is defined as follows.

∀  (τ1 = τ2) ∊ *C*, θ〈τ1〉 = θ〈τ2〉    ∀  (κ = ϰ) ∊ *C*, θ〈κ〉 = θ〈ϰ〉 *D* = {θ〈★ϰ_x_(τ)〉 | ★ϰ_x_(τ) ∊ *C*} θ ⊢sol *C* ↝ *D*

θ ⊢sol *C* ↝ *D*  ⊧ *D* θ ⊢sat *C* ↝ *D*

Definition X (Notational Derivations).    We write:
(1) θ; Γ; Σ ⊢_i _e_ : τ | *D* if Γ; Σ ⊢_i _e_ : τ | *C*, θ ⊢_sol *C* ↝ *D*, and θ ⊪ {Γ,  Σ,  τ,  *C*}
(2) θ; *D*; Γ; Σ ⊢_* _e_ : τ if θ〈*D*〉; θ〈Γ〉; θ〈Σ〉 ⊢_* θ〈_e_〉 : θ〈τ〉

Lemma III (Correctness of Unification).    If *U*(*C*) = (*D*, θ), then θ ⊢_sol *C* ↝ *D*

Lemma IV (Satisfiability of Unified Constraints).    If *U*(*C*) = (*D*, θ_u), then there exists a substitution θ_s such that θ_u ∘ θ_s ⊢_sat *C* ↝ *D*.

Lemma V (Principality of Unification).    If *U*(*C*) = (*D*, θ_u), where *C* is a set of constraints obtained from the type inference algorithm, then, for all θ_s such that θ_s ⊢_sol *C* ↝ *D*^′, we have θ_s ⊇ θ_u.

Lemma VI (Decidability of Unification).    The problem of computing a canonical derivation of *U*(*C*) for an arbitrary *C*, where no two applications of U-Sym rule happen consecutively is decidable.

Theorem II (Soundness of Type Inference).    If θ; Γ; Σ ⊢_i _e_ : τ | *D*, then
θ; *D*; Γ; Σ ⊢_* _e_ : τ.

Lemma VII (Type Checkability).    If Γ; Σ ⊢_i _e_ : τ | *C* and *U*(*C*) = (*D*, θ), then ∃  θ^′ such that  ⊧ θ^′〈*D*〉 and θ ∘ θ^′〈_e_〉 is canonical, and θ ∘ θ^′; *D*; Γ; Σ ⊢_* _e_ : τ.

Theorem III (Completeness of Type Inference).    If θ; *D*; Γ; Σ ⊢_* _e_ : τ, then there exists a θ^′ ⊇ θ such that θ^′; Γ; Σ ⊢_i _e_ : τ | *D*.

4 Related Work

Grossman [6] provides a theory of using quantified types with imperative C style mutation for Cyclone. However, his formalization requires explicit annotation for all polymorphic definitions and instantiations. In contrast, we believe that the best way to integrate polymorphism into the systems programming paradigm is by automatic inference. A further contribution of our work (in comparison to [6]) is that we give a formal specification and proof of correctness of the inference algorithm, not just the type system. Cyclone [10] uses region analysis to provide safe support for the address & operator. This technique is complementary to our work, and can be used to incorporate & operator in *B*.

C's const notion of immutability-by-alias offers localized checking of immutability properties, and encourages good programming practice by serving as documentation of programmers' intentions. Other systems have proposed immutability-by-name [2], referential immutability [ 19 ,24 ] (transitive immutability-by-reference), etc. These techniques are orthogonal and complementary to the immutability-by-location property in *B*. For example, we could have types like (const Ψτ) that can express both global and local usage properties of a location.

A monadic model [13] of mutability is used in pure functional languages like Haskell [14]. In this model, the type system distinguishes side-effecting computations from pure ones (and not just mutable locations from immutable ones). Even though this model is beneficial for integration with verification systems, it is considerably removed from the idioms needed by systems programmers. For example, Hughes argues that there is no satisfactory way of creating and using global mutable variables using monads [7]. There have been proposals for adding unboxed representation control to Haskell [ 12 ,8 ]. However, these systems are pure and therefore and do not consider the effects of mutability.

Cqual [5] provides a framework of type qualifiers, which can be used to infer maximal const qualifications for C programs. However, CQual does not deal with polymorphism of types. In a monomorphic language, we can infer types and qualifiers independently. Adding polymorphism to CQual would introduce substantial challenges, particularly if polymorphism should be automatically inferred. The inference of types and qualifiers (mutability) becomes co-dependent: we need base types to infer qualifiers; but, we also need the qualifiers to infer base types due to the value restriction. *B* supports a polymorphic language and performs simultaneous inference of base types and mutability.

5 Conclusions

In this paper, we have defined a language and type system for systems programming which integrates all of unboxed representation, consistent complete mutability support, and polymorphism. The mutability model is expressive enough to permit mutation of unboxed/stack locations, and at the same time guarantees that types are definitive about the mutability of every location across all aliases.

Complete support for mutability introduces challenges for type inference at copy boundaries. We have developed a novel algorithm that infers principal types using a system of constrained types. To our knowledge, this is the first sound and complete algorithm that infers both mutability and polymorphism in a systems programming language with copy compatibility.

The type inference algorithm is implemented as part of the BitC [20] language compiler. The core of the compiler involves 22,433 lines of C++ code, of which implementation of the type system accounts for about 7,816 lines. The source code can be obtained from http://bitc-lang.org.