1 Introduction

Systems programs rely on fine-grain control of data representation and use of state to achieve performance, conformance to hardware specification, and temporal predictability. Robustness and reuse of systems codes can be greatly improved by leveraging modern programming language features — such as static type safety, type inference, higher order functions, and polymorphism — but only if these features can be provided without sacrificing the above mentioned requirements. No existing language supports both of these feature sets simultaneously. Therefore, systems programmers continue to use Ada [8], C [10], C++ [9] or resort to domain specific and assembly level languages. We first discuss the support for these features in existing languages, identify the challenges in combining these feature sets and describe our approach toward solving this problem.

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 [18] or Haskell [15]) combines the advantages of static type safety with much of the convenience provided by dynamically typed languages like Python [20]. Automatic inference of polymorphism simplifies generic programming, and therefore increases the reuse and reliability of code. Safe languages like Java [19], C# [16], or Vault [2] do not support type inference. Cyclone [11] supports polymorphism only for functions that are explicitly annotated with a polymorphic type.

Representation Control:    A systems programming language must be expressive enough to specify details of data-structure layout (boxed or unboxed), alignment and allocation (stack or heap). This feature is essential for systems programming for reasons of performance (ex: to control cache and paging behavior), conformance to hardware specification (ex: page table entries), and interfacing with external C or assembly code and data. A careful implementation of the standard TCP/IP protocol stack in Standard ML incurs 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 in systems programs, data structure representation is as important as, or even more important than high level algorithms.

The philosophy of ML-like languages is that programs specify semantics and not realization (implementation). However, in systems programs, statements about representation and location are prescriptive, not descriptive. Compilers like TIL [25] implement unboxed representation as a discretionary optimization. Prescriptive requirements are not discretionary. First class treatment of representation is required in systems programming languages.

Mutability Support:    One of the key features essential for systems programming is support for first class mutability (c.f. C). The support for mutability must be first class in the sense that any location (stack or heap) can be mutable, and we should be able to specify mutability at field level granularity. Many modern programming languages — particularly those that support type inference — do not support this first class notion of mutability. ML does not support first class mutability; all mutable cells must reside in the heap. In Haskell, all state must be encapsulated within Monads [14]. In contrast to the C-like languages, these functional languages do have a mathematically sound notion of immutability.

We have identified three features — unboxed representation, mutability and polymorphic type inference — that are desirable in a systems programming language. While several existing languages support two of these features, none combine all three of them elegantly. In this paper, we endeavor to bridge this gap between systems programming and modern language designs through the BitC [22] programming language. BitC is a direct expression of typed lambda calculus with side effects, extended to be able to reflect the semantics of explicit representation. It supports polymorphic type inference and a new model of mutability which is expressive and has sound semantics.

BitC is a call-by-value expression language. BitC's support for unboxed mutability makes it desirable to allow some freedom in the compatibility of types with respect to their mutability at copy boundaries. This kind of compatibility has ramifications for type inference since there is no longer a unique way to type an expression. However, usability constraints require that we minimize the amount of type annotations required from the programmer. In this paper, we discuss some of these issues, and present a solution based on a simple extension to the Hindley-Milner inference algorithm [17] that applies certain heuristics to subjectively infer the appropriate type for all expressions.

2 The Language

BitC is a safe, systems programming language. A detailed description of the language and its support for systems programming (including a rich set of primitive data types and bit-fields, type classes [12] for overloading, representation of explicitly boxed and unboxed data-structures, discriminated unions, tagged-unions with inlined discriminators, etc.) can be found in the language definition [22]. In this paper, we limit our presentation to a core calculus of BitC called *B* in the interest of brevity. The user visible part of *B* is defined below:

Program variables are denoted by _x_, _y_, etc. and type variables by α, β, etc. _X__;^* denotes zero or more _X_s separated by a semicolon. The [] brackets denote optional parts of syntax. ⇑τ represents a reference (pointer) type and Ψτ represents a mutable type. The type τ \ *C* is a constrained type with the set of constraints *C*. The relation ≅ will be defined in section 4. The let construct can be used for allocating (possibly mutable) stack variables and to create let-polymorphic bindings. The expression dup(_e_), where e is of type τ, returns a reference of type ⇑τ to a heap-allocated copy of the value of _e_. The ^ operator is used to dereference heap cells. The := operator updates (mutates) both stack and heap locations. Unlike ML, := does not dereference its target. Pairs (,) are unboxed structures whose constituent elements contiguously allocated on the stack, or in their containing data-structure. _e_.1 and _e_.2 perform selection from pair values. Lists [...] have a boxed representation.

