Type Dispatch for Named Hierarchical Types ^{∗}

Neal Glew Cornell University

7 April 1999

Abstract

Type dispatch constructs are an important feature of many programming languages. Scheme has predicates for testing the runtime type of a value. Java has a class cast expression and a try statement for switching on an exception’s class. Crucial to these mechanisms, in typed languages, is type refinement: The static type system will use type dispatch to refine types in successful dispatch branches. Existing work in functional languages has addressed certain kinds of type dispatch, namely, intensional type analysis. However, this work does not extend to languages with subtyping nor to named types.

This paper describes a number of type dispatch constructs that share a common theme: class cast and class case constructs in object oriented languages, ML style exceptions, hierarchical extensible sums, and multimethods. I describe a unifying mechanism, tagging, that abstracts the operation of these constructs, and formalise a small tagging language. After discussing how to implement the tagging language, I present a more primitive language and give a formal translation from the tagging language.

1 Introduction

A number of programming languages allow dispatch on the runtime type of a value. For example, in Scheme [KCR98] there are predicates for testing if a value is the empty list, an integer, a pair, and so on. In many object oriented languages there are constructs for testing or switching on the class of an object.^{1} For example, Java [GJS96] has a cast expression and an exception catch mechanism for switching on the class of the exception object. The cast expression (classname)e tests whether e’s runtime class is in the hierarchy under the given class; if so, it refines e’s type to the given class; if not, an exception is thrown. The try statement try blk catch (classname_{1} x_{1}) blk_{1} ⋯ catch (classname_{n} x_{n}) blk_{n} executes blk, and if blk throws an exception, matches that exception against classname_{1} through classname_{n}. If classname_{i} is the first matching class, x_{i} is bound to the exception with type classname_{i}, and blk_{i} is executed. A final example of type dispatch is λ_{i}^{ML} [HM95, Mor95], the basis for an intermediate language in the TIL compiler [TMC^{+}96]. The λ_{i}^{ML} calculus has a typecase construct for determining the outermost type constructor of an unknown type. The typecase construct is used to implement specialised data representations in the presence of polymorphism and for writing polymorphic print and marshaling functions.

∗This material is based on work supported in part by the NSF grant CCR-9708915, AFOSR grant F49620-97-1-0013, and ARPA/RADC grant F30602-1-0317. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author and do not reflect the views of these agencies.

1Classes are closely related to runtime types; I will often use a class when I mean the corresponding type.

Scheme’s type predicates make the language much more expressive. Java’s implementation of exceptions crucially relies upon a class matching mechanism. The TIL compiler’s use of runtime type examination leads to significant optimisation benefits. The importance of type dispatch constructs justifies seeking formal foundations for them.

In typed languages, type refinement is a key property of type dispatch constructs: After switching on the runtime type of a value, that value’s static type changes to reflect the type being compared against. Consider the Java code (note that FileNotFound is a subclass of IOException, which is a descendant of Throwable):

          try { throw new FileNotFound(); } catch (IOException x) blk;

The try body throws an exception that has runtime type FileNotFound, but Java’s type rule for try gives the exception static type Throwable. The exception matches against the catch clause, and x is bound to the exception with static type IOException, a refinement of Throwable. A similar sort of refinement occurs in λ_{i}^{ML}. For example, consider:

Λα.λx:α.typecase α of α_{1} × α_{2} ⇒ e_{1} | …

x initially has static type α, but in expression e_{1} it is refined to α_{1} × α_{2}.

While type dispatch constructs in functional languages have been studied formally [HM95, Mor95, CWM98, CW99, etc.], this work does not extend to object oriented languages as it neglects two important features: subtypes and the creation of “new” (i.e. generative) types. To my knowledge, this paper is the first to formalise type dispatch constructs common in object oriented languages. The tagging language I will define handles both features mentioned above, and is quite general: It explains class cast and class case constructs in object oriented languages, ML style exceptions, and hierarchical extensible sums, and could be used in a typed compilation of multidispatch languages such as Cecil [Cha97].

Languages with type dispatch pose another problem. Consider compiling type dispatch to Typed Assembly Language [MWCG98, MCG^{+}99]. Since TAL does not have type dispatch primitives, the compiler writer has to design data structures and algorithms to use these data structures to perform type dispatch. Furthermore, these data structures and algorithms have to type check. TAL’s current type system is not expressive enough to type check a typical implementation. To address this inexpressiveness, this paper defines a typed target language without type dispatch primitives and a formal translation. Correctness theorems for the translation are stated and proven in a companion technical report [MCG^{+}99]. I used the key ideas in the target language to extend TAL [MCG^{+}99] so that the type dispatch mechanism described in this paper can be compiled to TAL; these extensions were straightforward. This result is significant for without it, type directed compilers must keep type dispatch as a primitive, and language based security must include type dispatch primitives (as the Java Virtual Machine does).

In the remainder of the paper, I will develop the tagging language mentioned earlier and discuss its implementation. I begin by describing in more detail the programming language constructs being addressed. From these constructs I extract a common theme, and define a small tagging language that abstracts their fundamental operation. Next, I informally discuss how this language could be implemented and the typing issues that arise. This leads to a formal target language and a formal translation from the tagging language to the target language. Finally, I describe some extensions.

2 Four Type Dispatch Constructs

Consider the following four language constructs:

Class Casting and Class Case: In Java, and in other class based languages, objects are created by instantiating a class, and that class is stored in the object when it is created. Java has a downcasting operation (c)e that evaluates e to an object and then tests to see if that object’s class is in the subhierarchy under class c. If so, the cast expression evaluates to the object but at the type implied by c, which is generally a refinement of e’s type. If not, an exception is thrown. More generally, these languages might provide a class case mechanism for testing membership in one of several classes. Java has this operation for the particular case of handling exceptions.

Exceptions: At first glance, ML style exceptions might not seem related to downcasting but, in fact, there is a strong connection. Exception declarations are similar to classes in that they create a new exception name with an associated type. Exception packets, like objects, are created from an exception name, and that name is stored in the packet. Exception matching, then, is like downcasting: Known exception names are compared against the name in an exception packet, and successful comparisons allow access to the carried value at the type of the known exception name. Unlike classes, which are be arranged hierarchically, ML style exception names are not hierarchical. On the other hand, Java implements exception packets by using objects, and the declaration of new exception names is achieved by subclassing throwable.

Hierarchical Extensible Sums: ML style exception packets are an example of extensible sums. The exception type is like a giant sum type that can be extended by user declarations. Each user declared exception name is a new branch in the sum. A hierarchical extensible sum allows the sum branches to be arranged in a hierarchy. For example, a programmer might define a hierarchical extensible sum type for the primitives of a compiler intermediate language. She might define a constructor of this sum, intbin, for binary integer primitives, and then subconstructors under intbin for addition, subtraction, and so on. The intermediate language’s type checker could match against intbin, since all these primitives have the same type, whereas a code generator would match against the more specific constructors to determine the correct instruction to generate. Hierarchical extensible sum types are being considered for ML2000, and appear in the language Moby [FR99], a research vehicle for ML2000.

Multimethods: Java has single dispatch: Methods can be thought of as functions that are specialised on their first argument’s class. Multimethods (c.f. Cecil [Cha97]) are a generalisation of this paradigm: A multimethod is a function that is specialised on any, possibly all, of its arguments’ classes. Implementing multimethods requires calling specialised let F ailure = newtag(string) in // exception F ailure of string let ep1 = tagged(⟨F ailure,“unimplemented”⟩) in // ep1 = F ailure “unimplemented”

⋮ iftagof ep1 = F ailure then // match ep1 with

x.printf “Computation failed: %s” x // F ailure(x) -> ⋯ else

printf “Some other exception” // | -> ⋯ fi

Figure 1: Exceptions Coded in the Tagging Language

code after determining which specialisation applies. The latter could be implemented by comparing the arguments’ runtime classes against patterns of known classes. In a type directed compilation framework, when one of these comparisons succeeds, the types of the arguments must be refined to match the types required by the specialised code. These comparisons are instances of the class case construct described above.

The core mechanism in all of these examples is a tagging mechanism. Exception names, classes, and the constructors of an extensible sum are all examples of tags that are placed with or within values. Associated with these tags are types that correspond to the tagged values. The language has a tag if or a tag case construct with type refinement in the successful branches of the test(s). Furthermore, in the case of classes and hierarchical sums, the tags form a tag hierarchy and the associated types are in a subtype hierarchy parallel to the tag hierarchy. Often, the tests are not “is tag t_{1} equal to tag t_{2}” but “is tag t_{1} in the subhierarchy under tag t_{2}”. The tagging language described in the next section formalises this core mechanism.

3 A Tagging Language

This section describes a tagging language that abstracts the core operation of the type dispatch constructs described in the previous section. The desired operations are: tagging a value with a type tag, comparing the tag of a tagged value against known tags, and creating hierarchies of type tags. A new tag is created by one of two operations: newtag(τ) or subtag(e, τ). In both cases the new tag is for tagging values of type τ and has type tag(τ). The newtag(·) form creates a top level tag, and the subtag(e, ·) form creates a subtag of tag e. Values are tagged with the operation tagged(⟨e_{1}, e_{2}⟩) where e_{1} is the type tag, and e_{2} the value to be tagged. The result is a value of type tagged. Tagged values are compared against known tags with the operation iftagof e_{1} = e_{2} then x.b_{1} else b_{2} fi where e_{1} is a tagged value and e_{2} is a tag. Informally, the tag in e_{1} is extracted and compared, along with all its ancestors in the tag hierarchy, to e_{2}. If any ancestor is equal to e_{2}, b_{1} is executed with x bound to the value in e_{1}. Otherwise b_{2} is executed.

An example of how to use these operations to code exceptions appears in Figure 1. For expository purposes, the example uses some constructs not in the formal language.

The tagging language has the above operations plus n-tuples and functions with their usual Syntax:

Values  v ::= x | tagged(v) | fix f(x:τ_{1}):τ_{2}.b
Contexts  E ::= [] | subtag(E, τ) | tagged(E) | ⟨v⃗, E, e⃗⟩ | E.i | E e | v E |
iftagof E = e_{2} then x.b_{1} else b_{2} fi | iftagof v = E then x.b_{1} else b_{2} fi
Heap Values  h ::= (τ, ϵ) | (τ, x) | ⟨v⃗⟩
Heaps  H ::= x_{1} = h_{1}, …, x_{n} = h_{n}
Program States P ::= let H in e

Reduction Rules:

let H in E[I] ↦ let H′ in E[e]
I  e  H′  Side Conditions
newtag(τ)  x  H, x = (τ, ϵ) x fresh
subtag(y, τ)  x  H, x = (τ, y) x fresh
⟨v⃗⟩  x  H, x = I  x fresh
x.i  v_{i}  H  H(x) = ⟨v_{1}, …, v_{n}⟩; 1 ≤ i ≤ n
v_{1} v_{2}  b[f, x := v_{1}, v_{2}] H  v_{1} = fix f(x:τ_{1}):τ_{2}.b

iftagof tagged(x) = y

then z.b_{1} else b_{2} fi b_{1}[z := v] H H(x) = ⟨x′, v, v⃗⟩; tagchk^{H}(x′, y)

iftagof tagged(x) = y

then z.b_{1} else b_{2} fi  b_{2}  H  H(x) = ⟨x′, v, v⃗⟩; not tagchk^{H}(x′, y)

Tag checking:

tagchk^{H}(x, y) =^{def} (x = y) ∨ (H(x) = (τ, x′) ∧ tagchk^{H}(x′, y))

Figure 2: Source Language Operational Semantics

introduction and elimination forms. The syntax is:

Types τ, σ ::= tag(τ) | tagged | ⟨τ⃗⟩ | τ_{1} → τ_{2}
Terms e, b ::= x | newtag(τ) | subtag(e, τ) | tagged(e) | iftagof e_{1} = e_{2} then x.b_{1} else b_{2} fi |
⟨e⃗⟩ | e.i | fix f(x : τ_{1}) : τ_{2}.b | e_{1} e_{2}

The notation X⃗ denotes a vector of objects drawn from syntactic category X. The f and x in fix f(x:τ_{1}):τ_{2}.b bind in b and the x in iftagof e_{1} = e_{2} then x.b_{1} else b_{2} fi binds in b_{1}. I consider syntactic objects equal up to α-equivalence.

The operational semantics is given in Figure 2. The generation of new tags is modeled by an allocation style semantics (c.f. Morrisett et al. [MFH95]). In an allocation style semantics terms are evaluated in the presence of a heap, H. Heaps are intended to model the store, and they map variables to heap values h. Variables are like pointers into memory, and heap values are like the contents of the memory pointed to. An advantage of this model is that it captures identity: Different tags get different variables even if they tag the same type and have the same supertag. For the tagging language, heap values are either tuples of values, ⟨v⃗⟩, or tag definitions (τ, s) where τ is the type being tagged and s is the optional supertag (ϵ denotes the absence of a supertag).

The most interesting rule is the one for iftagof · = · then · else · fi. The comparison of a tag and its ancestors against a known tag is formalised by the predicate tagchk^{H}(x, y) where H contains the tag definitions, x the unknown tag, and y the known tag. The definition of this predicate essentially says that either x and y are the same tag or x has a supertag and the predicate holds for supertag. The recursiveness of this definition deserves further comment. As tag hierarchies are acyclic, I intend heaps to be nonrecursive (that is, a heap value can only refer to variables defined earlier in the heap). The operational semantics creates heap values that are nonrecursive, and the typing rules (discussed shortly) force typeable heaps to be nonrecursive. Given that heaps are nonrecursive, tagchk^{H}(x, y) should be considered an inductive definition in the depth of x in the tag hierarchy. If cyclic heaps are considered, we would need to decide what cycles in the tag hierarchy mean, and adjust the definition of tagchk^{·}(·, ·) accordingly. The rest of the semantics is fairly standard for a context and substitution based reduction semantics. Note that the semantics is deterministic, call by value, and left to right.

The typing rules appear in Figure 3, and consist of judgements for subtyping and expression, heap value, heap, and program state typing. Subtyping for tag and tagged types is trivial, and the subtyping for tuples and functions is standard. Note that reflexivity and transitivity of subtyping is derivable from the rules given. The rule for subtag requires that e be a tag for type τ′ and that τ be a subtype of τ′, the later ensures that types associated with tags form a subtype hierarchy in parallel to the tag hierarchy. The rule for tagged(e) requires that e be a pair of a type tag for τ and a value of type τ. The rule for iftagof e_{1} = e_{2} then x.b_{1} else b_{2} fi requires e_{1} to have type tagged, e_{2} to be a tag for σ, b_{1} to type check in a context with x of type σ, and b_{2} to type check.

The typing rules are sound with respect to the operational semantics. The proof uses the standard techniques, and the only interesting case is in the type preservation of a successful tag comparison. In that case, a tag of type tag(σ_{1}) is compared against one of type tag(σ_{2}). If the comparison succeeds, the next program state has the form b_{1}[z := v] where b_{1} has the desired type if z has type σ_{2}. However, v has type σ_{1}, so we need to show that ⊢_{S} σ_{1} ≤ σ_{2}, which follows from this lemma:

Lemma 3.1 If ⊢_{S} H : Γ, Γ ⊢_{S} x : tag(σ_{1}), Γ ⊢_{S} y : tag(σ_{2}), and tagchk^{H}(x, y) then ⊢_{S} σ_{1} ≤ σ_{2}.

4 Implementation

Real machines do not provide primitives like newtag(τ), subtag(e, τ), tagged(e), and iftagof e_{1} = e_{2} then x.b_{1} else b_{2} fi. Compiler writers must select data structures to represent the tags and algorithms to implement tag comparisons. The goal of this section is to formalise a typed translation of the tagging language to another language without the above primitives. For now, think of the target of this translation as a typical lambda calculus with physical pointer equality and some typing machinery that I will develop in this section. This typing machinery is general enough to type other less naive strategies as I sketch in Section 5, and can be added to other low level languages such as Typed Assembly Language [MWCG98, MCG^{+}99].

Consider first how a compiler would translate the example in Figure 1 ignoring types. To create the new tag F ailure the compiler would allocate a new heap block storing in it the optional Typing contexts Γ are lists x_{1} : τ_{1}, …, x_{n} : τ_{n}.

⊢_{S} τ_{1} ≤ τ_{2}

⊢_{S} tag(τ) ≤ tag(τ)  ⊢_{S} tagged ≤ tagged
{⊢_{S} τ_{i} ≤ σ_{i} \atop ⊢_{S} ⟨τ_{1}, …, τ_{m}⟩ ≤ ⟨σ_{1}, …, σ_{n}⟩} (m ≥ n)  \begin{matrix}⊢_{S} τ_{2} ≤ τ_{1} & ⊢_{S} σ_{1} ≤ σ_{2} \\ ⊢_{S} τ_{1} → σ_{1} ≤ τ_{2} → σ_{2} \end{matrix}

Γ ⊢_{S} e : τ

