A Practical Soft Type System for Scheme

Andrew K. Wright^{∗} Robert Cartwright^{†}

Department of Computer Science Rice University Houston, TX 77251-1892 {wright,cartwright}@cs.rice.edu.

Rice University Technical Report TR93-218

December 6, 1993

Abstract

Soft type systems provide the benefits of static type checking for dynamically typed languages without rejecting untypable programs. A soft type checker infers types for variables and expressions and inserts explicit run-time checks to transform untypable programs to typable form. We describe a practical soft type system for R4RS Scheme. Our type checker uses a representation for types that is expressive, easy to interpret, and supports efficient type inference. Soft Scheme supports all of R4RS Scheme, including procedures of fixed and variable arity, assignment, continuations, and top-level definitions. Our implementation is available by anonymous FTP.

∗The first author was supported in part by the United States Department of Defense under a National Defense Science and Engineering Graduate Fellowship.

†The second author was supported by NSF grant CCR-9122518 and the Texas Advanced Technology Program under grant 003604-014.

1 Introduction

Dynamically typed languages like Scheme [5] permit program operations to be defined over any computable subset of the data domain. To ensure safe execution,^{1} primitive operations confirm that their arguments belong to appropriate subsets known as types. The types enforced by primitive operations induce types for defined operations. Scheme programmers typically have strong intuitive ideas about the types of program operations, but dynamically typed languages offer no tools to discover, verify, or express such types.

Static type systems like the Hindley-Milner type discipline [9, 14] provide a framework to discover and express types. Static type checking detects certain errors prior to execution and enables compilers to omit many run-time type checks. Unfortunately, static type systems inhibit the freedom of expression enjoyed with dynamic typing. To ensure safety, programs that do not meet the stringent requirements of the type checker are ineligible for execution. In rejecting untypable programs, the type checker also rejects meaningful programs that it cannot prove are safe. Equivalent typable programs are often longer and more complicated.

Soft type systems [4, 6] provide the benefits of static typing for dynamically typed languages. Like a static type checker, a soft type checker infers types for variables and expressions. But rather than reject programs containing untypable fragments, a soft type checker inserts explicit run-time checks to transform untypable programs to typable form. These run-time checks indicate potential program errors, enabling programmers to detect errors prior to program execution. Soft type checking minimizes the number of run-time checks in the compiled code, enabling dynamically typed languages to attain the efficiency of statically typed languages like ML.

We have developed a practical soft type system for R4RS Scheme [5], a modern dialect of Lisp. Soft Scheme is based on an extension of the Hindley-Milner polymorphic type discipline that requires no programmer supplied type annotations. It presents types in a natural type language that is easy for non-expert programmers to interpret. Type analysis is sufficiently accurate to provide useful diagnostic aid to programmers: our system has detected several elusive errors in its own source code. The type checker typically inserts only 10% of the run-time checks that are necessary for safe execution without soft typing. We have observed consequent speedups of up to 70% over a high quality Scheme compiler.

Soft Scheme is based on a soft type system designed by Cartwright and Fagan for an idealized functional language [4, 6]. Their type system extends Hindley-Milner typing with union types, recursive types, and a modicum of subtyping as subset on union types. Soft Scheme includes several major extensions to their technical results. First, we use a different representation for types that integrates polymorphism smoothly with union types and is more computationally efficient. Our representation also supports the incremental definition of new type constructors. Second, an improved check insertion algorithm inserts fewer runtime checks and yields more precise types. Third, our type system addresses the “grubby” features of a real programming language that Cartwright and Fagan’s study ignored. In particular, we treat uncurried procedures of fixed and variable arity, assignment, continuations, exceptions, and top-level definitions. Finally, our system augments Scheme with pattern matching and type definition extensions that facilitate more precise type assignment.

1Safe implementations of a programming language guarantee to terminate execution with an error message when a primitive is applied to arguments outside its domain.

1.1 Outline

The next section illustrates Soft Scheme with an example, describes the type language, and shows the reduction in run-time checking for some bench marks. Section 3 formally defines a soft type system for a functional core language. Section 4 extends this simple soft type system to R4RS Scheme, describes our pattern matching and type definition extensions, and discusses several problems. Sections 5 and 6 discuss related and future work.

2 Soft Scheme

Soft Scheme performs global type checking for R4RS Scheme programs. When applied to a program, the type checker prints only a summary of the inserted run-time checks. Type information may then be inspected interactively according to the programmer’s interest.

The following program defines and uses a function that flattens a tree to a proper list:^{2}

(define flatten (lambda (l)
(cond [(null? l) ’()]

[(pair? l) (append (flatten (car l)) (flatten (cdr l)))] [else (list l)])))

(define a ’(1 (2) 3)) (define b (flatten a))

Soft type checking this program yields the summary “TOTAL CHECKS 0”. This program requires no run-time checks as it is completely typable. The types of the top-level definitions follow:

flatten : (rec ([Y1 (+ nil (cons Y1 Y1) X1)])

(Y1 −> (list (+ (not cons) (not nil) X1))))

a : (cons num (cons (cons num nil) (cons num nil)))

b : (list num)

The type of a reflects the shape of the value ’(1 (2) 3), which abbreviates the expression (cons 1 (cons (cons 2 ’()) (cons 3 ’()))). Pairs, constructed by cons, have type (cons · ·). The empty list ’() has type nil. The type for b indicates that b is a proper list of numbers. The type (list num) abbreviates (rec ([Y (+ nil (cons num Y))]) Y), which denotes the least fixed point of the recursion equation Y = nil ∪ (cons num Y). Finally, flatten’s type (Y1 −> (list …)) indicates that flatten is a procedure of one argument returning a list. The argument type is defined by Y1 = nil ∪ (cons Y1 Y1) ∪ X1 where X1 is a type variable standing for any type. Hence, flatten accepts the empty list, pairs, or any other kind of value, i.e., flatten accepts any value. A result returned by flatten is a proper list of elements of type X1 , which do not include pairs or the empty list.

Now suppose we add the following lines to our program:

(define c (car b))

(define d (map add1 a))

(define e (map add1 (flatten ’(this (that)))))

2A proper list is a spine of pairs that ends on the right with the special constant ’() called “empty list”.

Type checking the extended program yields the summary:

c 1 (1 prim) d 1 (1 prim) e 1 (1 prim) (1 ERROR) TOTAL CHECKS 3 (1 ERROR)

This program requires three run-time checks at primitive operations, one in each of the definitions of c, d, and e. The modified program shows the locations of the run-time checks:

⋮

(define c (CHECK-car b))