3 The Mutability Model

Traditionally, there are two models of mutability studied in the case of imperative languages. One of them is the ML model, where there is a clear separation between name bindings and updatable locations. All updatable (mutable) locations live in the heap within ``ref cells''. Fetching the value inside a ref cell requires an explicit dereferencing operation. The major advantage of this approach is that types are definitive about the mutability of every location, across all aliases. In this sense, we can say that the support for mutability is mathematically ``well-founded.'' This model benefits tools that perform static analysis or model checking because conclusions drawn about location immutability need never be conservative. This model of mutability also increases the amount of optimization the compiler can safely perform without complex alias analysis.

The other well known model of mutability is the C model, wherein the support for mutability is ``first-class'' in the sense that locations with mutable type can be passed as arguments and stored in data-structures. This model permits mutation of stack variables and unboxed values. There is a notion of lvalues which are expressions that can be the target of an assignment, and rvalues, that are otherwise used in computations. The extraction of the value from a (mutable) location is implicit, and does not require dereferencing. However, in this model, types cannot distinguish mutable values from immutable ones. 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 compiler or other analytical engines are not entitled to believe that certain locations or fields are constant even if so declared.

*B* supports well-founded first class mutability. Similar to ML, we impose the ``one location, one type'' rule.
      let _cp_ : ⇑bool = dup(true) in let _p_ : ⇑Ψbool = _cp_    (* Error *)
We see that _cp_ has the type reference to bool (⇑bool). This type is incompatible with that of _p_, reference to mutable-bool (⇑Ψbool). In order to support unboxed mutability, we still need to have a notion of lvalues. This not only preserves the programmer's mental model of the relationship between locations storage, but also ensures that compiler transformations are semantics preserving. In *B*, the legal lvalues are defined by: _L__v ::= _x_ | _L__v.1 | _L__v.2 | _L__v^ | _L__v : τ

4 Copy Compatibility

Since *B* is a call-by-value language, it is desirable that we allow some freedom in the compatibility of types with respect to their mutability at a copy boundary. For example, in the following expression:
      let _fnxn_ = λ_x_.(let ___ = _x_ := _some-fnxn_ _x_ in _fnxn-returning-unit_ _x_) 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 the formal argument _x_ is a copy of _y_ and occupies a different location, this expression is type safe. We refer to this notion of compatibility of types as copy compatibility, denoted by ≅. In this example, bool ≅ Ψbool.

Copy compatibility need not be restricted to the outermost mutability compatibility, but must not extend past a reference boundary in order ensure that every location has unique type. We define copy compatibility for *B* as:

Copy compatibility can be permitted at argument passing, new variable binding, assignment, and basically at argument/return positions of all expressions, except where an lvalue is expected or returned. For example, the expression (_x_ : τ) : Ψτ is illegal since identifiers are lvalues, but the branches of a conditional can have different but copy compatible types, as in: if  true then _a_ : τ else _b_ : Ψτ.

5 Type Inference

We would like to employ an inference algorithm with the following properties:

1. The inference algorithm must be decidable without programmer annotations. The problem with programmer annotations is pragmatic rather than ideological: ease of prototyping requires that these annotations be minimized.

2. The inference algorithm must ideally be complete. In the absence of principal types, it must minimize programmer annotations in the common case, and must be capable of inferring all sound types at least when guided by explicit annotation. This requirement is orthogonal to requirement (1).

3. The inference algorithm must automatically infer polymorphism (without programmer annotations) in order to maximize code reuse and encourage good software engineering.

4. The inference algorithm must not require whole program analysis. Whole program inference precludes separate compilation, poses scalability problems for large projects, and can result in surprising behaviour if the inferred types for a program change due to modifications in a distant part of the code base.

With these considerations in mind, we chose a variation of the Hindley-Milner algorithm [17] in *B*. We now describe challenges for type inference due to copy compatibility, explore the design choices, and finally present our solution.

Challenges Due to Copy Compatibility:    When an exact type compatibility requirement is replaced in the language design by copy compatibility, it is no longer possible to infer a unique (simple) type for the expression. For example, in the expression let _p_ = true, we know that the type of the literal true is bool, but the type of _p_ could either be bool or Ψbool. Therefore, we give _p_ the so-called ``maybe'' type α↓bool, which is a shorthand for the constrained type α \ {α ≅ bool}. The actual type will later get resolved to either bool or Ψbool. Similarly, in the expression (inferred types are shown beside ∥).
      let _pr_ = (true, false) in ... ∥ _pr_ : α↓(β↓bool ✗ γ↓bool)