\begin{matrix}Γ ⊢_{S} e : τ_{1} & ⊢_{S} τ_{1} ≤ τ_{2} \\ Γ ⊢_{S} e : τ_{2} \end{matrix}  Γ ⊢_{S} x : τ (Γ(x) = τ)
Γ ⊢_{S} newtag(τ) : tag(τ)

Γ ⊢_{S} e : tag(τ′) ⊢_{S} τ ≤ τ′
Γ ⊢_{S} subtag(e, τ) : tag(τ)

Γ ⊢_{S} e : ⟨tag(τ), τ⟩ Γ ⊢_{S} tagged(e) : tagged

Γ ⊢_{S} e_{1} : tagged Γ ⊢_{S} e_{2} : tag(σ) Γ, x : σ ⊢_{S} b_{1} : τ Γ ⊢_{S} b_{2} : τ
Γ ⊢_{S} iftagof e_{1} = e_{2} then x.b_{1} else b_{2} fi : τ

(x ∉ dom(Γ))

{Γ ⊢_{S} e_{i} : τ_{i} \atop Γ ⊢_{S} ⟨e_{1}, …, e_{n}⟩ : ⟨τ_{1}, …, τ_{n}⟩}  {Γ ⊢_{S} e : ⟨τ_{1}, …, τ_{n}⟩ \atop Γ ⊢_{S} e.i : τ_{i}} (1 ≤ i ≤ n)
{Γ, f:τ_{1} → τ_{2}, x:τ_{1} ⊢_{S} b : τ_{2} \atop Γ ⊢_{S} fix f(x:τ_{1}):τ_{2}.b : τ_{1} → τ_{2}} (f, x ∉ dom(Γ))  \begin{matrix}Γ ⊢_{S} e_{1} : τ_{1} → τ_{2} & Γ ⊢_{S} e_{2} : τ_{1} \\ Γ ⊢_{S} e_{1} e_{2} : τ_{2} \end{matrix}

Γ ⊢_{S} h : τ ⊢_{S} H : Γ ⊢_{S} P : τ

Γ ⊢_{S} (τ, ϵ) : tag(τ)

Γ ⊢_{S} x : tag(τ′) ⊢_{S} τ ≤ τ′
Γ ⊢_{S} (τ, x) : tag(τ)

Γ ⊢_{S} v_{i} : τ_{i} Γ ⊢_{S} ⟨v_{1}, …, v_{n}⟩ : ⟨τ_{1}, …, τ_{n}⟩

\begin{matrix}⊢_{S} h_{1} : τ_{1} & … & x_{1} : τ_{1}, …, x_{n−1} : τ_{n−1} ⊢_{S} h_{n} : τ_{n} \\ ⊢_{S} x_{1} = h_{1}, …, x_{n} = h_{n} : x_{1} : τ_{1}, …, x_{n} : τ_{n} \end{matrix} (x_{1}, …, x_{n} distinct)

\begin{matrix}⊢_{S} H : Γ & Γ ⊢_{S} e : τ \\ ⊢_{S} let H in e : τ \end{matrix}

Figure 3: Source Language Typing Rules

supertag. To create the tagged value ep1 the compiler would create a pair consisting of F ailure and the literal string. So the first two lines might become:

let F ailure = ⟨none⟩ in let ep1 = ⟨F ailure,“unimplemented”⟩ in

To translate the last part of the example, the compiler would extract the tag in ep1, which is just a heap pointer, and compare it against F ailure. If they are equal x would be bound to the second component of ep1 and b_{1} executed. Otherwise, the supertag would be extracted and the process repeated until there is no supertag, in which case b_{2} would be executed. The translated code might be:

let z = ep1.1 in loop : if z = F ailure then let x = ep1.2 in b_{1}

else match z.1 with none → b_{2} | some(z′) → z := z′; goto loop

Now consider designing a type system to annotate the code above. The key difficulty is giving x the correct type. In general, the type of a tagged value like ep1 is unknown, yet if the comparison z = F ailure succeeds, the type of ep1.2 is string, and this fact is needed to give x type string. What makes this difficult is that z and F ailure are values unrelated to ep1. The target type system needs to do two things: First, it needs to generate type equalities from physical pointer comparisons; second, it needs to link z and ep1 together, so that type information generated by the comparison will change ep1’s type.

The solution is to introduce a new type for the values being used to implement type tags, and to use type variables to link tags to values being tagged. The target type tag(τ_{1}, τ_{2}) is similar to the tagging language tag type. However, where the tagging language hides the structure of the tag, the target language allows the user to specify the structure through the additional argument τ_{2}. In particular, a value v is in the type tag(τ_{1}, τ_{2}) if v also has type τ_{2} and the programmer declared v to be a tag for type τ_{1}. Continuing the example, F ailure is essentially a linked list with no data, which has type rec α.⟨α?⟩ (where τ? is an option type), except that the nodes are also tags for string. So F ailure has type rec α.tag(string, ⟨α?⟩). The tagged value ep1 is a pair of such a tag and a value except that the type of the value is abstracted, thus ep1 has type ∃β.⟨rec α.tag(β, ⟨α?⟩), β⟩. To get the initial value of z, ep1 is unpacked introducing β into the type context. Thus z has type rec α.tag(β, ⟨α?⟩). If z = F ailure succeeds then the type z tags and the type F ailure tags must be the same, that is, β is string. The target type system will use this in type checking let x = ep1.2 in b_{1}. Since ep1.2 has type β, which is string, x will get type the correct type.

Two complications arise with this basic scheme. The first concerns how to create values of type tag(τ_{1}, τ_{2}). Ideally, target code would just declare that a value of type τ_{2} was being used as a tag for τ_{1} with an operation tag(e, τ). However, this is unsound as the same value may be declared a tag for several types. To see this unsoundness consider the following malicious code:

let x_{1} = ⟨none⟩ in let x_{2} = tag(x_{1}, string) in let x_{3} = tag(x_{1}, float) in let y = ⟨x_{2}, “hello”⟩ in

The variables x_{1}, x_{2}, and x_{3} are all bound to the same heap value, a tuple with a single element none. However, the type system types x_{2} as a tag for strings and x_{3} as a tag for floats. The code uses x_{2} to created a tagged “hello” value, which is bound to y. Now consider the following innocent code:

fun foo[β](z : ⟨rec α.tag(β, ⟨α?⟩), β⟩) = if z.1 = x_{3} then sin(z.2) else 1.0 fi

The body of foo compares z.1 a tag for β to x_{3} a tag for float. Thus in the then branch z.2 is refined to type float and the sine computation type checks. However, suppose foo was applied to string and y. Since y.1 is x_{2} which equals x_{3}, the then branch is executed. But z.2 is a string and the sine computation fails. The target type system must ensure that x_{1} can be declared a tag of at most one type.

One way to ensure a value is declared a tag for at most one type, is to use a linear type system. If v is of linear type τ^{1}, then v can be “used” only once. Then it is sufficient for tag(e, τ) to require e : σ^{1} for some σ. However, this requires all the machinery of linear type systems in the target language. A simpler solution, pursued in this paper, is to allow tag(e, τ) only at points where new heap values are created. For example, ⟨e⃗⟩ creates a new heap value; the target operation tag(⟨e⃗⟩, τ) does the same thing but gives the result type tag(τ, ⟨τ⃗⟩) where e⃗ : τ⃗.

The other complication concerns the interaction between subtyping and tag types. Consider a subtag of F ailure, MyF ailure, that tags type string[10] (the type for strings of length 10).

(Note that string[10] is a subtype of string.) The translated code for MyF ailure is:

let MyF ailure = tag(⟨some(F ailure)⟩, string[10], in )

Consider how this type checks. As discussed before F ailure has type rec α.tag(string, ⟨α?⟩), and MyF ailure should have type rec α.tag(string[10], ⟨α?⟩). However, the right hand side above has type tag(string[10], ⟨(rec α.tag(string, ⟨α?⟩))?⟩). The later type would be an unrolling of the desired type if tag(string, …) was a subtype of tag(string[10], …). Thus it seems that in creating the data structures that implement type tags the tag type needs to be contravariant in its first argument.

However, making the tag type contravariant in the first argument is unsound for tag comparisons. Consider again, the code from above:

if z.1 = F ailure then let x = ep1.2 in b_{1} else … fi

Under the contravariant rule F ailure subsumes to a tag type for string[10], so the type system could type check let x = ep1.2 in b_{1} under the assumption that β is string[10]. Under this incorrect assumption, x has type string[10], but ep1.2 is actually a thirteen character string. Thus it seems that for tag comparisons the tag type should be at least invariant in its first argument (in fact, covariance is sound). Fortunately, the need for different subtyping behaviours arises in different situations: tag data structure creation and tag comparisons. Thus a variance mechanism (c.f. Abadi and Cardelli [AC96]) can be used to get each behaviour when it is needed.

Using these ideas, I present the target language in the next section, and then a translation from the tagging language to the target language in the following section.

4.1 Target Language

The target language combines the keys ideas of the previous section, tag types with a variance mechanism and physical pointer equality. The syntax is:

Types  τ, σ ::= α | tag^{ϕ}(τ_{1}, τ_{2}) | rec α.τ | ∃α.τ | τ? | ⟨τ⃗⟩ | τ_{1} → τ_{2}
Variances ϕ ::= + | − | ∘
Terms  e, b ::= x | tag(⟨e⃗⟩, τ) | if e_{1} = e_{2} then b_{1} else b_{2} fi |
roll^{τ} (e) | unroll(e) | pack[τ_{1}, e] as τ_{2} | unpack[α, x] = e_{1} in e_{2} |
none^{τ} | some(e) | if? e_{1} then x.b_{1} else b_{2} fi |
⟨e⃗⟩ | e.i | fix f(x : τ_{1}) : τ_{2}.b | e_{1} e_{2} | let x_{1} = e_{1} and x_{2} = e_{2} in e

The operation tag(⟨e⃗⟩, τ) creates a new tuple in the heap that can be used as a tag for the type τ; it has type tag^{∘}(τ, ⟨τ⃗⟩) where e⃗ : τ⃗. The type tag^{ϕ}(τ_{1}, τ_{2}) contains values of type τ_{2} that are used as tags for the type τ_{1}. The value in this type may have been created as a tag for a subtype of τ_{1} if ϕ is +, a supertype of τ_{2} if ϕ is −, but only τ_{1} if ϕ is ∘. Two values that tag types can be compared for physical pointer equality using the operation if e_{1} = e_{2} then b_{1} else b_{2} fi. This operation is asymmetric as it is intended to compare a tag for an unknown type, e_{1}, with a tag for a known type, e_{2}. If the two values are equal b_{1} is executed, and e_{2}’s tag type is used to refine e_{1}’s; otherwise b_{2} is executed. There are n-tuples and functions as before. In addition the translation will need recursive types, existentials, option types, and a parallel let form. The Syntax:

Values  v ::= x | roll^{τ} (v) | pack[τ_{1}, v] as τ_{2} | none^{τ} | some(v) | fix f(x : τ_{1}) : τ_{2}.b
Contexts  E ::= [] | tag(⟨v⃗, E, e⃗⟩, τ) | if E = e then b_{1} else b_{2} fi |
if v = E then b_{1} else b_{2} fi | roll^{τ} (E) | unroll(E) | pack[τ_{1}, E] as τ_{2} |
unpack[α, x] = E in e | some(E) | if? E then x.b_{1} else b_{2} fi |
⟨v⃗, E, e⃗⟩ | E.i | E e | v E | let x_{1} = E and x_{2} = e_{2} in e |
let x_{1} = v and x_{2} = E in e
Heap Values h ::= ⟨v⃗⟩ | tag(⟨v⃗⟩, τ)
Heaps  H ::= x_{1} = h_{1}, …, x_{n} = h_{n}
Programs  P ::= let H in e

Reduction Rules:

let H in E[I] ↦ let H′ in E[e]
I  e  H′  Side Conditions
⟨v⃗⟩ or tag(⟨v⃗⟩, τ)  x  H, x = I x fresh
if x = x then b_{1} else b_{2} fi  b_{1}  H
if x = y then b_{1} else b_{2} fi  b_{2}  H  x ≠ y
unroll(roll^{τ} (v))  v  H
unpack[α, x] = pack[τ_{1}, v] as τ_{2} in e e[α := τ_{1}, x := v] H
if? none^{τ} then x.b_{1} else b_{2} fi  b_{2}  H
if? some(v) then x.b_{1} else b_{2} fi  b_{1}[x := v]  H
x.i  v_{i}  H  H(x) = v or tag(v, τ)
1 ≤ i ≤ n, v = ⟨v_{1}, …, v_{n}⟩
v_{1} v_{2} b[f, x := v_{1}, v_{2}] H v_{1} = fix f(x : τ_{1}) : τ_{2}.b
let x_{1} = v_{1} and x_{2} = v_{2} in e′  e′[x_{1}, x_{2} := v_{1}, v_{2}] H

Figure 4: Target Language Operational Semantics

recursive and existential types are standard. An option type τ? is either the value none^{τ} or the value some(v) for some v : τ; the operation if? e_{1} then x.b_{1} else b_{2} fi can be used to discriminate the two. The let form could be defined in terms of tuples and functions, but was included to ease proving operational correctness.

The α in rec α.τ and ∃α.τ binds in τ; the α and x in unpack[α, x] = e_{1} in e_{2} binds in e_{2}; the x in if? e_{1} then x.b_{1} else b_{2} fi binds in b_{1}; the f and x in fix f(x:τ_{1}):τ_{2}.b bind in b; the x_{1} and x_{2} in let x_{1} = e_{1} and x_{2} = e_{2} in e bind in e.

The operational semantics is similar in spirit to the tagging language, and is given in Figure 4. Recall, that in an allocation style semantics, pointers are modeled by variables, and two pointers are equal if they are the same variable. Hence the rules for the if construct.

The static semantics appears in Figures 5 and 6. Note that a typing context of the form Δ, α ≤ τ must satsify the condition in parenthesis in the figure. This syntactic restriction ensures that all typing contexts are well formed, simplying the proof of soundness. The static semantics is straightforward except for the tagging constructs. First, values in the type tag^{ϕ}(τ_{1}, τ_{2}) also have type τ_{2}, and there is a specialised subsumption rule to reflect this. This rule is used to

Typing Contexts Δ ::= ϵ | Δ, α | Δ, α ≤ τ (ftv(τ) ⊆ Δ)
Value Contexts Γ ::= x_{1} : τ_{1}, …, x_{n} : τ_{n}
Δ ⊢_{T} τ (ftv(τ) ⊆ Δ)
{Δ ⊢_{T} τ \atop Δ ⊢_{T} τ ≤ τ}  \begin{matrix}Δ ⊢_{T} τ_{1} ≤ τ_{2} & Δ ⊢_{T} τ_{2} ≤ τ_{3} \\ Δ ⊢_{T} τ_{1} ≤ τ_{3} \end{matrix}  Δ ⊢_{T} α ≤ τ (α ≤ τ ∈ Δ)
Δ ⊢_{T} τ_{1} ≤ τ_{2} Δ ⊢_{T} σ_{1} ≤ σ_{2} Δ ⊢_{T} tag^{ϕ}(τ_{1}, σ_{1}) ≤ tag^{+}(τ_{2}, σ_{2}) (ϕ ∈ {+, ∘}) Δ ⊢_{T} τ_{2} ≤ τ_{1} Δ ⊢_{T} σ_{1} ≤ σ_{2} Δ ⊢_{T} tag^{ϕ}(τ_{1}, σ_{1}) ≤ tag^{−}(τ_{2}, σ_{2}) (ϕ ∈ {−, ∘})
Δ ⊢_{T} τ Δ ⊢_{T} σ_{1} ≤ σ_{2}
Δ ⊢_{T} tag^{∘}(τ, σ_{1}) ≤ tag^{∘}(τ, σ_{2})
Δ ⊢_{T} rec α.τ_{1} Δ ⊢_{T} rec β.τ_{2} Δ, β, α ≤ β ⊢_{T} τ_{1} ≤ τ_{2}

Δ ⊢_{T} rec α.τ_{1} ≤ rec β.τ_{2} (α ≠ β; α, β ∉ Δ)

{Δ, α ⊢_{T} τ_{1} ≤ τ_{2} \atop Δ ⊢_{T} ∃α.τ_{1} ≤ ∃α.τ_{2}} (α ∉ Δ)  {Δ ⊢_{T} τ_{1} ≤ τ_{2} \atop Δ ⊢_{T} τ_{1}? ≤ τ_{2}?}
{Δ ⊢_{T} τ_{i} ≤ σ_{i} \atop Δ ⊢_{T} ⟨τ_{1}, …, τ_{m}⟩ ≤ ⟨σ_{1}, …, σ_{n}⟩} (m ≥ n)  \begin{matrix}Δ ⊢_{T} τ_{2} ≤ τ_{1} & Δ ⊢_{T} σ_{1} ≤ σ_{2} \\ Δ ⊢_{T} τ_{1} → σ_{1} ≤ τ_{2} → σ_{2} \end{matrix}

Figure 5: Target Language Typing Rules for Types