(define d (map CHECK-add1 a))

(define e (map ERROR-add1 (flatten ’(this (that)))))

An unnecessary CHECK-car is inserted because the type checker is unable to establish from the type of b that car is applied to a pair.^{3} CHECK-add1 indicates that this primitive may fail when applied to some element of a, as indeed it will. Finally, ERROR-add1 indicates that this occurrence of add1 never succeeds—if it is ever reached, it will fail.

2.1 Presentation Types

Our type checker infers types in an encoded representation that reduces a limited form of subtyping to polymorphism. Soft Scheme decodes these types into more natural presentation types for programmers. Presentation types can precisely describe a rich collection of subsets of the data domain, yet they are simple enough for non-expert programmers to interpret. Conventional Hindley-Milner type systems form types from constants (e.g. num, nil), constructors (e.g. cons, −>), and type variables (X ). Our presentation types also include recursive types and a restricted form of union type.

Every presentation type is a union of a finite number of type constants and type constructions, collectively called prime types. A type may also include a single type variable:

(Type)  T ::= (+ P_{1} … P_{n}) | (+ P_{1} … P_{n} X)
(Prime Type) P ::= num | nil | … | (cons T_{1} T_{2}) | (T_{1} … T_{n} −> T) | N
(Place Holder) N ::= (not num) | (not nil) | … | (not cons) | (not −>)

We call the constants and constructors forming prime types tags, since they correspond to the type tags manipulated by typical implementations of dynamically typed languages.

Types must satisfy two restrictions. First, each tag may be used at most once within a union. This requirement precludes types like (+ (cons true false) (cons false true)); the less precise type (cons (+ true false) (+ true false)) must be used instead. Second, the same set of tags must always precede a particular type variable. For example, when (+ num nil (cons T_{1} T_{2}) X1) appears as the type of some program variable or expression, every other type in which X1 appears must list the tags num, nil, cons, and no others. Special constructions called place holders may be used to meet this requirement in types like ((+ false X2) −> (+ (not false) X2)). This requirement ensures that the range of a type variable excludes any types built from preceding tags. When a type variable is the sole element of a union, it ranges over all types. We then write X rather than (+ X).

3The primitive car extracts the first component of a pair. Its only valid input is a pair, but b’s type (list num) = (rec ([Y (+ nil (cons num Y))]) Y) includes nil.

Recursive types are introduced by first-order recursion equations:

(Recursive Type)  R ::= (rec ([X_{1} T_{1}] … [X_{n} T_{n}]) T) | T

The type (rec ([Y1 (+ nil (cons X Y1))]) Y1) is the type of proper lists containing elements of type X . This type occurs so frequently that we abbreviate it (list X). By convention, we name recursive type variables Yn.

Following are the types for a few well-known Scheme functions:

map  : ((X1 −> X2) (list X1) −> (list X2))
member : (X1 (list X2) −> (+ false (cons X2 (list X2))))

read : (rec ([Y1 (+ num nil … (cons Y1 Y1))]) (−> (+ eof num nil … (cons Y1 Y1))))

lastpair : (rec ([Y1 (+ (cons X1 Y1) X2)])

((cons X1 Y1) −> (cons X1 (+ (not cons) X2))))

The higher-order function map takes a function f of type (X1 −> X2) and a list l of type (list X1), and applies f to every element of l. It returns a list of the results. Function member takes a key x and a list l, and searches l for an occurrence of x. It returns the first sublist starting with element x if one exists; otherwise, it returns false. Procedure read parses an “s-expression” from an input device, returning an end-of-file object of type eof if no input is available. Finally, lastpair returns the last pair of a non-empty list. Appendix A contains more detailed examples.

2.2 Performance

Soft Scheme inserts run-time type checks only at uses of primitive operations that cannot be proven safe. Figure 1 summarizes run-time checking for the Scheme versions of the Gabriel Common Lisp bench marks.^{4} The percentages indicate how frequently our system inserts run-time checks compared to conventional compilers. The static frequency indicates the incidence of run-time checks inserted in the source code. The dynamic frequency indicates how often the inserted checks are executed. Note that Cpstak, Tak, and Takr are statically typable in our system and hence require no run-time checks at all.

Figure 2 indicates the real speedup that Soft Scheme can achieve over a high quality Scheme compiler (Chez Scheme 4.1t on an unloaded SparcStation 1). We have computed speedup with reference to Chez Scheme’s optimize-level 2 which performs maximum optimization while retaining safety. The potential speedup is the maximum obtainable speedup, achieved by ruthlessly discarding all run-time checks (optimize-level 3).^{5} The

4Obtained from the Scheme Repository at nexus.yorku.ca.

5Optimize-level 3 still retains argument count checks and some checks in primitives like assoc and member.

Static Frequency  Dynamic Frequency 0%  50  100% 0%  50  100% Boyer  •  Boyer • Browse  •  Browse  • Cpstak •  Cpstak • Ctak •  Ctak • Dderiv  •  Dderiv • Deriv  •  Deriv • Destruct  •  Destruct • Div •  Div  • Fft  •  Fft  • Puzzle •  Puzzle • Tak •  Tak • Takl  •  Takl  • Takr •  Takr • Traverse  •  Traverse  •

Figure 1: Reduction in Run-Time Checking for the Gabriel Bench Marks

0% 50

100%

□ potential ; • achieved

Boyer □ •

Browse □ •

Cpstak □ •

Ctak □ •

Dderiv □ •

Deriv □ •

Destruct

□

•

Div □ •

Fft □ •

Puzzle □ •

Tak □ •

Takl □ •

Takr □ •

Traverse

□

•

Figure 2: Speedup for the Gabriel Bench Marks

achieved speedup indicates the performance the soft typed program achieves without sacrificing safety. Puzzle illustrates the dramatic benefit (70% speedup) that can be obtained by removing run-time type checks from inner loops.

Soft Scheme significantly decreases run-time checking for all of the bench marks, even though these programs were not written with soft typing in mind. This reduction does not always lead to a significant performance improvement; it depends on how often the code containing the eliminated checks is executed. Programs like Browse and Traverse, for example, do not expose enough type information to enable the type checker to remove critical run-time checks from inner loops. As we discuss later, we have developed several extensions to Scheme that facilitate more precise type inference. By using these extensions, we can develop programs that avoid run-time checks where performance is critical.

3 Formal Framework

As the first step in a formal description of our soft type system, we define an idealized, dynamically typed, call-by-value language embodying the essence of Scheme. Core Scheme has the following abstract syntax:

(Exp)  e ::= v | (ap e_{1} e_{2}) | (CHECK-ap e_{1} e_{2}) | (let ([x e_{1}]) e_{2})
(Val)  v ::= c | x | (lambda (x) e)

where x ∈ Id are identifiers and c ∈ Const are constants. Const includes both basic constants (numbers, #t, #f, ’()) and primitive operations (add1, not, cons, car, etc). The keywords ap and CHECK-ap introduce unchecked and checked applications (explained below). Programs are closed expressions.

Core Scheme includes both unchecked and checked versions of every primitive operation. Invalid applications of unchecked primitives, like (ap add1 #t) or (ap car ’()), are meaningless. In an implementation, they can produce arbitrary results ranging from “core dump” to erroneous but apparently valid answers. Checked primitives are observationally equivalent to their corresponding unchecked versions, except that invalid applications of checked primitives terminate execution with the answer error. For example, (ap CHECK-add1 #t) yields error. Similarly, ap and CHECK-ap introduce unchecked and checked applications that are undefined (resp. yield error) when their first subexpression is not a procedure. Appendix B contains a formal operational semantics for Core Scheme.

Designing a soft type system for Core Scheme is a challenging technical problem. Conventional Hindley-Milner type systems are too weak to infer precise types for dynamically typed languages because they presume that monotypes are disjoint. In contrast, values in dynamically typed programs belong to many different types, and dynamically typed programs routinely exploit this fact. The next two subsections define a collection of static types and a static type inference system that permits many union types to be expressed as terms in a free algebra, just like conventional Hindley-Milner types. Flag variables enable polymorphism to encode subtyping as subset on union types. The third subsection indicates how to translate these more general types into presentation types. The last subsection adapts this static type system to a soft type system for Core Scheme.

3.1 Static Types

To construct a static type system for Core Scheme, we partition the data domain into disjoint subsets called prime types. The partitioning is determined by the domain equation defining the data domain D for Core Scheme:^{6}

D = D_{num} ⊕ D_{true} ⊕ D_{false} ⊕ D_{nil} ⊕ (D ⊗ D) ⊕ [D →_{sc} D]_{⊥} .

Each domain constant on the right hand side of the equation identifies a prime type. Similarly, each application of a domain constructor to domains identifies a prime type.

Our static types reflect the partitioning of the data domain. Every static type (σ, τ) is a disjoint union of zero or more prime types (κ^{f} σ⃗) followed by either a single type variable (α) or the empty type (ø):

κ_{1}^{f_{1}}σ⃗_{1} ∪ … ∪ κ_{n}^{f_{n}}σ⃗_{n} ∪ (α | ø)

6⊕ denotes the coalesced tagged sum of two Scott domains, ⊗ denotes strict Cartesian product, →_{sc} is the strict continuous function space constructor, and [ ]_{⊥} is the lifting construction on domains.

where κ ∈ Tag = {num, true, false, nil, cons, →}. Each prime type has a flag (f) that indicates whether the prime type is part of the union type. A flag indicates the prime type is present, indicates that it is absent, and a flag variable (φ) indicates the prime type may be present or absent depending on how the flag variable is instantiated. For example:^{7}

num ∪ ø  means “numbers;”
num ∪ nil ∪ ø  means “numbers or ’();”
num ∪ nil ∪ α  means “numbers or α but not ’();”
(α → (true ∪ false ∪ ø)) ∪ ø means “procedures from α to boolean.”

To be well-formed, types must be tidy: each tag may be used at most once within a union. More precisely, a tidy type has the form:

(Type) σ^{X}, τ^{X} ::= α^{X} | ø^{X} | μα^{X}. τ^{X} | (κ^{f}σ_{1}^{∅} … σ_{n}^{∅})^{X} ∪ τ^{X∪{κ}}  (κ ∉ X)
(Flag)  f ::= φ | |
α, β ∈ TypeVar  φ ∈ FlagVar  X ∈ 2^{Tag}

where TypeVar and FlagVar are disjoint sets of type variables and flag variables. The arity n of each term (κ^{f}σ_{1}^{∅} … σ_{n}^{∅})^{X} is determined by the arity of the tag κ. The superscript labels (X) attached to types are sets of tags that are unavailable for use in the type, and ensure that types are tidy. For example, the phrase:

(num )^{∅} ∪ (num )^{{num}} ∪ …

is not a well-formed type because the term (num )^{{num}} violates the restriction κ ∉ X in the formation of unions. Top-level types have label ∅. We usually omit labels when writing types. Similarly, an implementation of the type system need not manipulate labels.

Types represent regular trees with the tags κ and tidy union operator ∪ as internal nodes. Recursive types μα. τ represent infinite regular trees. The type μα. τ binds α in τ. The usual renaming rules apply to the bound variable α, and we have μα. τ = τ[α ↦ μα. τ]. Recursive types must be formally contractive, i.e., phrases like μα. α are not types. The type μβ. nil ∪ (cons α β) ∪ ø, denoting proper lists of α, is a common recursive type.

To accommodate polymorphism and subtyping, we introduce type schemes. A type scheme ∀α⃗φ⃗. τ is a type with variables {α⃗φ⃗} bound in τ. We omit ∀ when there are no bound variables, hence types are a subset of type schemes. Type schemes describe sets of types by substitution for bound variables. A substitution S is a finite label-respecting^{8} map from type variables to types and from flag variables to flags. St means the simultaneous replacement of every free variable in the type or flag t by its image under S. A type τ′ is an instance of type scheme ∀α⃗φ⃗. τ under substitution S:

τ′ ≺_{S} ∀α⃗φ⃗. τ (≺)

if Dom(S) = {α⃗φ⃗} and Sτ = τ′. For example, ((num ∪ ø) → (num ∪ ø)) ∪ ø is an instance of ∀α. (α → α) ∪ ø under the substitution {α ↦ (num ∪ ø)}.

7We use infix notation and write (σ_{1} →^{f} σ_{2}) ∪ … rather than (→^{f} σ_{1}σ_{2}) ∪ … for procedure types.

8Mapping type variables to types with the same label, which preserves tidiness.

As Rémy [17, 18] discovered, polymorphism can encode a limited form of subtyping. In our framework, we use polymorphism to express supersets and subsets of types. The type scheme ∀α. num ∪ α may be instantiated to any type that is a superset of num ∪ ø:

num ∪ ø

num ∪ true ∪ ø

num ∪ true ∪ false ∪ ø

⋮

The type scheme ∀φ_{1}φ_{2}. num^{φ_{1}} ∪ nil ^{φ_{2}} ∪ ø may be instantiated to any type that denotes a subset of num ∪ nil ∪ ø. There are four such types:

num ∪ nil ∪ ø  num ∪ nil ∪ ø
num ∪ nil ∪ ø  num ∪ nil ∪ ø.

We use this ability to encode supersets and subsets in assigning types to basic constants and primitives. Basic constants and the outputs of primitives may have any type that is a superset of their natural type. Unchecked primitives require that their inputs be subsets of the largest allowable input types.

The function TypeOf maps the constants of Core Scheme to type schemes describing their behavior. The encoding of the unions within a type varies according to whether the union occurs in a negative (input) or positive (output) position. A position is positive if it occurs within the first argument of an even number of → constructors, and negative if it occurs within an odd number. With recursive types, a position can be both positive and negative; we assume that primitives do not have such types. For unchecked primitives, negative unions are encoded using variables for valid inputs and and ø for invalid inputs. Positive unions use for “present” outputs and variables for “absent” fields. For example:

TypeOf (0) = ∀α. num ∪ α
TypeOf (add1) = ∀α_{1}α_{2}φ. ((num^{φ} ∪ ø) → (num ∪ α_{1})) ∪ α_{2}
TypeOf (number?) = ∀α_{1}α_{2}α_{3}. (α_{1} → (true ∪ false ∪ α_{2})) ∪ α_{3}

Checked primitives have similar types to their unchecked counterparts, but never use or ø since they accept all values. For example,

TypeOf (CHECK-add1) = ∀α_{1}α_{2}α_{3}φ. ((num^{φ} ∪ α_{3}) → (num ∪ α_{1})) ∪ α_{2}.

3.2 Static Type Inference

Figure 3 defines a type inference system that assigns types to Core Scheme expressions. Type environments (A) are finite maps from identifiers to type schemes. A[x ↦ τ] denotes the functional extension or update of A at x to τ. F V (τ) returns the free type and flag variables of a type τ. F V extends pointwise to type environments. The typing A ⊢ e : τ states that expression e has type τ in type environment A.

Provided the types assigned by TypeOf agree with the semantics of Core Scheme, we can prove that our static type system is sound. Appendix B defines a reduction relation → ⟼ for which every program either: (i) yields an answer v, (ii) diverges, (iii) yields error, or (iv) gets stuck (reaches a non-value normal form, like (ap add1 #t)). Type soundness ensures that typable programs yield answers of the expected type and do not get stuck.

(const) \frac{τ ≺_{S} TypeOf (c)}{A ⊢ c : τ} (var) \frac{τ ≺_{S} A(x)}{A ⊢ x : τ}

(ap) \frac{A ⊢ e_{1} : (τ_{2} →^{f} τ_{1}) ∪ ø  A ⊢ e_{2} : τ_{2}}{A ⊢ (ap e_{1} e_{2}) : τ_{1}}  (Cap) \frac{A ⊢ e_{1} : (τ_{2} →^{f} τ_{1}) ∪ τ_{3}  A ⊢ e_{2} : τ_{2}}{A ⊢ (CHECK-ap e_{1} e_{2}) : τ_{1}}

(lam) \frac{A[x ↦ τ_{1}] ⊢ e : τ_{2}}{A ⊢ (lambda (x) e) : (τ_{1} → τ_{2}) ∪ τ_{3}}  (let) \frac{A ⊢ e_{1} : τ_{1}  A[x ↦ Close(τ_{1}, A)] ⊢ e_{2} : τ_{2}}{A ⊢ (let ([x e_{1}]) e_{2}) : τ_{2}}
Close(τ, A) = ∀α⃗φ⃗. τ
where {α⃗φ⃗} ⊆ F V (τ) − F V (A)

Figure 3: Type Inference

Theorem 3.1 (Type Soundness) If ∅ ⊢ e : τ then either e diverges, or e → ⟼ error, or e → ⟼ v and ∅ ⊢ v : τ.

Proof. We use Wright and Felleisen’s technique based on subject reduction [24].

3.3 Translating to Presentation Types

The types assigned by this type system are awkward to read. To present more palatable types to the programmer, we define a translation into the succinct presentation type language introduced in Section 2.1. This translation eliminates (i) variables used to encode subtyping, and (ii) flags. Our decoding translation is a straightforward adaptation of that described by Cartwright and Fagan [4, 6].

3.4 Soft Type Checking

The preceding static type system can be used to statically type check Core Scheme programs. The type system will reject programs that contain incorrect uses of unchecked primitives, ensuring safe execution. But the type system will also reject some meaningful programs whose safety it cannot prove. To persuade the type checker to accept an untypable program, a programmer can manually convert it to typable form by judiciously replacing some unchecked operations with checked ones.^{9} A soft type checker automates this process.

Figure 4 defines a soft type inference system for Core Scheme programs. This system both assigns types and computes a transformed expression in which some unchecked primitives and applications are replaced by checked ones. A soft typing A ⊢_{s} e ⇒ e′ : τ states that in type environment A, the expression e transforms to e′ of type τ.

The function SoftTypeOf assigns type schemes to constants. For checked primitives and basic constants, SoftTypeOf assigns the same type schemes as TypeOf . For unchecked primitives, SoftTypeOf assigns type schemes that include special variables called absent

9The same process cannot be used with statically typed languages like ML because the Hindley-Milner type discipline provides insufficient monotypes. One must also add explicit definitions of union and recursive types, injections into these types, and projections out of them. The extra injections and projections increase the conceptual complexity of programs and introduce additional run-time overhead.

(const) \frac{τ ≺_{S} SoftTypeOf (c)}{A ⊢_{s} c ⇒ (empty\{Sν̃ | ν̃ ∈ Dom(S)\} → c, CHECK-c) : τ} (var) \frac{τ ≺_{S} A(x)}{A ⊢_{s} x ⇒ x : τ}

(ap) \frac{A ⊢_{s} e_{1} ⇒ e′_{1} : (τ_{2} →^{f} τ_{1}) ∪ τ̃_{3} A ⊢_{s} e_{2} ⇒ e′_{2} : τ_{2}}{A ⊢_{s} (ap e_{1} e_{2}) ⇒ ((empty\{τ̃_{3}\} → ap, CHECK-ap) e′_{1} e′_{2}) : τ_{1}}

(Cap) \frac{A ⊢_{s} e_{1} ⇒ e′_{1} : (τ_{2} →^{f} τ_{1}) ∪ τ_{3} A ⊢_{s} e_{2} ⇒ e′_{2} : τ_{2}}{A ⊢_{s} (CHECK-ap e_{1} e_{2}) ⇒ (CHECK-ap e′_{1} e′_{2}) : τ_{1}}

(lam) \frac{A[x ↦ τ_{1}] ⊢_{s} e ⇒ e′ : τ_{2}}{A ⊢_{s} (lambda (x) e) ⇒ (lambda (x) e′) : (τ_{1} → τ_{2}) ∪ τ_{3}}

(let) \frac{A ⊢_{s} e_{1} ⇒ e′_{1} : τ_{1} A[x ↦ SoftClose(τ_{1}, A)] ⊢_{s} e_{2} ⇒ e′_{2} : τ_{2}}{A ⊢_{s} (let ([x e_{1}]) e_{2}) ⇒ (let ([x e′_{1}]) e′_{2}) : τ_{2}}

SoftClose(τ, A) = ∀α⃗φ⃗. τ
where {α⃗φ⃗} ⊆ F V (τ) − (F V (A) ∪ AbsTypeVar ∪ AbsFlagVar)

Figure 4: Soft Type Inference

variables (ν̃). Absent variables record uses of unchecked primitives that may not be safe. Wherever the function TypeOf places a flag or ø term in the input type of a primitive, SoftTypeOf places a corresponding absent flag variable φ̃ ∈ AbsFlagVar or absent type variable α̃ ∈ AbsTypeVar. For example,

SoftTypeOf (add1) = ∀α_{1}α_{2}α̃_{3}φ. ((num^{φ} ∪ α̃_{3}) → (num ∪ α_{1})) ∪ α_{2}.

If an absent variable is instantiated to a non-empty type in the type assignment process then the corresponding primitive application must be checked. For example, the expression (ap add1 #t) instantiates the absent variable α̃_{3} in the type of add1 as (at least) true ∪ ø. Since true ∪ ø is not empty, this application of add1 must be checked. In contrast, the expression (ap add1 0) instantiates α̃_{3} as ø, so no run-time check is necessary. The function empty used by rules const and ap in Figure 4 determines whether every member of a set of types is empty. This is a simple syntactic test for the absence of flags.

To ensure that non-empty argument types propagate through intervening let-expressions to primitives that may require run-time checks, absent variables are not generalized by SoftClose. Hence, substitutions map absent flag variables to absent flags (f̃) and absent type variables to absent types (τ̃):

f̃ ∈ {f | F V (f) ⊂ AbsFlagVar}
τ̃ ∈ {τ | F V (τ) ⊂ (AbsFlagVar ∪ AbsTypeVar)}.

A simple example demonstrates why this restriction is necessary. The expression:

(let ([inc add1]) (ap inc #t))

requires add1 to be checked because it is applied to the value #t. In typing this expression, add1 is assigned type ((num^{φ′} ∪ α̃′) → …) where α̃′ and φ′ are fresh variables. Suppose SoftClose generalized absent variables. Generalizing the type of add1 would yield type scheme ∀α̃′′φ′′. ((num^{φ′′} ∪ α̃′′) → …) for inc. In typing the application (ap inc #t), α̃′′ would be instantiated as true ∪ β. However, instantiating α̃′′ would not affect α̃′ in the type of add1, so no run-time check would be inserted. Section 4.3 describes a better method of inserting checks that allows absent variables to be generalized.

Appendix C presents a Correspondence theorem to establish the correctness of this soft type system.

4 Practical Implementation

A practical soft type system must address the features of a real programming language. This section extends our simple soft type system to R4RS Scheme. We also present two extensions to Scheme that enable more precise type inference, and discuss several problems.

4.1 Typing Scheme

Scheme procedures may have a fixed arity or accept an unlimited number of arguments. Certain primitives also accept trailing optional arguments. We encode procedure types with the binary constructor −>∗ whose first argument is an argument list. Argument lists are encoded by the binary constructor arg and the constant noarg. Hence the type (X1 X2 X3 −> X4) merely abbreviates ((arg X1 (arg X2 (arg X3 noarg))) −>∗ X4). Variable arity procedure types use recursive argument lists. A consequence of this encoding is that run-time checks caused by applying procedures to the wrong number of arguments are distinguished from other run-time checks. CHECK-lambda is inserted where a lambdaexpression requires argument count checking. In practice, we find that such argument count checks often indicate program errors.

Assignment and the continuation operator call/cc are important features of Scheme. There are several solutions to typing assignment and continuations in a polymorphic framework. Our prototype uses the simplest method which restricts polymorphism to letexpressions where the bound expression is a syntactic value [23]. For Scheme, all expressions are values except those that contain an application of a non-primitive function or an “impure” primitive (like cons or call/cc).

In our prototype, call/cc has the type (((X1 −> X2) −> X1) −> X1). A use of call/cc may require a run-time check for either of two reasons: (i) the value to which call/cc is applied (of type ((X1 −> X2) −> X1)) is not a procedure of one argument; or (ii) the continuation obtained (of type (X1 −> X2)) is not treated as a procedure of one argument. The first case is handled as usual by inserting CHECK-call/cc. To address the second case, we replace each occurrence of call/cc in the program with the expression:

(lambda (v) (call/cc (lambda (k) (v (lambda (x) (k x))))))

This transformation, a composition of three η-expansions, introduces an explicit lambdaexpression for the continuation. The expression (lambda (x) (k x)) will be checked if the continuation may be mistreated.

A Scheme program is a sequence of definitions that may refer forwards or backwards to other definitions. To obtain polymorphism for definitions, we topologically sort the program’s definitions into strongly connected components. The components form a tree that may be organized into nested letrec-expressions and typed in the usual manner.

4.2 Extensions to Scheme

Our prototype includes two natural extensions to Scheme that enable more precise type assignment. Pattern matching enables the type checker to “learn” from type tests. For example, in the expression:

(let ([x 1]) (if (pair? x) (car x) 2))

no check should be necessary at car. However, as our type system assigns types to variables, the occurrence of x in (car x) has the same type as every other occurrence of x. This type includes num, hence a run-time check is inserted. In contrast, the equivalent code:^{10}

(let ([x 1]) (match x [(a . ) a] [ 2])

couples the type test to the decomposition of x. By extending the type system to directly type pattern matching expressions, we avoid the unnecessary run-time check. To improve the treatment of ordinary Scheme programs that do not use pattern matching, we translate simple forms of type testing if-expressions, like that above, into equivalent match-expressions.

Our second extension to Scheme is a type definition facility that allows the introduction of new type constructors. The expression:

(define-structure (Foo a b c))

defines constructors, predicates, selectors, and mutators for data of type (Foo ⋯). Programs that use type definitions are assigned more informative and more precise types than those that encode data structures using lists or vectors. A similar facility defines immutable data.

4.3 Problems

We have identified three problems with our system that result in imprecise typing.

Tidiness: Our tidy union types can express most common Scheme types. However, no decidable type system can express all computable subsets of the data domain. Five of the R4RS Scheme primitives do not have a tidy union type. These are: map and for-each for an arbitrary number of arguments; apply with more than two arguments; append when the last element is not a list; and make-vector without an initial value. All but the last can be handled by using an overly restrictive type and inserting unnecessary run-time checks. We prefer to ban uses of make-vector without an initial value. Overall, we feel that our type language provides a good balance between simplicity and expressiveness.

10The expression (match e [pat_{1} e_{1}] … [pat_{n} e_{n}]) compares the value of e against patterns pat_{1} … pat_{n}.

Any variables in the first matching pattern pat_{i} are bound to corresponding parts of the value of e, and e_{i} is evaluated in the extended environment. Pattern (pat_{1} . pat_{2}) matches a pair whose components match pat_{1} and pat_{2}. Pattern matches anything.

Reverse Flow: Several typing rules require that the types of two subexpressions be identical. For instance, if-expressions require their then- and else-clauses to have the same type:

\frac{A ⊢ e_{1} : τ_{1}  A ⊢ e_{2} : τ_{2}  A ⊢ e_{3} : τ_{2}}{A ⊢ (if e_{1} e_{2} e_{3}) : τ_{2}}

Also applications require the types of arguments to match the types the function expects (see rules ap and Cap in Figure 3). Consequently, type information flows both with and counter to the direction of value flow. Reverse flow can cause an inaccurate type to be inferred even though a more accurate tidy union type exists. For example, the function f:

(define f (lambda (x) (if P x #f)))

is inferred type ((false ∪ α_{1}) → (false ∪ α_{1})) ∪ α_{2}. The constant #f forces false into the type of x, and therefore into the input type of f. Hence the subtyping provided by polymorphism fails at applications of f. An argument to f is forced to include false in its type, even if that type would otherwise not include false . Were ((false^{φ} ∪ α_{1}) → (false ∪ α_{1})) ∪ α_{2} inferred for f, subtyping would work at uses of f.

The method of inserting run-time checks described in subsection 3.4 exacerbates the reverse flow problem. The insertion of a run-time check can cascade, forcing the insertion of many other unnecessary run-time checks. For example, the following program requires no run-time checks:

(let ([f add1]) (lambda (x) (f x) (* 2 x)))

In this program, f has type scheme ∀φα_{2}α_{3}. ((num^{φ} ∪ α̃) → (num ∪ α_{2})) ∪ α_{3}. Suppose we add the application (f #t) between (f x) and (* 2 x). Now the absent variable α̃ that is not generalized by the let-expression is replaced with true ∪ α̃′, and a run-time check is inserted at add1. But the input type of f is now num^{φ} ∪ true ∪ α̃′, hence reverse flow at the application (f x) forces the type of x to include true . Therefore * receives an unnecessary run-time check.

Our prototype avoids cascading by using a better technique to insert run-time checks. Absent variables are generalized by let-expressions in the same manner as ordinary variables. But whenever a generalized absent variable is instantiated, the instance type is recorded. A primitive requires a run-time check if any of the instance types of its absent variables are non-empty. An instance type is non-empty if it contains a -flag or if any of its instances are non-empty. The extra bookkeeping required for this technique is minimal. The improvement in typing precision and the attendant reduction in run-time checking can be significant.

We have also investigated several adaptations of structural subtyping [15] to address the reverse flow problem. Structural subtyping is more powerful than encoding subtyping with polymorphism as it permits subtyping at all function applications. By permitting more subtyping, soft type systems based on structural subtyping can infer more precise types. However, our experience to date with such systems has been disappointing. They yield only a small improvement in precision because existing extensions to recursive types [10, 22] do not yield principal types. This minor improvement comes at the cost of significantly less efficient type inference. We continue to investigate adaptations of structural subtyping.

Assignment: Because assignment interferes with polymorphism, and therefore with subtyping, assignment can be a major source of imprecision. Scheme includes both assignable variables, set by set!, and assignable pairs, set by set-car! and set-cdr!. Assignments to local variables seldom cause trouble. However, assignments to global variables or to pairs disable subtyping, and hence may cause the accumulation of large, inaccurate types. Using immutable pairs when possible adequately addresses the problem for set-car! and set-cdr!. At present, we have no satisfactory solutions for global variable assignments.

5 Related Work

Our practical soft type system is based on a soft type system designed by Cartwright and Fagan for an idealized functional language [4, 6]. Cartwright and Fagan discovered how to incorporate a limited form of union type in a Hindley-Milner polymorphic type system. Their method is based on an encoding technique Rémy developed to reduce record subtyping to polymorphism [17]. Their system has essentially the same types as Section 3.1 describes, except that all type variables must have label ∅. A type like ((false ∪α) → (false ∪α))∪ø where α has label {false} must instead be represented by enumerating all other tags in place of α:

(false ∪ num^{φ_{1}} ∪ … ∪ (cons^{φ_{n}} α_{1} α_{2})) → (false ∪ num^{φ_{1}} ∪ … ∪ (cons^{φ_{n}} α_{1} α_{2}))

Such types are difficult to decode into a natural type language that does not use flags. The representation does not support incremental definition of new type constructors, and type inference is not particularly efficient because simple types can have large representations.

Aiken and Wimmers have recently developed a sophisticated soft type system for the functional language FL [1, 2]. Their system supports a rich type language including tidy unions, recursive types, subtype constraints, intersection types, and conditional types. While we have not yet had the opportunity to analyze their system in detail, it is clear that their system assigns more precise types to some programs than our system does. But both their timing results and the complexity of their algorithm indicate that it is much slower than ours. If their system can be extended to imperative languages (assignment and control) and implemented efficiently, it could serve as the basis for a stronger soft type system for Scheme.

Several researchers have developed static type systems that extend the Hindley-Milner type discipline by adding a maximal type ⊤ as the type of otherwise untypable phrases [7, 8, 16, 20, 21]. This framework is too imprecise to form the basis for a soft type system because it does not support union types or inferred recursive types. The frequency with which ⊤ is assigned as the type of a phrase prevents its use as a reliable indicator of potential program errors. Nevertheless, Henglein has used a formulation of static typing enhanced with ⊤ to eliminate many run-time checks from Scheme programs.

The designers of optimizing compilers for Scheme and Lisp have developed type analyzers based on data flow analysis [3, 11, 12, 13, 19]. The information gathered by these systems is important for program optimization, but it is much too coarse to serve as the basis for a soft type system. None of the systems infer polymorphic types and most infer types that are simple unions of type constants.

6 Future Work

We have developed the first practical soft type system for Scheme. Soft Scheme is available by anonymous FTP from titan.cs.rice.edu in file public/wright/soft.tar.Z. Our pattern matching and type definition extensions for Scheme, which may be used independently of Soft Scheme, are also available in file public/wright/match.tar.Z.

Our current implementation processes an entire program at once, inferring type information and inserting run-time checks throughout. As such, the system is not well suited to large scale software development. We are investigating soft module systems to enable separate type checking and compilation of different parts of a program.

Acknowledgements

Kent Dybvig extended Chez Scheme overnight to permit mixing checked and unchecked primitives. Without his assistance, we could not have observed real execution time speedup.

References

[1] Aiken, A., and Wimmers, E. L. Type inclusion constraints and type inference. Proceedings of the International Conference on Functional Programming Languages and Computer Architecture (1993), 31–41.

[2] Aiken, A., Wimmers, E. L., and Lakshman, T. K. Soft typing with conditional types. Proceedings of the 21st Annual Symposium on Principles of Programming Languages (January 1994), to appear.

[3] Beer, R. D. Preliminary report on a practical type inference system for Common Lisp. Lisp Pointers 1, 2 (1987), 5–11.

[4] Cartwright, R., and Fagan, M. Soft typing. Proceedings of the SIGPLAN ’91 Conference on Programming Language Design and Implementation (June 1991), 278–292.

[5] Clinger, W., Rees, J., et al. Revised^{4} report on the algorithmic language Scheme. ACM Lisp Pointers IV (July-September 1991).

[6] Fagan, M. Soft Typing: An Approach to Type Checking for Dynamically Typed Languages. PhD thesis, Rice University, October 1990.

[7] Gomard, C. K. Partial type inference for untyped functional programs. Proceedings of the 1990 ACM Conference on LISP and Functional Programming (June 1990), 282–287.

[8] Henglein, F. Global tagging optimization by type inference. Proceedings of the 1992 ACM Conference on Lisp and Functional Programming (June 1992), 205–215.

[9] Hindley, R. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society 146 (December 1969), 29–60.

[10] Kaes, S. Type inference in the presence of overloading, subtyping and recursive types. Proceedings of the 1992 ACM Conference on Lisp and Functional Programming (June 1992), 193–204.

[11] Kaplan, M. A., and Ullman, J. D. A scheme for the automatic inference of variable types. Journal of the Association for Computing Machinery 27, 1 (January 1980), 128–145.

[12] Kind, A., and Friedrich, H. A practical approach to type inference in EuLisp. Lisp and Symbolic Computation 6, 1/2 (August 1993), 159–175.

[13] Ma, K. L., and Kessler, R. R. TICL—a type inference system for Common Lisp. Software Practice and Experience 20, 6 (June 1990), 593–623.

[14] Milner, R. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17 (1978), 348–375.

[15] Mitchell, J. C. Type inference with simple subtypes. Journal of Functional Programming 1, 3 (July 1991), 245–286. Preliminary version in: Coercion and Type Inference, Proc. 11th Annual Symposium on Principles of Programming Languages, 1984, pp. 175–185.

[16] O’Keefe, P. M., and Wand, M. Type inference for partial types is decidable. In Proceedings of the European Symposium on Programming, LNCS 582 (1992), Springer-Verlag, pp. 408–417.

[17] Rémy, D. Typechecking records and variants in a natural extension of ML. Proceedings of the 16th Annual Symposium on Principles of Programming Languages (January 1989), 77–87.

[18] Rémy, D. Type inference for records in a natural extension of ML. Tech. Rep. 1431, INRIA, May 1991.

[19] Shivers, O. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie Mellon University, May 1991. Also: Tech. Rep. CMU-CS-91-145.

[20] Thatte, S. R. Type inference with partial types. In Automata, Languages and Programming: 15th International Colloquium, LNCS 317 (July 1988), Springer-Verlag, pp. 615–629.

[21] Thatte, S. R. Quasi-static typing. Proceedings of the 17th Annual Symposium on Principles of Programming Languages (January 1990), 367–381.

[22] Tiuryn, J., and Wand, M. Type reconstruction with recursive types and atomic subtyping. In TAPSOFT ’93: Theory and Practice of Software Development (Berlin, Heidelber, New York, apr 1993), M.-C. Gaudel and J.-P. Jouannaud, Eds., Springer, pp. 686–701.

[23] Wright, A. K. Polymorphism for imperative languages without imperative types. Tech. Rep. 93-200, Rice University, February 1993.

[24] Wright, A. K., and Felleisen, M. A syntactic approach to type soundness. Tech. Rep. 91-160, Rice University, April 1991. To appear in: Information and Computation, 1994.

Appendices

A Examples

Following are some simple functions and their inferred types. None of these functions require run-time checks if they are passed arguments within their intended domain.

(define map ; apply a function to every element of a list

(lambda (f l)

(if (null? l)

’()

(cons (f (car l)) (map f (cdr l)))))) ;; ((Z1 −> Z2) (list Z1) −> (list Z2))

(define member ; search for a key in a list

(lambda (x l)

(match l [() #f]

[(y . rest) (if (equal? x y)

l

(member x rest))])))

;; (X1 (list X2) −> (+ false (cons X2 (list X2))))

(define lastpair ; find the last pair of a non-empty list

(lambda (s)

(if (pair? (cdr s))

(lastpair (cdr s))

s))) ;; (rec ([Y1 (+ (cons X1 Y1) X2)]) ;; ((cons X1 Y1) −> (cons X1 (+ (not cons) X2))))

(define subst* ; substitution for trees

(lambda (new old t)

(cond [(eq? old t) new]
[(pair? t) (cons (subst* new old (car t))

(subst* new old (cdr t)))]

[else t])))

;; (rec ([Y1 (+ (cons Y1 Y1) X1)]) ;; (Y1 X2 Y1 −> Y1))

(define append

(lambda l

(cond [(null? l) ()]

[(null? (cdr l)) (car l)]

[else (let loop ([m (car l)])
(if (null? m)

(apply append (cdr l))

(cons (car m) (loop (cdr m)))))])))

;; ((arglist (list X1)) −>∗ (list X1))

(define taut? ; test for a tautology

(lambda (x)

(match x [#t #t] [#f #f] [(? procedure?) (and (taut? (x #t)) (taut? (x #f)))])))

;; (rec ([Y1 (+ false true ((+ false true) −> Y1))]) ;; (Y1 −> (+ false true)))

;; from Aiken and Wimmers [2] (define Y ; least fixed point combinator

(lambda (f)

(lambda (y)

(((lambda (x) (f (lambda (z) ((x x) z)))) (lambda (x) (f (lambda (z) ((x x) z))))) y))))

;; (((X1 −> X2) −> (X1 −> X2)) −> (X1 −> X2)) (define last ; find last element of a list

(Y (lambda (f)

(lambda (x)

(if (null? (cdr x))

(car x)

(f (cdr x)))))))

;; ((cons Z1 (list Z1)) −> Z1)

B Operational Semantics

The following reduction relation specifies an operational semantics for Core Scheme (neglecting pairs, which are easy to add):

(let)  E[(let ([x v]) e)] ⟼ E[e[x ↦ v]]
(β_{v})  E[(apply (lambda (x) e) v)] ⟼ E[e[x ↦ v]]
(δ)  E[(apply c v)] ⟼ E[δ(c, v)] if c ∈ Prim and δ(c, v) ∈ Val
(wrong-prim)  E[(apply c v)] ⟼ error  if c ∈ Prim and δ(c, v) = error
(wrong-ap)  E[(CHECK-ap c v)] ⟼ error  if c ∉ Prim

where apply is either ap or CHECK-ap, and Prim ⊂ Const is the set of primitive operations. The reduction relation depends on a definition of evaluation contexts:

E ::= [] | (apply E e) | (apply v E) | (let ([x E]) e)

An evaluation context is an expression with one subexpression replaced by a hole, []. E[e] is the expression obtained by placing e in the hole of E. Our definition of evaluation contexts ensures that applications evaluate from left to right, as every non-value expression can be uniquely decomposed into an evaluation context and a redex.

The partial function δ : Prim × ClosedVal ⇀ (ClosedVal ∪ {error}) interprets the application of primitives. ClosedVal is the set of closed values; error is not a value. For all checked primitives CHECK-c, we require that δ(CHECK-c, v) be defined for all closed values v. For unchecked primitives, δ may be undefined at some arguments, and must never yield error. For corresponding pairs of unchecked and checked primitives (c, CHECK-c), we require that δ(c, v) and δ(CHECK-c, v) agree for all v, except that δ(c, v) is undefined when δ(CHECK-c, v) yields error:

δ(CHECK-c, v) = \{ \begin{matrix}δ(c, v) & if δ(c, v) ∈ ClosedVal \\ error & if δ(c, v) is undefined. \end{matrix}

When δ returns error for the application of a checked primitive, error immediately becomes the answer of the program via reduction wrong-prim. Similarly, checked applications of non-procedural values yield error via reduction wrong-ap.

With unchecked operations, evaluation can lead to a normal form that is neither a value nor error. Such normal forms arise when an unchecked primitive is applied to an argument for which it is not defined, e.g., (ap add1 #t), or when the first subexpression of an unchecked application is not a procedure, e.g., (ap 1 2). We say such an expression is stuck. Let → ⟼ be the reflexive and transitive closure of ⟼. Say that e diverges when there is an infinite reduction sequence e ⟼ e′ ⟼ e′′ ⟼ … All closed expressions either (i) yield an answer that is a closed value, (ii) diverge, (iii) yield error, or (iv) become stuck.

Lemma B.1 For closed expressions e, either e → ⟼ v where v is closed, e diverges, e → ⟼ error, or e → ⟼ e′ where e′ is stuck.

C Correspondence

To prove that the soft typed program and the original program are equivalent, recall that evaluation has four possible outcomes. A program may (i) yield an answer v, (ii) diverge, (iii) yield error, or (iv) get stuck. Let e ⊑ e′ mean that e′ may have more checked operations that e, but e and e′ are otherwise the same. Specifically, ⊑ is the reflexive, transitive, and compatible^{11} closure of the following relation:

c ⊑_{0} CHECK-c  \frac{e_{1} ⊑_{0} e′_{1}  e_{2} ⊑_{0} e′_{2}}{(ap e_{1} e_{2}) ⊑_{0} (CHECK-ap e′_{1} e′_{2})}

Soft type checking lifts invalid programs that get stuck to error.

Theorem C.1 (Correspondence) If ∅ ⊢_{s} e ⇒ e′ : τ then:

e → ⟼ v  ⇔ e′ → ⟼ v′  where v ⊑ v′;
e diverges  ⇔ e′ diverges;
e → ⟼ error or e gets stuck ⇔ e′ → ⟼ error.

Proof. We need two lemmas. The first shows that e′ has type τ in the static type system.

Lemma C.2 If A ⊢_{s} e ⇒ e′ : τ then A ⊢ e′ : τ.

This lemma is proved by induction over the structure of the deduction A ⊢_{s} e ⇒ e′ : τ.

Second, a program that has fewer checked operations performs the same evaluation steps, but may become stuck sooner.

Lemma C.3 (Simulation) For e_{1} ⊑ e′_{1}:

1. e_{1} ⟼ e_{2} ⇔ e′_{1} ⟼ e′_{2} where e_{2} ⊑ e′_{2};

2a. e_{1} ⟼ error ⇒ e′_{1} ⟼ error;  2b. e_{1} is stuck ⇒ (e′_{1} ⟼ error or e′_{1} is stuck);
3a. e′_{1} ⟼ error ⇒ (e_{1} ⟼ error or e_{1} is stuck); 3b. e′_{1} is stuck ⇒ e_{1} is stuck.

This lemma is proved by case analysis on the structure of the expressions.

With these lemmas, we can establish the theorem. From ∅ ⊢_{s} e ⇒ e′ : τ we have e ⊑ e′ by induction and case analysis of the rules in Figure 4. By induction with simulation:

1a. e → ⟼ v ⇔ e′ → ⟼ v′ where v ⊑ v′;  1b. e diverges ⇔ e′ diverges;
2a. e → ⟼ error ⇒ e′ → ⟼ error;  2b. e gets stuck ⇒ (e′ → ⟼ error or e′ gets stuck);
3a. e′ → ⟼ error ⇒ (e → ⟼ error or e gets stuck); 3b. e′ gets stuck ⇒ e gets stuck.

But ∅ ⊢ e′ : τ by Lemma C.2, hence by Type Soundness e′ cannot get stuck. Simplifying 2b and discarding 3b, we obtain the theorem.

11The compatible closure of a relation R is {(C[e_{1}], C[e_{2}])} for all (e_{1}, e_{2}) ∈ R and all contexts C. A context C is an expression with a hole in place of one subexpression.