copy compatibility is introduced at both the pair construction (arguments passed to the pair constructor), and the formation of a new binding.

Why Should We Infer Mutability?    It is natural to ask why mutability should be inferred at all. That is: why not require explicit annotation for all mutable values, and infer immutable types by default? In a language with copy compatibility, this will result in a proliferation of type annotations. Constructor applications, (polymorphic) type instantiations, accessor functions, etc. will have to be explicitly annotated with their types. For example, if _fst_ is an accessor function that returns the first element of a pair, and _m_ is a variable of type Ψbool, we will have to write:
      let _xyz_ = [(_fst_ (_m_, false) : Ψbool ✗ bool)] : [Ψbool] in ...
Therefore, if mutability is not inferred, it results in a substantial increase in the number of programmer annotations, and type inference becomes ineffective.

Incompleteness of Inference    The key idea of maybe types α↓τ is to defer commitments about the mutability status of types, and thus infer most-general types wherever possible. *B* is a let-polymorphic language and enforces the value restriction [27]. This means that the decision about the mutability of types cannot — in general — be deferred past their let bindings. For example, in the case of the expression: let _p_ = [] in ..., we cannot give _p_ the type ∀ α, β .β↓[α] (or ∀α.Ψ[α] or ∀α.β↓[α]). We must instead choose one of the polymorphic type ∀α.[α] or the monomorphic type β↓[α] That is, there is no principal type that can be inferred for _p_. Given this, we must fix these maybe types to be either mutable or immutable at a let-boundary. That is, the language definition must pick some solution for unsolved copy compatibility constraints before type generalization. In *B*, we trade completeness of inference to obtain a more expressive language without making major changes to the core type system.

Inference Considerations    First, we consider how to resolve copy compatibility constraints at a let boundary. One possibility is to fix all unresolved maybe types to immutable versions. For example:
      let _pf_ = (_n_ : Ψbool, λ_x_._x_) in ... ∥ _pf_ : ∀α.bool ✗ (α → α)
This scheme will preserve all polymorphism possible, but will mandate a programmer annotation for every mutable value. If mutable variants are chosen instead, no polymorphism can be inferred by default. Therefore, neither of these solutions are satisfactory. Further, from the standpoint of good programming ideology and static analysis, the inferred types must not be promiscuous with respect to mutability.

The previous section argued that we ``lose'' precision of inferred types (with respect to mutability) by the introduction of copy compatibility. Therefore, we can choose whether (or not) to introduce copy compatibility at various constructs like new bindings, function application/return, constructors, conditional expressions, etc. Another dimension of trade-off is whether to permit copy compatibility to the maximum permissible limit (as defined in section 4), or restrict it to top-level shallow mutability compatibility only. A further option is to require that all polymorphism be contained within function types, since function types can be polymorphic even if they abstract over mutable or maybe types.

Unless handled with care, full use of copy compatibility can result in the inferred types that are counter-intuitive to the programmer. For example:
      let _copyList_ = λ_lst_.match _lst_ with [] in [] else 
                                    match _lst_ with _x_::_rest_ in _x_::_copyList_ _rest_  in ...
For a naïve reader, the type of _copyList_ appears to be ∀α.[α] → [α] but is actually the more general type: ∀ α, β . [α] → [β] \ {α ≅ β}. Even though both the argument and return types of _copyList_ are of (boxed) list type, they are only required to be copy compatible because _copyList_ copies the constituent elements, thereby using new locations. Now, if we default maybe types that are ultimately unresolved to immutable, in the following definition we obtain:
      let _mutLst2_ = _copyList_ _mutLst_ : [Ψbool] in ... ∥ _mutLst_ : [bool] !!
which is a correct typing, but is most likely not what the programmer expects.

6 Type Inference in *B*