manipulate the datastructure a type tag contains. There are two rules for tag comparison: one is for typing the translation and the other is for proving type preservation and soundness. Rule t1 requires that e_{1} be a tag for an unknown type, in fact, for a supertype of an unknown type. It also requires that e_{2} be a tag for a known closed type, again, actually a subtype of the known type. I assume that, as in Java and ML, that classes and exception names are always associated with closed types. If the tags are equal then they must be tags for a type between the unknown type and the known type, that is, the unknown type is a subtype of the known one. The then branch b_{1} is checked with this additional information.

During the actual execution of translated code, the unknown type α is replaced by a known closed type. Therefore, to prove the preservation of typing across the reduction that replaces α, rule t2 allows the comparison of two known types. If ϵ ⊢_{T} σ_{1} ≤ σ_{2} does not hold then it is impossible for e_{1} to be equal to e_{2}, therefore b_{1} is only type checked when this condition holds. In fact, b_{1} will probably not type check at all when this condition does not hold, as it may use values of type σ_{1} where σ_{2}’s are expected.

The static semantics is sound with respect to the operational semantics. The proof appears in Appendix A. Standard techniques are used in the proof and the only difficulty is with the tag comparison operation. In showing type preservation for a successful tag comparison I use the fact that ϵ; Γ ⊢_{T} x : tag^{−}(σ_{1}, τ_{1}) and ϵ; Γ ⊢_{T} x : tag^{+}(σ_{2}, τ_{2}) implies ϵ ⊢_{T} σ_{1} ≤ σ_{2}, this is lemma A.9. Then by rule t2 the then branch must type check. Another difficulty is with the type substitution lemma. In particular in proving that if α; Γ ⊢_{T} if e_{1} = e_{2} then b_{1} else b_{2} fi : τ and ϵ ⊢_{T} σ then ϵ; Γ[α := σ] ⊢_{T} if e_{1} = e_{2} then b_{1} else b_{2} fi[α := σ] : τ[α := σ]. If rule t1 is used with α; Γ ⊢_{T} e_{1} : tag^{−}(α, τ_{1}) used to show the hypothesis then the conclusion has to follow from rule t2. There must be a certain coherence between these two rules.

\begin{matrix}Δ; Γ ⊢_{T} e : τ_{1} & Δ ⊢_{T} τ_{1} ≤ τ_{2} \\ Δ; Γ ⊢_{T} e : τ_{2} \end{matrix}  Δ; Γ ⊢_{T} x : τ (Γ(x) = τ)
Δ; Γ ⊢_{T} e_{i} : τ_{i} Δ ⊢_{T} τ

Δ; Γ ⊢_{T} tag(⟨e_{1}, …, e_{n}⟩, τ) : tag^{∘}(τ, ⟨τ_{1}, …, τ_{n}⟩)

Δ; Γ ⊢_{T} e : tag^{ϕ}(τ, σ) Δ; Γ ⊢_{T} e : σ

[rule t1] ϵ ⊢_{T} σ Δ; Γ ⊢_{T} e_{1} : tag^{−}(α, τ_{1}) Δ; Γ ⊢_{T} e_{2} : tag^{+}(σ, τ_{2}) Δ_{1}, α ≤ σ, Δ_{2}; Γ ⊢_{T} b_{1} : τ Δ; Γ ⊢_{T} b_{2} : τ Δ; Γ ⊢_{T} if e_{1} = e_{2} then b_{1} else b_{2} fi : τ (Δ = Δ_{1}, α, Δ_{2})

[rule t2]

ϵ ⊢_{T} σ_{1}
ϵ ⊢_{T} σ_{2}

Δ; Γ ⊢_{T} e_{1} : tag^{−}(σ_{1}, τ_{1}) Δ; Γ ⊢_{T} e_{2} : tag^{+}(σ_{2}, τ_{2})

\begin{matrix}ϵ ⊢_{T} σ_{1} ≤ σ_{2} \\ ⇒ \\ Δ; Γ ⊢_{T} b_{1} : τ \end{matrix}

Δ; Γ ⊢_{T} b_{2} : τ
Δ; Γ ⊢_{T} if e_{1} = e_{2} then b_{1} else b_{2} fi : τ
Δ; Γ ⊢_{T} e : σ[α := τ] Δ; Γ ⊢_{T} roll^{τ} (e) : τ (τ = rec α.σ)  Δ; Γ ⊢_{T} e : τ Δ; Γ ⊢_{T} unroll(e) : σ[α := τ] (τ = rec α.σ)
Δ ⊢_{T} τ_{1} Δ; Γ ⊢_{T} e : τ_{2}[α := τ_{1}]
Δ; Γ ⊢_{T} pack[τ_{1}, e] as ∃α.τ_{2} : ∃α.τ_{2}
Δ; Γ ⊢_{T} e_{1} : ∃α.τ_{1} Δ, α; Γ, x : τ_{1} ⊢_{T} e_{2} : τ Δ ⊢_{T} τ

Δ; Γ ⊢_{T} unpack[α, x] = e_{1} in e_{2} : τ

(α ∉ Δ, x ∉ Γ)

Δ ⊢_{T} τ Δ; Γ ⊢_{T} none^{τ} : τ?

Δ; Γ ⊢_{T} e : τ
Δ; Γ ⊢_{T} some(e) : τ?
Δ; Γ ⊢_{T} e_{1} : σ? Δ; Γ, x : σ ⊢_{T} b_{1} : τ Δ; Γ ⊢_{T} b_{2} : τ

Δ; Γ ⊢_{T} if? e_{1} then x.b_{1} else b_{2} fi : τ

(x ∉ Γ)

{Δ; Γ ⊢_{T} e_{i} : τ_{i} \atop Δ; Γ ⊢_{T} ⟨e_{1}, …, e_{n}⟩ : ⟨τ_{1}, …, τ_{n}⟩}  {Δ; Γ ⊢_{T} e : ⟨τ_{1}, …, τ_{n}⟩ \atop Δ; Γ ⊢_{T} e.i : τ_{i}} (1 ≤ i ≤ n)
\begin{matrix}Δ ⊢_{T} τ_{1} → τ_{2} & Δ; Γ, f : τ_{1} → τ_{2}, x : τ_{1} ⊢_{T} b : τ_{2} \\ Δ; Γ ⊢_{T} fix f(x : τ_{1}) : τ_{2}.b : τ_{1} → τ_{2} \end{matrix} (f, x ∉ Γ)

\begin{matrix}Δ; Γ ⊢_{T} e_{1} : τ_{1} → τ_{2} & Δ; Γ ⊢_{T} e_{2} : τ_{1} \\ Δ; Γ ⊢_{T} e_{1} e_{2} : τ_{2} \end{matrix}

Δ; Γ ⊢_{T} e_{1} : τ_{1} Δ; Γ ⊢_{T} e_{2} : τ_{2} Δ; Γ, x_{1}:τ_{1}, x_{2}:τ_{2} ⊢_{T} e : τ

Δ; Γ ⊢_{T} let x_{1} = e_{1} and x_{2} = e_{2} in e : τ (x_{1}, x_{2} ∉ Γ)

\begin{matrix}ϵ; ϵ ⊢_{T} h_{1} : τ_{1} & … & ϵ; x_{1} : τ_{1}, …, x_{n−1} : τ_{n−1} ⊢_{T} h_{n} : τ_{n} \\ ⊢_{T} x_{1} = h_{1}, …, x_{n} = h_{n} : x_{1} : τ_{1}, …, x_{n} : τ_{n} \end{matrix} (x_{1}, …, x_{n} distinct)

\begin{matrix}⊢_{T} H : Γ & ϵ; Γ ⊢_{T} e : τ \\ ⊢_{T} let H in e : τ \end{matrix}

Figure 6: Target Language Typing Rules for Terms

4.2 Translation

The translation from the tagging language to the target language is given in Figure 7. It is based on the ideas I sketched earlier. The key to the type translation is the translation of tag types. A tag for type τ is translated to a tuple with a tag option, suggesting the type rec α.tag^{−}([[τ]]_{type}, ⟨α?⟩). This is not quite correct as the tag itself needs to be invariant, so the translation is actually one unrolling of this type with the outermost tag type invariant, tag^{∘}([[τ]]_{type}, ⟨(rec α.tag^{−}([[τ]]_{type}, ⟨α?⟩))?⟩), except the option type is shifted into the recursive type, tag^{∘}([[τ]]_{type}, ⟨rec α.tag^{−}([[τ]]_{type}, ⟨α⟩)?⟩). The translation of tagged is just a pair of a tag for α and an α abstracted over α. The operations newtag(τ), subtag(e, τ), and tagged(e) are translated as I described earlier modulo all the typing annotations needed for recursive types, option types, and existential types. The tagchk^{H}(x, y) predicate is reified as a recursive function, tagchk(y_{1}, y_{2}, τ, σ), that searches the superchain and then returns a σ option where σ is the known type. The translation of the tag comparison operation uses the let form to evaluate the arguments, then unpacks the tagged value, uses the reified tag check predicate to do the comparison, and then executes the appropriate translated branch.

Technically the translation is type directed as it needs type information in two places. Thus, the translation may not be defined for all source terms, but it is easy to show that it is defined for all typeable source terms. Furthermore, because the tag type is invariant it is easy to show that there is only one type possible in the places where type information is required, so the translation is coherent. Rather than present the translation as a acting on typing derivations, I have indicated the necessary type information with a : τ notation on the source terms.

The translation is both type preserving and operationally correct. Proving type preservation is a straight forward inductive proof, and appears in Appendix B. Because I carefully chose the tagging and target language semantics to match on common constructs, and through the use of the let construct, operational correctness can be proven by a simulation argument. Most of the work is in showing that the tag check is implemented properly. The proof appears in Appendix C.

5 Extensions

The implementation given is quite naive, it takes time linear in the height of the tag hierarchy. Java implementations typically trade space for time, and represent tags as an array of all of the tags ancestors. This implementation requires only one array subscript and one physical pointer equality test, but uses space proportional to height of the tag hierarchy, and it is not suitable for multiple inheritance hierarchies. Appendix D gives an extension of the target language, and shows how to express this optimised implementation strategy in the extended language. I expect that most schemes for implementing multiple inheritance hierarchies efficiently could also be expressed in variants of the target language.

The particular target language chosen is not crucial to implementing type tagging mechanisms. In fact, the key ideas were used to augment TALx86 [MCG^{+}99], a typed assembly language [MWCG98] for Intel’s IA32 architecture, to provide support for downcasting in object oriented languages and support for exceptions. This implementation was straightforward:

tag(ϕ, τ)  = tag^{ϕ}(τ, ⟨tag′(τ)⟩)
tag′(τ)  = rec α.tag^{−}(τ, ⟨α⟩)?
[[tag(τ)]]_{type}  = tag(∘, [[τ]]_{type})
[[tagged]]_{type}  = ∃α.⟨tag(−, α), α⟩
[[⟨τ_{1}, …, τ_{n}⟩]]_{type}  = ⟨[[τ_{1}]]_{type}, …, [[τ_{n}]]_{type}⟩
[[τ_{1} → τ_{2}]]_{type}  = [[τ_{1}]]_{type} → [[τ_{2}]]_{type}
[[x_{1}:τ_{1}, …, x_{n}:τ_{n}]]_{ctxt}  = x_{1}:[[τ_{1}]]_{type}, …, x_{n}:[[τ_{n}]]_{type}
[[x]]_{exp}  = x
[[newtag(τ)]]_{exp}  = tag(⟨roll^{tag′([[τ]]_{type})}(none^{tag(−,[[τ]]_{type})})⟩, [[τ]]_{type})
[[subtag(e, τ)]]_{exp}  = tag(⟨roll^{tag′([[τ]]_{type})}(some([[e]]_{exp}))⟩, [[τ]]_{type})
[[tagged(e : ⟨tag(τ), τ⟩)]]_{exp} = pack[[[τ]]_{type}, [[e]]_{exp}] as [[tagged]]_{type}
tagchk(y_{1}, y_{2}, τ, σ)  = fix y_{3}(y_{4} : tag(−, τ)) : σ?.
if y_{4} = y_{2} then some(y_{1}.2) else
if? unroll(y_{4}.1) then y_{5}.y_{3} y_{5} else none^{σ} fi fi

[[iftagof e_{1} = e_{2} : tag(σ)

then x.b_{1} else b_{2} fi]]_{exp}  = let x_{1} = [[e_{1}]]_{exp} and x_{2} = [[e_{2}]]_{exp} in unpack[α, y_{1}] = x_{1} in

if? tagchk(y_{1}, x_{2}, α, [[σ]]_{type}) y_{1}.1 then x.[[b_{1}]]_{exp} else [[b_{2}]]_{exp} fi

[[⟨e_{1}, …, e_{n}⟩]]_{exp}  = ⟨[[e_{1}]]_{exp}, …, [[e_{n}]]_{exp}⟩
[[e.i]]_{exp}  = [[e]]_{exp}.i
[[fix f(x:τ_{1}):τ_{2}.e]]_{exp}  = fix f(x:[[τ_{1}]]_{type}):[[τ_{2}]]_{type}.[[e]]_{exp}
[[e_{1} e_{2}]]_{exp}  = [[e_{1}]]_{exp} [[e_{2}]]_{exp}
[[(τ, ϵ)]]_{hval}  = tag(⟨roll^{tag′([[τ]]_{type})}(none^{tag(−,[[τ]]_{type})})⟩, [[τ]]_{type})
[[(τ, x)]]_{hval}  = tag(⟨roll^{tag′([[τ]]_{type})}(some(x))⟩, [[τ]]_{type})
[[⟨v_{1}, …, v_{n}⟩]]_{hval}  = ⟨[[v_{1}]]_{exp}, …, [[v_{n}]]_{exp}⟩
[[x_{1} = h_{1}, …, x_{n} = h_{n}]]_{heap} = x_{1} = [[h_{1}]]_{hval}, …, x_{n} = [[h_{n}]]_{hval}
[[let H in e]]_{prog}  = let [[H]]_{heap} in [[e]]_{exp}

Figure 7: The Translation

One type constructor was extended, and two instructions and the static data mechanism were changed to use this extended type constructor. The TALx86 implementation includes a compiler for a language called Popcorn, a safe C-like language. Popcorn has ML style exceptions, and the compiler was modified to use the new type tagging mechanisms instead of the old ad hoc mechanisms.

6 Related Work

This work is closely related to work on type dispatch in functional languages [HM95, Mor95, CWM98, CW99, etc.]. In particular, the work on λ^{R} [CWM98] and its follow-up LX [CW99] both address the implementation of λ_{i}^{ML} type dispatch. There are two key differences between their work and mine. First, my tagging language is concerned with matching whole types and their subtypes, whereas λ^{R} is concerned with matching the top level structure of types: is v in τ versus does v have an arrow type and what are “tags” for the argument and result type. To achieve the type refinement of my target language a λ^{R} implementation would have to crawl over the entire structure of a “tag” for the unknown type, whereas my language can make the refinement with one pointer equality test. Furthermore, their language does not handle subtyping. Second, my language is concerned with branded types whereas λ^{R} is concerned with the types themselves. Consider my informal coding of exceptions. In Ocaml there are at least three exceptions that carry strings. Therefore, there will be at least three tags for the type string, and the distinction between a string tagged with Failure and the same string tagged with Invalid argument is important. In the λ^{R} setting this distinction is irrelevant, only the fact that the value is a string is important. Of course, λ^{R} is designed to implement intensional polymorphism and does that well, whereas my language cannot implement intensional polymorphism.

7 Summary

This paper has shown that a number of language mechanisms, among them class casting, class casing, exceptions, and extensible hierarchical sums, share a common mechanism: type tagging. A tagging language containing this core mechanism was defined and then translated into a more primitive language with just the notion of values being tags for types and physical pointer equality. The type soundness of the target language and the type preservation and operational correctness of the translation was proven. Thus, this paper provides a solid theoretical foundation for all the mechanisms mentioned above. Along with the work in functional languages, this work provides foundations for a theory of type dispatch in programming languages.

References

[AC96] Martín Abadi and Luca Cardelli. A Theory Of Objects. Springer-Verlag, 1996.

[Cha97] Craig Chambers. The Cecil language, specification and rationale. Technical report, Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington 98195-2350, USA, March 1997.

[CW99] Karl Crary and Stephanie Weirich. Flexible type analysis. Technical report, Department of Computer Science, Cornell University, 4130 Upson Hall, Ithaca, NY 14853-7501, USA, 1999. Forthcom-

           ing, available at http://www.cs.cornell.edu/sweirich.

[CWM98] Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type-erasure semantics. In Third ACM SIGPLAN International Conference on Functional Programming, pages 301–312, Baltimore Maryland, USA, September 1998.

[FR99] Kathleen Fisher and John Reppy. The design of a class mechanism for Moby. In ACM SIGPLAN Conference on Programming Language Design and Implementation, May 1999. To appear. Moby

           information is available at http://www.cs.bell-labs.com/~jhr/moby.

[GJS96] James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, 1996.

[HM95] Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In Twenty-Second ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 130–141, San Francisco, CA, USA, January 1995.

