Formalization of the BitC Type System

There is a persistent gap between modern language designs and the requirements of systems programmers. Systems programs rely on fine-grain control of data representation and use of state to achieve performance, conformance to hardware specification, and temporal predictability. Modern type systems such as those used in ML and Haskell rely on boxed representation of composite types and restricted support for mutability to enable features such as polymorphism, type inference, and sound type systems. No current language fully supports both feature sets, partly because no mutability model has been proposed that adequately combines explicitly unboxed types with consistent typing of mutability. C's ``const'' type qualifier is unsound, while from a systems programming perspective ML's ``ref'' construct is insufficiently expressive.

This paper introduces a new type system in which deep mutability is a first-class component of type. The type system is provably sound, expresses unboxed composite types, supports polymorphism and type inference, and reduces the amount of state that must be handled by stateful verification methods. The resulting system integrates these features in a way that is subjectively natural to systems programmers — in particular supporting naïve programmer intuitions about locations. A key element of this success is the adoption of certain ``hinting'' mechanisms that guide the inference process to the programmer-expected result. A practical and efficient implementation of this type system and inference mechanism has been constructed as part of the BitC programming language.

Chapter 2: Introduction

Safe systems programming is a focal topic for researchers in systems as well as programming languages and verification communities in the recent years. Although there seems to be a consensus about the fact that thirty years of programming in high level assembly is long enough [5], the level of correctness guarantee sought in the proposed alternatives vary greatly — ranging from memory safety [ 17 ,27 ] to static analysis or model checking to validate certain safety properties [2] to full semantic correctness verification [12] We are currently working on the Coyotos project [39], which investigates the possibility of a fully verified implementation of a secure microkernel. In order to achieve this, there is a need for a language framework that has the the right combination of expressiveness, formally founded semantics, control over low-level representation, and integration with modern verification technology.

Modern programming languages such as ML [26] or Haskell [19] provide newer, stronger, and more expressive type systems than systems programming languages such as C [ 22 ,16 ] or Ada [15]. These features improve the robustness and safety of programs, and it is desirable to incorporate them into languages that can be used for high-performance systems codes. Polymorphism facilitates better code reuse and organization. Type inference achieves the consistency advantages of static typing with a lower burden on the programmer, facilitating more rapid prototyping and development.

A key property of these ML-like languages is that the mutability model is a part of the type system. A term subset language suitable for modern logical frameworks [ 29 ,28 ,21 ,6 ] can be achieved simply by removing the ``ref'' construct. ML Types are decisive about the mutability of all locations (memory cells): every location has one and only one type across all aliases. Tools that perform static analysis or model checking benefit from the ML mutability model because conclusions drawn about location immutability need never be conservative [1]. This also reduces the state space that must be examined by stateful reasoning techniques. Since mutable values must not be let-polymorphic [3650], automatic inference of polymorphism requires a mathematically well-founded notion of mutability.

Unfortunately, most modern programming language implementations do not support certain key features that are essential for systems programming — most notably support for low-level representation management, and support for first class mutability. The support for mutability must be first class in the sense that a value of any type (and not just references) can be mutable, and we should be able to specify mutability at field level granularity.

Efforts have been made to retrofit safety and other high level language features into C-like low level languages. Systems like CCured [27] and Cyclone [17] use a combination of sound static analysis techniques, dynamic checks, user annotations, pointer restrictions and conservative garbage collection to ensure memory safety of C (or C-like) programs. First, a fundamental problem with the safe C-like languages is the lack of a rigorous semantic specification. Second, these systems conform to the C model of mutability, where all data is mutable (that is, types do not authentically distinguish mutable and immutable values see section 3.2). This promiscuity of mutability presents a great challenge for integration into a verification framework — we will either have to perform complex and whole program alias analyses, or draw conservative and weak conclusions about the semantic behavior of programs. The mutability model also limits the ability to perform polymorphic type inference. For example, Cyclone supports first class polymorphism only for function definitions [1153] that are explicitly annotated with a polymorphic type.

In this paper, we propose a new language BitC [55] which integrates all of the desirable features mentioned above into a single, consistent language framework. BitC is a type safe, higher order programming language that exposes machine-level representation of types, supports polymorphic type inference and well-founded first class mutability. BitC is a call-by-value expression language. Support for unboxed mutability means that we can allow some freedom in the compatibility of types with respect to their mutability at copy boundaries. This kind of compatibility has interesting ramifications for type inference, because there is no longer a unique way to type an expression. In this paper, we discuss some of these issues, and present a solution based on a simple extension to the Hindley-Milner inference algorithm [25]. A partial sketch of this approach was given in an earlier workshop paper [38]; the current paper presents the first complete treatment, consisting of a formalization and proof of soundness, as well as an implementation.

Chapter 3: Mutability Model and Type Inference

3.1 BitC

In this section, we give a brief introduction to BitC and the facilities available in BitC to suit systems programming. BitC supports a rich set of primitive datatypes and bit-fields: int8, int64, (bitfield uint32 8), float, double, etc. It also supports type classes [18] to support operator overloading over these types. For example:¹