Having identified the various issues and trade-offs involved in type inference, we now describe the particular design choices made in BitC/*B* for handling copy compatibility. They have been driven in part by our experience writing BitC programs. In *B*, we allow copy compatibility to the full extent, up to a reference boundary. We allow copy compatibility to be invoked at arguments and return positions of all expressions that do not expect a location (lvalue).

At a let boundary, an unresolved maybe type α↓τ is resolved to τ. Intuitively, this means that we will default maybe types to the types of their original copies unless a better type is inferred or specified. The type τ of the original value is remembered as a ``hint'' to fix unresolved maybe types at a let boundary. Here, we are approximating the user's intent to the lexical ``flow'' of type information. For example, in the following expression,
      let _mb_ : Ψbool = true in let _l1_ = [_mb_] in let _l2_ : Ψ[bool] = [_mb_]
the type β↓[α↓Ψbool] is first inferred for both _l1_ and _l2_ (due to copies at list construction and binding). In the case of _l1_, the final type is resolved to [Ψbool] in accordance to the hints since we have no further information. The type of _l2_ is Ψ[bool], since we have a (consistent) annotation -- there are no unresolved maybe types. Further, under this scheme, the _listCopy_ example described in the previous section gets the more intuitive type ∀α.[α] → [α]. In the case of conflicting hints, we pick the most immutable type obtainable from all hints. This ensures that inferred types are always deterministic. For example:
let _bp_ = if  true then (true, false) : Ψbool ✗ bool
                         else (false, true) : bool ✗ Ψbool in ... ∥ _bp_ : bool ✗ bool
Here, the hints provided by the two branches of the if do not agree, and we resolve the conflict by picking bool ✗ bool as the effective hint.

In the case of locally defined identifiers, the top-most mutability is inferred by studying the syntactic usage of the identifier. That is, if the identifier is used as the target of an assignment (:=), it is given a shallowly mutable type. This is an ad hoc rule that reduces the need for explicit programmer annotations in the common case like iterators. In a full language like BitC, this rule must not be used for globals in order to keep inference deterministic. Further, this ``infer mutability first'' rule cannot, in general, be extended beyond shallow mutability. For example, in the expression let _fPtr_ = dup(λ_x_._x_) in (_useF1_ _fPtr_, _useF2_ _fPtr_), we do not have enough local information before type inference to determine whether _useF1_ and _useF2_ set the contents of the cell pointed to by _fPtr_, or use it polymorphically.

Due to copy compatibility, two function types are equal regardless of the shallow mutability of the argument and return types. Therefore, we enforce a syntactic restriction that all function types must be written with immutable types at copy compatible positions. The intuition here is that type of a function must be described in the interface form, and must hide the ``internal'' mutability information. For example, for the function definition let _f_ = λ_x_._x_ := true in ..., the external type is _f_ : bool → unit, and the internal type is _f_ : Ψbool → unit.

We must ensure that the internal types of a function do not influence the result type of applications, but the effect of arguments on the return types must be preserved. This ensures that the implementation of an abstraction can be changed (ex: from a pure recursive computation to loop involving mutation) unbeknownst to its callers. For example:

The function _f_ returns _p_ : Ψbool, regardless of its input. The external type of _f_ abstracts away the mutability of _p_, and thus, _ff_ gets the type bool. _g_ is an identity function which returns its argument. The external type of _g_ preserves the mutability of the actual argument _p_, and thus _gg_ gets the type Ψbool.

Mutability Polymorphism: A type is said to be mutability-polymorphic if it ranges over all [im]mutability variants of a particular type. For example, ∀α.α↓bool is mutability polymorphic over bool. By far the most useful case of this feature is to define functions that are mutability-polymorphic over concrete types, since functions with a polymorphic type such as ∀α.α → α are polymorphic over all types, mutable or immutable. The above inference algorithm tries to heuristically fix the mutability of all expressions (including functions). However, this behavior can be overridden by explicit annotation. For example, the definition:
let _allTrue_ : ∀α.[α↓bool] → bool = ... in ... ∥ _allTrue_ : ∀α.[α↓bool] → bool
defines _allTrue_, a function whose argument is mutability-polymorphic over [bool].

7 Formalization

We now formalize our type system and inference algorithm. Due to space limitations, we will limit our presentation to the following subset of *B*, called *B*^′.

Syntax   

All the above syntactic forms can be parenthesized without change in meaning. The let-kind ``-'' is a placeholder for the unkinded (input) let form. A substitution is of Z for Y in X is written using the standard notation: X[Z/Y].

The calculus of *B*^′ defines two kinds of locations: stack locations holding unboxed values, and heap locations holding boxed values. Heap locations are first class values, but stack locations are not. This distinction is sufficient to illustrate the two cases that must be handled by the type system: the types of values passed / copied by value (only) need to be copy compatible, but the types of values passed by reference must be strictly equal. More complex rules can be constructed based on these primitive cases.

In this calculus, we make a distinction between two ``kinds'' of let expressions — let<sup>ψ</sup>: monomorphic, possibly mutable definition, and let<sup>∀</sup>: polymorphic definitions. The two kinds of let expressions have different execution semantics. This distinction is similar to Smith and Volpano's Polymorphic-C [23]. 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. The kind ``-'' is a placeholder for the unkinded input let expression. We write let to range over let^ψ and let^∀.