[KCR98] Richard Kelsey, William Clinger, and Jonathan Rees. Revised^{5} report on the algorithmic language Scheme. ACM SIGPLAN Notices, 33(9):26–76, September 1998. With H. Abelson, N. I. Adams, IV, D. H. Bartley, G. Brooks, R. K. Dybvig, D. P. Friedman, R. Halstead, C. Hanson, C. T. Haynes, E. Kohlbecker, D. Oxley, K. M. Pitman, G. J. Rozas, G. L. Steele, Jr., G. J. Sussman, and M. Wand.

[MCG^{+}99] Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, Daivd Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic type assembly language. February 1999. Submitted to WCSSS’99, available at http://www.cs.cornell.edu/talc.

[MFH95] Greg Morrisett, Matthias Felleisen, and Robert Harper. Abstract models of memory management. In ACM Conference on Functional Programming and Computer Architecture, 1995.

[Mor95] Greg Morrisett. Compiling with Types. PhD thesis, Carnegie Mellon University, December 1995. Published as CMU Technical Report CMU-CS-95-226.

[MWCG98] Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In Twenty-Fifth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85–97, San Diego California, USA, January 1998.

[TMC^{+}96] David Tarditi, Greg Morrisett, Perry Cheng, Christopher Stone, Robert Harper, and Peter Lee. TIL: A type-directed optimizing compiler for ML. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 181–192, Philadelphia, PA, USA, May 1996.

A Type Soundness of Target Calculus

The presence of the two subsumption rules and reflexive and transitive subtyping rules complicates the arguments for type soundness. Thus to start with, I will argue that derivations in the systems can be canonicalised and then argue based on the canonical derivations. First consider subtyping, and a more syntax directed set of subtyping rules.

Let S_{1} be the subtyping rules in Figure 5. Let S_{2} be S_{1} with the reflexive rule specialised to type variables and recursive types only, the transitive rule removed, and the rule for type variables replaced by:

{Δ ⊢_{T} τ_{1} ≤ τ_{2} \atop Δ ⊢_{T} α ≤ τ_{2}} (α ≤ τ_{1} ∈ Δ)

Lemma A.1 The judgement Δ ⊢_{T} τ_{1} ≤ τ_{2} is derivable in S_{1} if and only if it is derivable in S_{2}.

Proof: First I will show that S_{2} is reflexive and transitive, that is, that the general reflexive and the transitive rules are derivable. The proof for reflexivity proceeds by induction on the structure of τ. In the cases that τ is a type variable or a recursive type, the desired result follows by the specialised reflexive rules. In other cases the induction hypothesis is applied to the immediate subterms and then the one rule for that case is applied. The proof for transitivity proceeds by simultaneous induction on derivations of Δ ⊢_{T} τ_{1} ≤ τ_{2} and Δ ⊢_{T} τ_{2} ≤ τ_{3}. If either judgement was derived by the specialised reflexive rules, then the result is immediate. Otherwise, enumerate the cases for the last rule used in each derivation and notice that either the same rule is used or the variable rule is used. In the case that the same rule is used, apply the induction hypothesis to the hypotheses in the derivations and then apply the same rule again. In the case the type variable rule is used on Δ ⊢_{T} τ_{1} ≤ τ_{2}, apply the induction hypothesis to the hypothesis of this derivation and the other judgement and then apply the type rule again. In the case the type variable rule is used on Δ ⊢_{T} τ_{2} ≤ τ_{3}, it must be that τ_{2} is a type variable, so the only rule for deriving Δ ⊢_{T} τ_{1} ≤ τ_{2}, which has a type variable on the right hand side, is the type variable rule so the previous case applies.

Now I will show that a judgement derivable in S_{1} is derivable in S_{2}. I have just shown that the reflexive and transitive rules are derivable. The other rules except the one for type variables are rules of S_{2}. The type variable rule of S_{1} can be derived in S_{2} by applying the derived reflexive rule and then the type variable rule.

Finally I will show that a judgement derivable in S_{2} is derivable in S_{1}. All the rules of S_{2} are rules of S_{1} except for the type variable rule, this can be derived by applying S_{1}’s type variable rule and then the transitive rule. □

From now on, I will use both systems interchangeably.

Second, in a program derivation, I can assume that the derivation of a heap value ends in either the tag rule or the tuple rule. The only other applicable rules are the tag subsumption rule and the subsumption rule. These rules can be removed and then inserted at all places in the derivation to the right where the variable in question appears.

Third, in any expression derivation between any two uses of rules that are not tag subsumption or subsumption rules I can assume there is exactly one use of the subsumption rule and zero or more uses of the tag subsumption rule. Furthermore, it will often be the case the there are zero uses of the tag subsumption rule because the types in question will not have a tag form. The assumption is valid because the tag subsumption and subsumption clearly commute, two consequtive uses of the subsumption rule can be replaced with one by using the transitive rule, and a subsumption rule can be inserted by using the reflexive rule.

With these arguments about subtyping and about where subsumption and tag subsumption rules can appear, I proceed to show type soundness of the target calculus, through a series of lemmas.

Typing context Δ_{1} extends Δ_{2} if and only if the type variables defined by Δ_{2} all appear in Δ_{1} and in the same order, and either Δ_{2} does not give the type variable a bound or Δ_{1} gives it the same bound. Value context Γ_{1} extends Γ_{2} if and only if dom(Γ_{1}) ⊆ dom(Γ_{2}) and for all x ∈ dom(Γ_{2}) Γ_{1}(x) = Γ_{2}(x). Note that the value context used to type the main expression of a program extends all the value contexts used to type the heap values in the program.

Lemma A.2 (Weakening) If Δ_{1} extends Δ_{2} and Γ_{1} extends Γ_{2} then:

1. If Δ_{2} ⊢_{T} τ then Δ_{1} ⊢_{T} τ

2. If Δ_{2} ⊢_{T} τ_{1} ≤ τ_{2} then Δ_{1} ⊢_{T} τ_{1} ≤ τ_{2}

3. If Δ_{2}; Γ_{2} ⊢_{T} e : τ then Δ_{1}; Γ_{1} ⊢_{T} e : τ

Proof: The first result is immediate from the definitions. The proof of the other results proceeds by induction on the structure of the hypothesis derivation and the desired result follows in a straightforward way from the induction hypothesis on the hypotheses of the last rule used in the derivation. □

Lemma A.3 (Derived Judgements)

1. If Δ ⊢_{T} τ_{1} ≤ τ_{2} then Δ ⊢_{T} τ_{1} and Δ ⊢_{T} τ_{2}.

Proof: The proof proceeds by induction on the derivation of Δ ⊢_{T} τ_{1} ≤ τ_{2} and the result follows in a straightforward way from the induciton hypothesis on the hypotheses of the last rule used in the derivation, or in the case of the reflexive and recursive type rules, directly from a hypothesis. Note that the syntactic restriction on typing contexts is used in the case of the typing variable rule. □

Lemma A.4 (Type Substitution) If α ∉ Δ_{1} then:

1. If Δ_{1} ⊢_{T} σ and Δ_{1}, α, Δ_{2} ⊢_{T} τ or Δ_{1}, α ≤ σ′, Δ_{2} ⊢_{T} τ then Δ_{1}, Δ_{2}[α := σ] ⊢_{T} τ[α := σ].

2. If Δ_{1} ⊢_{T} σ and Δ_{1}, α, Δ_{2} ⊢_{T} τ_{1} ≤ τ_{2} then Δ_{1}, Δ_{2}[α := σ] ⊢_{T} τ_{1}[α := σ] ≤ τ_{2}[α := σ].

3. If Δ_{1} ⊢_{T} σ_{1} ≤ σ_{2} and Δ_{1}, α ≤ σ_{2}, Δ_{2} ⊢_{T} τ_{1} ≤ τ_{2} then Δ_{1}, Δ_{2}[α := σ_{1}] ⊢_{T} τ_{1}[α := σ_{1}] ≤ τ_{2}[α := σ_{1}].

4. If ϵ ⊢_{T} σ and Δ_{1}, α, Δ_{2}; Γ ⊢_{T} e : τ then Δ_{1}, Δ_{2}[α := σ]; Γ[α := σ] ⊢_{T} e[α := σ] : τ[α := σ].

5. If ϵ ⊢_{T} σ_{1} ≤ σ_{2} and Δ_{1}, α ≤ σ_{2}, Δ_{2}; Γ ⊢_{T} e : τ then Δ_{1}, Δ_{2}[α := σ_{1}]; Γ[α := σ_{1}] ⊢_{T} e[α := σ_{1}] : τ[α := σ_{1}].

Proof: The proof of the first result is immediate from the definitions.

The proof of the second result proceeds by induction on the derivation in S_{2} of Δ, α ⊢_{T} τ_{1} ≤ τ_{2}. Apply the induction hypothesis to the hypotheses of the last rule used in the derivation and then reapply the rule. This works in every case except if the last rule is the reflexive rule for α, in this case Δ ⊢_{T} α[α := σ] ≤ α[α := σ] follows by the reflexive rule, Δ_{1} ⊢_{T} σ, and the weakening lemma.

The proof of the third result is similar except if the last rule used is new type variable rule for α. In this case Δ_{1}, α ≤ σ_{2}, Δ_{2} ⊢_{T} α ≤ τ_{2}, and the hypothesis of the last rule is Δ_{1}, α ≤ σ_{2}, Δ_{2} ⊢_{T} σ_{2} ≤ τ_{2}. Applying the induction hypothesis, it must be that Δ_{1}, Δ_{2}[α := σ_{1}] ⊢_{T} σ_{2}[α := σ_{1}] ≤ τ_{2}[α := σ_{1}]. By the derived judgements lemma, Δ_{1} ⊢_{T} σ_{2}, so α ∉ ftv(σ_{2}), and thus Δ_{1}, Δ_{2}[α := σ_{1}] ⊢_{T} σ_{2} ≤ τ_{2}[α := σ_{1}]. By the we the weakening lemma Δ_{1}, Δ_{2}[α := σ_{1}] ⊢_{T} σ_{1} ≤ σ_{2}, so by tranisitivity Δ_{1}, Δ_{2}[α := σ_{1}] ⊢_{T} α[α := σ_{1}] ≤ τ_{2}[α := σ_{1}] as required.

The proof of the fourth and fifth results proceed by induction of the derivation of C ⊢_{T} e : τ (for appropriate C). In almost all cases the desired result follows in a straight forward manner from the induction hypothesis applied to the hypotheses of the last rule used in the derivation and from (1), (2) and (3) applied to typing hypotheses. The only interesting case is rule t1 when α in that rule is the same as the α in question. Applying the induction hypothesis to the first three and last hypothesis gives the first, third, fourth, and sixth hypotheses of rule t2. If ϵ ⊢_{T} σ_{1} ≤ σ_{2} then by the induction hypothesis applied to the fourth hypothesis, Δ_{1}, Δ_{2}[α := σ_{1}]; Γ[α := σ_{2}] ⊢_{T} b_{2}[α := σ_{2}] : τ[α := σ_{1}], which is the fifth hypothesis of rule t2. The second hypothsis follows from the derived judgements lemma, and rule t2 gives the desired result. □

Note that in typing derivations for programs, the α in Δ are always distinct, because Δ starts out empty and the rules only add α not already in Δ. Thus the condition α ∉ Δ_{1} will always be satsified for judgements that come from program derivations.

Lemma A.5 If Δ ⊢_{T} rec α.τ_{1} ≤ rec α.τ_{2} then Δ ⊢_{T} τ_{1}[α := rec α.τ_{1}] ≤ τ_{2}[α := rec α.τ_{2}].

Proof: In S_{2} there are two rules for Δ ⊢_{T} rec α.τ_{1} ≤ rec α.τ_{2}: the reflexive rule for recursive types or the rule for recursive types. In the case of the reflexive rule, τ_{1} = τ_{2} so τ_{1}[α := rec α.τ_{1}] = τ_{2}[α := rec α.τ_{2}] and the desired result follows by the reflexive rule in S_{1}. In the case of the recursive types rule, it must be that Δ, α ⊢_{T} τ_{1} ≤ τ_{2}. The desired result follows by the type substitution lemma. □

Lemma A.6 (Decomposition) An expression e is either a value or of the form E[ι] for some E and some ι drawn from the following grammar:

ι ::= h | if v_{1} = v_{2} then b_{1} else b_{2} fi | unroll(v) | unpack[α, x] = v in e |
if? v then x.b_{1} else b_{2} fi | v.i | v_{1} v_{2} | let x_{1} = v_{2} and x_{2} = v_{2} in e

Proof: The proof proceeds by induction on the structure of e and a massive inspection of the various forms for e and E. □

Lemma A.7 (Context Typing) If ϵ; Γ ⊢_{T} E[ι] : τ then there exists σ such that ϵ; Γ ⊢_{T} ι : σ and for all e if ϵ; Γ, Γ′ ⊢_{T} e : σ then ϵ; Γ, Γ′ ⊢_{T} E[e] : τ. Furthermore, the derivation of ϵ; Γ ⊢_{T} ι : σ does not end in a use of either the subsumption or tag subsumption rule.

Proof: The proof proceeds by induction on the derivation of ϵ; Γ ⊢_{T} E[ι] : τ. The desired result follows straightforwardly from the induction hypothesis on the appropriate hypothesis of the last rule in the derivation. □

A value typing Γ has a heap form if and only if ∀τ ∈ ran(Γ) : τ = ⟨τ⃗⟩ or tag^{ϕ}(⟨τ⟩, σ). Note that if ⊢_{T} H : Γ then Γ has a heap form, hence the name.

Lemma A.8 (Canonical Forms) If Γ has a heap form and ϵ; Γ ⊢_{T} v : τ then v has the form given by the following table:

τ  v
tag^{ϕ}(τ_{1}, τ_{2})  x
rec α.σ  roll^{rec α.σ′}(v′)
∃α.σ  pack[τ′, v′] as ∃α.σ′
σ?  none^{σ′} or some(v′)
⟨σ⃗⟩  x
σ_{1} → σ_{2}  fix f(x : τ_{1}) : τ_{2}.v

Proof: The derivation of ϵ; Γ ⊢_{T} v : τ consists of a nonsubsumption rule followed by an optional tag subsumption rule and an optional subsumption rule. By inspection of S_{2} with an empty typing context note that all the applicable rules for subsumption do not change the form of τ. Next, notice that tag subsumption changes τ from a tuple form to a tag form. Now, inspect the rules for typing values for each of the forms for τ and notice that only one or two rules are applicable in each case and have the forms shown for v in the table. □

Lemma A.9 If ϵ; Γ ⊢_{T} x : tag^{−}(σ_{1}, τ_{1}) and ϵ; Γ ⊢_{T} x : tag^{+}(σ_{2}, τ_{2}) then ϵ ⊢_{T} σ_{1} ≤ σ_{2}.

Proof: The only rules for deriving the judgements are the variable rule and the subsumption rule, therefore there must be a τ such that ϵ ⊢_{T} τ ≤ tag^{−}(σ_{1}, τ_{1}) and ϵ ⊢_{T} τ ≤ tag^{+}(σ_{2}, τ_{2}). In S_{2} the only rules that can derive these judgements are the tag subtyping rules, so it must be the case that τ = tag^{∘}(σ, τ) and that ϵ ⊢_{T} σ_{1} ≤ σ and ϵ ⊢_{T} σ ≤ σ_{2}. The desired result follows by the transitivity rule. □

Lemma A.10 (Value Substitution) If Δ; Γ_{1} ⊢_{T} e_{1} : τ_{1} and Δ; Γ_{1}, x : τ_{1}, Γ_{2} ⊢_{T} e_{2} : τ_{2} then Δ; Γ_{1}, Γ_{2} ⊢_{T} e_{2}[x := e_{1}] : τ_{2}.

Proof: The proof proceeds by induction on the derivation of Δ; Γ, x : τ_{1} ⊢_{T} e_{2} : τ_{2}. The desired result follows in a striaghforward manner from the induction hypothesis applied to the hypotheses of the last rule in the derivation. □

Theorem A.11 (Type Preservation) If ⊢_{T} P_{1} : τ and P_{1} ↦ P_{2} then ⊢_{T} P_{2} : τ.

Proof: Let P_{1} = let H_{1} in E[ι] and P_{2} = let H_{2} in E[e] where ι, e, and H_{2} are given by one of the rules in Figure 4. The derivation of ⊢_{T} P_{1} : τ must be by the rule for programs, so there exists Γ_{1} such that ⊢_{T} H_{1} : Γ_{1} and ϵ; Γ_{1} ⊢_{T} E[ι] : τ. So by lemma A.7 there exists σ such that Γ_{1} ⊢_{T} ι : σ. The goal is to find Γ_{2} such that ⊢_{T} H_{2} : Γ_{1}, Γ_{2} and ϵ; Γ_{1}, Γ_{2} ⊢_{T} e : σ. Then by lemma A.7 ϵ; Γ_{1}, Γ_{2} ⊢_{T} E[e] : τ and by the program rule ⊢_{T} P_{2} : τ as desired. The proof proceeds by a case analysis of the rule used for P_{1} ↦ P_{2}.