(define (inc x) (+ x 1))
inc: (forall ((Arith 'a) (IntLit 'a)) (fn ('a) 'a))

Like C, BitC provides full control over data structure representation, which is necessary for high-performance systems programming. Composite types (structures and unions) may be explicitly declared as boxed (:ref) or unboxed (:val). The default representation is boxed. For example:

 (defstruct (pair 'a 'b):val fst: 'a snd: 'b)
 (defunion (list 'a) nil 
                    (cons car:'a cdr:(list 'a)))

BitC also has homogeneous aggregate types in the form of arrays (unboxed) and vectors (boxed).

BitC is a stateful language. Variables or individual fields may be given a mutable type. In the following example, rec defines an unboxed structure in which one of the fields is mutable, while xyz is a stack variable that is mutable.

(defstruct rec:val id:uint32 mVal:(mutable int64))
(let ((xyz:(mutable bool) #t)) ...)
xyz: (mutable bool)

The dup operator performs a heap copy and returns the corresponding heap location. For example:

(define bPtr (dup #t))
bPtr: (ref bool)

Unlike ML, heap copy does not entail mutability. The type of bPtr in the above example is (ref bool), which just states that bPtr is a reference (pointer) to a location containing an immutable value of type bool. Expressions that have a reference type can later be dereferenced through the deref (or ^) operator. BitC does not have an address-of (&) operator to obtain the address of stack locations. As in the case of most safe languages, heap locations are first class values, but stack locations are not. We use the unqualified term ``location'' wherever both stack and heap locations are applicable.

BitC supports let-polymorphism as in ML. Polymorphism is supported even over unboxed types. However, in some cases, we may want to restrict the polymorphism to reference types only, in order to ensure that the definition is not polyinstantiated (or otherwise adjusted to handle unboxed types). In BitC, there is a built in type classes called ref-type to which all boxed types belong. Now, we can write a polymorphic identity function that only works on reference types as:

 (define id:(forall ((ref-type 'a)) (fn ('a) 'a))
   (lambda (x) x))

There are several syntactic constructs in BitC to support a metalanguage, which allows application-specific safety properties to be embedded within a program. This meta-language will eventually be interfaced with a theorem prover in order to discharge the proof obligations expressed by the programmer.

3.2 Mutability Model in BitC

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.''

The other well known model of mutability is the C model, wherein the support for mutability is ``first-class'' in the sense that mutation of stack variables and unboxed values are supported. 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 (and safe-C languages) it is legal to write:

const int *cpi = ...;
int *pi = cpi;   // Warning only.
*pi = 5;         // OK!

The alleged ``constness'' of the location pointed to by cpi is a local property with (only) respect to this alias (cpi) and not a statement of true immutability of the location referenced by it. The compiler or other analytical engines are not entitled to believe that certain locations or fields are constant even if so declared.

BitC supports well-founded first class mutability. Similar to ML, we impose the the ``one location, one type'' rule.

(let ((cpi:(ref int32) (dup 10)))
  (let ((pi:(ref (mutable int32)) cpi)) ;ERROR

In order to support unboxed mutability, we still need to have a notion of lvalues. It is necessary for both preserving the programmer's mental model of the relationship between locations and storage, as well as ensuring that compiler transformations are semantics preserving. In an assignment context, the following syntactic forms in BitC accept only lvalues at positions indicated as lval, and return lvalues (except set!, which returns unit):

id
(array-nth lval ndx)
(vector-nth e ndx)
(member lval ident)
(deref e)
(set! lval e)

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 [7] (a simplified form of const), referential immutability [35] (immutability-by-reference that can be enforced shallowly or transitively) etc., which have versatile applications. These techniques are orthogonal and complementary to the immutability-by-location property that we have in BitC. For example, we could have types like (const (mutable τ)) that can express both global and local usage properties of a location.

3.3 Copy Compatibility

Since BitC 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 argument passing, assignment, and binding boundaries. We will refer to this as copy compatibility, denoted by ≅. For example:

(define (plus1 x:(mutable int32)) 
  (set! x (+ x 1)) x)       
plus1: (fn (mutable int32) int32)

(define v1 (plus1 10:int32))
v1: int32

In the application (plus1 10:int32) above, the type of the actual parameter 10 is int32 and that of the formal parameter x is (mutable int32). Here, we allow int32 ≅ (mutable int32).

Copy compatibility need not be restricted to the outermost mutability compatibility, but must not extend past a reference boundary. This is necessary to enforce the the invariant that every location must have a unique type, since the target of the reference is not copied. We define copy compatibility as follows:

τ ≅ (mutable τ) for any type τ (direct compatibility).
(array τ) ≅ (array (mutable τ)). Arrays are unboxed types, the entire array is copied by value.
(vector τ) ≇ (vector (mutable τ))
(ref τ) ≇ (ref (mutable τ)).
Compatibility of composites: Composite types are copy compatible if and only if all of their fields have equal types in the case of boxed types and copy compatible types in the case of unboxed types. In order to enforce this rule, the following restriction must be imposed for unboxed parametric types: instantiations of any type variable used within another reference type must match exactly. For example in the following structure:
```
(defstruct (St 'a 'b):val f1:'a f2:(ref 'b))
```
instantiations of 'a are only required to be copy compatible, but instantiations of 'b must match exactly.
```
(St char char) ≅ (St (mutable char) char)
(St char char) ≇ (St char (mutable char))
```

In addition to argument passing, and new variable bindings, we can also permit copy compatibility at argument and return position of all expressions that do not return an lvalue. This is because we can think of them in terms of equivalent SSA forms, which introduce temporary bindings for all intermediate results. For example, we can permit the various branches of conditional expressions to have to have different but copy compatible types:

(if #t m:(mutable int32) 10:int32)

3.4 Type Inference

When an exact type compatibility requirement is replaced in the language design by copy compatibility, it is no longer possible to infer a unique type for the expression. For example, in the following expression:

(let ((p 10:int32)) ... )

we know that the type of the literal 10 is int32, but the type of p could either be int32, or (mutable int32). When we cannot ascertain the mutability status of a bound identifier, we give it the so-called ``maybe'' type (?mutable? int32), which is actually a shorthand for the constrained type α \ {α ≅ int32}. That is, it is undecided as to whether the actual type is int32, or (mutable int32), and can be resolved by later unification. If it is not, a choice must eventually be fixed by the language definition. For example, the let form:

(let ((p (pair 1:int32 #t))) ... )

introduces copy compatibility at both the pair constructor application, and the formation of a new binding for p. The types assigned by the compiler are:

p:(?mutable? (pair (?mutable? int32) 
                   (?mutable? bool))

3.4.1 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 an expression language with copy compatibility, inferring immutable types by default 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 that returns the first element of a pair and m is a variable with type (mutable bool), we will have to write:

(define xyz 
  (vector (fst (pair m 10)
               :(pair (mutable bool) int32)))
  :(vector (mutable int32)))

Pierce and Turner have conducted a study on the impact of requiring explicit type annotations in higher order typed programming languages [31]. Their measurements on about 1,60,000 lines of Objective Caml [23] code revealed that polymorphic type instantiations happen every third line of code, anonymous function definitions happen once in 10-100 lines of code and local bindings occur about once every twelve lines. Therefore, in BitC, not inferring mutability would make type inference a liability rather than an asset in the case of stateful programs.

3.4.2 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. BitC is a let-polymorphic language and enforces the value restriction [3650]. This means that the decision about the mutability of types cannot be deferred past their let bindings, since mutable types must not be generalized. For example, in the case of the expression:

(let ((p nil)) ... )

we cannot give p the type

(forall ('a) (?mutable? (list 'a)))

We must instead choose one of:

(forall ('a) (list 'a)) ; polymorphic
(?mutable? (list 'a))   ; monomorphic

That is, there is no principal type that we can infer for p. Given this, we must fix these maybe types to either mutable or immutable at a let-boundary. In the next section, we will identify various choices for how to fix these maybe types, and discuss their merits and limitations.

In contrast, ML is able to infer principal types since its inference rules are purely syntax directed. In BitC, we trade completeness of inference to obtain a more expressive language without making any major changes to the core type system.

3.4.3 Inference Considerations

In this section we outline certain design considerations for a type inference scheme in the presence of copy compatibility. An ideal scheme must not require excessive programmer annotations in the common case, and must be capable of inferring all sound types at least when guided by explicit annotation.

The problem with programmer annotations is pragmatic rather than ideological: we do not view programmer specification of types as bad per se (indeed, in certain places BitC requires annotations), but ease of prototyping requires that these annotations be minimized. As a matter of good programming ideology and interfacing with other static analysis or verification tools, the inferred types must not be promiscuous with respect to mutability.

First, we consider how to solve the copy compatibility constraints introduced by the maybe types. One possibility is to fix all unresolved maybe types to immutable versions. For example:

(let ((p (pair n:(mutable int32) 
               (lambda (x) x)))) ...)
p: (pair int32 (fn ('a) 'a))

This scheme will preserve all polymorphism possible, but will mandate a programmer annotation for every mutable location. The alternative would be to choose the mutable variants, in which case we will effectively have no polymorphism (by default). In the case of local definitions, we can collect more usage information and fix maybe-ness accordingly.

The previous section argued that we ``lose'' precision of inferred types (with respect to mutability) by the introduction of copy compatibility. We can think of this as a trade-off between freedom in type compatibility and precision of inference. Therefore, we can choose whether to (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 we permit copy compatibility to the maximum permissible limit (as defined in section 3.3), 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 we can make function types 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:

(import ls bitc.list)
(define (list2vec lst)
  (make-vector (length lst) 
    (lambda (n) (ls.list-nth lst n))))

For a naïve reader, the type of list2vec appears to be (fn ((list 'a)) (vector 'a)), but is actually the more general type:

(forall ((copy-compat 'a 'b)) 
            (fn ((list 'a)) (vector 'b)))

copy-compat is a special type class that relates two copy compatible types. Now, if we default maybe types that are ultimately unresolved to immutable, in the following definition we obtain:

(define mVec (list2vec mLst:(list (mutable bool)))
mVec: (vector bool)  ;; !!!

which is a correct typing, but is most likely not what the programmer expects. In this case, even though the both the argument and return types of list2vec are reference types, they are only required to be copy compatible because list2vec copies the constituent elements, thereby using new locations.

3.5 Type Inference in BitC

Having identified the various issues and trade-offs involved in type inference, we now describe the particular design choices made in BitC for handling copy compatibility. This is by no means ``the'' solution to the problem, but reflects our judgment of the best way to capture the programmer's intuition about the flow of types in the language. It has been driven in part by our experience writing BitC programs. In BitC, 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.

Every time we form a ``maybe'' type due to a copy operation, we remember the original type as a hint to resolve the copy compatibility constraints in the resultant type. At a let boundary, we resolve any unresolved compatibility constraints by unifying with this hint. Intuitively, this means that we will default maybe types to the types of their original copies, unless overridden by an explicit annotation. Here, we are approximating the user's intent to the lexical ``flow'' of type information. For example:

(define mb:(mutable bool) #t))
mb: (mutable bool)

(define p (vector mb))
p: (vector (mutable bool))

(define q:(vector bool) (vector mb))
q: (vector bool)

The type of p shows how maybe types are defaulted based on hint information, and the type of q shows how this can be overridden by programmer annotation. Since we default unresolved maybe-types to original ones the list2vec example described in section 3.4.3 now gets the more intuitive type:

list2vec: (fn ((list 'a)) (vector 'a))

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 a set!, it is given a shallowly mutable type. This is an ad hoc rule that tries to reduce the need for explicit type qualifications by the programmer in the common case (ex: iterators). However, this rule must not be invoked for top-level (global) definitions. Otherwise, inferred types will no longer be deterministic, as the top level definitions have unlimited scope.

(define (fact x) (do ((ans 1 ans) 
		      (i x (- i 1)))
		     ((== i 0) ans)
		     (set! ans (* ans i))))

In the case of conflicting hints in the different branches of conditional expressions, we pick the most immutable of all hints. This ensures that inferred types are always deterministic. For example:

(define boolPair 
  (if #t 
    (pair #t #f):((mutable bool), bool) 
    (pair #f #t):(bool, (mutable bool))))
p: (bool, bool)

If there are any residual compatibility constraints even after unifying with hints, we resolve them to immutable variants.

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 (the external type), and must hide the ``internal'' mutability information.

(define (f x) (set! x x))
Internal Type f: (fn ((mutable 'a)) ())
External Type f: (fn ('a) ())

Even though function types must be written in external form, any type-qualifications on the arguments of a function within its body correspond to the internal types, and may contain mutable qualifications.

(define abc:(fn ((mutable bool)) 'a) ...) ;; ERROR
(define (abc x:(mutable bool)) ... )      ;; OK

This internal/external type notion is also important in the process of resolving copy compatibility constraints using hints. We should be sure 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. For example:

(define p:(mutable bool) #t)
(define (f x) p)  ;; f: (fn ('a) bool)
(define (g x) x)  ;; g: (fn ('a) 'a)

(define ff (f p)) ;; ff: bool
(define gg (g p)) ;; gg: (mutable bool)

Further, two instances of a type class can co-exist only if all methods have different external signatures. For example:

(deftypeclass (TCL 'a 'b)
  mtd: (fn ('a (vector 'b)) 'a)))

(definstance (TCL bool bool) ...)
(definstance (TCL (mutable bool) bool) ..) ;CONFLICT!
(definstance (TCL bool (mutable bool)) ..) ;OK.

Chapter 4: Formalization

4.1 The Language

In the interest of brevity, we will limit ourselves to the following core calculus:

Syntax

Identifiers	_x_ ::=	_y_ `\|` _z_ \| ...
Stack Locations	l ::=	l₁ `\|` l₂ \| ...
Heap Locations	ℓ ::=	ℓ₁ `\|` ℓ₂ \| ...
Values	_v_ ::=	() `\|` true `\|` false `\|` ℓ `\|` λ_x_._e_
lvalues	£ ::=	l `\|` ℓ`^`
Expressions	_e_ ::=	_v_ `\|` _e_ _e_ `\|` _e_ : τ `\|` _e_ `:=` _e_ `\|` `let`^κ _x_[:τ] = _e_ `in` _e_
		`\|` `dup`(_e_) `\|` _e_`^` `\|` `if` _e_ `then` _e_ `else` _e_
Let-kinds	κ ::=	- `\|` α `\|` ψ `\|` ∀

All syntactic forms introduced in this document can be parenthesized without change in meaning. An optional qualification is provided on the identifier defined in a let expression since the same effect cannot be obtained by qualifying the defining expression (due to copy compatibility). The let-kind ``-'' is a placeholder for the unkinded let form.

4.2 Dynamic Semantics

Syntax

Stack	S ::=	∅ `\|` S, l ↦ _v_
Heap	H ::=	∅ `\|` H, ℓ ↦ _v_

The system state is represented by the triple S; H; _e_ consisting of the stack, the heap, and the expression to be evaluated. Evaluation itself is a two place relationship S; H; _e_ ⇒ S^′; H^′; _e_^′ that denotes transformation in the system state due to a single step of execution.

E-RVAL

S(l) = _v_

S; H; l ⇒ S; H; _v_

E-LEFT-TQ

S; H; _e_ : τ ⇛ S; H; _e_

E-TQ

S; H; _e_ : τ ⇒ S; H; _e_

E-LET-TQ

S; H; let _x_ : τ = _e_₁ in _e_₂ ⇒ S; H; let _x_ = _e_₁ in _e_₂

E-APP-STEP-FN

S; H; _e_₁ ⇒ S^′; H^′; _e_^′₁

S; H; _e_₁ _e_₂ ⇒ S^′; H^′; _e_^′₁ _e_₂

E-APP-STEP-ARG

S; H; _e_₂ ⇒ S^′; H^′; _e_^′₂

S; H; _v_₁ _e_₂ ⇒ S^′; H^′; _v_₁ _e_^′₂

E-APP

l ∉ dom(S)

S; H; λ_x_._e_ _v_ ⇒ S, l ↦ _v_; H; _e_[l/_x_]

E-LET-STEP

S; H; _e_₁ ⇒ S^′; H^′; _e_^′₁

S; H; let _x_ = _e_₁ in _e_₂ ⇒ S^′; H^′; let _x_ = _e_^′₁ in _e_₂

E-LET-M

l ∉ dom(S)

S; H; let^ψ _x_ = _v_₁ in _e_₂ ⇒ S, l ↦ _v_₁; H; _e_₂[l/_x_]

E-LET-P

S; H; let^∀ _x_ = _v_₁ in _e_₂ ⇒ S; H; _e_₂[_v_₁/_x_]

E-IF-STEP

S; H; _e_ ⇒ S^′; H^′; _e_^′

S; H; if _e_ then _e_₁ else _e_₂ ⇒ S^′; H^′; if _e_^′₁ then _e_₂ else _e_₃

E-IF-TRUE

S; H; if true then _e_₁ else _e_₂ ⇒ S; H; _e_₁

E-IF-FALSE

S; H; if false then _e_₁ else _e_₂ ⇒ S; H; _e_₂

E-DUP-STEP

S; H; _e_ ⇒ S^′; H^′; _e_^′

S; H; dup(_e_) ⇒ S^′; H^′; dup(_e_^′)

E-DUP

ℓ ∉ dom(H)

S; H; dup(_v_) ⇒ S; H, ℓ ↦ _v_; ℓ

E-LEFT-DEREF-STEP

S; H; _e_ ⇒ S^′; H^′; _e_^′

S; H; _e_^ ⇛ S^′; H^′; _e_^′^

E-DEREF-STEP

S; H; _e_ ⇒ S^′; H^′; _e_^′

S; H; _e_^ ⇒ S^′; H^′; _e_^′^

E-DEREF

H(ℓ) = _v_

S; H; ℓ^ ⇒ S; H; _v_

E-SET-STEP-LHS

S; H; _e_₁ ⇛ S^′; H^′; _e_^′₁

S; H; _e_₁ := _e_₂ ⇒ S^′; H^′; _e_^′₁ := _e_₂

E-SET-STEP-RHS

S; H; _e_₂ ⇒ S^′; H^′; _e_^′₂

S; H; £ := _e_₂ ⇒ S^′; H^′; £ := _e_^′₂

E-SET-STACK

S, l ↦ _v_₁; H; l := _v_₂ ⇒ S, l ↦ _v_₂; H; ()

E-SET-HEAP

S; H, ℓ ↦ _v_₁; ℓ^ := _v_₂ ⇒ S; H, ℓ ↦ _v_₂; ()

Dynamic Semantics

Table 4.1 shows the evaluation rules for our core language. Following the theoretical development in [ 1153 ,54 ], we give separate execution semantics for left and right execution (evaluation of expressions that appear on the LHS and RHS of an assignment _e__l := _e__r) denoted by ⇛ and ⇒ respectively.

In the above operational semantics rules, a distinction is made between the stack and the heap in order to ensure that we can only capture references to heap cells (E-DUP, E-LEFT-DEREF, and E-DEREF work only on the heap). The heap locations are first class values but stack locations are not. Therefore stack locations cannot escape beyond their scope (although the bindings themselves are not removed from the stack, in the interest of of simplicity). E-RVAL represents implicit value extraction for stack locations. State updates can be performed either on the stack or on the heap (E-SET-STACK and E-SET-HEAP). We assume that the program is alpha-converted so that there are no name collisions due to inner bindings. We do not model garbage collection, and assume an infinite supply of stack and heap cells.

We cannot give one correct execution semantics for the (unkinded) expression: let _x_ = _v_ in _e_, since there is not enough syntactic support to determine whether _x_ is a (mutable) location or a polymorphic immutable term. The correct step to take is always clear from static type information. We must take the LET-M path for all mutable definitions, and the LET-P path for all polymorphic definitions. For immutable non-polymorphic definitions, either step will work, but we always choose LET-M.

Therefore, we make a distinction among two ``kinds'' of let definitions as: let^ψ (monomorphic, possibly mutable definition) and let^∀ (polymorphic definition). The non-polymorphic version of let is shown as let^ψ and not let because an immutable monomorphic/concrete definition is also defined using this construct. Now, we give separate execution semantics for each of there let forms. Since the type rules only derive a type for the correct kinds of let in each case, execution of typed expressions is always expected to take the correct path.

We use let to range over let^ψ and let^∀. and will still use the unkinded term let, when either version is (equally) applicable. Note that let is different from let because two occurrences of let in the same context correspond to the same kind, whereas two occurrences of let need not match the same kind.

4.3 Static Semantics

Syntax

Types	τ ::=	α `\|` `unit` `\|` `bool` `\|` τ → τ
ref / pointer		`\|` ⇑τ
Mutable type		`\|` Ψτ
Type Scheme	σ ::=	τ `\|` ∀α.σ
Binding Environment	Γ ::=	∅ `\|` Γ, _x_ ↦ σ
Store Typing	Σ ::=	∅ `\|` Σ, ℓ ↦ τ `\|` Σ, l ↦ τ
Logical Relations	Ω ::=	?true? `\|` ?false? `\|` Ω ∧ Ω `\|` Ω ∨ Ω `\|` ¬Ω `\|` ?Predicate??(?Ω^*?)?

A substitution is of Z for Y in X is written using the standard notation: X[Z/Y]. Substitutions within a type up to a ref boundary are written as: τ[Z/Y].

4.3.1 Copy Compatibility

Compatibility of types that differ in shallow mutability at copy boundaries is called copy compatibility [56], denoted by ≅, and is defined as:

τ ≅ τ
Ψτ ≅ τ

In our algebra of types, we have the equation ΨΨτ ≡ Ψτ.

We also define the operators △ and ▽ that increase or decrease the mutability of a type, defined as:

△(Ψτ) = Ψτ and △(τ) = Ψτ, where τ ≠ Ψτ^′
▽(Ψτ) = τ and ▽(τ) = τ, where τ ≠ Ψτ^′

It is obvious that ∀τ.▽(τ) ≅ τ ≅ △(τ), and ∀τ, τ^′.τ ≅ τ^′ iff ▽(τ) = ▽(τ^′) iff △(τ) = △(τ^′).

4.3.2 Compatibility of Function Types

Two function types are equal regardless of the shallow mutability of the argument and return types [56]. Due to copy compatibility, two function types are equivalent in all respects regardless of the (shallow) mutability of the argument and return positions. Therefore we always write all function types in the following normalized form:²

The (contravariant) argument type is written in the maximally immutable form (devoid of shallow mutability).
The (covariant) return type is written in the maximally mutable form.

This ensures that the ``external'' type of a function is maximally permissive with respect to mutability. However, during type inference, if we infer the type ▽(τ_arg) → △(τ_ret) as the external type of a function, this normalization can later get violated due to substitution of type-variables. Therefore, we define the ⌊τ⌋ and ⌈τ⌉ ``meta-constructors'' which (respectively) minimize and maximize the mutability of a type, but are interpreted lazily.

We also define (and implicitly use) the following equivalences in the algebra of types:

⌊τ⌋ ≡ ▽(τ) (lazily)
⌈τ⌉ ≡ △(τ) (lazily)

4.3.3 Copy Coercions

TS-MUT1

Ψτ ≼: τ

TS-MUT2

τ ≼: τ^′

Ψτ ≼: Ψτ^′

TS-REF

τ = τ^′

⇑τ ≼: ⇑τ^′

TS-FN

τ₁ = τ^′₁ τ₂ = τ^′₂

τ₁ → τ₂ ≼: τ^′₁ → τ^′₂

TS-CEIL

⌈τ⌉ ≼: τ

TS-FLOOR

τ ≼: ⌊τ⌋

TS-REFL

τ ≼: τ

TS-TRANS

τ₂ ≼: τ₁ τ₁ ≼: τ

τ₂ ≼: τ

Copy Coercion Rules

Table 4.2 shows how we can obtain copy compatibility by copy coercions (similar to subtyping). We can now define copy compatibility as:

τ₁ ≅ τ₂ ≡ τ₁ ≼: ▽(τ₂)

The TS-REF rule ensures that copy compatibility does not extend beyond a ref-boundary. Since two function types are equivalent in all respects regardless of the (shallow) mutability of the argument and return positions, we will write all function types in normalized form. The (contravariant) argument type is written in the maximally immutable form (devoid of shallow mutability), and the (covariant) return type is written in the maximally mutable form. This ensures that the ``outer'' type of a function is maximally permissive with respect to mutability. The TS-FN rule therefore is invariant in terms of its arguments and return types.

We will also write Γ; Σ ⊢ _e_ ≼: τ as a shorthand for: Γ; Σ ⊢ _e_ : τ^′, τ^′ ≼: τ.

4.3.3.1 Problem with Subsumption-like Coercion Rule

In BitC, explicit qualifications are a statement of absolute typing and not type compatibility. Preserving this rule, requires that we must not have generic subsumption like rules for copy coercion. That is, if we have the following subsumption like rules:

TW-TQEXPR (WRONG)

Γ; Σ ⊢ _e_ : τ

Γ; Σ ⊢ (_e_ : τ) : τ

TW-SUB

Γ; Σ ⊢ _e_ : τ^′ τ^′ ≼: τ

Γ; Σ ⊢ _e_ : τ

We can then write:

let _x_ = () in if true then _x_ : unit else _x_ := ()

Here, in the else branch of if, we can derive the typing _x_ : Ψunit and in the then, through subsumption also obtain _x_ : unit, which violates our absolute-compatibility at qualification rule.

Therefore, we will not introduce this rule, but instead introduce copy coercion operations at all copy compatible positions in the type rules.

4.3.4 Location Semantics

The lvalue rules shown in Table 4.3 ensure that only those expressions permitted by location semantics [ 55 ,56 ] appear on the left hand side of an assignment expression.

L-ID

⊢_lval _x_

L-HLOC

⊢_lval ℓ

L-SLOC

⊢_lval l

L-DEREF

⊢_lval _e_^

L-TQ

⊢_lval _e_

⊢_lval _e_ : τ

Location Semantics Rules

4.3.5 Declarative Type Rules

T-UNIT

Γ; Σ ⊢ () : unit

T-TRUE

Γ; Σ ⊢ true : bool

T-FALSE

Γ; Σ ⊢ false : bool

T-ID

Γ(_x_) = ∀α^*.τ

Γ; Σ ⊢ _x_ : τ[τ^′^*/α^*]

T-HLOC

Σ(ℓ) = τ

Γ; Σ ⊢ ℓ : ⇑τ

T-SLOC

Σ(l) = τ

Γ; Σ ⊢ l : τ

T-LAMBDA

Γ, _x_ ↦ τ₁; Σ ⊢ _e_ : τ₂

Γ; Σ ⊢ λ_x_._e_ : ▽(τ₁) → △(τ₂)

T-APP

Γ; Σ ⊢ _e_₁ ≼: τ₂ → τ₀ Γ; Σ ⊢ _e_₂ ≼: τ₂ τ₀ ≼: τ^′₀

Γ; Σ ⊢ _e_₁ _e_₂ : τ^′₀

T-SET

Γ; Σ ⊢ _e_₁ ≼: Ψτ Γ; Σ ⊢ _e_₂ ≼: τ ⊢_lval _e_₁

Γ; Σ ⊢ _e_₁ := _e_₂ : unit

T-IF

Γ; Σ ⊢ _e_₁ ≼: bool Γ; Σ ⊢ _e_₂ ≼: τ Γ; Σ ⊢ _e_₃ ≼: τ τ^′ ≼: τ

Γ; Σ ⊢ if _e_₁ then _e_₂ else _e_₃ : τ^′

T-TQEXPR

Γ; Σ ⊢ _e_ : τ

Γ; Σ ⊢ (_e_ : τ) : τ

T-DUP

Γ; Σ ⊢ _e_ ≼: τ τ^′ ≼: τ

Γ; Σ ⊢ dup(_e_) : ⇑τ^′

T-DEREF

Γ; Σ ⊢ _e_ ≼: ⇑τ

Γ; Σ ⊢ _e_^ : τ

T-LET-M [TQ]

Γ; Σ ⊢ _e_₁ ≼: τ₁ τ ≼: τ₁ Γ; Σ; _e_₁ ⊢_gen τ ⋖ σ ⊢_loc _x_ : σ Γ, _x_ ↦ σ; Σ ⊢ _e_₂ : τ₂

Γ; Σ ⊢ (let^ψ _x_[:τ] = _e_₁ in _e_₂) : τ₂

Q-LOC

σ = τ

⊢_loc _x_ : σ

T-LET-P [TQ]

Γ; Σ ⊢ _e_₁ ≼: τ₁ τ ≼: τ₁ Γ; Σ; _e_₁ ⊢_gen τ ⋖ σ ⊢_term _x_ : σ Γ, _x_ ↦ σ; Σ ⊢ _e_₂ : τ₂

Γ; Σ ⊢ (let^∀ _x_[:τ] = _e_₁ in _e_₂) : τ₂

Q-TERM

σ = ∀α^*.τ

⊢_term _x_ : σ

Declarative Type Rules

Declarative Type rules are given in Table 4.4. The standard type judgment Γ; Σ ⊢ _e_ : τ is understood as: given a binding environment Γ and store typing Σ the expression _e_ has type τ. We write _e_ ≼: τ as a shorthand for: _e_ : τ^′, τ^′ ≼: τ, for some type τ^′. In the type rules, we introduce copy coercions at all positions where copy compatibility is applicable. Type generalization at a let is decided by the judgment ⊢_gen .

4.3.6 Generalization

This section uses the ``full'' value restriction as proposed by Wright [3650]. Relaxations to this rule based on Garriague's scheme [52] were proposed in [56]. Those rules must be incorporated at a later stage.

G-VALUE

?Value??(?_e_?)? ?Immut??(?τ?)? α^* = ?ftv?(τ) ∖ ?ftv?(Γ) ∖ ?ftv?(Σ)

Γ; Σ; _e_ ⊢_gen τ ⋖ ∀α^*.τ

G-EXPANSIVE

Γ; Σ; _e_ ⊢_gen τ ⋖ τ

Generalization Rules

The type generalization rules are shown in Table 4.5. The rule G-VALUE-PF is not actually used for typing user programs, but is only necessary to prove preservation of types.

4.3.6.1 DEFINITION: Free Type Variables

We denote the set of free type variables in a type τ as ?ftv?(τ).

?ftv?(α) = α
?ftv?(unit) = {}
?ftv?(bool) = {}
?ftv?(⇑τ) = ?ftv?(τ)
?ftv?(Ψτ) = ?ftv?(τ)
?ftv?(τ₁ → τ₂) = ?ftv?(τ₁) ∪ ?ftv?(τ₂)
We also write:
?ftv?(τ^*) = ∪ ?ftv?(τ)
?ftv?(σ) = ?ftv?(α^*) ∪ ?ftv?(τ) where σ = ∀α^*.τ
?ftv?(Γ) = ∪ ?ftv?(σ) forall _x_ : σ ∊ Γ
?ftv?(Σ) = ∪ ?ftv?(τ) forall ℓ : τ ∊ Σ or l : τ ∊ Σ
?ftv?(*C*) = ∪ ?ftv?(τ) where *C* is a set of constraints, and τ is a type involved in any constituent constraint.
FTVS(X, Y, ... ) = FTVS(X) ∪ FTVS(Y) ∪ ..., where X, Y, ... are any of the above permissible arguments.

4.3.6.2 DEFINITION: Value Restriction

?Value?(_v_) = ?true?
?Value?(_x_) = ?true?
?Value?(ℓ) = ?true?
?Value?(l) = ?true?
?Value?(_e_ : τ) = ?Value??(?_e_?)?
?Value?(dup(_e_)) = ?Value??(?_e_?)?
?Value?(_e_^) = ?Value??(?_e_?)?
?Value?(if _e_₁ then _e_₂ else _e_₃) = ?Value??(?_e_₁?)? ∧ ?Value??(?_e_₂?)? ∧ ?Value??(?_e_₃?)?
?Value?(let _x_ = _e_₁ in _e_₂) = ?Value??(?_e_₁?)? ∧ ?Value??(?_e_₂?)?
?Value?(_e_) = ?false?
?Immut?(unit) = ?true?
?Immut?(bool) = ?true?
?Immut?(α) = ?true?
?Immut?(τ₁ → τ₂) = ?true?
?Immut?(⇑τ) = ?Immut??(?τ?)?
?Immut?(∀α^*.τ) = ?Immut??(?τ?)?
?Immut?(τ) = ?false?

4.3.7 Soundness of Declarative system

4.3.7.1 DEFINITION: Stack and Heap Typing

A heap H and a stack S are said to be well typed with respect to a binding context Γ and store typing Σ, and written Γ; Σ ⊢ H + S if

dom(Σ) = dom(H) ∪ dom(S)
∀ℓ ∊ dom(H), Γ; Σ ⊢ H(ℓ) ≼: Σ(ℓ)
∀l ∊ dom(S), Γ; Σ ⊢ S(l) ≼: Σ(l)

4.3.7.2 LEMMA: Inversion of Typing Relation

If Γ; Σ ⊢ () : τ then τ = unit.
If Γ; Σ ⊢ true : τ then τ = bool.
If Γ; Σ ⊢ false : τ then τ = bool.
If Γ; Σ ⊢ ℓ : τ then τ = ⇑τ^′.
If Γ; Σ ⊢ λ_x_._e_ : τ then τ = τ^′₁ → τ^′₂ such that τ^′₁ = ▽(τ₁), τ^′₂ = △(τ₂), and, Γ, _x_ ↦ τ₁; Σ ⊢ _e_ : τ₂.
If Γ; Σ ⊢ _e_^ : τ then Γ; Σ ⊢ _e_ ≼: τ^′.
Other cases are similar.

Proof: Immediate from the definition of typing relation.

4.3.7.3 LEMMA: Inversion of Copy Coercion

If τ ≼: bool then τ = bool or τ = Ψbool.
If τ ≼: unit then τ = unit or τ = Ψbool.
If τ ≼: τ₁ → τ₂ then τ = τ₁ → τ₂ or τ = Ψ(τ₁ → τ₂).
If τ ≼: ⇑τ^′ then τ = ⇑τ^′ or τ = Ψ⇑τ^′.
If τ ≼: Ψτ^′ then τ = Ψτ^″ such that τ^″ ≼: τ^′.
If τ ≼: Ψτ^′ then τ ≼: τ^′.

Proof: By induction on the copy coercion derivation.

4.3.7.4 LEMMA: Canonical Forms

If _v_ is a value, and Γ; Σ ⊢ _v_ ≼: unit, then, _v_ is ().
If _v_ is a value, and Γ; Σ ⊢ _v_ ≼: bool, then, _v_ is either true or false.
If _v_ is a value, and Γ; Σ ⊢ _v_ ≼: ⇑τ, then, _v_ is ℓ, ℓ ∊ dom(Σ).
If _v_ is a value, and Γ; Σ ⊢ _v_ ≼: τ₁ → τ₂, then, _v_ is λ_x_._e_.

Proof: By induction on the derivation of Γ; Σ ⊢ _v_ ≼: τ.

If Γ; Σ ⊢ _v_ ≼: bool, we have Γ; Σ ⊢ _v_ : τ and τ ≼: bool by Inversion of copy coercion relation, τ = bool or τ = Ψbool. If τ = bool, it is clear that the final rule in the derivation must be T-TRUE, or T-FALSE, in which case the result is immediate. The case τ = Ψbool cannot happen because there is no rule that derives a mutable type for a value, and we assume that the induction hypothesis Γ; Σ ⊢ _v_ : τ holds.

Other cases of the lemma are similar.

4.3.7.5 LEMMA: Progress

If _e_ is a closed, well typed term, that is, ∅; Σ ⊢ _e_ : τ for some τ and Σ, given any heap H and stack S such that Γ; Σ ⊢ H + S,

If ⊢_lval _e_, then _e_ is either a valid lvalue £ (that is, £ = l, l ∊ dom(S) or £ = ℓ^, ℓ ∊ dom(H)) or else ∃ _e_^′, S^′, H^′ such that:S; H; _e_ ⇛ S^′; H^′; _e_^′.
_e_ is a value _v_ or else ∃ _e_^′, S^′, H^′ such that S; H; _e_ ⇒ S^′; H^′; _e_^′.

Proof: By induction on the typing derivation.

Case T-UNIT, T-TRUE, T-FALSE, T-HLOC, T-LAMBDA: (Values) Result is immediate for right execution, and cannot happen for right execution
Case T-ID: cannot happen, there is no execution rule for variables.
Case T-SLOC: Immediate for left execution. Right execution and can always continue with E-RVAL rule as the stack is well typed (Γ; Σ ⊢ H + S).
Case T-APP: Only right execution is possible, no application is well typed as an lvalue. We have: _e_ = _e_₁ _e_₂, _e_₁ ≼: τ₁ → τ₂, and _e_₂ ≼: τ₁. If _e_₁ or _e_₂ is not a value, we can take E-APP-STEP-FN or E-APP-STEP-ARG. Otherwise, when both _e_₁ and _e_₂ are values, by canonical forms lemma, _e_₁ is of the form λ_x_._e_^′, and we can take the step E-APP.
Case T-IF: Similar to T-APP, only right execution is permitted.
Case T-SET: Only right execution is applicable. We have: _e_ = _e_₁ := _e_₂, _e_₁ ≼: τ₁ → τ₂, Γ; Σ ⊢ _e_₁ ≼: Ψτ, Γ; Σ ⊢ _e_₂ ≼: τ, and ⊢_lval _e_₁. If _e_₁ not an lvalue, since we have ⊢_lval _e_₁ we can take E-SET-STEP-LHS by induction hypothesis. Similarly, if _e_₂ is not a value, we can take E-SET-STEP-RHS. Finally, if _e_₁ = £ and _e_₁ = _v_, we can take the step E-SET-STACK or E-SET-HEAP as applicable.
Case T-DUP: Only right execution is permitted, and can take E-DUP-STEP or E-SUP-STEP as applicable.
Case T-DEREF: We have: _e_ = _e_₁^, and Γ; Σ ⊢ _e_₁ ≼: ⇑τ. Execution can take E-LEFT-DEREF-STEP or E-DEREF-STEP as applicable if _e_₁ is not a value. If _e_₁ ≼: ⇑τ is a value, then, from the canonical forms lemma, _e_₁ = ℓ, ℓ ∊ dom(Σ). Now, since this is an lvalue, we are done in the case of left execution. In the case of right execution, we can take step E-DEREF since the heap is well typed (Γ; Σ ⊢ H + S).
Case T-LET-M: Only right execution is applicable. We have: _e_ = (let^ψ _x_ = _e_₁ in _e_₂), τ ≼: τ₁, Γ; Σ; _e_₁ ⊢_gen τ ⋖ σ, and ⊢_loc _x_ : σ, andΓ, _x_ ↦ σ; Σ ⊢ _e_₂ : τ₂. If _e_₁ is not a value, we can take E-LET-STEP. Otherwise, we can take E-STEP-M.
Case T-LET-P: Only right execution is applicable. We have: _e_ = (let^ψ _x_ = _e_₁ in _e_₂), τ ≼: τ₁, Γ; Σ; _e_₁ ⊢_gen τ ⋖ σ, and ⊢_term _x_ : σ, andΓ, _x_ ↦ σ; Σ ⊢ _e_₂ : τ₂. If _e_₁ is not a value, we can take E-LET-STEP. Otherwise, can take E-LET-P.
Case T-TQEXPR and Case T-LET-M-TQ, T-LET-P-TQ are similar.

4.3.7.6 LEMMA: Weakening

We will write Γ; Σ ⊢ _e_ : τ ⋖ σ as a shorthand for Γ; Σ ⊢ _e_ : τ, and Γ; Σ; _e_ ⊢_gen τ ⋖ σ.

If Γ; Σ ⊢ _e_ : τ then,
1. If Γ^′ ⊇ Γ then Γ^′; Σ ⊢ _e_ : τ.
2. If Σ^′ ⊇ Σ then Γ; Σ^′ ⊢ _e_ : τ.
If Γ; Σ ⊢ _e_ : τ ⋖ σ, σ = ∀α^*.τ
1. If Γ^′ ⊇ Γ and ?ftv?(Γ^′) ∩ ?ftv?(α^*) = ∅ then Γ^′; Σ ⊢ _e_ : τ ⋖ σ.
2. If Σ^′ ⊇ Σ and ?ftv?(Σ^′) ∩ ?ftv?(α^*) = ∅ then Γ; Σ^′ ⊢ _e_ : τ ⋖ σ.

Proof: Straightforward induction on the typing derivation.

4.3.7.7 LEMMA: Value Substitution

If Γ, _x_ : σ; Σ ⊢ _e_ : τ, ?Immut??(?σ?)? and Γ; Σ ⊢ _v_ : τ_v, and Γ; Σ; _e_ ⊢_gen τ_v ⋖ σ then Γ; Σ ⊢ _e_[_v_/_x_] : τ

Proof: By induction on the typing derivation of Γ, _x_ : σ; Σ ⊢ _e_ : τ. We proceed by case analysis on the final step of the derivation.

Case T-ID: We have _e_ = _y_ where _y_ ∊ Γ, _x_, σ.

There are two sub cases to consider. If _x_ = _y_, then, _y_[_v_/_x_] = _v_, and the result type τ is an instantiation of the type scheme σ. One of the assumptions of the lemma states that Γ; Σ ⊢ _v_ : τ_v ⋖ σ. That is, τ ⊑ σ, and we can infer any more-specific type (and in particular the type being instantiated at the T-ID rule) instead for this substitution of the expression _v_. Therefore, we have Γ; Σ ⊢ _e_[_v_/_x_] : τ.

If _x_ ≠ _y_, then _y_[_v_/_x_] = _y_, and the result is immediate.
Case T-LAMBDA: We have _e_ = λ_y_._e_^′, and τ = τ₁ → τ₂, and Γ, _x_ : σ, _y_ : τ₁; Σ ⊢ _e_^′ : τ₂.

We can assume that _x_ ≠ _y_. Since it is clear that the type τ₁ of _y_ can either use variables already in Γ or fresh type variables, we know that ?ftv?(Γ, _y_ : τ₁) ∩ ?ftv?(σ) = ∅. Thus, by weakening lemma, we have: Γ, _y_ : τ₁; Σ ⊢ _v_ : τ_v ⋖ σ , and, by induction hypothesis, Γ, _y_ : τ₁; Σ ⊢ _e_^′[_v_/_x_] : τ₂. Finally, by the T-LAMBDA rule, we have: Γ; Σ ⊢ λ_x__y.(_e_^′[_v_/_x_]) : τ₁ → τ₂, and thus Γ; Σ ⊢ λ_x__y._e_^′[_v_/_x_] : τ₁ → τ₂, which is the desired result.
T-SET case is similar, except that the substitution cannot happen on the LHS of an assignment, since we do not perform substitution of mutable values.
Other cases are similar.

4.3.7.8 LEMMA: Location Substitution

If Γ, _x_ : τ₀; Σ ⊢ _e_ : τ, and for some Σ^′ ⊇ Σ, Σ(l) = τ₀ : , then Γ; Σ^′ ⊢ _e_[l/_x_] : τ.

Proof: By induction on the typing derivation of Γ, _x_ : τ; Σ ⊢ _e_ : τ, similar to lemma 4.3.7.7.

4.3.7.9 LEMMA: Stack and Heap Assignment

If Γ; Σ ⊢ H, ℓ ↦ _v_ + S, and Σ(ℓ) ≼: τ, and Γ; Σ ⊢ _v_^′ : τ, then, Γ; Σ ⊢ H, ℓ ↦ _v_^′ + S.
Similarly, if Γ; Σ ⊢ H + S, l ↦ _v_ and Σ(l) ≼: τ, and Γ; Σ ⊢ _v_^′ : τ, then, Γ; Σ ⊢ H + S, l ↦ _v_^′.

Proof: Immediate from the definition of stack and heap typing.

4.3.7.10 LEMMA: Preservation

If Γ; Σ ⊢ _e_ : τ and Γ; Σ ⊢ H + S then,

If S; H; _e_ ⇛ S^′; H^′; _e_^′, then, there exists a Σ^′ ⊇ Σ such that Γ; Σ^′ ⊢ _e_^′ : τ and Γ; Σ^′ ⊢ H^′ + S^′.
If S; H; _e_ ⇒ S^′; H^′; _e_^′, there exists a Σ^′ ⊇ Σ such that Γ; Σ^′ ⊢ _e_^′ ≼: τ^′, Γ; Σ^′ ⊢ H^′ + S^′ and ▽(τ) = ▽(τ^′).

Proof: By induction on the derivation of Γ; Σ ⊢ _e_ : τ. We proceed by the case analysis of the final step.

Case T-ID, T-TRUE, T-FALSE, T-HLOC, T-LAMBDA cannot happen.
Case T-SLOC: Only right execution is applicable. We have: _e_ = l and Σ(l) : τ. The only applicable step is E-RVAL, and we have _e_^′ = S(l). From the definition of stack typing, we have: S(l) ≼: Σ(l) and thus _e_^′ ≼: τ which implies ▽(τ) = ▽(τ^′).
Case T-APP: _e_ = _e_₁ _e_₂, and Γ; Σ ⊢ _e_₁ ≼: τ₂ → τ₀, and Γ; Σ ⊢ _e_₂ ≼: τ₂, and τ₀ ≼: τ, and _e_ : τ where τ₂ = ▽(τ^′₂)τ₀ = △(τ^′₀) and .

This cannot happen for left execution. For right execution, we proceed by further case analysis of the applicable execution rules for S; H; _e_ ⇒ S^′; H^′; _e_^′.
1. Case E-APP-STEP-FN: We have: S; H; _e_₁ ⇒ S^′; H^′; _e_^′₁ and _e_^′ = _e_^′₁ _e_₂. By induction hypothesis, we have: Γ; Σ^′ ⊢ _e_^′₁ ≼: τ₂ → τ₀ for some Σ^′ ⊇ Σ. One of the assumptions of the T-APP rule states that Γ; Σ ⊢ _e_₂ ≼: τ₂, and by weakening lemma, we have, Γ; Σ^′ ⊢ _e_₂ ≼: τ₂. Finally, by the T-APP rule, we conclude that (_e_^′₁ _e_₂) : τ.
2. Case E-APP-STEP-ARG: Similar to the previous sub-case.
3. Case E-APP: We have: _e_₁ = λ_x_._e_₀ and _e_₂ = _v_ and and _e_^′ = _e_₀[l/_x_] and S, l ↦ _v_; H; _e_₁ ⇒ S^′; H^′; _e_^′₁.
  
  By the inversion lemma for λ_x_._e_₀ we have Γ, Σ ⊢ _e_₀ : τ^′₀.
  
  Further from location substitution lemma, we have Γ; Σ^′ ⊢ _e_₀[l/_x_] : τ^′₀ where Σ^′ ⊇ Σ and Σ(l) : τ^′₂.
  
  Thus, we have τ₀ ≼: τ^′₀ and τ₀ ≼: τ. Therefore, it is clear that ▽(τ^′₀) = ▽(τ).
Case T-SET: _e_ = _e_₁ := _e_₂, and Γ; Σ ⊢ _e_₁ ≼: Ψτ, and Γ; Σ ⊢ _e_₂ ≼: τ ⊢_lval _e_₁

If the step taken is E-SET-STEP-LHS or E-SET-STEP-RHS, the result follows from the induction hypothesis and T-SET rule (as in the case of T-APP). If the step taken is E-SET-STACK or E-SET-HEAP, the result follows from the stack and heap assignment lemma.
Case T-DEREF: We have: _e_ = _e_^′^ and Γ; Σ ⊢ _e_^′ ≼: ⇑τ. If the step taken is E-LEFT-DEREF-STEP or E-LEFT-DEREF, the result follows from induction hypothesis and T-DEREF rule. If the step taken is E-DEREF (right execution only) _e_^′ is a value, and from canonical forms lemma, we know that _e_^′ = ℓ and ℓ ∊ dom(Σ) and the result follows from the fact that Γ; Σ ⊢ H + S.
Case T-LET-P: Right execution only. We have: _e_ = (let^∀ _x_ = _e_₁ in _e_₂) and Γ; Σ ⊢ _e_₁ ≼: τ₁ and τ ≼: τ₁ and Γ; Σ; _e_₁ ⊢_gen τ ⋖ σ and Γ, _x_ ↦ σ; Σ ⊢ _e_₂ : τ₂. There are two sub-cases to consider:
1. If we take step E-LET-STEP, S; H; _e_₁ ⇒ S^′; H^′; _e_^′₁ and _e_^′ = (let^∀ _x_ = _e_^′₁ in _e_₂). If _e_ = _v_ It is clear that ?Value??(?_e_₁?)? implies ?Value??(?_e_^′₁?)?. Now, the result follows from the induction hypothesis and the E-LET-P rule.
2. If we take the step E-LET-P, _e_ = (let^∀ _x_ = _v_ in _e_₂) Since _x_ : σ has a polymorphic type, (that is, σ = ∀α^*.τ) we know that ?Immut??(?τ?)?. Also, from canonical forms lemma, all values have an immutable type. Therefore, τ = τ₁. Now, the result follows from value substitution lemma.
Case T-LET-M: Similar to T-LET-P, except that we should always use the GEN-EXPANSIVE rule during generalization, and use the location substitution lemma instead of the value substitution lemma
Cases T-IF, T-DUP, T-TQEXPR, and T-LET-M-TQ T-LET-P-TQ are similar.

4.3.7.11 DEFINITION: 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_^′.

4.3.7.12 THEOREM: Type Soundness

If ∅; Σ ⊢ _e_ : τ and Γ; Σ ⊢ H + S and S; H; _e_ ⇒* S^′; H^′; _e_^′ then S^′; H^′; _e_^′ is not stuck. That is, execution of a well typed expression cannot lead to a stuck state. Here, ⇒* represents the reflexive-transitive-closure of ⇒.

Proof: By straightforward induction on the length of ⇒*. If _e_ = _v_, proof is immediate. Otherwise, from Lemma 4.3.7.5 (Progress), we know that we can take at least one step forward. Further, from Lemma 4.3.7.10 (Preservation), we know that a (left/right) execution of a well typed expression in with respect to a well typed stack and heap will always result in another well typed expression, stack and heap. Proof now follows from induction hypothesis.

4.3.8 Equational Inference Algorithm

Syntax

Types	τ ::=	...
Constrained Type		`\|` τ \ C
Constraint Sets	C ::=	∅ `\|` {(τ = τ `\|` τ ≅ τ `\|` τ ≼: τ)^*}
Substitutions	θ ::=	∅ `\|` [α ↣ τ] `\|` θ ∘ θ

We will denote applications of a list of substitutions of these substitutions as θ〈X〉, while an individual substitution is written using the standard notation X[Z/Y].

The inference judgment Γ; Σ ⊢_eq _e_ : τ | *C* should be understood as: given the stack (binding) context Γ and heap (store) context Σ, we can infer the type τ for the expression _e_ under the set of constraints *C*. In the interest brevity, we will not track the freshness of type variables. We just write ⊢_new α^* to mean that the sequence of type variables α^* are new type variables.

TE-UNIT

Γ; Σ ⊢_eq () : unit | ∅

TE-TRUE

Γ; Σ ⊢_eq true : bool | ∅

TE-FALSE

Γ; Σ ⊢_eq false : bool | ∅

TE-ID

Γ(_x_) = ∀α^*.τ ⊢_new β^*

Γ; Σ ⊢_eq _x_ : τ[β^*/α^*] | ∅

TE-HLOC

Σ(ℓ) = τ

Γ; Σ ⊢_eq ℓ : ⇑τ | ∅

TE-SLOC

Σ(l) = τ

Γ; Σ ⊢_eq l : τ | ∅

TE-LAMBDA

Γ, _x_ ↦ α; Σ ⊢_eq _e_ : τ | *C*

Γ; Σ ⊢_eq λ_x_._e_ : ⌊α⌋ → ⌈τ⌉ | *C*

TE-APP

Γ; Σ ⊢_eq _e_₁ : τ₁ | *C*₁ Γ; Σ ⊢_eq _e_₂ : τ₂ | *C*₂ ⊢_new α

Γ; Σ ⊢_eq _e_₁ _e_₂ : α | *C*₁ ∪ *C*₂ ∪ {τ₁ ≼: ⌊β⌋ → ⌈γ⌉, τ₂ ≼: ⌊β⌋, ⌈γ⌉ ≼: α}

TE-IF

Γ; Σ ⊢_eq _e_₁ : τ₁ | *C*₁ Γ; Σ ⊢_eq _e_₂ : τ₂ | *C*₂ Γ; Σ ⊢_eq _e_₃ : τ₃ | *C*₃ ⊢_new α

Γ; Σ ⊢_eq if _e_₁ then _e_₂ else _e_₃ : α | *C*₁ ∪ *C*₂ ∪ *C*₃ ∪ {τ₁ ≼: bool, τ₂ ≼: β, τ₃ ≼: β, α ≼: β}

TE-TQEXPR

Γ; Σ ⊢_eq _e_ : τ^′ | *C*

Γ; Σ ⊢_eq (_e_ : τ) : τ | *C* ∪ {τ^′ = τ}

TE-SET

Γ; Σ ⊢_eq _e_₁ : τ₁ | *C*₁ Γ; Σ ⊢_eq _e_₂ : τ₂ | *C*₂ ⊢_lval _e_₁ ⊢_new α

Γ; Σ ⊢_eq _e_₁ := _e_₂ : unit | *C*₁ ∪ *C*₂ ∪ {τ₁ = Ψα, τ₁ ≼: ⌊τ₂⌋}

TE-DUP

Γ; Σ ⊢_eq _e_ : τ | *C* ⊢_new α

Γ; Σ ⊢_eq dup(_e_) : ⇑α | *C* ∪ {α ≼: ⌊τ⌋}

TE-DEREF

Γ; Σ ⊢_eq _e_ : τ | *C* ⊢_new α

Γ; Σ ⊢_eq _e_^ : α | *C* ∪ {τ ≼: ⇑α}

TE-LET-M [TQ]

Γ; Σ ⊢_eq _e_₁ : τ₁ | *C*₁ *C*^′₁ = *C*₁ ∪ {τ ≼: ⌊τ₁⌋} θ ⊧_unf *C*^′₁ Γ; Σ; _e_₁ ⊢_gen θ〈τ〉 ⋖ σ

⊢_loc _x_ : σ θ〈Γ〉, _x_ ↦ σ; θ〈Σ〉 ⊢_eq _e_₂ : τ₂ | *C*₂

Γ; Σ ⊢_eq let^ψ _x_ = _e_₁ in _e_₂ : τ₂ | *C*₂ ∪ {∀[α ↣ τ] ∊ θ, α = τ}

TE-LET-P [TQ]

Γ; Σ ⊢_eq _e_₁ : τ₁ | *C*₁ *C*^′₁ = *C*₁ ∪ {τ ≼: ⌊τ₁⌋} θ ⊧_unf *C*^′₁ Γ; Σ; _e_₁ ⊢_gen θ〈τ〉 ⋖ σ

⊢_term _x_ : σ θ〈Γ〉, _x_ ↦ σ; θ〈Σ〉 ⊢_eq _e_₂ : τ₂ | *C*₂

Γ; Σ ⊢_eq let^∀ _x_[:τ] = _e_₁ in _e_₂ : τ₂ | *C*₂ ∪ {∀[α ↣ τ] ∊ θ, α = τ}

Equational Inference Rules

Equational Inference rules are shown in Table 4.6. We will hereinafter write LET-α to range over LET-M and LET-P. We propagate solved constraints at a let-boundary (TE-LET-α and TE-LET-α-TQ rules) as equality constraints rather then substitutions. This is done just to present the rules in a simple form. A real implementation must propagate the substitutions so that closure computation does not increase exponentially. In this equational presentation of inference, types can be fixed by equality constraints, or compatibility requirements expressed as copy coercion constraints. The coercion constraints are used as hints and we obtain the substituted type by subsumption. The solution to these constraints closely corresponds to the rule defined in BitC. In this section, we do not present the fact that mutability of local variables are determined by examining the expression in which they are used. The actual implementation in BitC uses an eager unification algorithm, and is explained in the next section.

4.3.9 Unification

Unification Rules are shown in Table 4.7. We write θ ⊧ *C* to mean that the substitution θ satisfies the set of constraints *C*. A constraint set *C* is said to be the normalized form of *C* if it is written as a set of atomic constraints by using the copy coercion rules defined in Table 4.2 (note that this conversion is total). Further this set is closed, such that all transitive relationships are explicitly added. (see Definition 4.3.9.1). The unification judgment ⊧_UNF *C* says that the constraint set *C* when written equivalent canonical form as *C*^′ is consistent and acyclic. The statement θ ⊧_unf *C* is understood as: The substitution θ obtained as a result of unification and constraint solving satisfies the set of constraints *C*.

E-UNIFY

?Close?(*C*) = *C* ⊧_consistent *C* ⊧_acyclic *C*

⊧_UNF *C*

E-UNIFY-SOLVE

⊧_UNF *C* θ ⊧_sol *C*

θ ⊧_unf *C*

Equational Unification Rules

4.3.9.1 DEFINITION: Constraint Set Closure

For each τ₁ → τ₂ = τ^′₁ → τ^′₂ ∊ *C* add τ₁ = τ^′₁ and τ₂ = τ^′₂.
For each τ₁ → τ₂ ≼: τ^′₁ → τ^′₂ ∊ *C* add τ₁ = τ^′₁ and τ₂ = τ^′₂.
For each ⇑τ = ⇑τ^′ ∊ *C* add τ = τ^′.
For each ⇑τ ≼: ⇑τ^′ ∊ *C* add τ = τ^′.
For each Ψτ = Ψτ^′ ∊ *C* add τ = τ^′.
For each Ψτ ≼: Ψτ^′ ∊ *C* add τ ≼: τ^′.
For each τ₁ = τ₂ ∊ *C* and τ₂ = τ₃ ∊ *C* add τ₁ = τ₃.
For each τ₁ ≼: τ₂ ∊ *C* and τ₂ ≼: τ₃ ∊ *C* add τ₁ ≼: τ₃.
For each τ₁ = τ₂ ∊ *C* and τ₂ ≼: τ₃ ∊ *C* add τ₁ ≼: τ₃.
For each τ₁ ≼: τ₂ ∊ *C* and τ₂ = τ₃ ∊ *C* add τ₁ ≼: τ₃.

Continue till no more constraints can be added.

4.3.9.2 Solving the Constraints

SOL-EQ

α = τ ∊ *C* θ = [α ↣ τ] θ^′ ⊧_Sol θ〈*C* ∖ {α = τ}〉

θ ∘ θ^′ ⊧_Sol *C*

SOL-SUB

α = τ^′ ∉ *C* *C*_a = {∀α ≼: τ₁ ∊ *C*, ∀τ₂ ≼: α ∊ *C*} τ = some type such that θ = [α ↣ τ] θ ⊧ *C*_a

θ^′ ⊧_Sol θ〈*C* ∖ {α ≼: τ}〉

θ ∘ θ^′ ⊧_Sol *C*

Solving Equational Constraints

Judgments to solve equational constraints are shown in Table 4.8.

4.3.10 Soundness of Equational Inference

4.3.10.1 THEOREM: Soundness of Constraint Closure

If θ ⊧ *C* then θ ⊧ Close(*C*).

Proof: Immediate from the definition of closure computation and copy coercion rules.

4.3.10.2 THEOREM: Correctness of Constraint Solver

θ ⊧_Sol *C* iff θ ⊧ *C*.

Proof: Evident from the definition of the constraint solver.

4.3.10.3 THEOREM: Correctness of Unification

Unification produces a valid substitution that satisfies all the constraints in a constraint set. That is, if θ ⊧_unf *C* then θ ⊧ *C*.

Proof: Evident the definition of unification, and Theorem 4.3.10.2.

4.3.10.4 THEOREM: Decidability of Unification

θ ⊧_unf *C* is decidable.

Proof: Follows from following facts:

The constraint set *C* is finite. Closure computation follows set-union semantics and will eventually terminate after all possible constraints are added (as evident from the cope coercion relationships).
Consistency check is bounded by the cardinality of the constraint set and is thus decidable.
There are no forms that introduce cyclic types in this system. Even otherwise, cycle check is also bounded by the cardinality of the constraint set.
The constraint solver builds a solution tree by always invoking itself on smaller sets. Therefore, there can be no infinite derivations.

4.3.10.5 LEMMA: Substitution on Declarative Derivation

If Γ; Σ ⊢ _e_ : τ then θ〈Γ〉; θ〈Σ〉 ⊢ _e_ : θ〈τ〉.

Proof: Straightforward induction on the derivation of Γ; Σ ⊢ _e_ : τ, except for the fact that we should use appropriate α-renaming on generalized variables ∀σ ∊ Γ, so that generalized variables do not get substituted.

4.3.10.6 LEMMA: Weakening of Substitutions

If θ ⊧ *C*₁ ∪ *C*₂ then θ ⊧ *C*₁ and θ ⊧ *C*₂.
If θ ⊧_Sol *C*₁ ∪ *C*₂ then θ ⊧ *C*₁ and θ ⊧ *C*₂.

Proof: Part (1) is immediate. Part(2) follows from Theorem 4.3.10.2.

4.3.10.7 LEMMA: Composition of Solutions and Substitutions

If θ₁ ⊧_unf *C*₁ and *C*₂ ⊆ *C*₁ then ∃ θ₂ such that θ₁ = θ₂ ∘ θ₀ and θ₂ ⊧_unf *C*₂.

4.3.10.8 THEOREM: Soundness of Equational Inference

If Γ; Σ ⊢_eq _e_ : τ | *C* and θ ⊧_unf *C* then θ〈Γ〉; θ〈Σ〉 ⊢ _e_ : θ〈τ〉.

Proof: By induction on the equational inference derivation, proceeding by case analysis on the final step of derivation (we vacuously assume α-reduction):

Cases TE-UNIT, TE-TRUE, TE-FALSE, TE-ID, TE-HLOC, TE-SLOC are trivial.
Case TE-LAMBDA: From induction hypothesis, we have: θ〈Γ, _x_ ↦ α〉; θ〈Σ〉 ⊢ _e_^′ : θ〈τ〉. This can be re-written as: θ〈Γ〉, _x_ ↦ θ〈α〉; θ〈Σ〉 ⊢ _e_^′ : θ〈τ〉. Now, from the T-LAMBDA rule, we can conclude that θ〈Γ〉; θ〈Σ〉 ⊢ λ_x_._e_^′ : θ〈α〉 → θ〈τ〉.
Case TE-APP: By induction hypothesis, and Lemma 4.3.10.5 and Lemma 4.3.10.7 we have: θ〈Γ〉; θ〈Σ〉 ⊢ _e_₁ ≼: θ〈τ₁〉θ〈Γ〉; θ〈Σ〉 ⊢ _e_₂ ≼: θ〈τ₂〉. By inspecting the constraints that get added at the T-APP step we can conclude that the result of substitution must imply θ〈τ₁〉 ≼: ▽(θ〈τ₂〉) → △(θ〈α〉). We also have the axiom △(θ〈α〉) ≼: θ〈α〉. Now, from T-APP rule, we can obtain θ〈Γ〉; θ〈Σ〉 ⊢ _e_₁ _e_₂ : θ〈α〉
Cases TE-IF, TE-SET, TE-DUP, TE-DEREF and TE-SET are similar.
Case TE-LET-α: By induction hypothesis, (similar to TE-APP case) we have: θ_u〈Γ〉; θ_u〈Σ〉 ⊢ _e_₁ : θ_u〈τ₁〉 and θ_u ⊧_unf *C*^′₁. Let τ be a type such that τ ≼: ⌊θ〈τ₁〉⌋. This can be re-written as: θ〈τ₁〉 ≼: τ^′ and τ ≼: τ^′ to match the requirements of T-LET-α rule. Also, since both T-LET-α and TE-LET-α use the same generalization rules, we can obtain: θ_u〈Γ〉; θ_u〈Σ〉; _e_₁ ⊢_gen τ ⋖ θ〈σ〉. By Lemma 4.3.10.7 θ〈Γ〉; θ〈Σ〉 ⊢ _e_₁ : θ〈τ₁〉 and by suitable variable renaming we can obtainθ_u〈Γ〉; θ_u〈Σ〉; _e_₁ ⊢_gen τ ⋖ θ〈σ〉. By induction hypothesis, we also have: θ〈Γ〉, _x_ ↦ θ〈σ〉; θ〈Σ〉 ⊢ _e_₂ : θ〈τ₂〉. Therefore, from T-LET-α rule, we can obtain θ〈Γ〉; θ〈Σ〉 ⊢ let _x_ = _e_₁ in _e_₂ : θ〈τ₂〉.
Cases TE-TQEXPR and TE-LET-α-TQ are similar.

4.3.11 Inference with Eager Unification

Syntax

Types	τ ::=	...
Maybe Type		`\|` τ↓τ^′

While performing eager unification, we cannot always infer a mutable type and later apply subsumption to obtain a less mutable type in favor of polymorphism. This is because, we must differentiate between types whose mutability is fixed (equality constraint due to the TE-SET rule) or, we have inferred a mutable type that is subject to change (copy coercion constraint). In order to achieve this, we maintain compatibility constraints on types themselves. We write τ↓τ^′ as a shorthand for the constrained type τ \ {τ ≅ τ^′}. We can think of the type τ↓τ^′ as a ``maybe type'' τ which must be copy compatible but not necessarily equal to the type τ^′. The type τ^′ is used as a hint to default the mutability of τ, unless it gets automatically fixed as a result of unification. In out language we only have maybe-mutability constraints, but we will still continue to use the constrained type notation τ \ *C* in some cases while expressing generic mathematical properties over constrained types.

TI-UNIT

Γ; Σ; Π ⊢_i () : unit ∥ ∅; Π

TI-HLOC

Σ(ℓ) = τ

Γ; Σ; Π ⊢_i ℓ : ⇑τ ∥ ∅; Π

TI-SLOC

Σ(l) = τ

Γ; Σ; Π ⊢_i l : τ ∥ ∅; Π

TI-ID

Γ(_x_) = ∀α^*.τ

Γ; Σ; Π ⊢_i _x_ : τ[β^*/α^*] ∥ ∅; Π_β^*

TI-TRUE

Γ; Σ; Π ⊢_i true : bool ∥ ∅; Π

TI-FALSE

Γ; Σ; Π ⊢_i false : bool ∥ ∅; Π

TI-LAMBDA

Γ, _x_ ↦ α; Σ; Π_α ⊢_i _e_ : τ ∥ θ; Π^′

Γ; Σ; Π ⊢_i λ_x_._e_ : ⌊θ〈α〉⌋ → ⌈τ⌉ ∥ θ; Π^′

TI-TQEXPR

Γ; Σ; Π ⊢_i _e_ : τ^′ ∥ θ^′; Π^′ θ ⊢_unf τ^′ = θ^′〈τ〉

Γ; Σ; Π ⊢_i (_e_ : τ) : θ〈τ^′〉 ∥ θ ∘ θ^′; Π^′

TI-APP

Γ; Σ; Π_αβγδε ⊢_i _e_₁ : τ₁ ∥ θ₁; Π^′ θ₁〈Γ〉; θ₁〈Σ〉; Π^′ ⊢_i _e_₂ : τ₂ ∥ θ₂; Π^″

θ^′₁ ⊢_unf θ₂〈τ₁〉 = β↓(⌊δ⌋ → ⌈α⌉) θ = θ₁ ∘ θ₂ ∘ θ^′₁ θ^* = ?ftv?(θ〈α〉) ∖ ?ftv?(θ〈δ〉) τ = ▽(θ〈α〉)[⌊θ⌋^*/θ^*]

θ^′₂ ⊢_unf τ₂ = γ↓⌊θ〈δ〉⌋ τ^′ = ε↓θ^′₂〈τ〉

Γ; Σ; Π ⊢_i _e_₁ _e_₂ : τ^′ ∥ θ₁ ∘ θ₂ ∘ θ^′₁ ∘ θ^′₂; Π^″

TI-IF

Γ; Σ; Π_αβγδε ⊢_i _e_₁ : τ₁ ∥ θ₁; Π₁ θ₁〈Γ〉; θ₁〈Σ〉; Π₁ ⊢_i _e_₂ : τ₂ ∥ θ₂; Π₂

θ₁ ∘ θ₂〈Γ〉; θ₁ ∘ θ₂〈Σ〉; Π₂ ⊢_i _e_₃ : τ₃ ∥ θ₃; Π₃ θ = θ₁ ∘ θ₂ ∘ θ₃ θ^′₂ ⊢_unf θ〈τ₂〉 = α↓β

θ^′₃ ⊢_unf θ ∘ θ^′₂〈τ₃〉 = γ↓θ^′₂〈β〉 θ^′₁ ⊢_unf θ ∘ θ^′₂ ∘ θ^′₃〈τ₁〉 = δ↓bool

θ^′ = θ ∘ θ^′₁ ∘ θ^′₂ ∘ θ^′₃ τ₀ = ε↓join(θ^′〈τ₂〉, θ^′〈τ₃〉)

Γ; Σ; Π ⊢_i if _e_₁ then _e_₂ else _e_₃ : τ₀ ∥ θ^′; Π₃

TI-SET

Γ; Σ; Π_αβ ⊢_i _e_₁ : τ₁ ∥ θ₁; Π^′ θ₁〈Γ〉; θ₁〈Σ〉; Π^′ ⊢_i _e_₂ : τ₂ ∥ θ₂; Π^″

θ^′₁ ⊢_unf θ₂〈τ₁〉 = Ψα θ^′₂ ⊢_unf θ^′₁〈τ₂〉 = β↓θ^′₁ ∘ θ₂〈τ₁〉

Γ; Σ; Π ⊢_i _e_₁ := _e_₂ : unit ∥ θ₁ ∘ θ₂ ∘ θ^′₁ ∘ θ^′₂; Π^″

TI-DUP

Γ; Σ; Π_α ⊢_i _e_ : τ ∥ θ; Π^′ τ^′ = α↓τ

Γ; Σ; Π ⊢_i dup(_e_) : ⇑τ^′ ∥ θ; Π^′

TI-DEREF

Γ; Σ; Π_αβ ⊢_i _e_ : τ ∥ θ; Π^′ θ^′ ⊢_unf τ = β↓⇑α

Γ; Σ ⊢_i _e_^ : θ ∘ θ^′〈α〉 ∥ θ ∘ θ^′; Π^′

TI-LET-M [TQ]

Γ; Σ; Π_α ⊢_i _e_₁ : τ₁ ∥ θ₁; Π₁ θ ⊢_unf θ₁〈τ〉 = α↓τ₁ θ^′; _x_; _e_₂ ⊢_solve θ ∘ θ₁〈τ〉 :≫ τ^′ ⊢_loc _x_ : σ

θ₁ ∘ θ ∘ θ^′〈Γ〉; θ₁ ∘ θ ∘ θ^′〈Σ〉; _e_₁ ⊢_gen τ ⋖ σ θ₁ ∘ θ ∘ θ^′〈Γ〉, _x_ ↦ σ; θ₁ ∘ θ ∘ θ^′〈Σ〉; Π₁ ⊢_i _e_₂ : τ₂ ∥ θ₂; Π₂

Γ; Σ; Π ⊢_i let^ψ _x_[:τ] = _e_₁ in _e_₂ : τ₂ ∥ θ ∘ θ^′ ∘ θ₁ ∘ θ₂; Π₂

TI-LET-P [TQ]

Γ; Σ; Π_α ⊢_i _e_₁ : τ₁ ∥ θ₁; Π₁ θ ⊢_unf θ₁〈τ〉 = α↓τ₁ θ^′; _x_; _e_₂ ⊢_solve θ ∘ θ₁〈τ〉 :≫ τ^′ ⊢_term _x_ : σ

Γ; Σ; Π ⊢_i let^∀ _x_[:τ] = _e_₁ in _e_₂ : τ₂ ∥ θ ∘ θ^′ ∘ θ₁ ∘ θ₂; Π₂

Type Inference Rules

The inference judgment Γ; Σ; Π ⊢_i _e_ : τ ∥ θ; Π^′ should be understood as: given the stack (binding) context Γ and heap (store) context Σ, we can infer the type τ for the expression _e_. θ is list of substitutions obtained as a result of unifications performed in the process of inference, which must be propagate to further derivations. We thread a tape of type variables Π through the derivations (as in [57]) so that fresh type variables can be introduced reliably. Π is a tape that supplies fresh type variables. Π^′ is the tape rolled past the current derivation. Also, we write Π_α^* to denote denotes the tape that is rolled past the type variables α^*. Hindley Milner style inference rules are shown in Table 4.9.

The TI-LAMBDA rule uses the meta-constructors defined above to infer a normalized type for functions. The TI-APP rule infers copy compatible types by introducing maybe types at three positions — the function type itself (by unifying θ₂〈τ₁〉 and β↓(⌊δ⌋ → ⌈α⌉)), the argument type (by unifying τ₂ with γ↓⌊θ〈δ〉⌋) and the return type (through ε↓θ^′₂〈τ〉). Computing the type τ shows how the the hint for the result of an application is calculated. We start with an immutable version of the return type ▽(θ〈α〉). θ^* is the set of type variables that appear in the return type of the function but not in its argument type. We constrain θ^* to be immutable by shallow substitution with ⌊θ⌋^*. This ensures that mutability not induced by the argument does not affect the return type. Later unification with τ₂ ensures that the mutability induced by the actual argument is preserved in the hint. Similarly, the TI-IF rule infers copy compatible types for the two branches and the result. It calculates the most immutable type as the hint for the result type by computing the join [3051] of θ^′〈τ₂〉 and θ^′〈τ₃〉 (note that two copy compatible types always have a join). Other rules are similar.

4.3.12 Unification

The unification judgment θ ⊢_unf τ₁ = τ₂ is understood as τ₁ unifies with (can be transformed to structurally equal) τ₂ under the substitution θ. Eager unification rules can be found in Table 4.10. Definitions for some auxiliary functions used by the unifier are given in Table 4.11.

UNIFY

θ ⊢_u ℜ(τ₁) = ℜ(τ₂)

θ ⊢_unf τ₁ = τ₂

U-REFL

∅ ⊢_u τ = τ

U-COMMUT

θ ⊢_u τ = τ^′

θ ⊢_u τ^′ = τ

U-TVAR

α ≠ τ

[α ↣ τ] ⊢_u α = τ

U-REF

θ ⊢_u τ₁ = τ₂

θ ⊢_u ⇑τ₁ = ⇑τ₂

U-MUT

θ ⊢_u τ₁ = τ₂

θ ⊢_u Ψτ₁ = Ψτ₂

U-FN

θ ⊢_u τ₁ = τ^′₁ θ^′ ⊢_u θ〈τ₂〉 = θ〈τ^′₂〉 ⊧_acyclic θ ∘ θ^′

θ ∘ θ^′ ⊢_u τ₁ → τ₂ = τ^′₁ → τ^′₂

U-CT1

τ₂ ≠ τ₃↓τ^′₃ τ₂ ≠ α θ ⊢_u ℑ(τ^′₁) = ▽(τ₂) θ^′ ⊢_u θ〈τ₁〉 = θ〈τ₂〉 ⊧_acyclic θ ∘ θ^′

θ ∘ θ^′ ⊢_u τ₁↓τ^′₁ = τ₂

U-CT2

θ ⊢_u ℑ(τ^′₁) = ℑ(τ^′₂) θ^′ ⊢_u θ〈τ₁〉 = θ〈τ₂〉 ⊧_acyclic θ ∘ θ^′

θ ∘ θ^′ ⊢_u τ₁↓τ^′₁ = τ₂↓τ^′₂

U-CEIL

θ ⊢_u τ₁ = τ₂

θ ⊢_u ⌈τ₁⌉ = ⌈τ₂⌉

U-FLOOR

θ ⊢_u τ₁ = τ₂

θ ⊢_u ⌊τ₁⌋ = ⌊τ₂⌋

Unification Rules

τ ≠ τ₁↓τ₂

ℑ(τ) = ▽(τ)

τ = τ₁↓τ₂ ℑ(τ₂) = τ^′₂

ℑ(τ) = τ^′₂

ℜ(unit) = ⌊unit⌋

ℜ(bool) = ⌊bool⌋

ℜ(α) = α

ℜ(τ) = τ^′

ℜ(Ψτ) = ⌈Ψτ^′⌉

ℜ(τ) = τ^′

ℜ(⇑τ) = ⌊⇑τ^′⌋

ℜ(τ₁) = τ^′₁ ℜ(τ₂) = τ^′₂

ℜ(τ₁ → τ₂) = ⌊τ^′₁ → τ^′₂⌋

ℜ(τ₁) = τ^′₁ ℜ(τ₂) = τ^′₂

ℜ(τ₁↓τ₂) = τ^′₁↓τ^′₂

ℜ(▽(τ)) = τ^′ τ^′ = ⌊τ^″⌋

ℜ(⌊τ⌋) = τ^′

ℜ(▽(τ)) = τ^′ τ^′ ≠ ⌊τ^″⌋

ℜ(⌊τ⌋) = ⌊τ^′⌋

ℜ(△(τ)) = τ^′

ℜ(⌈τ⌉) = τ^′

Auxiliary Functions for Unification

The unification judgment θ ⊢_unf τ₁ = τ₂ is understood as τ₁ unifies with τ₂ under the substitution θ. The interesting cases are U-CT1 and U-CT2. U-CT1 shown the unification of a maybe type τ₁↓τ^′₁ with an unconstrained type τ₂. In this case, an immutable version of the constraint is extracted by the ℑ operator, and is unified with an immutable version of τ₂. Once compatibility is established, we unify the type τ₁ to equal τ₂. U-CT2 shows the unification of two maybe types. After establishing compatibility, we unify the actual types τ₁ and τ₂ so that they ultimately resolve to the same type.

The function ℜ(τ) transforms a type τ into an equivalent canonical form where all meta constructors are made explicit at all structural levels of τ. Strictly speaking, unified types are equal only under the ℜ relationship. However, since ℜ(τ) ≡ τ, we will just say that unified types are equal.

4.3.13 Solving Copy Compatibility Constraints

The judgment θ; _x_; _e_ ⊢_solve τ₁ :≫ τ₂ should be read as: the (possibly) constrained type τ₁ for the identifier _x_ (possibly) used in the expression _e_ is transformed³ to the unconstrained type τ₂ by solving all the copy compatibility constraints in τ₁. The ⊢_solve rule fixes the top-level mutability of an ``open'' type by examining whether _x_ is the target of an assignment in the expression _e_. The judgment ⊢_sol will actually solve the constraints, either trivially (there are no constraints, or the constraints have already been solved by unification), or by unifying the type with the constraint. Rules for solving copy compatibility constraints can be found in Table 4.12. The relation ⊧_consistent τ₁↓τ₂ is defined in Section 4.3.14.5.

SOLVE-KNOWN

τ ≠ τ₁↓τ₂ θ ⊢_sol τ :≫ τ^′

θ; _x_; _e_ ⊢_solve τ :≫ τ^′

SOLVE-MUT

θ ⊢_sol τ₁↓τ₂ :≫ τ ?mutated??(?_x_, _e_?)?

θ; _x_; _e_ ⊢_solve τ₁↓τ₂ :≫ △(τ)

SOLVE-IMMUT

θ ⊢_sol τ₁↓τ₂ :≫ τ ¬?mutated??(?_x_, _e_?)?

θ; _x_; _e_ ⊢_solve τ₁↓τ₂ :≫ ▽(τ)

SOL-UNIT

∅ ⊢_sol unit :≫ unit

SOL-BOOL

∅ ⊢_sol bool :≫ bool

SOL-FN

θ ⊢_sol τ₁ :≫ τ^′₁ θ^′ ⊢_sol θ〈τ₂〉 :≫ τ^′₂

θ ∘ θ^′ ⊢_sol τ₁ → τ₂ :≫ θ^′〈τ^′₁〉 → τ^′₂

SOL-MUT

θ ⊢_sol τ :≫ τ^′

θ ⊢_sol Ψτ :≫ Ψτ^′

SOL-REF

θ ⊢_sol τ :≫ τ^′

θ ⊢_sol ⇑τ :≫ ⇑τ^′

SOL-CEIL

θ ⊢_sol τ :≫ τ^′

θ ⊢_sol ⌈τ⌉ :≫ ⌈τ^′⌉

SOL-FLOOR

θ ⊢_sol τ :≫ τ^′

θ ⊢_sol ⌊τ⌋ :≫ ⌊τ^′⌋

SOL-CT-VAR

τ₁ = α θ ⊢_sol τ₂ :≫ τ^′₂ θ^′ = [α ↣ τ^′₂]

θ ∘ θ^′ ⊢_sol τ₁↓τ₂ :≫ τ^′₂

SOL-CT-CONST

τ₁ ≠ α ⊧_consistent τ₁↓τ₂ θ ⊢_sol τ₁ :≫ τ^′₁

θ ⊢_sol τ₁↓τ₂ :≫ τ^′₁

Solving copy compatibility constraints.

4.3.14 Soundness of Eager Inference

4.3.14.1 DEFINITION: Normalization of Constrained Types

The eager unification algorithm maintains constraints on types. However, these can be written in a normal form as in the case of equational inference so that all constraints only appear on the outermost type. For example:

α↓⇑β↓τ = α \ {α ≅ ⇑(β \ {β ≅ τ})}
= α \ {α ≅ ⇑β, β ≅ τ}
≡ α \ {α ≼: γ, ⇑β ≼: γ, β ≼: δ, τ ≼: δ}

Therefore we define a normalization of inferred types as: Ν(τ) = τ \ *C*, wherein:

τ contains no constraints within it.
*C* only contains copy coercion or equality constraints.
All meta-constructors in τ are fully interpreted using the equivalences defined in section 4.3.2. That is, the type τ contains no meta-constructors.

We write Ν(τ) = τ if Ν(τ) = τ \ *C*, and *C* consists only of tautological constraints.

4.3.14.2 DEFINITION: Normalization of Constraint Sets

A constraint set *C* is said to be the normalized form of *C* (that is, Ν(*C*) = *C*) if:

Let *C*^′ be a set of constraints equivalent to *C*, but expressed only using subtype and equality constraints.
*C* = ?close??(?*C*^′?)?. That is, *C* is written as a set of atomic constraints by using the copy coercion rules defined in Table 4.2 (note that this conversion is total). Further, all transitive relationships are explicitly added

4.3.14.3 DEFINITION: Normalization of Contexts

The binding context Γ is said to be the normalized form of Γ (that is, Ν(Γ) = Γ) if ∀ _x_ : τ ∊ Γ , _x_ : τ ∊ Γ and Ν(τ) = τ.

Similarly, the store context Σ is said to be the normalized form of Σ (that is, Ν(Σ) = Σ) if ∀ ℓ : τ ∊ Σ , it is true that ℓ : τ ∊ Σ and Ν(τ) = τ; and ∀ l : τ ∊ Σ , it is true that l : τ ∊ Σ, and Ν(τ) = τ.

4.3.14.4 DEFINITION: Solvable Entities

Syntax

Solvable Entities

ω ::=

τ | Γ | Σ | ω + ω

Note that:

Normalization is defined on all atomic solvable entities. We add the rule: If Ν(ω₁) = ω₁ \ *C*₁ and Ν(ω₂) = ω₂ \ *C*₂ then Ν(ω₁ + ω₂) = ω₁ + ω₂ \ *C*₁ ∪ *C*₂.
As usual, we write Ν(ω) = ω if Ν(ω) = ω \ *C* where *C* consists only of tautological constraints.
Substitution is defined on all atomic solvable entities. We define: θ〈ω₁ + ω₂〉 = θ〈ω₁〉 + θ〈ω₂〉.
For the sake of brevity, we write ∅ + ω = ω + ∅ = ω.
Definition of ⊆ over solvable entities:
1. τ ⊆ τ^′ if the type τ is structurally a part of the type τ^′.
2. Γ ⊆ Γ^′ if Γ^′ contains all the mappings in Γ, and possibly more.
3. Σ ⊆ Σ^′ if Σ^′ contains all the mappings in Σ, and possibly more.
4. ω₁ + ω₂ ⊆ ω^′₁ + ω^′₂ if ω₁ ⊆ ω^′₁ and ω₂ ⊆ ω^′₂.
Definition of ⊇ over solvable entities:
1. τ ⊇ τ^′ if the type τ^′ is structurally a part of the type τ.
2. Γ ⊇ Γ^′ if Γ contains all the mappings in Γ^′, and possibly more.
3. Σ ⊇ Σ^′ if Σ contains all the mappings in Σ^′, and possibly more.
4. ω₁ + ω₂ ⊇ ω^′₁ + ω^′₂ if ω₁ ⊇ ω^′₁ and ω₂ ⊇ ω^′₂.

4.3.14.5 DEFINITION: Consistency of Solvable Entities

A (possibly) constrained type or context ω is said to be consistent, that is, ⊧_consistent ω iff Ν(ω) = ω \ *C* and ⊧_consistent *C*.

4.3.14.6 DEFINITION: Reachable Store

We define |Σ|^{_e_₁, _e_₂, ...} as a store such that |Σ|^{_e_₁, _e_₂, ...}〈Σ〉 and |Σ|^{_e_₁, _e_₂, ...} contains mappings for only those locations that are reachable from _e_₁, _e_₂, ... (that is, the location is syntactically a part of _e_₁, _e_₂, ...).

4.3.14.7 DEFINITION: MTVs

We define the function ?MTVS?(ω) = α^* to be the set of all type variables within the solvable entity ω. That is, it returns the set of all type-variables α^* where α occurs within a maybe type as α↓τ_h.

?MTVS?(α) = {}
?MTVS?(unit) = {}
?MTVS?(bool) = {}
?MTVS?(α↓τ_h) = α ∪ ?MTVS??(?τ_h?)?
?MTVS?(τ↓τ_h) = ?MTVS??(?τ?)? where τ ≠ α
?MTVS?(⇑τ) = ?MTVS??(?τ?)?
?MTVS?(Ψτ) = ?MTVS??(?τ?)?
?MTVS?(τ₁ → τ₂) = ?MTVS??(?τ₁?)? ∪ ?MTVS??(?τ₂?)?
?MTVS?(∅) = {} (empty context).
?MTVS?(Γ, _x_ : τ) = ?MTVS??(?Γ?)? ∪ ?MTVS??(?τ?)?
?MTVS?(Σ, ℓ : τ) = ?MTVS??(?Σ?)? ∪ ?MTVS??(?τ?)?
?MTVS?(Σ, l : τ) = ?MTVS??(?Σ?)? ∪ ?MTVS??(?τ?)?
?MTVS?(ω₁ + ω₂) = ?MTVS??(?ω₁?)? ∪ ?MTVS??(?ω₂?)?

4.3.14.8 DEFINITION: FTVs (Extension)

We need to enhance the definition of FTVS as:

...
?ftv?(τ₁↓τ₂) = ?ftv?(τ₁) ∪ ?ftv?(ℑ(τ₂))
?ftv?(ω₁ + ω₂) = ?ftv?(ω₁) ∪ ?ftv?(ω₂).

4.3.14.9 DEFINITION: NTVs

We define the set of unconstrained variables as:

?NTVS?(α) = {α}
?NTVS?(unit) = {}
?NTVS?(bool) = {}
?NTVS?(α↓τ_h) = ?NTVS??(?τ_h?)?
?NTVS?(τ↓τ_h) = ?NTVS??(?τ?)? where τ ≠ α
?NTVS?(⇑τ) = ?NTVS??(?τ?)?
?NTVS?(Ψτ) = ?NTVS??(?τ?)?
?NTVS?(τ₁ → τ₂) = ?NTVS??(?τ₁?)? ∪ ?NTVS??(?τ₂?)?
?NTVS?(∅) = {} (empty context).
?NTVS?(Γ, _x_ : τ) = ?NTVS??(?Γ?)? ∪ ?NTVS??(?τ?)?
?NTVS?(Σ, ℓ : τ) = ?NTVS??(?Σ?)? ∪ ?NTVS??(?τ?)?
?NTVS?(Σ, l : τ) = ?NTVS??(?Σ?)? ∪ ?NTVS??(?τ?)?
?NTVS?(ω₁ + ω₂) = ?NTVS??(?ω₁?)? ∪ ?NTVS??(?ω₂?)?

4.3.14.10 DEFINITION: TVs

The set of all type variables in a solvable entity is given by TVS() function, defined as follows: Note that this function is different from FTVS(). (see Definition 4.3.14.8.

?TVS?(ω) = ?MTVS??(?ω?)? ∪ ?NTVS??(?ω?)?

4.3.14.11 DEFINITION: ⊢_sol

We write θ ⊢_sol τ to mean that the substitution is θ is obtained by solving the copy compatibility constraints in τ. We define solving all solvable entities as follows:

S-EMPTY-CTX

∅ ⊢_sol ∅

S-EMPTY-TYPE

θ ⊢_sol τ :≫ τ^″

θ ⊢_sol τ

S-GAMMA

θ₁ ⊢_sol τ θ₂ ⊢_sol θ₁〈Γ〉

θ₁ ∘ θ₂ ⊢_sol Γ, _x_ : τ

S-STORE-HL

θ₁ ⊢_sol τ θ₂ ⊢_sol θ₁〈Σ〉

θ₁ ∘ θ₂ ⊢_sol Σ, ℓ : τ

S-STORE-SL

θ₁ ⊢_sol τ θ₂ ⊢_sol θ₁〈Σ〉

θ₁ ∘ θ₂ ⊢_sol Σ, l : τ

S-MULTIPLE

θ₁ ⊢_sol ω₁ θ₂ ⊢_sol θ₁〈ω₂〉

θ₁ ∘ θ₂ ⊢_sol ω₁ + ω₂

4.3.14.12 DEFINITION: ⊧_sol

Ν(θ〈ω〉) = θ〈ω〉 θ = θ_s ∘ θ_o dom(θ_s) = ?MTVS??(?ω?)? θ_o〈θ〈ω〉〉 = θ〈ω〉

θ ⊧_sol ω

That is, θ solves all copy compatibility constraints in ω, but does not otherwise affect the resultant θ〈ω〉. It is, however, free to contain other substitutions that do not matter wrt θ〈ω〉. Note that ⊧_sol is a special case of ⊧ and ⊧_Sol .

4.3.14.13 DEFINITION: Strong Consistency

⊧_consistent ω ?MTVS??(?ω?)? ∩ ?NTVS??(?ω?)? = ∅

⊧_cst ω

Since we have ⊧_consistent ω, if α↓τ_h1 and α↓τ_h2 are structurally a part of ω, we must have ℑ(α↓τ_h1) ≅ ℑ(α↓τ_h2). Further, ?MTVS??(?ω?)? ∩ ?NTVS??(?ω?)? = ∅ guarantees that constrained type variables do not appear unconstrained elsewhere in ω. We call this property strong consistency, denoted by ⊧_cst .

4.3.14.14 DEFINITION: Compatible Solutions (Substitutions)

We write θ₁ ≅ θ₂ if ∀ [α ↣ τ₁] ∊ θ₁ , it is true that [α ↣ τ₂] ∊ θ₂ (that is,dom(θ₁) = dom(θ₂)), and τ₁ ≅ τ₂.

4.3.14.15 DEFINITION: Equivalent Substitutions

We write ω ⊢_eqi θ₁ ≈ θ₂ if θ₁〈ω〉 = θ₂〈ω〉

For example: α ⊢_eqi [α ↣ τ] ≈ [α ↣ β] ∘ [β ↣ τ].

4.3.14.16 DEFINITION: Sub-Substitutions

We write θ^′ ⊆ θ if ∃ θ₁, θ₂ such that θ = θ₁ ∘ θ₂, and θ^′ = θ₁.
We write θ^′ ⊑ θ if ∃ θ₁, θ₂ such that θ = θ₁ ∘ θ₂, and θ^′ ≅ θ₁.

4.3.14.17 THEOREM: Correctness of Eager Unification

If Ν(τ₁) = τ₁ \ *C*₁, and Ν(τ₂) = τ₂ \ *C*₂, and θ ⊢_unf τ₁ = τ₂, then:

If ⊧_UNF *C*₁ and ⊧_UNF *C*₂, then ⊧_UNF {τ₁ = τ₂} ∪ *C*₁ ∪ *C*₂
If ⊧_consistent τ₁ and ⊧_consistent τ₂ then ⊧_consistent θ〈τ₁〉 + θ〈τ₂〉 and ⊧_acyclic θ

4.3.14.18 THEOREM: Correctness of the Constraint Solver

If θ ⊢_sol ω, then θ ⊧_sol ω.

We will also use the following equivalent forms (or special cases of the above statement):

If θ ⊢_sol ω, then ⊧_consistent θ〈ω〉.
If θ ⊢_sol ω, then Ν(θ〈ω〉) = θ〈ω〉.
If θ ⊢_sol τ :≫ τ^′ then Ν(τ^′) = τ^′.

4.3.14.19 THEOREM: Totality of the Constraint Solver

If ⊧_consistent ω then ∃ θ such that θ ⊢_sol ω.
If θ ⊧_sol ω then ∃ θ^′ ⊑ θ such that θ ⊢_sol ω.

4.3.14.20 THEOREM: Decidability of Unification and Solver

θ ⊢_unf τ₁ = τ₂ and θ ⊢_sol τ :≫ τ^′ are decidable.

Proof: The unifier and constraint solver builds a solution tree by always invoking itself types having smaller shapes of types (except for the U-COMMUT rule, but we can consider a canonical derivation in which no two U-COMMUT rules are used consecutively in the unification derivation). Since types are of bounded size, and there are no infinite or circular substitutions, these derivations must be bounded.

4.3.14.21 LEMMA: Properties of ⊧_sol

If θ ⊧_sol ω then ⊧_consistent θ〈ω〉.
If ⊧_consistent θ〈ω〉 then ∃ θ such that θ ⊧_sol ω.
θ ⊧_sol ω iff Ν(θ〈ω〉) = θ〈ω〉.

4.3.14.22 LEMMA: Properties of Equivalent Substitutions

If ω ⊢_eqi θ₁ ≈ θ₂, then:

θ₁ ⊧_sol ω implies θ₂ ⊧_sol ω.
⊧_consistent θ₁〈ω〉 implies ⊧_consistent θ₂〈ω〉.
⊧_cst θ₁〈ω〉 implies ⊧_cst θ₂〈ω〉.
Ν(θ₁〈ω〉) = θ₁〈ω〉 implies Ν(θ₂〈ω〉) = θ₂〈ω〉.

Proof: Evident from the definition of equivalent substitutions.

4.3.14.23 LEMMA: Strong Consistency Implies Consistency

If ⊧_cst ω, then ⊧_consistent ω.

Proof: Evident from Definition 4.3.14.13.

4.3.14.24 LEMMA: Properties of Compatible Constrained Types

If Ν(τ) = τ, and Ν(τ^′) = τ^′, and τ ≅ τ^′, then ⌈τ⌉ ≼: τ^′ ≼: ⌊τ⌋
If Ν(θ〈τ〉) = θ〈τ〉, then ⌈θ〈τ〉⌉ ≼: △(θ〈τ〉) ≼: θ〈τ〉 ≼: ▽(θ〈τ〉) ≼: ⌊θ〈τ〉⌋
If Ν(θ〈τ〉) = θ〈τ〉 and {θ^*} ⊆ ?ftv?(τ) and τ^′ = τ[⌊θ⌋^*/θ^*], then ⌈θ〈τ〉⌉ ≼: θ〈τ〉 ≼: θ〈τ^′〉 ≼: ▽(θ〈τ^′〉)
If Ν(θ〈τ〉) = θ〈τ〉 and {θ^*} ⊆ ?ftv?(τ) and τ^′ = τ[⌈θ⌉^*/θ^*], then △(θ〈τ^′〉) ≼: θ〈τ^′〉 ≼: θ〈τ〉 ≼: ⌊θ〈τ〉⌋.

Proof: Evident from the definition of copy coercion relationships in Section 4.3.3.

4.3.14.25 LEMMA: Relationship of Solutions

If θ₁ ⊧_sol ω and θ₂ ⊧_sol ω then ∃ θ₁₁, θ₁₂, θ₂₁, θ₂₂ such that

θ₁ = θ₁₁ ∘ θ₁₂ and θ₂ = θ₂₁ ∘ θ₂₂
dom(θ₁₁) = dom(θ₂₁) = ?MTVS??(?ω?)?
θ₁₁ ≅ θ₂₁
θ₁₂〈ω〉 = θ₂₂〈ω〉 = ω

4.3.14.26 LEMMA: Uniqueness of Solutions Produced by the Solver

If θ₁ ⊢_sol ω and θ₂ ⊢_sol ω, then θ₁ = θ₂.

4.3.14.27 LEMMA: Relationship between ⊢_solve and ⊢_sol

If θ₁ ⊢_sol τ :≫ τ^′ and θ₂; _x_; _e_ ⊢_solve τ :≫ τ^″ then τ^′ ≅ τ^″ and θ₁ ≅ θ₂.

4.3.14.28 LEMMA: Commutativity of + over Solvable Entities

If θ ⊧_sol ω₁ + ω₂ then θ ⊧_sol ω₂ + ω₁.
If θ ⊢_sol ω₁ + ω₂ then ∃ θ^′ ≅ θ such that θ^′ ⊢_sol ω₂ + ω₁.
If ⊧_consistent ω₁ + ω₂ then ⊧_consistent ω₂ + ω₁.
If ⊧_cst ω₁ + ω₂ then ⊧_cst ω₂ + ω₁.

4.3.14.29 LEMMA: Weakening over Solvable Entities

If ⊧_consistent ω₁ + ω₂ then ⊧_consistent ω₁ and ⊧_consistent ω₂.
If ⊧_consistent ω and ω^′ ⊆ ω then ⊧_consistent ω^′.
If ⊧_cst ω₁ + ω₂ then ⊧_cst ω₁ and ⊧_cst ω₂.
If ⊧_cst ω and ω^′ ⊆ ω then ⊧_cst ω^′.
If Ν(θ〈ω〉) = θ〈ω〉 and ω^′ ⊆ ω, then Ν(θ〈ω^′〉) = θ〈ω^′〉.
If θ ⊧_sol ω₁ + ω₂ then ∃ θ^′ ⊆ θ and ∃ θ^″ ⊆ θ such that θ^′ ⊧_sol ω₁ and θ^″ ⊧_sol ω₂.
If θ ⊧_sol ω and ω^′ ⊆ ω, then ∃ θ^′ ⊆ θ such that θ^′ ⊧_sol ω^′.
If ⊧_cst ω₁ + ω₂ and θ ⊧_sol ω₁ + ω₂ then θ ⊧_sol ω₁ and θ ⊧_sol ω₂.
If ⊧_cst ω and θ ⊧_sol ω and ω^′ ⊆ ω, then θ ⊧_sol ω^′.

4.3.14.30 LEMMA: Extension to Weakening Lemma 4.3.7.6.

If Γ; Σ ⊢ _e_ : τ and Γ^′ ⊇ Γ and Σ^′ ⊇ Σ and Ν(Γ^′) = Γ^′ and Ν(Σ^′) = Σ^′, then, Γ^′; Σ^′ ⊢ _e_ : τ.

4.3.14.31 LEMMA: Substitution on Strongly Compatible Entities

⊧_cst ω_f + ω + ω_s
⊧_cst θ〈ω〉 for some substitution θ.
dom(θ) ∩ ?TVS??(?ω_f + ω + ω_s?)? ⊆ ?TVS??(?ω?)?.

Then, ⊧_cst θ〈ω_f + ω + ω_s〉.

Proof: From assumption (3), we know that only substitutions in θ that can affect ω_f + ω + ω_s are substitutions to type variables that are present in ω. From the definition of strong solubility, we know that all constrained types are compatibly constrained throughout the solvable entity. Therefore a substitution for some type variable within ω cannot violate the strong consistency of ω_f + ω + ω_s.

Note that ω_f or ω_s need not always present since we can imagine the presence of ∅ in that position.

4.3.14.32 LEMMA: Substitution Preserves Compatibility of Solutions

θ₁ ⊧_sol ω
θ₂ ⊧_sol θ〈ω〉 for some θ
dom(θ₁) ∩ dom(θ₂ ∘ θ) = ?MTVS??(?ω?)?

Then, ∃ θ^′₁, θ₀ such that

θ₁ ≅ θ^′₁
ω ⊢_eqi θ₂ ∘ θ ≈ θ^′₁ ∘ θ₀.

Proof: By construction of θ^′₁ and θ₀.

For every substitution [α ↣ τ] ∊ θ₁, where α ∉ ?MTVS??(?ω?)?, add it to θ^′₁.
For every substitution [α ↣ τ] ∊ θ₂ ∘ θ, where α ∉ ?MTVS??(?ω?)?, add it to θ₀.
∀ α ∊ ?MTVS??(?ω?)? , ∃ [α ↣ τ] ∊ θ₁ and ∃ [α ↣ τ^′] ∊ θ₂ ∘ θ . If α appears within ω in the form α↓τ_h, we must have τ ≅ θ₁〈ℑ(τ_h)〉. We must also have τ^′ ≅ θ₂ ∘ θ〈ℑ(τ_h)〉
1. If τ ≅ τ^′, then add [α ↣ τ^′] to θ^′₁.
2. If τ ≄ τ^′ Since we have ⊧_consistent θ₂ ∘ θ〈ω〉 (from assumption (2) and Theorem 4.3.14.18) and the fact that substitution must preserve the shape of a solvable entity, τ^′ can only differ from τ in top-level mutability, and/or by being a more specialized type (has some substitutions for type variables within τ). Therefore, ∃ θ^″ (which possibly uses fresh type variables) such that the substitution[α ↣ τ^′] in θ₂ ∘ θ can be equivalently re-written as [α ↣ τ^″] ∘ θ^″ where τ ≅ τ^″. Now add [α ↣ τ^″] to θ^′₁ and θ^″ to θ₀..

4.3.14.33 LEMMA: Unification Preserves Strong Consistency

If ⊧_cst τ₁ + τ₂ and θ ⊢_unf τ₁ = τ₂ then ⊧_cst θ〈τ₁〉 + θ〈τ₂〉

Proof: Follows from Theorem 4.3.14.17, and by observing the rules U-TVAR, U-CT1 and U-CT2.

4.3.14.34 LEMMA: Corollary to Lemma 4.3.14.33.

If ⊧_cst ω + τ + τ^′ and θ_v ⊢_unf τ^′ = τ then ⊧_cst θ_v〈ω〉 + θ_v〈τ〉 + θ_v〈τ^′〉

Proof: Follows from Lemma 4.3.14.33 and Lemma 4.3.14.31.

4.3.14.35 LEMMA: Unification of Maybe Types

If θ_u ⊢_unf τ₁ = τ₀↓τ₂ and θ_s ⊧_sol θ_u〈τ₁〉 + θ_u〈τ₀↓τ₂〉, then:

θ_u ∘ θ_s〈τ₁〉 ≼: ⌊θ_u ∘ θ_s〈τ₂〉⌋ and ⌈θ_u ∘ θ_s〈τ₂〉⌉ ≼: θ_u ∘ θ_s〈τ₁〉
θ_u ∘ θ_s〈τ₁〉 ≼: ▽(θ_u ∘ θ_s〈τ₂〉) and △(θ_u ∘ θ_s〈τ₂〉) ≼: θ_u ∘ θ_s〈τ₁〉

Proof: From the definition of maybe types, we have τ₀ ≅ τ₂. Due to the unification θ_u ⊢_unf τ₁ = τ₀↓τ₂, we have θ_u〈τ₁〉 ≅ θ_u〈τ₂〉. From θ_s ⊧_sol θ_u〈τ₁〉 + θ_u〈τ₀↓τ₂〉 and Lemma 4.3.14.21, we have: ⊧_consistent θ_s ∘ θ_u〈τ₁〉 + θ_s ∘ θ_u〈τ₀↓τ₂〉 Therefore, we must have: θ_s ∘ θ_u〈τ₁〉 ≅ θ_s ∘ θ_u〈τ₂〉. Again, from Lemma 4.3.14.21, we have: Ν(θ_s ∘ θ_u〈τ₁〉) = θ_s ∘ θ_u〈τ₁〉 and Ν(θ_s ∘ θ_u〈τ₀↓τ₂〉) = θ_u〈τ₀↓τ₂〉. Since normalization does not violate any properties, we have: θ_s ∘ θ_u〈τ₁〉 ≅ θ_u〈τ₂〉. The conclusions are now evident from the definition of copy coercions in Section 4.3.3.

4.3.14.36 LEMMA: Corollary to Lemma 4.3.14.35

If θ_u ⊢_unf τ₁ = τ₀↓τ₂ and θ_s ⊧_sol θ ∘ θ_u〈τ₁〉 + θ ∘ θ_u〈τ₀↓τ₂〉, then:

θ_s ∘ θ ∘ θ_u〈τ₁〉 ≼: ⌊θ_s ∘ θ ∘ θ_u〈τ₂〉⌋ and ⌈θ_s ∘ θ ∘ θ_u〈τ₂〉⌉ ≼: θ_s ∘ θ ∘ θ_u〈τ₁〉
θ_s ∘ θ ∘ θ_u〈〉 ≼: ▽(θ_s ∘ θ ∘ θ_u〈τ₂〉) and △(θ_s ∘ θ ∘ θ_u〈τ₂〉) ≼: θ_s ∘ θ ∘ θ_u〈τ₁〉

Proof: Straightforward extension to Lemma 4.3.14.35.

4.3.14.37 LEMMA: Inferred Substitutions are Consistent.

If Γ; Σ; Π ⊢_i _e_ : τ ∥ θ_u; Π^′, then ⊧_cst θ_u〈Γ〉 + θ_u〈|Σ|^_e_〉 + τ.

Proof: By induction on the derivation of Γ; Σ; Π ⊢_i _e_ : τ ∥ θ_u; Π^′ using Lemma 4.3.14.33, and noting the fact that (1) all substitutions produced during inference are in turn produced by the unifier (or the solver) (2) all maybe types in the inference rules are introduced with fresh type variables (3) the two parts of a maybe type are never separated from each other.

Since the store Σ can contain arbitrary typing assumptions in addition to the ones required for this derivation, we define the property on a canonicalized subset of the store.

4.3.14.38 LEMMA: Inferred Substitutions are Cumulatively Consistent.

Γ; Σ; Π ⊢_i _e_₁ : τ₁ ∥ θ_u1; Π^′
θ_u1〈Γ〉; θ_u1〈Σ〉; Π^′ ⊢_i _e_₂ : τ₂ ∥ θ_u2; Π^″

Then ⊧_cst θ_u2 ∘ θ_u1〈Γ〉 + θ_u2 ∘ θ_u1〈|Σ|^{_e_₁, _e_₂}〉 + θ_u2〈τ₁〉 + τ₂

Proof: Since θ_u2 is obtained in an environment that already has applied the substitutions in θ_u1, and since this derivation occurs on a different tape, θ_u1 and θ_u2 contain mutually exclusive substitutions.

The only effect θ_u2 can have on τ₁ is by providing a substitution for some type variable α which is a non-universally quantified free type variables in θ_u1〈Γ〉 and is present in τ₁. The result now follows from Lemma 4.3.14.37 and Lemma 4.3.14.31.

4.3.14.39 LEMMA: Substitution on Declarative Derivation [Extension to Lemma 4.3.10.5].

Γ; Σ ⊢ _e_ : τ
θ is some substitution such that Ν(θ〈τ + Γ + Σ〉) = θ〈τ + Γ + Σ〉

Then, θ〈Γ〉; θ〈Σ〉 ⊢ _e_ : θ〈τ〉

Proof: Straightforward extension to Lemma 4.3.10.5.

4.3.14.40 LEMMA: Corollary to Lemma 4.3.14.39.

Γ; Σ ⊢ _e_ : τ
θ is some substitution such that ⊧_consistent θ〈τ + Γ + Σ〉

Then, ∃ θ_e such that: θ_e ∘ θ〈Γ〉; θ_e ∘ θ〈Σ〉 ⊢ _e_ : θ_e ∘ θ〈τ〉

Proof: Straightforward extension to Lemma 4.3.14.39. The extra substitution θ_e is necessary to solve any constraints introduced by the substitution θ.

4.3.14.41 LEMMA: Elimination of Irrelevant Substitutions.

If:

θ ⊧_sol τ + Γ + Σ
θ〈Γ〉; θ〈Σ〉 ⊢ _e_ : θ〈τ〉

Then, ∃ θ^′ ⊆ θ such that θ^′ ⊧_sol τ + Γ + |Σ|^_e_ and θ^′〈Γ〉; θ^′〈|Σ|^_e_〉 ⊢ _e_ : θ^′〈τ〉

Proof: Follows from Lemma 4.3.14.29 and by observing the declarative type rules in Table 4.4.

4.3.14.42 LEMMA: Equivalent Substitutions Preserve Declarative Derivation.

τ + Γ + Σ ⊢_eqi θ₁ ≈ θ₂
θ₁〈Γ〉; θ₁〈Σ〉 ⊢ _e_ : θ₁〈τ〉

Then θ₂〈Γ〉; θ₂〈Σ〉 ⊢ _e_ : θ₂〈τ〉

Proof: From Definition 4.3.14.15, we have θ₁〈τ + Γ + Σ〉 = θ₂〈τ + Γ + Σ〉. That is, θ₁〈τ〉 = θ₂〈τ〉 and θ₁〈Γ〉 = θ₂〈Γ〉 and θ₁〈Σ〉 = θ₂〈Σ〉. The result is now evident from assumption (2).

4.3.14.43 LEMMA: Compatible Substitutions Preserve Declarative Derivation.

θ_s ⊧_sol τ + Γ + Σ
θ_s〈Γ〉; θ_s〈Σ〉 ⊢ _e_ : θ_s〈τ〉
θ_s ≅ θ^′_s

Then, θ^′_s〈Γ〉; θ^′_s〈Σ〉 ⊢ _e_ : θ^′_s〈τ〉.

Proof: From Definition 4.3.14.12, we know that θ_s = θ_m ∘ θ_o where θ_m contains substitutions to ?MTVS??(?τ + Γ + Σ?)? and θ_o is irrelevant to τ + Γ + Σ. From the definition of compatibility of substitutions, θ^′_s must have compatible substitutions to only these type variables. The required result can be obtained by straightforward induction on the derivation of θ^′_s〈Γ〉; θ^′_s〈Σ〉 ⊢ _e_ : θ^′_s〈τ〉.

4.3.14.44 LEMMA: Corollary to Lemma 4.3.14.43.

θ_s ⊧_sol τ + Γ + Σ
θ_s〈Γ〉; θ_s〈Σ〉 ⊢ _e_ : θ_s〈τ〉
θ^′_s ⊧_sol τ + Γ + Σ

Then, θ^′_s〈Γ〉; θ^′_s〈Σ〉 ⊢ _e_ : θ^′_s〈τ〉.

Proof: Follows from Lemma 4.3.14.25 and Lemma 4.3.14.43.

4.3.14.45 LEMMA: Corollary to Lemma 4.3.14.44.

θ_e ⊧_sol τ + Γ + |Σ|^_e_
θ_e〈Γ〉; θ_e〈|Σ|^_e_〉 ⊢ _e_ : θ_e〈τ〉
θ_s ⊧_sol τ + Γ + Σ

Then, θ_s〈Γ〉; θ_s〈Σ〉 ⊢ _e_ : θ_s〈τ〉.

Proof:

From assumption (3), the fact that |Σ|^_e_ ⊆ Σ, and Lemma 4.3.14.29, we conclude that ∃ θ^′_s ⊆ θ_s such that θ^′_s ⊧_sol τ + Γ + |Σ|^_e_.
From assumption (2) and (3) and case (1) above, and Lemma 4.3.14.44, we have θ^′_s〈Γ〉; θ^′_s〈|Σ|^_e_〉 ⊢ _e_ : θ^′_s〈τ〉.
From case (1), we can write: θ_s = θ_o ∘ θ^′_s.
From assumption (3) and Lemma 4.3.14.21, we have Ν(θ_s〈Γ + Σ + τ〉) = θ_s〈Γ + Σ + τ〉.
Since we have: |Σ|^_e_ ⊆ Σ, (and thus θ_s〈|Σ|^_e_〉 ⊆ θ_s〈Σ〉), from case (4) and Lemma 4.3.14.29, we obtain Ν(θ_s〈Γ + |Σ|^_e_ + τ〉) = θ_s〈Γ + |Σ|^_e_ + τ〉.
Case (5) can be re-written as: Ν(θ_o〈θ^′_s〈Γ + |Σ|^_e_ + τ〉〉) = θ_o〈θ^′_s〈Γ + |Σ|^_e_ + τ〉〉.
From cases (2), (6) and Lemma 4.3.14.39, we have: θ_o〈θ^′_s〈Γ〉〉; θ_o〈θ^′_s〈|Σ|^_e_〉〉 ⊢ _e_ : θ_o〈θ^′_s〈τ〉〉. That is, θ_s〈Γ〉; θ_s〈|Σ|^_e_〉 ⊢ _e_ : θ_s〈τ〉.
Since we have: Σ ⊇ |Σ|^_e_, (and thus θ_s〈Σ〉 ⊇ θ_s〈|Σ|^_e_〉), from cases (4), (7), and Lemma 4.3.14.30, we finally obtain: θ_s〈Γ〉; θ_s〈Σ〉 ⊢ _e_ : θ_s〈τ〉.

4.3.14.46 LEMMA: Altering Shallow Mutability.

{θ^*} ⊆ ?ftv?(τ) and θ ⊧_sol τ, then θ ⊧_sol τ[⌊θ⌋^*/θ^*] and θ ⊧_sol τ[⌈θ⌉^*/θ^*].

Proof: Since a substitution is performed shallowly (up to the reference boundary), it cannot violate copy compatibility (copy coercion) constraints. Since all type variables are still as general as before, and no new variables are used, θ is still a solution for all constraints in the modified type. Note that we can end up with types of the form ⌊⌈τ⌉⌋ (or ⌈⌊τ⌋⌉), which is equivalent to ⌊τ⌋ (or ⌈τ⌉).

4.3.14.47 LEMMA: Corollary to Lemma 4.3.14.46.

{θ^*} ⊆ ?ftv?(τ) and θ ⊧_sol ω_f + τ + ω_s, then θ ⊧_sol ω_f + τ[⌊θ⌋^*/θ^*] + ω_s and θ ⊧_sol ω_f + τ[⌈θ⌉^*/θ^*] + ω_s.

Proof: Straightforward extension to Lemma 4.3.14.47

4.3.14.48 LEMMA: Corollary to Lemma 4.3.14.47.

{θ^*} ⊆ ?ftv?(τ) and θ_s ⊧_sol θ〈ω_f + τ + ω_s〉, then θ_s ⊧_sol θ〈ω_f + τ[⌊θ⌋^*/θ^*] + ω_s〉 and θ_s ⊧_sol θ〈ω_f + τ[⌈θ⌉^*/θ^*] + ω_s〉.

Proof: Straightforward extension to Lemma 4.3.14.47

4.3.14.49 LEMMA: Valid Substitutions Preserve Declarative Derivation.

θ₁ ⊧_sol τ + Γ + Σ
θ₁〈Γ〉; θ₁〈Σ〉 ⊢ _e_ : θ₁〈τ〉
θ₂ ⊧_sol θ〈τ + Γ + Σ〉 for some substitution θ
dom(θ₁) ∩ dom(θ₂ ∘ θ) = ?MTVS??(?τ + Γ + Σ?)?

Then, θ₂ ∘ θ〈Γ〉; θ₂ ∘ θ〈Σ〉 ⊢ _e_ : θ₂ ∘ θ〈τ〉

Proof:

From Lemma 4.3.14.32, assumption (1), (3), and (4), we conclude that ∃ θ^′₁, θ₀ such that
1. θ₁ ≅ θ^′₁
2. τ + Γ + Σ ⊢_eqi θ₂ ∘ θ ≈ θ^′₁ ∘ θ₀
From assumption (1), (2), case (1.a) above, and Lemma 4.3.14.43, we have: θ^′₁〈Γ〉; θ^′₁〈Σ〉 ⊢ _e_ : θ^′₁〈τ〉
From assumption (3) and Lemma 4.3.14.21, we have Ν(θ₂ ∘ θ〈τ + Γ + Σ〉) = θ₂ ∘ θ〈τ + Γ + Σ〉
From cases (3), (1.b), and Lemma 4.3.14.22, we have Ν(θ^′₁ ∘ θ₀〈τ + Γ + Σ〉) = θ^′₁ ∘ θ₀〈τ + Γ + Σ〉 That is, Ν(θ₀〈θ^′₁〈τ + Γ + Σ〉〉) = θ₀〈θ^′₁〈τ + Γ + Σ〉〉.
From cases (2), (4), and Lemma 4.3.14.39, we have: θ₀〈θ^′₁〈Γ〉〉; θ₀〈θ^′₁〈Σ〉〉 ⊢ _e_ : θ₀〈θ^′₁〈τ〉〉. That is, θ^′₁ ∘ θ₀〈Γ〉; θ^′₁ ∘ θ₀〈Σ〉 ⊢ _e_ : θ^′₁ ∘ θ₀〈τ〉.
Finally, from cases (1.b), (4), and Lemma 4.3.14.42, we have: θ₂ ∘ θ〈Γ〉; θ₂ ∘ θ〈Σ〉 ⊢ _e_ : θ₂ ∘ θ〈τ〉.

4.3.14.50 THEOREM: Soundness of Eager Inference

If:

Γ; Σ; Π ⊢_i _e_ : τ ∥ θ_u; Π^′
θ_s ⊢_sol τ + θ_u〈Γ〉 + θ_u〈Σ〉.
θ_su = θ_s ∘ θ_u

Then, θ_su〈Γ〉; θ_su〈Σ〉 ⊢ _e_ : θ_s〈τ〉.

Proof: By induction on the derivation of Γ; Σ; Π ⊢_i _e_ : τ ∥ θ₁; Π^′. We proceed by case analysis on the last step (again assuming α-reduction vacuously):

Cases TI-UNIT, TI-TRUE. TI-FALSE, TI-ID, TI-HLOC, TI-SLOC are trivial.
Case TI-LAMBDA:
1. We know that:
  1. Γ, _x_ ↦ α; Σ; Π_α ⊢_i _e__i : τ_r ∥ θ_u; Π^′
    
    Γ; Σ; Π ⊢_i λ_x_._e__i : ⌊θ_u〈α〉⌋ → ⌈τ_r⌉ ∥ θ_u; Π^′
  2. θ_s ⊢_sol ⌊θ_u〈α〉⌋ → ⌈τ_r⌉ + θ_u〈Γ〉 + θ_u〈Σ〉
2. From induction hypothesis, we have:
  1. If θ_si ⊢_sol τ_r + θ_u〈Γ, _x_ : α〉 + θ_u〈Σ〉
  2. Then, θ_si ∘ θ_u〈Γ, _x_ : α〉; θ_si ∘ θ_u〈Σ〉 ⊢ _e__i : θ_si〈τ_r〉
  3. That is, θ_si〈θ_u〈Γ, _x_ : α〉〉; θ_si〈θ_u〈Σ〉〉 ⊢ _e__i : θ_si〈τ_r〉
3. From case (2.b.i) above, and Definition 4.3.14.11 rule S-GAMMA, we have: θ_si ⊢_sol τ_r + θ_u〈Γ〉 + θ_u〈α〉 + θ_u〈Σ〉
4. From case (2.c) above and Lemma 4.3.14.28 (commutativity), we conclude that ∃ θ^′_si ≅ θ_si such that θ^′_si ⊢_sol τ_r + θ_u〈α〉 + θ_u〈Γ〉 + θ_u〈Σ〉.
5. From Definition 4.3.14.11 rule S-MULTIPLE, we can write: θ^′_si = θ_f ∘ θ_o where θ_f ⊢_sol τ_r + θ_u〈α〉 and θ_o ⊢_sol θ_f〈θ_u〈Γ〉 + θ_u〈Σ〉〉.
6. Given θ_f ⊢_sol τ_r + θ_u〈α〉, using the SOL-FN rule, we can conclude that θ_f ⊢_sol ⌊θ_u〈α〉⌋ → ⌈τ_r⌉.
7. Therefore, θ^′_si ⊢_sol ⌊θ_u〈α〉⌋ → ⌈τ_r⌉ + θ_u〈Γ〉 + θ_u〈Σ〉. That is, θ^′_si = θ_s
8. From cases (d) and (g), we conclude that θ_si ≅ θ_s.
9. From case (2.b.i) and Theorem 4.3.14.18, we have: θ_si ⊧_sol τ_r + θ_u〈Γ, _x_ : α〉 + θ_u〈Σ〉.
10. From cases (2.i), (2.b.iii), (2.h), and Lemma 4.3.14.43, we have: θ_s〈θ_u〈Γ, _x_ : α〉〉; θ_s〈θ_u〈Σ〉〉 ⊢ _e__i : θ_s〈τ_r〉
11. Since θ_su = θ_s ∘ θ_u, we can write θ_su〈Γ, _x_ : α〉; θ_su〈Σ〉 ⊢ _e__i : θ_s〈τ_r〉. That is, θ_su〈Γ〉, _x_ : θ_su〈α〉; θ_su〈Σ〉 ⊢ _e__i : θ_s〈τ_r〉. Or, θ_su〈Γ〉, _x_ : θ_su〈α〉; θ_su〈Σ〉 ⊢ _e__i : θ_s〈τ_r〉.
12. From the T-LAMBDA rule, we have: θ_su〈Γ〉; θ_su〈Σ〉 ⊢ λ_x_._e__i : ▽(θ_su〈α〉) → △(θ_s〈τ_r〉)
13. By definition, ▽(θ_su〈α〉) → △(θ_su〈τ_r〉) = ⌊θ_su〈α〉⌋ → ⌈θ_s〈τ_r〉⌉ = ⌊θ_su〈α〉⌋ → ⌈θ_s〈τ_r〉⌉ = θ_s〈⌊θ_u〈α〉⌋ → ⌈τ_r⌉〉
14. From cases (2.j) and (2.k) , we finally have: θ_su〈Γ〉; θ_su〈Σ〉 ⊢ λ_x_._e__i : θ_s〈⌊θ_u〈α〉⌋ → ⌈τ_r⌉〉

Case TI-APP:

We know that:

[I]    Γ; Σ; Π_αβγδε ⊢_i _e__f : τ_f ∥ θ_uf; Π^′

[II]    θ_uf〈Γ〉; θ_uf〈Σ〉; Π^′ ⊢_i _e__a : τ_a ∥ θ_ua; Π^″

[III]    θ_vf  ⊢_unf θ_ua〈τ_f〉 = β↓(⌊δ⌋ → ⌈α⌉)

[IV]    θ^* = ?ftv?(θ_vf〈α〉) ∖ ?ftv?(θ_vf〈δ〉)

[V]    τ_rh = ▽(θ_vf〈α〉)[⌊θ⌋^*/θ^*]

[VI]    θ_va  ⊢_unf τ_a = γ↓⌊θ_vf〈δ〉⌋

[VII]    τ_res = ε↓θ_va〈τ_rh〉

Γ; Σ; Π ⊢_i _e__f _e__a : τ_res ∥ θ_va ∘ θ_vf ∘ θ_ua ∘ θ_uf; Π^″

Note that this inference rule is the same as the one in Table 4.9, in which all substitutions are written in every step (without abbreviation), and some redundant substitutions removed.

θ_u = θ_va ∘ θ_vf ∘ θ_ua ∘ θ_uf
θ_s ⊢_sol τ_res + θ_u〈Γ〉 + θ_u〈Σ〉
θ_su = θ_s ∘ θ_u
_e_ = _e__f _e__a

From induction hypothesis (wrt [I]), we have:
1. If θ_sf ⊢_sol τ_f + θ_uf〈Γ〉 + θ_uf〈Σ〉
2. Then, θ_sf ∘ θ_uf〈Γ〉; θ_sf ∘ θ_uf〈Σ〉 ⊢ _e__f : θ_sf〈τ_f〉
Similarly, from induction hypothesis (wrt [II]), we have:
1. If θ_sa ⊢_sol τ_a + θ_ua ∘ θ_uf〈Γ〉 + θ_ua ∘ θ_uf〈Σ〉
2. Then, θ_sa ∘ θ_ua ∘ θ_uf〈Γ〉; θ_sa ∘ θ_ua ∘ θ_uf〈Σ〉 ⊢ _e__a : θ_sa〈τ_a〉
From cases (3.b.i), (3.c.i) and Theorem 4.3.14.18, we have:
1. θ_sf ⊧_sol τ_f + θ_uf〈Γ〉 + θ_uf〈Σ〉
2. θ_sa ⊧_sol τ_a + θ_ua ∘ θ_uf〈Γ〉 + θ_ua ∘ θ_uf〈Σ〉
1. From [I], [II], and Lemma 4.3.14.38, we have: ⊧_cst θ_ua ∘ θ_uf〈Γ〉 + θ_ua ∘ θ_uf〈|Σ|^{_e__f, _e__a}〉 + θ_ua〈τ_f〉 + τ_a.
2. We know that |Σ|^_e__f _e__a = |Σ|^{_e__f, _e__a}, and thus from case (3.a.v), |Σ|^_e_ = |Σ|^{_e__f, _e__a}.
3. From cases (3.e.i) and (3.e.ii), we obtain: ⊧_cst θ_ua ∘ θ_uf〈Γ〉 + θ_ua ∘ θ_uf〈|Σ|^_e_〉 + θ_ua〈τ_f〉 + τ_a.
4. From case (3.e.iii) and Lemma 4.3.14.23, we obtain:
  ⊧_consistent θ_ua ∘ θ_uf〈Γ〉 + θ_ua ∘ θ_uf〈|Σ|^_e_〉 + θ_ua〈τ_f〉 + τ_a.
From case (3.e.iv) and Lemma 4.3.14.21, we conclude that ∃ θ_e such that θ_e ⊧_sol θ_ua ∘ θ_uf〈Γ〉 + θ_ua ∘ θ_uf〈|Σ|^_e_〉 + θ_ua〈τ_f〉 + τ_a.
1. We know that |Σ|^_e__f ⊆ |Σ|^_e_. Therefore, from cases (3.e.iii), (3.f), and Lemma 4.3.14.29 (weakening), we have: θ_e ⊧_sol θ_ua ∘ θ_uf〈Γ〉 + θ_ua ∘ θ_uf〈|Σ|^_e__f〉 + θ_ua〈τ_f〉.
  
  That is, θ_e ⊧_sol θ_ua〈θ_uf〈Γ〉〉 + θ_ua〈θ_uf〈|Σ|^_e__f〉〉 + θ_ua〈θ_uf〈τ_f〉〉. Note that θ_uf〈τ_f〉 = τ_f
2. From (3.b.i), (3.d.i), and Lemma 4.3.14.41, we can conclude that ∃ θ^′_sf such that:
  1. θ^′_sf ⊧_sol θ_uf〈Γ〉 + θ_uf〈|Σ|^_e__f〉 + θ_uf〈τ_f〉
  2. θ^′_sf〈θ_uf〈Γ〉〉; θ^′_sf〈θ_uf〈|Σ|^_e__f〉〉 ⊢ _e__f : θ^′_sf〈θ_uf〈τ_f〉〉.
3. It is clear that dom(θ^′_sf) ∩ dom(θ_e ∘ θ_ua) = ?MTVS??(?θ_uf〈Γ〉 + θ_uf〈|Σ|^_e__f〉 + θ_uf〈τ_f〉?)?, because the derivation [II] occurs in an environment that already contains the substitutions θ_sf (and thus θ^′_sf), and it works on a different tape Π^′, and thus uses fresh type variables when new type variables are introduced.
From cases (3.g.ii.A), (3.g.ii.B), (3.g.i), (3.g.iii), and Lemma 4.3.14.49, we have: θ_e ∘ θ_ua〈θ_uf〈Γ〉〉; θ_e ∘ θ_ua〈θ_uf〈|Σ|^_e__f〉〉 ⊢ _e__f : θ_e ∘ θ_ua〈θ_uf〈τ_f〉〉.

That is, θ_e ∘ θ_ua ∘ θ_uf〈Γ〉; θ_e ∘ θ_ua ∘ θ_uf〈|Σ|^_e__f〉 ⊢ _e__f : θ_e ∘ θ_ua ∘ θ_uf〈τ_f〉.
Since |Σ|^_e_ ⊇ |Σ|^_e__f, we have θ_e ∘ θ_ua ∘ θ_uf〈|Σ|^_e_〉 ⊇ θ_e ∘ θ_ua ∘ θ_uf〈|Σ|^_e__f〉. From case (f) and Lemma 4.3.14.21 and Lemma 4.3.14.29, we can obtain Ν(θ_e ∘ θ_ua ∘ θ_uf〈Γ〉) = θ_e ∘ θ_ua ∘ θ_uf〈Γ〉 and Ν(θ_e ∘ θ_ua ∘ θ_uf〈|Σ|^_e_〉) = θ_e ∘ θ_ua ∘ θ_uf〈|Σ|^_e_〉 Now, from case (h) and Lemma 4.3.14.30, we have θ_e ∘ θ_ua ∘ θ_uf〈Γ〉; θ_e ∘ θ_ua ∘ θ_uf〈|Σ|^_e_〉 ⊢ _e__f : θ_e ∘ θ_ua ∘ θ_uf〈τ_f〉.
Similarly, we have θ_e ∘ θ_ua ∘ θ_uf〈Γ〉; θ_e ∘ θ_ua ∘ θ_uf〈|Σ|^_e_〉 ⊢ _e__a : θ_e ∘ θ_ua ∘ θ_uf〈τ_a〉.
1. It is evident that ⊧_cst β↓(⌊δ⌋ → ⌈α⌉)
2. Since α, β, and δ are fresh type variables, we can write (using case (3.e.iii)): ⊧_cst θ_ua ∘ θ_uf〈Γ〉 + θ_ua ∘ θ_uf〈|Σ|^_e_〉 + θ_ua〈τ_f〉 + τ_a + β↓(⌊δ⌋ → ⌈α⌉).
3. Due to Lemma 4.3.14.28 (commutativity) and case (3.k.ii), we can write:
  ⊧_cst θ_ua ∘ θ_uf〈Γ〉 + θ_ua ∘ θ_uf〈|Σ|^_e_〉 + τ_a + θ_ua〈τ_f〉 + β↓(⌊δ⌋ → ⌈α⌉).
4. From case (3.k.iii), [III], and Lemma 4.3.14.34, we have:
  ⊧_cst θ_vf ∘ θ_ua ∘ θ_uf〈Γ〉 + θ_vf ∘ θ_ua ∘ θ_uf〈|Σ|^_e_〉 + τ_a + θ_vf〈θ_ua〉 + θ_vf〈β↓(⌊δ⌋ → ⌈α⌉)〉.
Again, due to case (3.k.iv) and Lemma 4.3.14.23, and Lemma 4.3.14.21, we conclude that ∃ θ^′_e such that
θ^′_e ⊧_sol θ_vf ∘ θ_ua ∘ θ_uf〈Γ〉 + θ_vf ∘ θ_ua ∘ θ_uf〈|Σ|^_e_〉 + τ_a + θ_vf ∘ θ_ua〈τ_f〉 + θ_vf〈β↓(⌊δ⌋ → ⌈α⌉)〉.

Similar to the argument in cases (g) through (j), we obtain:
1. θ^′_e ∘ θ_vf ∘ θ_ua ∘ θ_uf〈Γ〉; θ^′_e ∘ θ_vf ∘ θ_ua ∘ θ_uf〈|Σ|^_e_〉 ⊢ _e__f : θ^′_e ∘ θ_vf ∘ θ_ua ∘ θ_uf〈τ_f〉.
2. θ^′_e ∘ θ_vf ∘ θ_ua ∘ θ_uf〈Γ〉; θ^′_e ∘ θ_vf ∘ θ_ua ∘ θ_uf〈|Σ|^_e_〉 ⊢ _e__a : θ^′_e ∘ θ_vf ∘ θ_ua ∘ θ_uf〈τ_a〉.
Since θ_vf ∘ θ_ua ∘ θ_uf〈τ_a〉 = τ_a and θ_u = θ_va ∘ θ_vf ∘ θ_ua ∘ θ_uf, similar to cases (k) and (j) above, for the unification performed in step [VI], we conclude that ∃ θ^″_e such that:
1. Let
  1. ω₁ = θ_va ∘ θ_vf ∘ θ_ua ∘ θ_uf〈Γ〉
  2. ω₂ = θ_va ∘ θ_vf ∘ θ_ua ∘ θ_uf〈|Σ|^_e_〉
  3. ω₃ = θ_va ∘ θ_vf ∘ θ_ua〈τ_f〉
  4. ω₄ = θ_va〈τ_a〉
  5. ω₅ = θ_va ∘ θ_vf〈β↓(⌊δ⌋ → ⌈α⌉)〉
  6. ω₆ = θ_va〈γ↓⌊θ_vf〈δ〉⌋〉
2. ⊧_cst ω₁ + ω₂ + ω₃ + ω₄ + ω₅ + ω₆.
3. θ^″_e ⊧_sol ω₁ + ω₂ + ω₃ + ω₄ + ω₅ + ω₆.
4. θ^″_e ∘ θ_u〈Γ〉; θ^″_e ∘ θ_u〈|Σ|^_e_〉 ⊢ _e__f : θ^″_e ∘ θ_u〈τ_f〉.
5. θ^″_e ∘ θ_u〈Γ〉; θ^″_e ∘ θ_u〈|Σ|^_e_〉 ⊢ _e__a : θ^″_e ∘ θ_u〈τ_a〉.
1. From [III], we have: θ_vf ⊢_unf θ_ua〈τ_f〉 = β↓(⌊δ⌋ → ⌈α⌉)
2. From cases (3.m.ii), (3.m.iii) and Lemma 4.3.14.29 (weakening), we have: θ^″_e ⊧_sol ω₃ + ω₅〈〉. That is, θ^″_e ⊧_sol θ_va ∘ θ_vf ∘ θ_ua〈τ_f〉 + θ_va ∘ θ_vf〈β↓(⌊δ⌋ → ⌈α⌉)〉〈〉.
3. The case (3.n.ii) can be re-written as: θ^″_e ⊧_sol θ_va ∘ θ_vf〈θ_ua〈τ_f〉〉 + θ_va ∘ θ_vf〈β↓(⌊δ⌋ → ⌈α⌉)〉.
4. From cases (3.n.i), (3.n.iii) and Lemma 4.3.14.36, we have:
  θ^″_e ∘ θ_va ∘ θ_vf〈θ_ua〈τ_f〉〉 ≼: ▽(θ^″_e ∘ θ_va ∘ θ_vf〈⌊δ⌋ → ⌈α⌉〉).
  
  That is, θ^″_e ∘ θ_va ∘ θ_vf ∘ θ_ua〈τ_f〉 ≼: θ^″_e ∘ θ_va ∘ θ_vf〈⌊δ⌋ → ⌈α⌉〉.
5. The case (3.n.iv) can be re-written as:
  θ^″_e ∘ θ_va ∘ θ_vf ∘ θ_ua ∘ θ_uf〈τ_f〉 ≼: θ^″_e ∘ θ_va ∘ θ_vf ∘ θ_ua ∘ θ_uf〈⌊δ⌋ → ⌈α⌉〉, since these substitutions have no effect.
6. Due to case (3.a.ii), the above case (3.n.v) is equivalent to θ^″_e ∘ θ_u〈τ_f〉 ≼: θ^″_e ∘ θ_u〈⌊δ⌋ → ⌈α⌉〉
7. The case (3.n.vi) is further equivalent to θ^″_e ∘ θ_u〈τ_f〉 ≼: ⌊θ^″_e ∘ θ_u〈δ〉⌋ → ⌈θ^″_e ∘ θ_u〈α〉⌉.
8. Similarly, from the unification performed in step [VI], we have: θ^″_e ∘ θ_u〈τ_a〉 ≼: ⌊θ^″_e ∘ θ_u〈δ〉⌋.
1. From cases (3.m.iv) and (3.n.vii) we obtain:
  θ^″_e ∘ θ_u〈Γ〉; θ^″_e ∘ θ_u〈|Σ|^_e_〉 ⊢ _e__f ≼: ⌊θ^″_e ∘ θ_u〈δ〉⌋ → ⌈θ^″_e ∘ θ_u〈α〉⌉.
2. From cases (3.m.v) and (3.n.viii) we obtain:
  θ^″_e ∘ θ_u〈Γ〉; θ^″_e ∘ θ_u〈|Σ|^_e_〉 ⊢ _e__a ≼: ⌊θ^″_e ∘ θ_u〈δ〉⌋.
1. From (3.m.ii) and (3.m.iii) and Lemma 4.3.14.29, we have θ^″_e ⊧_sol ω₁ + ω₂ + θ_va ∘ θ_vf〈α〉.
2. The case (3.p.i) can be re-written as: θ^″_e ⊧_sol θ_va〈ω₁ + ω₂ + θ_vf〈α〉〉. (Note: ω₁ and ω₂ already contain substitutions from θ_va).
3. From [IV], we have {θ^*} ⊆ ?ftv?(θ_vf〈α〉)
4. From cases (3.p.ii), (3.p.iii) and Lemma 4.3.14.48, we have: θ^″_e ⊧_sol θ_va〈ω₁ + ω₂ + θ_vf〈α〉[⌊θ⌋^*/θ^*]〉. (Note: Here, we instantiated ω_s of Lemma 4.3.14.48 to ∅).
5. From (3.m.iv), it is evident that: θ^″_e ⊧_sol ω₁ + ω₂ + θ_va〈▽(θ_vf〈α〉)[⌊θ⌋^*/θ^*]〉. That is, θ^″_e ⊧_sol ω₁ + ω₂ + θ_va〈τ_rh〉.
1. Let θ_E = θ^″_e ∘ [ε ↣ θ_va〈τ_rh〉]. A substitution for ε with any type τ ≅ θ_va〈τ_rh〉 will actually work in this case.
2. From cases (3.p.v), (3.q.1) Lemma 4.3.14.21, and Definition 4.3.14.12, we can easily obtain: θ_E ⊧_sol ω₁ + ω₂ + γ↓⌊θ_vf〈δ〉⌋. That is, θ_E ⊧_sol ω₁ + ω₂ + τ_ret.
1. Similar to case (3.p.i), we obtain θ^″_e ⊧_sol θ_va〈θ_vf〈α〉〉
2. From case (3.r.i) and Lemma 4.3.14.21, we obtain: Ν(θ^″_e〈θ_va〈θ_vf〈α〉〉〉) = θ^″_e〈θ_va〈θ_vf〈α〉〉〉. That is, Ν(θ^″_e ∘ θ_va〈θ_vf〈α〉〉) = θ^″_e ∘ θ_va〈θ_vf〈α〉〉.
3. From cases (3.r.ii), (3.p.iii) and Lemma 4.3.14.24, we obtain: θ^″_e ∘ θ_va〈⌈θ_vf〈α〉⌉〉 ≼: θ^″_e ∘ θ_va〈▽(θ_vf〈α〉)[⌊θ⌋^*/θ^*]〉.
4. It is evident that θ_va ∘ θ_vf〈α〉 ⊧_eqi θ^″_e ≈ θ_E. Therefore, we can also say θ_va〈⌈θ_vf〈α〉⌉〉 ⊧_eqi θ^″_e ≈ θ_E and θ_va〈▽(θ_vf〈α〉)[⌊θ⌋^*/θ^*]〉 ⊧_eqi θ^″_e ≈ θ_E.
5. From cases (3.r.iii) and (3.r.iv), we have: θ_E ∘ θ_va〈⌈θ_vf〈α〉⌉〉 ≼: θ_E ∘ θ_va〈▽(θ_vf〈α〉)[⌊θ⌋^*/θ^*]〉. That is, ⌈θ_E ∘ θ_va ∘ θ_vf〈α〉⌉ ≼: θ_E ∘ θ_va〈τ_rh〉.
6. From case (3.q.i), we know that θ_E〈τ_res〉 = θ_E ∘ θ_va〈τ_rh〉. (We actually only need a compatibility result here, in case we chose any other compatible type in case (3.q.i)).
7. From cases (3.r.v) and (3.v.vi), we obtain ⌈θ_E ∘ θ_va ∘ θ_vf〈α〉⌉ ≼: θ_E〈τ_res〉.
8. The case (3.r.vii) can be written as ⌈θ_E ∘ θ_u〈α〉⌉ ≼: θ_E〈τ_res〉, since the extra substitutions have no effect.
1. From case (3.q.i), it is evident that ω₁ + ω₂ + ⌊θ^″_e ∘ θ_u〈δ〉⌋ → ⌈θ^″_e ∘ θ_u〈α〉⌉ ⊧_eqi θ_E ≈ θ^″_e. Therefore, from case (3.o.i) and Lemma 4.3.14.42, we have: θ_E ∘ θ_u〈Γ〉; θ_E ∘ θ_u〈|Σ|^_e_〉 ⊢ _e__f ≼: ⌊θ_E ∘ θ_u〈δ〉⌋ → ⌈θ_E ∘ θ_u〈α〉⌉.
2. Similarly, we have: θ_E ∘ θ_u〈Γ〉; θ_E ∘ θ_u〈|Σ|^_e_〉 ⊢ _e__a ≼: ⌊θ_E ∘ θ_u〈δ〉⌋.
Now, from cases (3.s.i), (3.s.ii), (3.r.viii) and T-APP rule, we obtain: θ_E ∘ θ_u〈Γ〉; θ_E ∘ θ_u〈|Σ|^_e_〉 ⊢ _e__f _e__a : θ_E〈τ_res〉.
1. From case (3.q.ii) and Lemma 4.3.14.28 (commutativity), we obtain: θ_E ⊧_sol τ_ret + ω₁ + ω₂.
2. From case (3.a.iii) and Theorem 4.3.14.18, we have: θ_s ⊧_sol τ_res + θ_u〈Γ〉 + θ_u〈Σ〉
3. From cases (3.u.i), (t), (3.u.ii), and Lemma 4.3.14.45, we obtain: θ_s ∘ θ_u〈Γ〉; θ_s ∘ θ_u〈Σ〉 ⊢ _e__f _e__a : θ_s〈τ_res〉.
4. Finally, from cases (3.a.iv) and (3.a.v), we obtain the desired result: θ_su〈Γ〉; θ_su〈Σ〉 ⊢ _e_ : θ_s〈τ_res〉.

Cases TI-LET-α: Similar to case (4) (TI-APP), except for the use of Lemma 4.3.14.27.
Cases TI-IF, TI-DUP, TI-DEREF, TI-SET, TI-TQEXPR, TI-LET-α-TQ are similar.

4.3.14.51 LEMMA: Corollary–1 to Soundness of Eager Inference

If:

Γ; Σ; Π ⊢_i _e_ : τ ∥ θ_u; Π^′
θ_s ⊢_sol τ :≫ τ^′
θ_e ⊢_sol θ_s ∘ θ_u〈Γ + |Σ|^_e_〉
θ = θ_e ∘ θ_s ∘ θ_u

Then θ〈Γ〉; θ〈Σ〉 ⊢ _e_ : τ^′.

Proof: Follows from Theorem 4.3.14.50 Definition 4.3.14.4, and Lemma 4.3.14.37.

4.3.14.52 THEOREM: Corollary–2 to Soundness of Eager Inference

If:

Γ; Σ; Π ⊢_i _e_ : τ ∥ θ_u; Π^′
θ_s ⊢_sol τ :≫ τ^′

Then ∃ θ_e such that

θ = θ_e ∘ θ_s ∘ θ_u
θ〈Γ〉; θ〈Σ〉 ⊢ _e_ : τ^′.

Proof: Follows from Lemma 4.3.14.51.

Chapter 5: Implementation

The bootstrap compiler for BitC has been implemented in C++. Currently, the backend emits portable C code. The core of the compiler involves 28,686 lines of C++ code, of which implementation of type system accounts for about 6,894 lines and the implementation of polymorphism accounts for 992 lines.

The bootstrap compiler for BitC implements polymorphism by brute-force polyinstantiation. This simplifies the implementation of overloading (type-classes) at the cost of requiring whole-program compilation. The algorithm is incremental, supporting use in an interactive environment [37]. More sophisticated techniques for implementing polymorphism over unboxed types are explored in the literature [ 24 ,13 ,32 ]. We view the current implementation as experimental, though it does have the practical advantage (important to us) that emitted types and code are directly inter-callable with C.

There are several proposals for implementing polymorphism over unboxed types. For example, by using coercions [24] into a boxed representation when used in a polymorphic context, using dictionaries [13] that is, passing extra type-parameters to functions, hybrid variations of the above [32] or full polyinstantiation (C++ templates). Depending on the option we pick, there are different trade-offs with respect to the amount of RTTI support needed, separate compilation, efficiency, code size, etc.

Chapter 6: Related Work

Cyclone [17] supports first class polymorphism and polymorphic recursion for functions definitions. This approach is feasible in Cyclone, where there is a distinction between functions (code) and function pointers (data). In an expression language with inner functions, it is more intuitive to treat all first class values alike. Cyclone supports partial type reconstruction so that so that most types and instantiations of polymorphic types can be automatically inferred. Grossman provides a detailed account of using quantified types with imperative C style mutation and & operator in Cyclone [1153]. His formalization develops a general theory wherein any expression can be polymorphic, but requires explicit annotation for all polymorphic definitions and instantiations. Since C (and Cyclone) have no notion of immutability, both languages require explicit annotation of polymorphism. In contrast, we believe that the best way to integrate polymorphism into the systems programming paradigm is by automatic — albeit incomplete — inference. One contribution of our work (in comparison to [1153]) is that we give a formal specification and proof of correctness of the inference algorithm, not just the type system.

Smith and Volpano have proposed an ML-style polymorphic type system for a dialect of C [33]. Their system uses different binding constructs for polymorphic and mutable bindings — let, letvar, letarr. They impose the ML-like restriction that all first class references, vars and arrays must be mutable, and function arguments and let-bound identifiers be immutable, because of which they do not have to deal with copy compatibility issues. Their language does not have structures and union types, and thus does not address complications due to parametrized types, and unboxed composite types with mixed unboxed mutable and immutable types. Our language, while being strictly more expressive, also provides a more natural expression of programs.

A monadic model [20] of mutable state is used in pure functional languages like Haskell [19]. The main advantage of this approach is that the type system provides guarantees not only about the immutability of locations but also distinguishes side effecting computations from others. Therefore, this model is well suited for integration with theorem provers and deduction systems. However, this model is also considerably different from the normal programming idioms used by systems programmers. Hallgren et al. have recently proposed a monadic interface to low level hardware and formally specified certain behavioral properties about it [12]. They have also implemented a prototype operating systems in Haskell based on this system, and it would be interesting to see if this approach scales to a full implementation that provides real time guarantees. In BitC, we have considered providing syntactic constructs that guarantee side-effect free computation. For example we could have a defining form defpure that is similar to define, but allows purely applicative definitions only. This has the advantage of providing a separation of stateful computation from pure ones, as well as the simplicity of staying within the Hindley-Milner type system.

Diatchki et al have proposed support for bit-level word types in Haskell [8]. Their solution could be extended to the full defrepr mechanism of BitC. Communication with the authors has revealed that there is a proposal for extending their prototype interpreter into a full implementation in the GHC compiler [10]. The VFiasco project aims at formalizing the semantics of C++ and using it directly for verification of the Fiasco microkernel written in C++. They present formal semantics for some datatypes of C++ in [14], but do not model C++ pointers, unions or mutability.

Cqual [9] provides a general framework for inference and use of type qualifiers. One of the applications presented in [9] is inference of (maximal) const qualifications for types in C programs, similar to mutability inference in BitC. However, their system does not deal with polymorphism or parametrized composite datatypes. SysObjC [3] extends the C programming language with object-like value types, but does address type safety in the face of polymorphism.

C# is a safe, high-level language supports mutability and low-level representation, but does not support type inference. Spec# [4] is an extension of C# that also provides an integrated verification framework. Their framework is complementary to our system, and can benefit from BitC's mutability model [34].

Chapter 7: Conclusion

In this paper, we have proposed a well-founded first-class mutability model. It is well founded in the sense that types are definitive about the mutability of all locations, and every location has one and only one type across all aliases. The model is first class in the sense that it supports unboxed objects and mutability of stack variables. This makes a language with this type system suitable for systems programming as well as for integration with a verification framework.

There is a fundamental conflict of goals between the ability to infer principal types and to allow freedom of mutability-compatibility at copy boundaries. We have identified various trade-offs and some design choices in this regard, along with their pros and cons. We have proposed a solution to this problem that uses certain hinting mechanisms to infer types based on the ``natural'' flow of type information in an expression. We have also provided a formal framework and for out type system and proved it sound. The type system is implemented as part of the BitC language compiler. Source code for the BitC compiler can be obtained from http://coyotos.org.

Bibliography

Thomas Ball, Todd Millstein, Sriram K. Rajamani ``Polymorphic predicate abstraction.'' Microsoft Research Technical Report MSR_2001_10 June 2002.
Thomas Ball and Sriram K. Rajamani. ``The SLAM Project: Debugging System Software via Static Analysis.'' Proc. 2002 ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, 2002.
Ádám Balogh and Zoltán Csörnyei. ``SysObjC: C Extension for Development of Object-Oriented Operating Systems.'' Proc. Third ECOOP Workshop on Programming Languages and Operating Systems. San Jose, CA. October 2006.
Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. ``The Spec# programming system: An overview.'' CASSIS 2004, LNCS vol. 3362 2004.
E. Brewer, J. Condit, B. McCloskey, and F. Zhou. ``Thirty Years is Long Enough: Getting Beyond C.'' Proc. Tenth Workshop on Hot Topics in Operating System (HotOS X), USENIX, 2005.
The Coq Development Team ``The Coq Proof Assistant Reference Manual'' http://coq.inria.fr/doc/main.html
R. Deline and M. Fahndrich ``Enforcing high-level protocols in low-level software.'' Proc. of the ACM Conference on Programming Language Design and Implementation pp 5969. 2001.
Iavor S. Diatchki, Mark P. Jones, and Rebekah Leslie. ``High- level Views on Low-level Representations.'' Proc. 10th ACM Conference on Functional Programming pp. 168–179. September 2005.
Jeffrey S. Foster, Manuel Fähndrich, and Alexander Aiken. ``A Theory of Type Qualifiers.'' Proc. SIGPLAN Conference on Programming Language Design and Implementation (PLDI'99). pp. 192–203. 1999.
The GHC Team ``The Glorious Glasgow Haskell Compilation System User's Guide, Version 6.6'' http://www.haskell.org/ghc/docs/ latest/html/users_guide/index.html
D. Grossman, ``Quantified Types in an Imperative Language'' ACM Transactions on Programming Languages and Systems 2006.
T. Hallgren, M. P. Jones, R. Leslie, and A. Tolmach. ``A Principled Approach to Operating System Construction in Haskell.'' Proc. International Conference on Functional Programming (ICFP'05), Sep. 2005. Tallinn, Estonia. pp. 116–128.
R. Harper and G. Morrisett. ``Compiling polymorphism using intentional type analysis.'' ACM Symp. on Principles of Programming Languages pp 130-141, January 1995
Michael Hohmuth and Hendrik Tews ``The VFiasco approach for a verified operating system.'' ECOOP Workshop on Programming Languages and Operating Systems 2005.
ISO, International Standard ISO/IEC 8652:1995 (Information Technology — Programming Languages — Ada) International Standards Organization (ISO). 1995.
ISO, International Standard ISO/IEC 9899:1999 (Programming Languages - C) International Standards Organization (ISO). 1999.
T. Jim, G. Morrisett, D. Grossman, M. Hicks, J. Cheney, and Y. Wang ``Cyclone: A safe dialect of C.'' Proc. of USENIX Annual Technical Conference pp 275288, 2002.
Mark P. Jones ``Qualified types: theory and practice.'' Cambridge Distinguished Dissertations In Computer Science ISBN:0-521-47253-9, 1995
Simon Peyton Jones (ed.). Haskell 98 Language and Libraries: The Revised report. Cambridge University Press. 2003.
Launchbury, J. and Peyton Jones, S. L. ``State in Haskell.'' LISP and Symbolic Computation 8, 4 (Dec.), pp 293-341, 1995.
M. Kaufmann, J. S. Moore. ``Computer Aided Reasoning: An Approach'' Kluwer Academic Publishers, 2000.
Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language. Prentice Hall, 1988
Xavier Leroy, ``The Objective Caml System Release 3.09, Documentation and User's Manual.'' http://caml.inria.fr/pub/docs/ manual-ocaml/index.html
X. Leroy, ``Unboxed objects and polymorphic typing.'' ACM SIGPLAN Symposium on Principles of Programming Languages pages 177--188, January 1992. 8(4):343--355, 1995.
Robin Milner ``A theory of type polymorphism in programming.'' Journal of Computer and System Sciences pp 348-375, 1978.
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML - Revised The MIT Press, May 1997.
G. Necula, S. Mcpeak, and W. Weimer ``CCured: Type-safe retrofitting of legacy code.'' Proc. of Symposium on Principles of Programming Languages pp 128139, 2002.
T. Nipkow, L. C. Paulson and M. Wenzel ``Isabelle/HOL — A Proof Assistant for Higher-Order Logic.'' Springer LNCS series volume 2283 2002.
Frank Pfenning and Carsten Schürmann. ``System description: Twelf — a meta-logical framework for deductive systems.'' Proc. of International Conference on Automated Deduction (CADE-16) pp 202-206, Springer-Verlag LNAI 1632, 1999.
Benjamin C. Pierce ``Types and Programming Languages'' The MIT Press, Massachusetts Institute of Technology ISBN 0-262-16209-1, 2002.
Benjamin C. Pierce and David N. Turner. ``Local Type Inference.'' In Proc. of Symposium on Principles of Programming Languages pp 252-265, 1998.
Zhong Shao. ``Flexible representation analysis.'' Proc. ACM SIGPLAN International conference on Functional programming pp 85 - 98, 1997.
G. Smith and D. Volpano. ``A sound polymorphic type system for a dialect of C.'' Science of Computer Programming 32(2--3):49--72, 1998.
Spec# team ``Spec# 1.0.6404 for Microsoft Visual Studio 2005 Release Notes'' http://research.microsoft.com/specsharp /1.0.6404/relnotes.htm
Matthew S. Tschantz and Michael D. Ernst, ``Javari: Adding reference immutability to Java'' Object-Oriented Programming Systems, Languages, and Applications pp 211-230, October 2005.
A. K. Wright, ``Simple Imperative Polymorphism'' Lisp and Symbolic Computation 8(4):343--355, 1995.
Swaroop Sridhar ``Implementation of Polymorphism in BitC'' http://www.coyotos.org/ docs/bitc/polyinst.html
S. Sridhar and J. Shapiro. ``Type Inference for Unboxed Types and First Class Mutability'' Proc. 3rd ECOOP Workshop on Programming Languages and Operating Systems (PLOS 2006) San Jose, CA. 2006.
J. S. Shapiro, Eric Northup, M. Scott Doerrie, and Swaroop Sridhar. Coyotos Microkernel Specification, 2006, available online at www.coyotos.org.
Tim Harris, Simon Marlow and Simon Peyton Jones ``Haskell on a shared-memory multiprocessor'' Proc. of the 2005 ACM SIGPLAN workshop on Haskell. pp 49-61, 2005.
H. XI ``Imperative programming with dependent types.'' Proc. of IEEE Symposium on Logic in Computer Science pp 375387, 2000.
J. S. Shapiro, J. M. Smith, and D. J. Farber. ``EROS, A Fast Capability System'' Proc. 17th ACM Symposium on Operating Systems Principles. Dec 1999. pp. 170–185. Kiawah Island Resort, SC, USA.
M. Fähndrich, M. Aiken, C. Hawblitzel, O. Hodson, G. Hunt, J. R. Lauris, and S. Levi. ``Language Support for Fast and Reliable Message-based Communication in Singularity OS.'' Proc. EUROSYS 2006, Leuven Belgium. 2006
M. Aiken, M. Fähndrich, C. Hawblitzel, G. Hunt, and J. R. Lauris. ``Deconstructing Process Isolation.'' Microsoft Technical Report MSR-TR-2006-43. Microsoft, Inc. 2006
M. Fähndrich and R. DeLine "Adoption and Focus: Practical Linear Types for Imperative Programming." Proc. of the ACM Conference on Programming Language Design and Implementation June 2002.
Bernd Schoeller. ``Strengthening Eiffel contracts using models.'' Hung Dang Van and Zhiming Liu, editors, Proceeding of the Workshop on Formal Aspects of Component Software FACS'03, September 2003.
Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte. ``A Simple Sequential Reasoning Approach for Sound Modular Verification of Mainstream Multithreaded Programs'' Proc. of Multithreading in Hardware and Software: Formal Approaches to Design and Verification (TV 2006), Seattle, 2006.
Geoffrey Smith and Dennis Volpano. ``Polymorphic typing of variables and references'' ACM Transactions on Programming Languages and Systems Pages: 254 - 267, May 1996
Simon Peyton Jones and Philip Wadler ``Imperative functional programming.'' Proc. ACM SIGPLAN Principles of Programming Languages. 1993
A. K. Wright, ``Simple Imperative Polymorphism'' Lisp and Symbolic Computation 8(4):343--355, 1995.
Benjamin C. Pierce ``Types and Programming Languages'' The MIT Press, Massachusetts Institute of Technology ISBN 0-262-16209-1, 2002.
J. Garrigue, ``Relaxing the Value Restriction'' International Symposium on Functional and Logic Programming 2004.
D. Grossman, ``Quantified Types in an Imperative Language'' ACM Transactions on Programming Languages and Systems 2006.
D. Grossman ``Safe programming at the C level of abstraction.'' Ph.D. dissertation. Cornell University 2003.
J. S. Shapiro, S. Sridhar, M. S. Doerrie, ``BitC Language Specification'' http://coyotos.org/docs/bitc/spec.html
S. Sridhar, J. S. Shapiro ``Design of Type and Mutability Inference in BitC'' Systems Research Laboratory Technical Report SRL2006-01 Johns Hopkins University, 2006. http://www.coyotos.org/docs/bitc/mutinfer.html
Jeff Vaughan ``A proof of correctness for the Hindley-Milner type inference algorithm'' http://www.seas.upenn.edu/~vaughan2/docs/hmproof.pdf

We use texttt font to show program fragments and an emphasized texttt font to show the inferred types.
Of course, types are not displayed in this form to the user. Function types are always printed in ``interface form,'' which does not expose the ``internal'' mutability of argument or return types [56].
This transformation can be thought of as a (safe) coercion. Hence the use of the operator .

Formalization of the BitC Type System

SRL Technical Report SRL2007-01

Table of Contents

Chapter 1: Abstract

Chapter 2: Introduction

Chapter 3: Mutability Model and Type Inference

3.1 BitC

3.2 Mutability Model in BitC

3.3 Copy Compatibility

3.4 Type Inference

3.4.1 Why Should We Infer Mutability?

3.4.2 Incompleteness of Inference

3.4.3 Inference Considerations

3.5 Type Inference in BitC

Chapter 4: Formalization

4.1 The Language

4.2 Dynamic Semantics

4.3 Static Semantics

4.3.1 Copy Compatibility

4.3.2 Compatibility of Function Types

4.3.3 Copy Coercions

4.3.3.1 Problem with Subsumption-like Coercion Rule

4.3.4 Location Semantics

4.3.5 Declarative Type Rules

4.3.6 Generalization

4.3.6.1 DEFINITION: Free Type Variables

4.3.6.2 DEFINITION: Value Restriction

4.3.7 Soundness of Declarative system

4.3.7.1 DEFINITION: Stack and Heap Typing

4.3.7.2 LEMMA: Inversion of Typing Relation

4.3.7.3 LEMMA: Inversion of Copy Coercion

4.3.7.4 LEMMA: Canonical Forms

4.3.7.5 LEMMA: Progress

4.3.7.6 LEMMA: Weakening

4.3.7.7 LEMMA: Value Substitution

4.3.7.8 LEMMA: Location Substitution

4.3.7.9 LEMMA: Stack and Heap Assignment

4.3.7.10 LEMMA: Preservation

4.3.7.11 DEFINITION: Stuck State

4.3.7.12 THEOREM: Type Soundness

4.3.8 Equational Inference Algorithm

4.3.9 Unification

4.3.9.1 DEFINITION: Constraint Set Closure

4.3.9.2 Solving the Constraints

4.3.10 Soundness of Equational Inference

4.3.10.1 THEOREM: Soundness of Constraint Closure

4.3.10.2 THEOREM: Correctness of Constraint Solver

4.3.10.3 THEOREM: Correctness of Unification

4.3.10.4 THEOREM: Decidability of Unification

4.3.10.5 LEMMA: Substitution on Declarative Derivation

4.3.10.6 LEMMA: Weakening of Substitutions

4.3.10.7 LEMMA: Composition of Solutions and Substitutions

4.3.10.8 THEOREM: Soundness of Equational Inference

4.3.11 Inference with Eager Unification

4.3.12 Unification

4.3.13 Solving Copy Compatibility Constraints

4.3.14 Soundness of Eager Inference

4.3.14.1 DEFINITION: Normalization of Constrained Types

4.3.14.2 DEFINITION: Normalization of Constraint Sets

4.3.14.3 DEFINITION: Normalization of Contexts

4.3.14.4 DEFINITION: Solvable Entities

4.3.14.5 DEFINITION: Consistency of Solvable Entities

4.3.14.6 DEFINITION: Reachable Store

4.3.14.7 DEFINITION: MTVs

4.3.14.8 DEFINITION: FTVs (Extension)

4.3.14.9 DEFINITION: NTVs

4.3.14.10 DEFINITION: TVs

4.3.14.11 DEFINITION: ⊢sol

4.3.14.12 DEFINITION: ⊧sol

4.3.14.13 DEFINITION: Strong Consistency

4.3.14.14 DEFINITION: Compatible Solutions (Substitutions)

4.3.14.15 DEFINITION: Equivalent Substitutions

4.3.14.16 DEFINITION: Sub-Substitutions

4.3.14.17 THEOREM: Correctness of Eager Unification

4.3.14.18 THEOREM: Correctness of the Constraint Solver

4.3.14.19 THEOREM: Totality of the Constraint Solver

4.3.14.20 THEOREM: Decidability of Unification and Solver

4.3.14.21 LEMMA: Properties of ⊧sol

4.3.14.22 LEMMA: Properties of Equivalent Substitutions

4.3.14.23 LEMMA: Strong Consistency Implies Consistency

4.3.14.11 DEFINITION: ⊢_sol

4.3.14.12 DEFINITION: ⊧_sol

4.3.14.21 LEMMA: Properties of ⊧_sol

4.3.14.27 LEMMA: Relationship between ⊢_solve and ⊢_sol