ι = ⟨v⃗⟩ or tag(v⃗, τ): In this case e = x for some fresh x and H_{2} = H_{1}, x = ι. Clearly, by the rule for heaps, ⊢_{T} H_{1}, x = ι : Γ_{1}, x : σ. So selecting Γ_{2} = x : σ, it remains to show that

Γ_{1}, Γ_{2} ⊢_{T} x : σ which follows by the variable rule.

ι = if x = x then b_{1} else b_{2} fi: In this case e = b_{1} and H_{2} = H_{1}. Selecting Γ_{2} = ϵ it remains to show that Γ_{1} ⊢_{T} b_{1} : τ. Since ι type checks in an empty type context, only rule t2 is applicable. Therefore the derivation of ϵ; Γ_{1} ⊢_{T} ι : σ has the form:

ϵ; Γ_{1} ⊢_{T} x : tag^{−}(σ_{1}, τ_{1}) ϵ; Γ_{1} ⊢_{T} x : tag^{+}(σ_{2}, τ_{2}) \begin{matrix}ϵ ⊢_{T} σ_{1} ≤ σ_{2} \\ ⇒ \\ ϵ; Γ_{1} ⊢_{T} b_{1} : σ \end{matrix} ⋯
ϵ; Γ_{1} ⊢_{T} if x = x then b_{1} else b_{2} fi : σ

By the two judgements on x and lemma A.9 it must be that ϵ ⊢_{T} σ_{1} ≤ σ_{2}. By the judgement on b_{1}, ϵ; Γ_{1} ⊢_{T} b_{1} : σ as required.

ι = if x = y then b_{1} else b_{2} fi: In this case e = b_{2} and H_{2} = H_{1}. Selecting Γ_{2} = ϵ it remains to show that ϵ; Γ_{1} ⊢_{T} b_{2} : σ. By similar reasoning to the previous case, ϵ; Γ_{1} ⊢_{T} ι : σ has the

form: ⋯ ϵ; Γ_{1} ⊢_{T} b_{2} : σ

ϵ; Γ_{1} ⊢_{T} if x = x then b_{1} else b_{2} fi : σ

The desired result is the judgement on b_{2}.

ι = unroll(roll^{σ_{1}}(v)): In this case e = v and H_{2} = H_{1}. Selecting Γ_{2} = ϵ, it remains to show that ϵ; Γ_{1} ⊢_{T} e : σ. The derivation of ϵ; Γ_{1} ⊢_{T} ι : σ has the form:

{ϵ; Γ_{1} ⊢_{T} v : σ_{2}[α := σ_{1}] \atop ϵ; Γ_{1} ⊢_{T} roll^{σ_{1}}(v) : σ_{1}} ϵ ⊢_{T} σ_{1} ≤ σ_{3}
ϵ; Γ_{1} ⊢_{T} roll^{σ_{1}}(v) : σ_{3}

ϵ; Γ_{1} ⊢_{T} ι : σ where σ = σ_{4}[α := σ_{3}], σ_{1} = rec α.σ_{2}, and σ_{3} = rec α.σ_{4}. Note that the tag sumsumption rule cannot be used between the roll and unroll rule because the types have a recursive form not a tag form. By ϵ ⊢_{T} σ_{1} ≤ σ_{3} and lemma A.5, ϵ ⊢_{T} σ_{2}[α := σ_{1}] ≤ σ_{3}[α := σ_{4}]. The later is σ, so by judgement on v and subsumption ϵ; Γ ⊢_{T} v : σ as required.

ι = unpack[α, c] = pack[τ_{1}, v] as τ_{2} in b: In this case e = b[α := τ_{1}, x := v] and H_{2} = H_{1}. Selecting Γ_{2} = ϵ, it remains to show that ϵ; Γ_{1} ⊢_{T} e : σ. The derivation of ϵ; Γ_{1} ⊢_{T} ι : σ has the form:

ϵ ⊢_{T} τ_{1} ϵ; Γ_{1} ⊢_{T} v : τ_{3}[α := τ_{1}] ϵ; Γ_{1} ⊢_{T} pack[τ_{1}, v] as τ_{2} : τ_{2} ϵ ⊢_{T} τ_{2} ≤ ∃α.τ_{4} ϵ; Γ_{1} ⊢_{T} pack[τ_{1}, v] as τ_{2} : ∃α.τ_{4}α; Γ_{1}, x : τ_{4} ⊢_{T} b : σ ϵ ⊢_{T} σ
ϵ; Γ_{1} ⊢_{T} ι : σ

where τ_{2} = ∃α.τ_{3}. Note that the tag subsumption rule cannot be used between the pack and unpack rules because the types have an existential form not a tag form. In S_{2} there is only one rule for ϵ ⊢_{T} ∃α.τ_{3} ≤ ∃α.τ_{4} so it must be that α ⊢_{T} τ_{3} ≤ τ_{4}. By the type substitution lemma, ϵ ⊢_{T} τ_{3}[α := τ_{1}] ≤ τ_{4}[α = τ_{1}]. By subsumption ϵ; Γ_{1} ⊢_{T} v : τ_{4}[α := τ_{1}]. Now, by the type substitution lemma, ϵ; (Γ_{1}, x : τ_{4})[α := τ_{1}] ⊢_{T} b[α := τ_{1}] : σ[α := τ_{1}]. Since Γ_{1} is the type for H_{1} it has no free type variables so (Γ_{1}, x : τ_{4})[α := τ_{1}] = Γ_{1}, x : τ_{4}[α := τ_{1}], and ϵ ⊢_{T} σ implies ftv(σ) = ∅ so σ[α := τ_{1}] = σ. So ϵ; Γ_{1}, x : τ_{4}[α := τ_{1}] ⊢_{T} b[α := τ_{1}] : σ. By the value substitution lemma ϵ; Γ_{1} ⊢_{T} b[α := τ_{1}, x := v] : σ as required.

ι = if? none^{τ′} then x.b_{1} else b_{2} fi: In this case e = b_{2} and H_{2} = H_{1}. Selecting Γ_{2} = ϵ it remains to show that ϵ; Γ_{1} ⊢_{T} e : σ. The derivation of ϵ; Γ_{1} ⊢_{T} ι : σ must have the form:

ϵ; Γ_{1} ⊢_{T} none^{τ′} : τ′? ϵ; Γ_{1}, x : τ′ ⊢_{T} b_{1} : σ ϵ; Γ_{1} ⊢_{T} b_{2} : σ
ϵ; Γ_{1} ⊢_{T} ι : σ

Note that the tag subsumption rule cannot be used between the none rule and the opt if rule because the types have an opt form not a tag form. The judgemnet on b_{2} is the desired result.

ι = if? some(v) then x.b_{1} else b_{2} fi: In this case e = b_{1}[x := v] and H_{2} = H_{1}. Selecting Γ_{2} = ϵ it remains to show that ϵ; Γ_{1} ⊢_{T} e : σ. The derivation of ϵ; Γ_{1} ⊢_{T} ι : σ must have the form:

{ϵ; Γ_{1} ⊢_{T} v : τ_{2} \atop ϵ; Γ_{1} ⊢_{T} some(v) : τ_{2}?} ϵ ⊢_{T} τ_{2}? ≤ τ_{1}?
ϵ; Γ_{1} ⊢_{T} some(v) : τ_{1}? ϵ; Γ_{1}, x : τ_{1} ⊢_{T} b_{1} : σ ϵ; Γ_{1} ⊢_{T} b_{2} : σ
ϵ; Γ_{1} ⊢_{T} ι : σ

Note that the tag subsumption rule cannot be used between the some rule and the opt if rule because the types have an opt form not a tag form. In S_{2} there is only one rule for deriving ϵ ⊢_{T} τ_{2}? ≤ τ_{1}?, so it must be that ϵ ⊢_{T} τ_{2} ≤ τ_{1}. By the judgement on v and subsumption ϵ; Γ_{1} ⊢_{T} v : τ_{1}. By the judgement on b_{1} and the value substitution lemma ϵ; Γ_{1} ⊢_{T} b_{1}[x := v]σ : as required.

ι = x.i: In this case e = v_{i} and H_{2} = H_{1}. Selecting Γ_{2} = ϵ it remains to show that ϵ; Γ_{1} ⊢_{T} e : σ. There are two cases: H(x) = ⟨v_{1}, …, v_{n}⟩ or H(x) = tag(⟨v_{1}, …, v_{n}⟩, τ′). Consider the former first. The derivation of ⊢_{T} H_{1} : Γ_{1} must have the form:

\begin{aligned}⋯ & {ϵ; Γ_{i} ⊢_{T} v_{i} : τ_{i} \atop ϵ; Γ′ ⊢_{T} ⟨v_{1}, …, v_{n}⟩ : ⟨τ_{1}, …, τ_{n}⟩} & ⋯ \\ & ⊢_{T} …, x = ⟨v_{1}, …, v_{n}⟩, …: Γ_{1} \end{aligned}

for some Γ′ that Γ_{1} extends. The derivation of ϵ; Γ_{1} ⊢_{T} ι : σ must have the form:

\begin{matrix}ϵ; Γ_{1} ⊢_{T} x : ⟨τ_{1}, …, τ_{n}⟩ & ϵ ⊢_{T} ⟨τ_{1}, …, τ_{m}⟩ ≤ ⟨σ_{1}, …, σ_{n}⟩ \\ ϵ; Γ_{1} ⊢_{T} x : ⟨σ_{1}, …, σ_{m}⟩ \end{matrix} ; ϵ; Γ_{1} ⊢_{T} ι : σ

where σ = σ_{i}. Note that the tag subsumption rule cannot be used between the tuple rule and the projection rule because the types have a tuple form not a tag form. In S_{2} there is only one rule for ϵ ⊢_{T} ⟨τ_{1}, …, τ_{m}⟩ ≤ ⟨σ_{1}, …, σ_{n}⟩, so it must be that ϵ ⊢_{T} τ_{i} ≤ σ_{i}. Thus by the judgement for v_{i} and subsumption ϵ; Γ_{i} ⊢_{T} v_{i} : σ. By the weakening lemma ϵ; Γ_{1} ⊢_{T} v_{i} : σ as required.

Now consider the case H(x) = tag(⟨v_{1}, …, v_{n}⟩, τ′). Now ⊢_{T} H_{1} : Γ_{1} will have the form:

⋯

ϵ; Γ_{i} ⊢_{T} v_{i} : τ_{i} ϵ ⊢_{T} τ′

ϵ; Γ_{i} ⊢_{T} tag(⟨v_{1}, …, v_{n}⟩, τ′) : tag^{∘}(τ′, ⟨τ_{1}, …, τ_{n}⟩) ⋯

⊢_{T} …, x = tag(⟨v_{1}, …, v_{n}⟩, τ′), …: Γ_{1}

and the derivation of ϵ; Γ_{1} ⊢_{T} x : ⟨τ_{1}, …, τ_{n}⟩ has an extra rule:

{ϵ; Γ_{1} ⊢_{T} x : tag^{∘}(τ′, ⟨τ_{1}, …, τ_{n}⟩) \atop ϵ; Γ_{1} ⊢_{T} x : ⟨τ_{1}, …, τ_{n}⟩}

Otherwise the reasoning is the same.

ι = v_{1} v_{2}: Note that v_{1} = fix f(x : τ_{1}) : τ_{2}.b. In this case e = b[f, x := v_{1}, v_{2}] and H_{2} = H_{1}. Selecting Γ_{2} = ϵ it remains to show that ϵ; Γ_{1} ⊢_{T} e : σ. The derivation of ϵ; Γ_{1} ⊢_{T} ι : σ must have the form:

\begin{matrix}\begin{matrix}{ϵ; Γ_{1}, f:τ_{1} → τ_{2}, x:τ_{1} ⊢_{T} b : τ_{2} \atop ϵ; Γ_{1} ⊢_{T} v_{1} : τ_{1} → τ_{2}} & ϵ ⊢_{T} τ_{1} → τ_{2} ≤ σ_{1} → σ \\ ϵ; Γ_{1} ⊢_{T} v_{1} : σ_{1} → σ \end{matrix} & ϵ; Γ_{1} ⊢_{T} v_{2} : σ_{1} \\ ϵ; Γ_{1} ⊢_{T} ι : σ \end{matrix}

Note that the tag subsumption rule cannot be used between the fix rule and the application rule because the types have a function form not a tag form. In S_{2} there is only one rule for ϵ ⊢_{T} τ_{1} → τ_{2} ≤ σ_{1} → σ, so it must be that ϵ ⊢_{T} σ_{1} ≤ τ_{1} and ϵ ⊢_{T} τ_{2} ≤ σ. Using the former, the judgement for v_{2} and subsumption, ϵ; Γ_{1} ⊢_{T} v_{2} : τ_{1}. Then, by the value subsitution lemma and the judgements for v_{1} and b, ϵ; Γ_{1} ⊢_{T} b[f, x := v_{1}, v_{2}] : τ_{2}. Finally, using ϵ ⊢_{T} τ_{2} ≤ σ and subsumption the desired result follows.

ι = let x_{1} = v_{1} and x_{2} = v_{2} in e′: In this case e = e′[x_{1}, x_{2} := v_{1}, v_{2}] and H_{2} = H_{1}. Selecting Γ_{2} = ϵ it remains to show that ϵ; Γ_{1} ⊢_{T} e : σ. The derivation of ϵ; Γ_{1} ⊢_{T} ι : σ must have the form:

\begin{aligned}ϵ; Γ_{1} ⊢_{T} v_{1} : τ_{1} & ϵ; Γ_{1} ⊢_{T} v_{2} : τ_{2} & ϵ; Γ_{1}, x_{1}:τ_{1}, x_{2}:τ_{2} ⊢_{T} e′ : σ \\ & ϵ; Γ_{1} ⊢_{T} ι : σ \end{aligned}

By the value substitution lemma and the judgements for v_{2} and e′, ϵ; Γ_{1}, x_{1}:τ_{1} ⊢_{T} e′[x_{2} := v_{2}] : σ. By the value substitution lemma and the judgement for v_{1}, ϵ; Γ_{1} ⊢_{T} e′[x_{1}, x_{2} :=

v_{1}, v_{2}] : σ, as required.

□

A terminal configuration is a program of the form let H in v. A program that is irreducible and not a terminal configuration is called stuck.

Theorem A.12 (Progress) If ⊢_{T} P : τ then either P is a terminal configuration or there exists a P′ such that P ↦ P′.

Proof: Let P = let H in e, then by the decomposition lemma either e is a value in which case P is a terminal configuration as required or e = E[ι] for some ι as given in that lemma. The derivation of ⊢_{T} P : τ must be by the rule for programs, so there exists Γ such that ⊢_{T} H : Γ and ϵ; Γ ⊢_{T} E[ι] : τ. Note that the former implies that Γ has a heap form. By the latter and lemma A.7 there exists σ such that Γ ⊢_{T} ι : σ. I will show that the latter implies that ι has one of the forms for I in Figure 4 and that the side conditions are satisfied. The proof proceeds by a case analysis of the form of ι:

ι = h: In this case ι has the first form in the table and clearly a fresh x can be chosen.

ι = if v_{1} = v_{2} then b_{1} else b_{2} fi: The derivation of ϵ; Γ ⊢_{T} ι : σ must have the form:

⋯ ϵ; Γ ⊢_{T} v_{1} : tag^{−}(σ_{1}, τ_{1}) ϵ; Γ ⊢_{T} v_{2} : tag^{+}(σ_{2}, τ_{2}) ⋯
ϵ; Γ ⊢_{T} ι : σ

By the canonical forms lemma case (1) v_{1} and v_{2} are variables and therefore ι has either the second or the third form for I as required.

ι = unroll(v): The derivation of ϵ; Γ ⊢_{T} ι : σ must have the form:

{ϵ; Γ ⊢_{T} v : rec α.σ′ \atop ϵ; Γ ⊢_{T} ι : σ}

By the canonical forms lemma case (2) v has the form roll^{rec α.σ′′}(v′) and therefore ι has the fourth form for I as required.

ι = unpack[α, x] = v in b: The derivation of ϵ; Γ ⊢_{T} ι : σ must have the form:

\begin{matrix}ϵ; Γ ⊢_{T} v : ∃α.σ′ & ⋯ \\ ϵ; Γ ⊢_{T} ι : σ \end{matrix}

By the canonical forms lemma case (3) v has the form pack[τ′, v′] as ∃α.σ′′, therefore ι has the fifth form for I as required.

ι = if? v then x.b_{1} else b_{2} fi: The derivation of ϵ; Γ ⊢_{T} ι : σ must have the form:

\begin{matrix}ϵ; Γ ⊢_{T} v : σ′? & ⋯ \\ ϵ; Γ ⊢_{T} ι : σ \end{matrix}

By the canonical forms lemma case (4) v has the form none^{σ′′} or some(v′), therefore ι has either the sixth or seventh form for I as required. ι = v.i: The derivation of ϵ; Γ ⊢_{T} ι : σ must have the form:

{ϵ; Γ ⊢_{T} v : ⟨σ_{1}, …, σ_{m}⟩ \atop ϵ; Γ ⊢_{T} ι : σ} (1 ≤ i ≤ m)

By the canonical forms lemma case (5) v is a variable x, therefore ι has the eigth form for I and it remains to show that the side conditions are satisfied. Since ϵ; Γ ⊢_{T} x : ⟨σ_{1}, …, σ_{m}⟩ requires that x ∈ dom(Γ) and ⊢_{T} H : Γ requires that dom(H) = dom(Γ). There must be a v = ⟨v_{1}, …, v_{n}⟩ such that H(x) = v or H(x) = tag(v, τ′). Thus the first and third side conditions are satisfied. By an inspection of the rules for ϵ; Γ ⊢_{T} x : ⟨σ_{1}, …, σ_{m}⟩ it must be the case that there are τ_{1}, …, τ_{n} such that ϵ ⊢_{T} ⟨τ_{1}, …, τ_{n}⟩ ≤ ⟨σ_{1}, …, σ_{m}⟩. In S_{2} there is only one rule for this judgement so it must be that n ≥ m, so since 1 ≤ i ≤ m the second side condition is also satisfied.

ι = v_{1} v_{2}: In this case ι has the ninth form for I, it remains to show the side condition is satisfied. The derivation of ϵ; Γ ⊢_{T} ι : σ must have the form:

\begin{matrix}ϵ; Γ ⊢_{T} v_{1} : σ_{1} → σ_{2} & ⋯ \\ ϵ; Γ ⊢_{T} ι : σ \end{matrix}

By the canonical forms lemma case (6) v has the form fix f(x : τ_{1}) : τ_{2}.b as required.

ι = let x_{1} = v_{1} and x_{2} = v_{2} in e′: Clearly ι has the tenth form for I and there are no side conditions that need to be satisfied.

□

Theorem A.13 (Type Safety) If ⊢_{T} P_{1} : τ and P_{1} ↦^{∗} P_{2} then P_{2} is not stuck.

Proof: The proof proceeds by induction of the length of P_{1} ↦ P_{2}, the type preservation lemma, and the progress lemma. □

B Type Correctness of Translation

The main result of this appendix is that the translation preserves subtyping, typability and the types of various syntactic constructs. These theorems are interpersed with some technical lemmas, particular a typing derivation for the reified tag checker tagchk(y_{1}, y_{2}, τ, σ). These results make fairly substantial use of the weakening lemma from Appendix A, but are otherwise self contained.

Lemma B.1 ftv(tag(ϕ, τ)) = ftv(τ) and ftv(tag′(τ)) ⊆ ftv(τ).

Proof: By inspection notice that ftv(tag(ϕ, τ)) = ftv(τ) ∪ ftv(tag′(τ)) and ftv(tag′(τ)) = ftv(τ) − {α}, the desired result follows immediately. □

Theorem B.2 For all types τ in the tagging language ϵ ⊢_{T} [[τ]]_{type}.

Proof: The desired result follows if ftv([[τ]]_{type}) = ∅. The proof of the latter proceeds by induction of the structure of τ. Consider the forms that τ could take:

τ = tag(σ): The desired result follows immediately from the induction hypothesis on σ and lemma B.1.

τ = tagged: By inspection ftv([[tagged]]_{type}) = (ftv(tag(−, α)) ∪ {α}) − {α}. By lemma B.1 this is equal to ({α} ∪ {α}) − {α} = ∅.

τ = ⟨τ_{1}, …, τ_{n}⟩: By inspection ftv([[⟨τ_{1}, …, τ_{n}⟩]]_{type}) = ftv([[τ_{1}]]_{type})∪⋯∪ftv([[τ_{n}]]_{type}). By the induction hypothesis this is equal to ∅ ∪ ⋯ ∪ ∅ = ∅.

τ = τ_{1} → τ_{2}: By inspection ftv([[τ_{1} → τ_{2}]]_{type}) = ftv([[τ_{1}]]_{type}) ∪ ftv([[τ_{2}]]_{type}). By the induction hypothesis this is equal to ∅ ∪ ∅ = ∅.

□

Theorem B.3 If ⊢_{S} τ_{1} ≤ τ_{2} then ϵ ⊢_{T} [[τ_{1}]]_{type} ≤ [[τ_{2}]]_{type}.

Proof: The proof proceeds by induction on the derivation of ⊢_{S} τ_{1} ≤ τ_{2}. Consider which rule was used to derive this judgement:

tag rule: The result follows by theorem B.2 and the reflexive rule in the target calculus.

tagged rule: The result follows by theorem B.2 and the reflexive rule in the target calculus.

tuple rule: By the rule it must be that m ≥ n and ⊢_{S} τ_{i} ≤ σ_{i}. By the induction hypothesis, it must be that ϵ ⊢_{T} [[τ_{1}]]_{type} ≤ [[σ_{i}]]_{type}, so:

ϵ ⊢_{T} [[τ_{i}]]_{type} ≤ [[σ_{i}]]_{type}

ϵ ⊢_{T} [[⟨τ_{1}, …, τ_{n}⟩]]_{type} ≤ [[⟨σ_{1}, …, σ_{m}⟩]]_{type} (m ≥ n)

function rule: By the rule it must be that ⊢_{S} σ_{1} ≤ τ_{1} and ⊢_{S} τ_{2} ≤ σ_{2}. By the induction hypothesis is must be that ϵ ⊢_{T} [[σ_{1}]]_{type} ≤ [[τ_{1}]]_{type} and ϵ ⊢_{T} [[τ_{2}]]_{type} ≤ [[σ_{2}]]_{type}, so:

ϵ ⊢_{T} [[σ_{1}]]_{type} ≤ [[τ_{1}]]_{type} ϵ ⊢_{T} [[τ_{2}]]_{type} ≤ [[σ_{2}]]_{type}
ϵ ⊢_{T} [[τ_{1} → σ_{1}]]_{type} ≤ [[τ_{2} → σ_{2}]]_{type}
□

Lemma B.4 If Δ ⊢_{T} τ_{1} ≤ τ_{2} and ϕ ∈ {−, ∘} then Δ ⊢_{T} tag(ϕ, τ_{2}) ≤ tag(−, τ_{1}).

Proof: First a derivation for Δ ⊢_{T} tag′(τ_{2}) ≤ tag′(τ_{1}):

Δ, β, α ≤ β ⊢_{T} τ_{1} ≤ τ_{2} {Δ, β, α ≤ β ⊢_{T} α ≤ β \atop Δ, β, α ≤ β ⊢_{T} ⟨α⟩ ≤ ⟨β⟩}
Δ, β, α ≤ β ⊢_{T} tag^{−}(τ_{2}, ⟨α⟩) ≤ tag^{−}(τ_{1}, ⟨β⟩)
Δ, β, α ≤ β ⊢_{T} tag^{−}(τ_{2}, ⟨α⟩)? ≤ tag^{−}(τ_{1}, ⟨β⟩)?
Δ ⊢_{T} tag′(τ_{2}) ≤ tag′(τ_{1})

Note that the weakening lemma was used to get Δ, β, α ≤ β ⊢_{T} τ_{1} ≤ τ_{2}. Second a derivation for Δ ⊢_{T} tag(ϕ, τ_{2}) ≤ tag(−, τ_{1}):

Δ ⊢_{T} τ_{1} ≤ τ_{2}

Δ ⊢_{T} tag′(τ_{2}) ≤ tag′(τ_{1})
Δ ⊢_{T} ⟨tag′(τ_{2})⟩ ≤ ⟨tag′(τ_{1})⟩
Δ ⊢_{T} tag(ϕ, τ_{2}) ≤ tag(−, τ_{1})
□

Lemma B.5 If ϵ ⊢_{T} σ, α is arbitrary, Γ(y_{1}) = ⟨tag(−, α), α⟩, and Γ(y_{2}) = tag(+, σ) then α; Γ ⊢_{T} tagchk(y_{1}, y_{2}, α, σ) : tag(−, α) → σ?.

Proof: First, by the weakening lemma α ⊢_{T} σ. Second, by lemma B.1 ftv(tag(−, α)) = {α}, and by target types well formedness rule ftv(σ) = ∅. Thus ftv(tag(−, α) → σ?) = {α} and α ⊢_{T} tag(−, α) → σ?. Let Γ′ = Γ, y_{3} : tag(−, α) → σ?, y_{4} : tag(−, α). By the weakening lemma α ≤ σ; Γ′ ⊢_{T} y_{1} : ⟨tag(−, α), α⟩ and α; Γ′ ⊢_{T} y_{2} : tag^{+}(σ, ⟨tag′(σ)⟩). Let the A be the following derivation:

\begin{matrix}{α ≤ σ; Γ′ ⊢_{T} y_{1} : ⟨tag(−, α), α⟩ \atop α ≤ σ; Γ′ ⊢_{T} y_{1}.2 : α} & α ≤ σ ⊢_{T} α ≤ σ \\ α ≤ σ; Γ′ ⊢_{T} y_{1}.2 : σ \end{matrix}

α ≤ σ; Γ′ ⊢_{T} some(y_{1}.2) : σ?

Let B be the following derivation:

α; Γ′, y_{5} : tag(−, α) ⊢_{T} y_{3} : tag(−, α) → σ? α; Γ′, y_{5} : tag(−, α) ⊢_{T} y_{5} : tag(−, α)
α; Γ′, y_{5} : tag(−, α) ⊢_{T} y_{3} y_{5} : σ?

Note that the first unrolling of tag′(α) is tag(−, α)?. Using this, let C be the following derivation:

α; Γ′ ⊢_{T} y_{4} : tag(−, α)
α; Γ′ ⊢_{T} y_{4} : ⟨tag′(α)⟩

(tag subsume)

α; Γ′ ⊢_{T} y_{4}.1 : tag′(α)
α; Γ′ ⊢_{T} unroll(y_{4}.1) : tag(−, α)? B

{α ⊢_{T} σ \atop α; Γ ⊢_{T} none^{σ} : σ?}

α; Γ′ ⊢_{T} if? unroll(y_{4}.1) then y5.y3 y_{5} else none^{σ} fi : σ?

The desired result follows from this derivation:

α ⊢_{T} tag(−, α) → σ?

ϵ ⊢_{T} σ
α; Γ′ ⊢_{T} y_{4} : tag^{−}(α, ⟨tag′(α)⟩)
α; Γ′ ⊢_{T} y_{2} : tag^{+}(σ, ⟨tag′(σ)⟩)
A
C

α; Γ′ ⊢_{T} if y_{4} = y_{2} then some(y_{2}.2) else if? ⋯ then ⋯ else ⋯ fi fi : σ?

α; Γ ⊢_{T} tagchk(y_{1}, y_{2}, α, σ) : tag(−, α) → σ?
□

Theorem B.6 If Γ ⊢_{S} e : τ then ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e]]_{exp} : [[τ]]_{type}.

Proof: The proof proceeds by induction on the derivation of Γ ⊢_{S} e : τ. Consider the last rule used in the derivation:

subsumption rule: In this case Γ ⊢_{S} e : τ_{1} and ⊢_{S} τ_{1} ≤ τ_{2} so by the induction hypothesis and theorem B.3, ϵ; [[Γ]]_{ctxt} ⊢_{T} e : [[τ_{1}]]_{type} and ϵ ⊢_{T} [[τ_{1}]]_{type} ≤ [[τ_{2}]]_{type}. The desired result follows by target subsumption.

variable rule: In this case Γ(x) = τ so by the definition of [[Γ]]_{ctxt}, [[Γ]]_{ctxt}(x) = [[τ]]_{type} and the desired result follows by the target variable rule.

newtag rule: In this case e = newtag(σ) and τ = tag(σ). By theorem B.2 ϵ ⊢_{T} [[σ]]_{type}, and by lemma B.1 ϵ ⊢_{T} tag(−, [[σ]]_{type}). Also note that one unrolling of tag′([[σ]]_{type}) is tag(−, [[σ]]_{type})?. The desired result follows by this derivation:

ϵ ⊢_{T} tag(−, [[σ]]_{type})
ϵ; [[Γ]]_{ctxt} ⊢_{T} none^{tag(−,[[σ]]_{type})} : tag(−, [[σ]]_{type})?
ϵ; [[Γ]]_{ctxt} ⊢_{T} roll^{tag′([[σ]]_{type})}(none^{tag(−,[[σ]]_{type})}) : tag′([[σ]]_{type}) ϵ ⊢_{T} [[σ]]_{type}
ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e]]_{exp} : tag(∘, [[σ]]_{type})

subtag rule: In this case e = subtag(e_{1}, σ), Γ ⊢_{S} e_{1} : σ_{1}, and ⊢_{S} σ ≤ σ_{1}. By theorem B.3 ϵ ⊢_{T} [[σ]]_{type} ≤ [[σ_{1}]]_{type}, and by lemma B.4 ϵ ⊢_{T} tag(∘, [[σ_{1}]]_{type}) ≤ tag(−, [[σ]]_{type}). By the induction hypothesis ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e_{1}]]_{exp} : tag(∘, [[σ_{1}]]_{type}), so by target subsumption ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e_{1}]]_{exp} : tag(−, [[σ]]_{type}). Also note that one unrolling of tag′([[σ]]_{type}) is tag(−, [[σ]]_{type})?. The desired result follows by this derivation:

ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e_{1}]]_{exp} : tag(−, [[σ]]_{type})
ϵ; [[Γ]]_{ctxt} ⊢_{T} some([[e_{1}]]_{exp}) : tag(−, [[σ]]_{type})?
ϵ; [[Γ]]_{ctxt} ⊢_{T} roll^{tag′([[σ]]_{type})}(some([[e_{1}]]_{exp})) : tag′([[σ]]_{type}) ϵ ⊢_{T} [[σ]]_{type}
ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e]]_{exp} : tag(∘, [[σ]]_{type})

tagged rule: In this case e = tagged(e′), Γ ⊢_{S} e′ : ⟨tag(σ), σ⟩, and τ = tagged. By the induction hypothesis ϵ; [[Γ]]_{ctxt} ⊢_{T} e′ : ⟨tag(∘, [[σ]]_{type}), [[σ]]_{type}⟩. The following is a subtyping derivation:

ϵ ⊢_{T} [[σ]]_{type} ≤ [[σ]]_{type} ϵ ⊢_{T} ⟨tag′([[σ]]_{type})⟩ ≤ ⟨tag′([[σ]]_{type})⟩

ϵ ⊢_{T} tag(∘, [[σ]]_{type}) ≤ tag(−, [[σ]]_{type}) ϵ ⊢_{T} [[σ]]_{type} ≤ [[σ]]_{type}

ϵ ⊢_{T} ⟨tag(∘, [[σ]]_{type}), [[σ]]_{type}⟩ ≤ ⟨tag(−, [[σ]]_{type}), [[σ]]_{type}⟩

So by subsumption ϵ; [[Γ]]_{ctxt} ⊢_{T} e′ : ⟨tag(−, [[σ]]_{type}), [[σ]]_{type}⟩. The dersired result then follows by the following derivation, which uses the pack rule:

ϵ ⊢_{T} [[σ]]_{type} ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e′]]_{exp} : ⟨tag(−, [[σ]]_{type}), [[σ]]_{type}⟩
ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e]]_{exp} : [[tagged]]_{type}

if tag rule: In this case e = iftagof e_{1} = e_{2} then x.b_{1} else b_{2} fi, Γ ⊢_{S} e_{1} : tagged, Γ ⊢_{S} e_{2} : tag(σ), Γ, x : σ ⊢_{S} b_{1} : τ, and Γ ⊢_{S} b_{2} : τ. Let Γ′ be:

[[Γ]]_{ctxt}, x_{1} : [[tagged]]_{type}, x_{2} : tag(+, [[σ]]_{type}), y_{1} : ⟨tag(−, α), α⟩

By theorem B.2 ϵ ⊢_{T} [[σ]]_{type}, so by lemma B.5:

α; Γ′ ⊢_{T} tagchk(y_{1}, y_{2}, α, [[σ]]_{type}) : tag(−, α) → [[σ]]_{type}?

Let A be the following derivation:

α; Γ′ ⊢_{T} tagchk(y_{1}, x_{2}, α, [[σ]]_{type}) : tag(−, α) → [[σ]]_{type}? α; Γ′ ⊢_{T} y_{1} : ⟨tag(−, α), α⟩

α; Γ′ ⊢_{T} y_{1}.1 : tag(−, α)
α; Γ′ ⊢_{T} tagchk(y_{1}, x_{2}, α, [[σ]]_{type}) y_{1}.1 : [[σ]]_{type}?

By the induction hypothesis ϵ; [[Γ, x : σ]]_{ctxt} ⊢_{T} [[b_{1}]]_{exp} : [[τ]]_{type} and ϵ; [[Γ]]_{ctxt} ⊢_{T} [[b_{2}]]_{exp} : [[τ]]_{type}. By the weakening lemma α; Γ′, x : [[σ]]_{type} ⊢_{T} [[b_{1}]]_{exp} : [[τ]]_{type} and α; Γ′ ⊢_{T} [[b_{2}]]_{exp} : [[τ]]_{type}. Let B be the following derivation:

A α; Γ′, x : [[σ]]_{type} ⊢_{T} [[b_{1}]]_{exp} : [[τ]]_{type} α; Γ′ ⊢_{T} [[b_{2}]]_{exp} : [[τ]]_{type}
α; Γ′ ⊢_{T} if? tagchk(y_{1}, x_{2}, α, [[σ]]_{type}) y_{1}.1 then x.[[b_{1}]]_{exp} else [[b_{2}]]_{exp} fi : [[τ]]_{type}

By theorem B.2 ϵ ⊢_{T} [[τ]]_{type}. Let C be the following derivation:

ϵ; [[Γ]]_{ctxt}, x_{1}:[[tagged]]_{type}, x_{2}:tag(+, [[σ]]_{type}) ⊢_{T} x_{1} : ∃α.⟨tag(−, α), α⟩ B ϵ ⊢_{T} [[τ]]_{type}
ϵ; [[Γ]]_{ctxt}, x_{1}:[[tagged]]_{type}, x_{2}:tag(+, [[σ]]_{type}) ⊢_{T} unpack[α, y_{1}] = x_{1} in ⋯: [[τ]]_{type}

Since ϵ ⊢_{T} [[τ]]_{type} it must be that ftv([[τ]]_{type}) = ∅ so by lemma B.1 ftv(tag′([[τ]]_{type})) = ∅ so ftv(⟨tag′([[τ]]_{type})⟩) = ∅ so ϵ ⊢_{T} ⟨tag′([[τ]]_{type})⟩. Thus ϵ ⊢_{T} [[τ]]_{type} ≤ [[τ]]_{type} and ϵ ⊢_{T} ⟨tag′([[τ]]_{type})⟩ ≤ ⟨tag′([[τ]]_{type})⟩. By the tag subtyping rule ϵ ⊢_{T} tag(∘, [[σ]]_{type}) ≤ tag(+, [[σ]]_{type}). By the induction hypothesis ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e_{2}]]_{exp} : tag(∘, [[σ]]_{type}) So let D be the following derivation:

ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e_{2}]]_{exp} : tag(∘, [[σ]]_{type}) ϵ ⊢_{T} tag(∘, [[σ]]_{type}) ≤ tag(+, [[σ]]_{type})
ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e_{2}]]_{exp} : tag(+, [[σ]]_{type})

By the induction hypothesis ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e_{1}]]_{exp} : [[tagged]]_{type}. The desired result follows from this derivation:

ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e_{1}]]_{exp} : [[tagged]]_{type} D C
ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e]]_{exp} : [[τ]]_{type}

tuple rule: In this case e = ⟨e_{1}, …, e_{n}⟩, τ = ⟨τ_{1}, …, τ_{n}⟩, and Γ ⊢_{S} e_{i} : τ_{i}. By the induction hypothesis ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e_{i}]]_{exp} : [[τ_{i}]]_{type}. The desired result follows by applying the target tuple rule.

projection rule: In this case e = e′.i, Γ ⊢_{S} e′ : ⟨τ_{1}, …, τ_{n}⟩, 1 ≤ i ≤ n, and τ = τ_{i}. By the induction hypothesis ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e′]]_{exp} : [[⟨τ_{1}, …, τ_{n}⟩]]_{type}. The later is equal to ⟨[[τ_{1}]]_{type}, …, [[τ_{n}]]_{type}⟩ so the desired result follows by applying the target projection rule.

function rule: In this case e = fix f(x:τ_{1}):τ_{2}.b, Γ, f:τ_{1} → τ_{2}, x:τ_{1} ⊢_{S} b : τ_{2}, and τ = τ_{1} → τ_{2}. By theorem B.2 it must be that ϵ ⊢_{T} [[τ_{1}]]_{type} → [[τ_{2}]]_{type}. By the induction hypothesis, it must be that ϵ; [[Γ, f:τ_{1} → τ_{2}, x:τ_{1}]]_{ctxt} ⊢_{T} [[b]]_{exp} : [[τ_{2}]]_{type}. Since [[Γ, f:τ_{1} → τ_{2}, x:τ_{1}]]_{ctxt} = [[Γ]]_{ctxt}, f:[[τ_{1}]]_{type} → [[τ_{2}]]_{type}, x:[[τ_{1}]]_{type} and [[τ_{1} → τ_{2}]]_{type} = [[τ_{1}]]_{type} → [[τ_{2}]]_{type}, the desired result follows by an application of the fix rule. application rule: In this case e = e_{1} e_{2}, Γ ⊢_{S} e_{1} : τ_{2} → τ, and Γ ⊢_{S} e_{2} : τ_{2}. By the

induction hypothesis ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e_{1}]]_{exp} : [[τ_{2} → τ]]_{type} and ϵ; [[Γ]]_{ctxt} ⊢_{T} [[e_{2}]]_{exp} : [[τ_{2}]]_{type}. Since [[τ_{2} → τ]]_{type} = [[τ_{2}]]_{type} → [[τ]]_{type}, the desired result follows by applying the target application rule.

□

Theorem B.7 If Γ ⊢_{S} h : τ then [[Γ]]_{ctxt} ⊢_{T} [[h]]_{hval} : [[τ]]_{type}.

Proof: There are three cases:

h = (σ, ϵ): In this case τ = tag(σ). By theorem B.2 ϵ ⊢_{T} [[σ]]_{type}, and by lemma B.1 ϵ ⊢_{T} tag(−, [[σ]]_{type}). Also note that one unrolling of tag′([[σ]]_{type}) is tag(−, [[σ]]_{type})?. The desired result follows by this derivation:

ϵ ⊢_{T} tag(−, [[σ]]_{type})
ϵ; [[Γ]]_{ctxt} ⊢_{T} none^{tag(−,[[σ]]_{type})} : tag(−, [[σ]]_{type})?
ϵ; [[Γ]]_{ctxt} ⊢_{T} roll^{tag′([[σ]]_{type})}(none^{tag(−,[[σ]]_{type})}) : tag′([[σ]]_{type}) ϵ ⊢_{T} [[σ]]_{type}
ϵ; [[Γ]]_{ctxt} ⊢_{T} [[h]]_{hval} : tag(∘, [[σ]]_{type})

h = (σ, x): In this case Γ ⊢_{S} x : tag(σ_{x}), ⊢_{S} σ ≤ σ_{x}, and τ = tag(σ). By theorem B.3 ϵ ⊢_{T} [[σ]]_{type} ≤ [[σ_{x}]]_{type}, and by lemma B.4 ϵ ⊢_{T} tag(∘, [[σ_{x}]]_{type}) ≤ tag(−, [[σ]]_{type}). By theorem B.6 ϵ; [[Γ]]_{ctxt} ⊢_{T} x : tag(∘, [[σ_{x}]]_{type}), so by target subsumption ϵ; [[Γ]]_{ctxt} ⊢_{T} x : tag(−, [[σ]]_{type}). Also note that one unrolling of tag′([[σ]]_{type}) is tag(−, [[σ]]_{type})?. The desired result follows by this derivation:

ϵ; [[Γ]]_{ctxt} ⊢_{T} x : tag(−, [[σ]]_{type})
ϵ; [[Γ]]_{ctxt} ⊢_{T} some(x) : tag(−, [[σ]]_{type})?
ϵ; [[Γ]]_{ctxt} ⊢_{T} roll^{tag′([[σ]]_{type})}(some(x)) : tag′([[σ]]_{type}) ϵ ⊢_{T} [[σ]]_{type}
ϵ; [[Γ]]_{ctxt} ⊢_{T} [[h]]_{hval} : tag(∘, [[σ]]_{type})

h = ⟨v_{1}, …, v_{n}⟩: In this case τ = ⟨τ_{1}, …, τ_{n}⟩ and Γ ⊢_{S} v_{i} : τ_{i}. By theorem B.6 ϵ; [[Γ]]_{ctxt} ⊢_{T} [[v_{i}]]_{exp} : [[τ_{i}]]_{type}. The desired result follows by applying the target tuple rule.

□

Theorem B.8 If ⊢_{S} H : Γ then ⊢_{T} [[H]]_{heap} : [[Γ]]_{ctxt}.

Proof: Let H = x_{1} = h_{1}, …, x_{n} = h_{n} and Γ = x_{1}:τ_{1}, …, x_{n}:τ_{n}, then it must be that x_{1}:τ_{1}, …, x_{i−1}:τ_{i−1} ⊢_{S} h_{i} : τ_{i}. By theorem B.7 [[x_{1}:τ_{1}, …, x_{i−1}:τ_{i−1}]]_{ctxt} ⊢_{T} [[h_{i}]]_{hval} : [[τ_{i}]]_{type}. Now [[x_{1}:τ_{1}, …, x_{i−1}:τ_{i−1}]]_{ctxt} = x_{1}:[[τ_{1}]]_{type}, …, x_{i−1}:[[τ_{i−1}]]_{type}. So the desired result follows by applying the target heap rule. □

Theorem B.9 If ⊢_{S} P : τ then ⊢_{T} [[P]]_{prog} : [[τ]]_{type}.

Proof: Let P = let H in e. There must be a Γ such that ⊢_{S} H : Γ and Γ ⊢_{S} e : τ. By theorem B.8 ⊢_{T} [[H]]_{heap} : [[Γ]]_{ctxt} and by theorem B.6 [[Γ]]_{ctxt} ⊢_{T} [[e]]_{exp} : [[τ]]_{type}. The desired result follows by the target program rule. □

C Operational Correctness

The purpose of this appendix is to show that the translation preserves the operational semantics of tagging language in the target language. In particular I show that the translated term simulates the source term, which is usually considered a sufficient way to show semantics preservation.

Define [[E]]_{ectxt} to be [[E[x]]]_{exp}[x := []] for some fresh x. By a straighforward induction it follows that [[E]]_{ectxt} is a target evaluation context.

Lemma C.1 [[e_{1}[x := e_{2}]]]_{exp} = [[e_{1}]]_{exp}[x := [[e_{2}]]_{exp}]

Proof: The proof proceeds by induciton of the structure of e_{1} and reduces in a straight forward manner to the induction hypothesis applied to the subterms of e_{1}. □

Lemma C.2 [[E[e]]]_{exp} = [[E]]_{ectxt}[[[e]]_{exp}]

Proof: The result is immediate from the definition of [[·]]_{ectxt} and lemma C.1 and the properties of substitution. □

Lemma C.3 If ⊢_{S} H : Γ, Γ ⊢_{S} x : tag(τ_{x}), and y is arbitrary then there exists an n ≥ 1 such that there exist w_{1}, …, w_{n}, and τ_{1}, …, τ_{n}, such that y ∉ {w_{1}, …, w_{n−1}}, x = w_{1}, ∀1 ≤ i < n : H(w_{i}) = (τ_{i}, w_{i+1}), and:

tagchk^{H}(x, y) ∧ w_{n} = y
∨ not tagchk^{H}(x, y) ∧ w_{n} ≠ y ∧ H(w_{n}) = (τ_{n}, ϵ)

Proof: The proof proceeds by induction on the size of H. If x = y then take n = 1, w_{1} = y, and τ_{1} = τ_{x} and the result clearly follows. Otherwise, by an inspection of the tagging language typing rules and induction of the derivation of H ⊢_{S} Γ : it must be that H = H_{1}, x = h_{x}, H_{2}, ⊢_{S} H_{1} : Γ_{1}, and Γ_{1} ⊢_{S} h_{x} : tag(τ_{x}). By inspection of the tagging languagetyping rules there are two possible cases for h_{x}: (τ_{x}, ϵ) and (τ_{x}, w), so consider these cases:

h_{x} = (τ_{x}, ϵ): In this case tagchk^{H}(x, y) does not hold. The required result follows if n = 1, w_{1} = x, and τ_{1} = τ_{x}.

h_{x} = (τ_{x}, w): By the tagging language typing rules Γ_{1} ⊢_{S} w : tag(τ_{w}) for some τ_{w}. Since H_{1} is smaller than H, by the induction hypothesis there exists m ≥ 1, z_{1}, …, z_{m}, and σ_{1}, …, σ_{m} such that y ∉ {z_{1}, …, z_{m−1}}, w = z_{1}, ∀1 ≤ i < m : H(z_{i}) = (σ_{i}, z_{i+1}), and:

tagchk^{H}(x, y) ∧ w_{n} = y
∨ not tagchk^{H}(x, y) ∧ w_{n} ≠ y ∧ H(w_{n}) = (τ_{n}, ϵ)

The required result follows if n = m + 1, w_{1} = x, w_{i+1} = z_{i} for 1 ≤ i ≤ m, τ_{1} = τ_{x}, and τ_{i+1} = σ_{i} for 1 ≤ i ≤ m and by noting that tagchk^{H}(x, y) = tagchk^{H}(w, y).

□

Lemma C.4 If ⊢_{S} H : Γ, H(x) = ⟨x′, v, v⃗⟩, and Γ ⊢_{S} x′ : tag(τ_{1}) then:

let [[H]]_{heap} in E[tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) x′] ↦^{+} let [[H]]_{heap} in E[e]
where e = \{ \begin{matrix}some(v) & tagchk^{H}(x′, y) \\ none^{[[σ]]_{type}} & not tagchk^{H}(x′, y) \end{matrix}

Proof: Let P (x) = let [[H]]_{heap} in [[E]]_{ectxt}[x]. By lemma C.3 there exists n ≥ 1, w_{1}, …, w_{n}, and τ_{1}, …, τ_{n} such that y ∉ {w_{1}, …, w_{n−1}}, x′ = w_{1}, ∀1 ≤ i < n : H(w_{i}) = (τ_{i}, w_{i+1}) and:

tagchk^{H}(x′, y) ∧ w_{n} = y
∨ not tagchk^{H}(x′, y) ∧ w_{n} ≠ y ∧ H(w_{n}) = (τ_{n}, ϵ)

First I will show that for 1 ≤ i < n:

P (tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) w_{i}) ↦^{+} P (tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) w_{i+1})

Note that w_{i} ≠ y and that:

[[H]]_{heap}(w_{i}) = [[(τ_{i}, w_{i+1})]]_{hval} = tag(⟨roll^{tag′([[τ_{i}]]_{type})}(some(w_{i+1}))⟩, [[τ_{1}]]_{type})

Then:

P (tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) w_{i})
↦ P (if w_{i} = y then ⋯ else if? unroll(w_{i}.1) then ⋯ else ⋯ fi fi)
↦ P (if? unroll(w_{i}.1) then y_{5}.tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) y_{5} else ⋯ fi)
↦ P (if? unroll(roll^{tag′([[τ_{i}]]_{type})}(some(w_{i+1}))) then y_{5}.tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) y_{5}
else ⋯ fi)
↦ P (if? some(w_{i+1}) then y_{5}.tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) y_{5} else ⋯ fi)
↦ P (tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) w_{i+1})

So by induction:

P (tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) x′) ↦^{∗} P (tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) w_{n})

Now there are two cases: tagchk^{H}(x′, y) or not. Assume tagchk^{H}(x′, y), then w_{n} = y so:

P (tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) w_{n})
↦ P (if w_{n} = y then some(x.2) else ⋯ fi)
↦ P (some(x.2))
↦ P (some(v))

Now assume not tagchk^{H}(x′, y), then w_{n} ≠ y and H(w_{n}) = (τ_{n}, ϵ). Note that:

[[H]]_{heap}(w_{n}) = [[(τ_{n}, ϵ)]]_{hval} = tag(⟨roll^{tag′([[τ_{n}]]_{type})}(none^{tag(−,[[τ_{n}]]_{type})})⟩, [[τ_{n}]]_{type})

So:

P (tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) w_{n})
↦ P (if w_{n} = y then ⋯ else if? unroll(w_{n}.1) then ⋯ else none^{[[σ]]_{type}} fi fi)
↦ P (if? unroll(w_{n}.1) then ⋯ else none^{[[σ]]_{type}} fi)
↦ P (if? unroll(roll^{tag′([[τ_{n}]]_{type})}(none^{tag(−,[[τ_{n}]]_{type})})) then ⋯ else none^{[[σ]]_{type}} fi)
↦ P (if? none^{tag(−,[[τ_{n}]]_{type})} then ⋯ else none^{[[σ]]_{type}} fi)
↦ P (none^{[[σ]]_{type}})
□

Theorem C.5 If ⊢_{S} P_{1} : τ and P_{1} ↦ P_{2} then [[P_{1}]]_{prog} ↦^{+} [[P_{2}]]_{prog}.

Proof: Let P_{1} = let H_{1} in E[I] and P_{2} = let H_{2} in E[e] be given by the rules in Figure 2. By the definition of [[·]]_{prog} and lemma C.2 [[P_{1}]]_{prog} = let [[H_{1}]]_{heap} in [[E]]_{ectxt}[[[I]]_{exp}] and [[P_{2}]]_{prog} = let [[H_{2}]]_{heap} in [[E]]_{ectxt}[[[e]]_{exp}] so it remains to show that the former reduces to the latter is some finite nonzero number of steps. Consider the various cases for I:

I = newtag(τ): In this case e = x and H_{2} = H_{1}, x = (τ, ϵ). Note that [[I]]_{exp} = tag(⟨⋯⟩, ⋯) = [[(τ, ϵ)]]_{hval} is a heap value so:

let [[H_{1}]]_{heap} in [[E]]_{ectxt}[[[I]]_{exp}]
↦ let [[H_{1}]]_{heap}, x = [[(τ, ϵ)]]_{hval} in [[E]]_{ectxt}[x]
= let [[H_{2}]]_{heap} in [[E]]_{ectxt}[[[e]]_{exp}]

I = subtag(y, τ): The same argument as the previous case applies except that [[I]]_{exp} is a different heap value.

I = ⟨v_{1}, …, v_{n}⟩: The same argument as the previous case applies except that [[I]]_{exp} is a different heap value.

I = x.i: In this case e = v_{i}, H_{2} = H_{1}, H_{1}(x) = ⟨v_{1}, …, v_{n}⟩, and 1 ≤ i ≤ n. Note that [[I]]_{exp} = x.i and [[H_{1}]]_{heap}(x) = [[H_{1}(x)]]_{hval} = ⟨[[v_{1}]]_{exp}, …, [[v_{n}]]_{exp}⟩. So:

let [[H_{1}]]_{heap} in [[E]]_{ectxt}[[[I]]_{exp}]
↦ let [[H_{1}]]_{heap} in [[E]]_{ectxt}[[[v_{i}]]_{exp}]
= let [[H_{2}]]_{heap} in [[E]]_{ectxt}[[[e]]_{exp}]

I = v_{1} v_{2} and v_{1} = fix f(x:τ_{1}):τ_{2}.b: In this case e = b[f, x := v_{1}, v_{2}] and H_{2} = H_{1}. Note that [[I]]_{exp} = [[v_{1}]]_{exp} [[v_{2}]]_{exp} and [[v_{1}]]_{exp} = fix f(x:[[τ_{1}]]_{type}):[[τ_{2}]]_{type}.[[b]]_{exp}. So:

let [[H_{1}]]_{heap} in [[E]]_{ectxt}[[[I]]_{exp}]
↦ let [[H_{1}]]_{heap} in [[E]]_{ectxt}[[[b]]_{exp}[f, x := [[v_{1}]]_{exp}, [[v_{2}]]_{exp}]]
= let [[H_{1}]]_{heap} in [[E]]_{ectxt}[[[b[f, x := v_{1}, v_{2}]]]_{exp}]
= let [[H_{2}]]_{heap} in [[E]]_{ectxt}[[[e]]_{exp}]

Note that lemma C.1 was used twice in the second step.

I = iftagof tagged(x) = y then z.b_{1} else b_{2} fi: In this case H_{2} = H_{1} and H(x) = ⟨x′, v, v⃗⟩. Since ⊢_{S} P_{1} : τ there must be a Γ such that ⊢_{S} H_{1} : Γ and Γ ⊢_{S} E[I] : τ. By a fairly straight forward induction of the structure of E, it can be shown that there exists τ′ such that Γ ⊢_{S} I : τ′. By inspection of tagging language typing rules, it must be that the tag if rule was used and hence that Γ ⊢_{S} tagged(x) : tagged and that Γ ⊢_{S} e_{2} : tag(σ) for some σ. By further inspection of the rules, it must be that the tagged rule was used and hence that Γ ⊢_{S} x : ⟨tag(τ_{1}), τ_{1}⟩. By inspection of the rules it must be that Γ(x′) = tag(τ_{1}) and hence Γ ⊢_{S} x′ : tag(τ_{1}). Thus all of the hypotheses to lemma C.4 are satisfied. Note that [[I]]_{exp} is:

let x_{1} = pack[[[τ_{1}]]_{type}, x] as [[tagged]]_{type} and x_{2} = y in unpack[α, y_{1}] = x_{1} in
if? tagchk(y_{1}, x_{2}, α, [[σ]]_{type}) y_{1}.1 then z.[[b_{1}]]_{exp} else [[b_{2}]]_{exp} fi

So:

let [[H_{1}]]_{heap} in [[E]]_{ectxt}[[[I]]_{exp}]
↦ let [[H_{1}]]_{heap} in
[[E]]_{ectxt}[unpack[α, y_{1}] = pack[[[τ_{1}]]_{type}, x] as [[tagged]]_{type} in
if? tagchk(y_{1}, y, α, [[σ]]_{type}) y_{1}.1 then z.[[b_{1}]]_{exp} else [[b_{2}]]_{exp} fi]
↦ let [[H_{1}]]_{heap} in
[[E]]_{ectxt}[if? tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) x.1 then z.[[b_{1}]]_{exp} else [[b_{2}]]_{exp} fi]
↦ let [[H_{1}]]_{heap} in
[[E]]_{ectxt}[if? tagchk(x, y, [[τ_{1}]]_{type}, [[σ]]_{type}) x′ then z.[[b_{1}]]_{exp} else [[b_{2}]]_{exp} fi]
↦ let [[H_{1}]]_{heap} in [[E]]_{ectxt}[if? f then z.[[b_{1}]]_{exp} else [[b_{2}]]_{exp} fi]

Where f = some(v) if tagchk^{H}(x_{1}, y) and f = none^{[[σ]]_{type}} otherwise. There are two cases: tagchk^{H}(x_{1}, y) or not. Assume the former. Then f = some(v) and e = b_{2}[z := v] and:

let [[H_{1}]]_{heap} in [[E]]_{ectxt}[if? f then z.[[b_{1}]]_{exp} else [[b_{2}]]_{exp} fi]
↦ let [[H_{1}]]_{heap} in [[E]]_{ectxt}[[[b_{1}]]_{exp}[z := v]]
= let [[H_{2}]]_{heap} in [[E]]_{ectxt}[[[b_{1}[z := v]]]_{exp}]
= let [[H_{2}]]_{heap} in [[E]]_{ectxt}[[[e]]_{exp}]

Note that lemma C.1 was used in the second to last step. Now assume the other case. Then f = none^{[[σ]]_{type}} and e = [[b_{2}]]_{exp} and:

let [[H_{1}]]_{heap} in [[E]]_{ectxt}[if? f then z.[[b_{1}]]_{exp} else [[b_{2}]]_{exp} fi]
↦ let [[H_{1}]]_{heap} in [[E]]_{ectxt}[[[b_{2}]]_{exp}]
= let [[H_{2}]]_{heap} in [[E]]_{ectxt}[[[e]]_{exp}]
□

Theorem C.6 If ⊢_{S} P : τ then P ↛ if and only if [[P]]_{prog} ↛.

Proof: First, by an inspection of the translation rules, a value is translated into a value, and a nonvalue is translated into a nonvalue. Second, by the soundness of the tagging language, if P ↛ then P has the form let H in v, which means [[P]]_{prog} is a terminal configuration, which is irreducible in the target language. Third, by the type preservation lemma ⊢_{T} [[P]]_{prog} : [[τ]]_{type}. So if [[P]]_{prog} ↛ then by the target language type soundness [[P]]_{prog} is a terminal configuration. Therefore P must have the form let H in v, which is irreducible in the tagging language. □

Putting the last two theorems together, a typeable tagging language program diverges if and only if its translation diverges, and converges to a terminal configuration if and only if its translation converges to the translation of that terminal configuration. I take this as an adequate (but overly strict) meaning for operational correctness.

D Array Optimisation

Common implementations of downcasting for single inheritance hierarchies use arrays instead of linked lists, and trade space for time. Let person by a top level tag, student a subtag of person, and graduate a subtag of student. Under the array scheme, person is implemented as an array of length one containing itself. Student is implemented as an array of length two whose second element is itself and first element is person. Graduate is implemented as an array of length three whose third element is itself, second element is student, and first element is person. In general a tag at depth i in the tag hierarchy is implemented as an array of length i whose i-th element is itself, and whose first through i − 1-th elements are the tag’s ancestors at depth 1 through i − 1. Note that if t_{1} is under t_{2} in the tag hierarchy then t_{2} appears in the t_{1} array, and at index equal to t_{2}’s depth. Note also that a tags depth is just the length of the array representing it. Therefore the predicate tagchk^{H}(x, y) can be performed by comparing entry y.size of array x to y. The rest of this section will present a variant of the target calculus, and a formal translation corresponding to this array scheme. The array scheme requires space proportional to the number of tags times the depth of the tag hierarchy but constant time for a tag check; the scheme used in the main body of this report requires space porportional to the number of tags but time proportional to the depth of the tag hierarchy.

First, to accomodate the cyclic datastructures inherent in the array scheme, the target language heaps need to be cyclic. This is achieved by changing the typing rule for heaps to:

\begin{matrix}ϵ ⊢_{T} τ_{i} & Γ ⊢_{T} h_{i} : τ_{i} \\ ⊢_{T} x_{1} = h_{1}, …, x_{n} = h_{n} : Γ \end{matrix} (Γ = x_{1}:τ_{1}, …, x_{n}:τ_{n})

Second, arrays need to be added to the language. The extended syntax is:

τ, σ ::= ⋯ | array(τ) | int
e, b ::= ⋯ | fix x = tag({e_{1}, …, e_{n}}, τ) | fix x = tag(extend(e_{1}, e_{2}), τ) |
e.size | e_{1}[e_{2}] ⇒ x.b_{1} else b_{2}
v ::= ⋯ | i
E ::= ⋯ | fix x = tag({v⃗, E, e⃗}, τ) | fix x = tag(extend(E, e), τ) |
fix x = tag(extend(v, E), τ) | E.size | E[e] ⇒ x.b_{1} else b_{2} | v[E] ⇒ x.b_{1} else b_{2}
h ::= ⋯ | tag({v_{1}, …, v_{n}}, τ)

Arrays are created by one of two operations. As I will use arrays only for implementing tags, both operations are special recursive definition forms that introduce tags. The expression fix x = tag(a, τ) creates a new array a which will be used as a tag for type τ; x may be used in a to refer to the new array. The first form, a = {e_{1}, …, e_{n}}, creates an array of size n with elements e_{1} through e_{n}. The second form, a = extend(e_{1}, e_{2}), creates an array that is a copy of array e_{1} but with an additional element whose value is e_{2}. An array’s size is obtained with e.size. The subscript operation is a little unusual, in that, it combines an explicit bounds with the subscript operation. The expression e_{1}[e_{2}] ⇒ x.b_{1} else b_{2} evalutes e_{1} to an array and e_{2} to an integer, then if e_{2} is within the array bounds, x is bound to the desired element and b_{1} is evaluated, otherwise b_{2} is evaluated.

The additional reduction rules necessary to formalise the operations are:

I  e  H′  Side Conditions
fix x = tag({v_{1}, …, v_{n}}, τ) x  H, x = h x ∉ H, h = tag({v_{1}, …, v_{n}}, τ)
fix x = tag(extend(y, v), τ) x  H, x = h x ∉ H, h = tag({v_{1}, …, v_{n}, v}, τ)
H(y) = tag({v_{1}, …, v_{n}}, σ)
x.size  n  H  H(x) = tag({v_{1}, …, v_{n}}, σ)
x[i] ⇒ x.b_{1} else b_{2}  b_{1}[x := v_{i}] H  H(x) = tag({v_{1}, …, v_{n}}, σ)
1 ≤ i ≤ n
x[i] ⇒ x.b_{1} else b_{2} b_{2} H H(x) = tag({v_{1}, …, v_{n}}, σ)
¬(1 ≤ i ≤ n)

The additional typing rules are:

Δ ⊢_{T} τ_{1} ≤ τ_{2}
Δ ⊢_{T} array(τ_{1}) ≤ array(τ_{2})
Δ ⊢_{T} σ Δ; Γ, x:σ ⊢_{T} e_{i} : τ′
Δ; Γ ⊢_{T} fix x = tag({e_{1}, …, e_{n}}, τ) : σ

(x ∉ Γ; σ = tag^{∘}(τ, array(τ′)))
Δ ⊢_{T} σ Δ; Γ, x:σ ⊢_{T} e_{1} : array(τ′) Δ; Γ, x:σ ⊢_{T} e_{2} : τ′
Δ; Γ ⊢_{T} fix x = tag(extend(e_{1}, e_{2}), τ) : σ

(x ∉ Γ; σ = tag^{∘}(τ, array(τ′)))
Δ; Γ ⊢_{T} e : array(τ)
Δ; Γ ⊢_{T} e.size : int

Δ; Γ ⊢_{T} i : int
Δ; Γ ⊢_{T} e_{1} : array(σ) Δ; Γ ⊢_{T} e_{2} : int Δ; Γ, x:σ ⊢_{T} b_{1} : τ Δ; Γ ⊢_{T} b_{2} : τ
Δ; Γ ⊢_{T} e_{1}[e_{2}] ⇒ x.b_{1} else b_{2} : τ
ϵ ⊢_{T} τ ϵ; Γ ⊢_{T} v_{i} : σ
Γ ⊢_{T} tag({v_{1}, …, v_{n}}, τ) : tag^{∘}(τ, array(σ))

This extended language is type sound. The proof is very similar to the one given in Appendix A but has additional cases for the new constructs. These constructs, while presented in an unusual way, are standard and have been proven sound before.

Third, I need to give a new translation that uses the array scheme. In fact, most of the old translation can be reused, I just need to change some key items. At the type level only the auxilary functions need to change, and they now reflect the array data structure rather than the linked list data structure. At the term level the translation of newtag, subtag, and the auxilary tag check function need to change to reflect the new datastructure.

tag(ϕ, τ)  = tag^{ϕ}(τ, array(tag′(τ)))
tag′(τ)  = rec α.tag^{−}(τ, array(α))
[[newtag(τ)]]_{exp}  = fix x = tag({roll^{tag′([[τ]]_{type})}(x)}, [[τ]]_{type})
[[subtag(e, τ)]]_{exp} = fix x = tag(extend([[e]]_{exp}, roll^{tag′([[τ]]_{type})}(x)), [[τ]]_{type})
tagchk(y_{1}, y_{2}, τ, σ) = fix y_{3}(y_{4} : tag(−, τ)) : σ?.
y_{4}[y_{2}.size] ⇒
y_{5}.if unroll(y_{5}) = y_{2} then some(y_{1}.2) else none^{σ} fi
else none^{σ}

The translation of heaps is trickier, because in translating a subtag, (τ, y), all the ancestors of y are needed. To provide this information, the heap being constructed is threaded through the translation of heap values.

[[x = (τ, ϵ)]]_{hval}^{H}  = x = tag({roll^{tag′([[τ]]_{type})}(x)}, [[τ]]_{type})
[[x = (τ, y)]]_{hval}^{H}  = x = tag({v_{1}, …, v_{n}, roll^{tag′([[τ]]_{type})}(x)}, [[τ]]_{type})
where H(y) = tag({v_{1}, …, v_{n}}, σ)
[[x = ⟨v_{1}, …, v_{n}⟩]]_{hval}^{H}  = x = ⟨[[v_{1}]]_{exp}, …, [[v_{n}]]_{exp}⟩
[[x_{1} = h_{1}, …, x_{n} = h_{n}]]_{heap} = H_{n}
where H_{0} = ϵ, H_{i+1} = H_{i}, [[h_{i+1}]]_{hval}^{H_{i}}

The new translation is type preserving and operationally correct. The proofs are very similar to those given in Appendices B and C. In the case of type preservation, the proof of lemma B.1, the proof of lemma B.4, the cases for newtag and subtag in the proof of theorem B.6, the statement and proof of theorem B.7, and the proof of theorem B.8 change in a straighforward manner to reflect the array datastructure.

The proof of operational correctness involves more substantial changes. Lemma C.3 is replaced by the two lemmas below. The proof of lemma C.4, and the cases for newtag and subtag in the proof of theorem C.5 change to reflect the new datastructure.

Lemma D.1 If ⊢_{S} H : Γ and Γ ⊢_{S} x : tag(τ_{x}) then there exists an n ≥ 1 such that there exists w_{1}, …, w_{n}, and τ_{1}, …, τ_{n}, such that x = w_{n}, ∀1 < i ≤ n : H(w_{i}) = (τ_{i}, w_{i−1}), and H(w_{1}) = (τ_{1}, ϵ). Define tchain^{H}(x) = ⟨w_{1}, …, w_{n}⟩.

Lemma D.2 If ⊢_{S} H : Γ, Γ ⊢_{S} x : tag(τ_{x}), and Γ ⊢_{S} y : tag(τ_{y}) then tagchk^{H}(x, y) if and only if w_{|tchain^{H}(y)|} = y where tchain^{H}(x) = ⟨w_{1}, …, w_{n}⟩.

Both the array scheme and the linked list scheme are examples of a more general scheme. They both use unique pointers to represent tags and some sort of datastructure to capture the hierarchy. Tag checking is performed by searching the datastructure for one or more pairs of tags to compare, and the tag check succeeds only if one of these pointer comparisons succeed. Any such scheme should be implementable in a variant of the target language suitable extended with constructs to implement the datastructure. Such schemes include a number of efficient implementations of multiple inheritance tag hierarchies.