Type Dispatch for Named Hierarchical Types ^{∗}

Neal Glew

Department of Computer Science Cornell University

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 branches. Considerable previous work has addressed type case constructs for structural type systems without subtyping, but these do not extend to named type systems with subtyping, as is common in object oriented languages. Previous work on type dispatch in named type systems with subtyping has not addressed its implementation formally.

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 I formalise a small tagging language. After discussing how to implement the tagging language, I present a typed language without type dispatch primitives, and a give a formal translation from the tagging language.

1 Introduction

A number of programming languages include type dispatch constructs: conditional constructs that test the runtime type of a value. For example, Scheme [KCR98] has predicates for testing if a value is the empty list, an integer, a pair, and so on. These predicates make Scheme more expressive than it would be without them, and can be used to write polymorphic print and marshalling functions and metaprograms like eval. The intermediate language λ_{i}^{ML} [HM95, Mor95], used in the TIL compiler [TMC^{+}96], has a case construct similar to Scheme’s type predicates.

The code typecase α of α_{1} × α_{2} ⇒ e_{1} | α_{1} → α_{2} ⇒ e_{2} | ⋯ will execute e_{1} if α is a pair type, and execute e_{2} if α is a function type. The construct is crucial for implementing specialised data representations in the presence of polymorphism, and for writing polymorphic print and marshalling functions.

Class based object oriented languages have a related but slightly different construct: the ability to dispatch on an object’s runtime class. The class from which an object is instantiated is called its runtime class. The static type systems of these languages determine a conservative approximation of the runtime class of each expression: The static class of an expression is always a superclass of the runtime class of any object that expression might evaluate to. In part to make up for this conservatism, these languages allow the programmer to test the runtime class of an object with a class cast or a class case mechanism. For example, in Java [GJS96] the expression (c)e tests if e’s runtime class is a subclass of c, and if not throws an exception. Java also has a class case construct, but only for examining the class of an exception packet. 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’s runtime class against classname_{1} through classname_{n}. If classname_{i} is the first matching class, x_{i} is bound to the exception, and blk_{i} is executed. The ability to examine runtime classes is crucial to Java’s exception mechanism, and is generally useful in a number of other situations.

In typed languages, type refinement is a key property of type dispatch constructs: After dispatching on the runtime type of a value, that value’s static type changes to reflect the new type information. For example, in the λ_{i}^{ML} code:

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

x initially has static type α, but in expression e_{1} it is refined to α_{1} × α_{2}. Similarly in Java, if Student is a subclass of Person and x is declared to have type Person, then in the expression (Student)x, while x has static type Person the whole expression has the refined type Student.

The importance of type dispatch constructs to languages that have them, and the need to implement sound type refinement, justifies seeking formal foundations for them. There are two aspects to the formal analysis of these programming language constructs: First, the constructs themselves should be formalised as primitives in some small language and desired properties proven (e.g., type soundness). Second, the common implementation techniques should be formalised as translations between the above languages and ones without type dispatch primitives, and the translations proven correct.

∗This paper 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.

To appear in the 1999 ACM SIGPLAN International Conference on Functional Programming, September 1999, Paris, France.

Previous work on type dispatch in typed languages does exist. Abadi et al. [ACPP91] introduce the type dynamic with a type case construct, formalise its semantics and typing rules, and prove soundness. The afore mentioned work on λ_{i}^{ML} treats a similar construct, also formalising it and proving soundness. Crary, Weirich, and Morrisett [CWM98, CW99] show how to formalise type case in a type erasure interpretation rather than the type passing interpretation used in other works. Their work also addresses the implementation aspect that I mentioned: Their language LX [CW99] has no term level type dispatch primitives, only the necessary typing machinery.

This work on type dynamic and type case does not extend to the case for object oriented languages as it neglects two important features: subtypes and the creation of “new” (i.e., generative) types. For these features, the only previous work is that of Reppy and Riecke [RR96] who describe an extension of SML with objects. Included in their language are hierarchically organised object type constructors, and a case mechanism for dispatching on an object’s runtime class. They formalise this construct, and prove it sound. They sketch an implementation, but do not formalise it. This paper formalises a tagging language, which contains a similar construct. The tagging language explains class cast and class constructs, ML style exceptions, and hierarchical extensible sums, and could be used in a typed compilation of multidispatch languages such as Cecil [Cha97].

This paper also formalises a translation of the tagging language into a variant of the typed lambda calculus with some additional typing machinery. Like Crary, Weirich, and Morrisett, I use a type erasure interpretation, and the both the tagging and target languages are eraseable.^{1} Correctness theorems for the translation are stated here and proven in a companion technical report [Gle99]. I implemented the ideas in a type directed compiler as part of the TALx86 project [MCG^{+}99]. TALx86 is a typed assembly language, and the key ideas of the target language were used to augment TALx86’s type system; 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 and discuss its implementation. I begin by describing in more detail the programming language constructs being addressed. From these constructs I extract a core mechanism, 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 has static type 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 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 exceptions are also an example of extensible sums. The exception type is like a global 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. Reppy and Riecke [RR96] describe hierarhical extensible sums in connection with their class case mechanism, and note how they generalise ML style exceptions. Reppy and Fisher are incorporating a form of hierarchical extensible sums 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 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. Multimethods are similar to Castagna et al.’s overloaded functions [CGL95], except the latter are considered in a structural rather than named typed system.

1The erasure of a term is obtained by deleting all its typing annotations. A langauge is eraseable, or is said to have a type erasure interpretation, if its terms behave exactly as their erasures do.

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/case construct with type refinement in the successful branches. 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. Usually, the tests of a tag case are not “is tag t_{1} equal to tag t_{2}” but “is tag t_{1} in the subhierarchy under tag t_{2}”. I shall call “testing if a tag is under another in the tag hierarchy” a tag check. 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: creating hierarchies of type tags, tagging a value with a tag, and comparing the tag of a tagged value against known 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. For example, the ML style exception declaration exception Failure of string could be coded in the tagging language as:

let Failure = newtag(string) in

Note that for expository purposes, examples will use constructs not in the formal language, such as strings, integers, floating point numbers, and let declarations. For an example of subtags, assume string[10] is the type of strings of length 10, and is a subtype of string. The subexception declaration exception MyFailure extends Failure of string[10] could be coded as:

let MyFailure = subtag(Failure, string[10]) in

Values are tagged with the operation mktagged(⟨e_{1}, e_{2}⟩) where e_{1} is the tag, and e_{2} the value to be tagged. The result is a value of type tagged. For example, the creation of an exception packet let ep = Failure “unimplemented” could be coded as:

let ep = mktagged(Failure, “unimplemented”) in

Tagged values are compared against known tags with the operation if tagof(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. For example, exception matching such as:

match ep with

Failure(x) -> printf “Computation failed: %s” x | -> printf “Some other exception” could be coded as:

if tagof(ep) ≤ Failure then

x.printf “Computation failed: %s” x else

printf “Some other exception”

fi

The tagging language has the above operations plus ntuples and functions with their usual introduction and elimination forms. The syntax is:

Types τ, σ ::= tag(τ) | tagged | ⟨τ⃗⟩ | τ_{1} → τ_{2}
Terms e, b ::= x | newtag(τ) | subtag(τ, e) |

mktagged(e) |

if tagof(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 term fix f(x:τ_{1}):τ_{2}.b binds f and x in b, and if tagof(e_{1}) ≤ e_{2} then x.b_{1} else b_{2} fi binds x in b_{1}. I consider syntactic objects equal up to α-equivalence. The capture avoiding substitution of x for y in z is written z[y := x], and simultaneous substitution is written z[y_{1}, y_{2},:= x_{1}, x_{2}]. A sequence of objects from a syntactic class X will be written X⃗.

The operational semantics is given in Figure 1. The key part of the semantics is modelling the identity of tags. Intuitively, the abstract machine that executes tagging language programs has a memory that stores the identities and details of all tags created in the execution so far. I use a well known technique for modelling memory called an allocation style semantics (c.f. Morrisett et al. [MFH95]). In this style of semantics, a program state let H in e consists of a heap H that models the memory, and an expression e that is currently being evaluated. Heaps are finite maps from addresses to values stored in the memory, called heap values h. Addresses are usually formalised by an abstract construct called locations, or for the tagging language an abstract construct called tag names might be used. For simplicity, I use variables instead. The tagging language’s heap values are tuples ⟨v⃗⟩^{2} and tag definitions (τ, s). The latter consists of the type being tagged τ and the optional supertag s, which is either ϵ for no supertag, or a variable that is the identity of the supertag.

The most interesting reduction rules are the rules for if tagof(·) ≤ · then · else · fi. A tag check of x against y is formalised by the predicate tagchk^{H}(x, y) where H is the heap containing the tag definitions, x is the address of the unknown tag, and y is the address of the known tag. The definition of this predicate says that either x and y are the same tag or x has a supertag and the predicate holds for the 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. 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 Syntax:

2Tuples are allocated in the heap to make the tagging language and the target language closer. This makes it easier to prove operational correctness of the translation.

Values  v ::= x | mktagged(v) | fix f(x:τ_{1}):τ_{2}.b
Contexts  E ::= [] | subtag(τ, E) | mktagged(E) | ⟨v⃗, E, e⃗⟩ | E.i | E e | v E |
if tagof(E) ≤ e_{2} then x.b_{1} else b_{2} fi | if tagof(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

if tagof(mktagged(x)) ≤ y

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

if tagof(mktagged(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 1: Source Language Operational Semantics

a context and substitution based reduction semantics. Note that the semantics is deterministic, call by value, and left to right.

The tagging language is eraseable, and the types τ in the operations newtag(τ) and subtag(e, τ) and the tag definitions (τ, ϵ) and (τ, x) are not needed at runtime.

The typing rules appear in Figure 2, and consist of judgements for subtyping ⊢_{S} τ_{1} ≤ τ_{2} and for typing expressions Γ ⊢_{S} e : τ, heap values Γ ⊢_{S} h : τ, heaps ⊢_{S} H : Γ, and program states ⊢_{S} P : τ. Here Γ is a typing context that lists the types of variables. Subtyping for tag and tagged types is trivial, and subtyping for tuples and functions is standard. Note that reflexivity and transitivity of subtyping is derivable from the rules given. The rule for subtags requires that e be a tag for type τ′ and that τ be a subtype of τ′. The latter ensures that types associated with tags form a subtype hierarchy in parallel to the tag hierarchy. The rule for mktagged(e) requires that e be a pair of a type tag for τ and a value of type τ. The rule for if tagof(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 some type σ, 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 machine languages do not provide primitives like newtag(τ), subtag(τ, e), mktagged(e), and if tagof(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 checks. 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 examples in the previous section ignoring types. To create the new tag Failure the compiler would dynamically allocate a new block of memory. Since, throughout the lifetime of this new block, its address is different from the address of any other dynamically allocated memory block, the compiler can use this address as a unique identifier for the tag. The compiler needs to record the position of Failure in the tag hierarchy, so it stores a null pointer into the newly allocated block to indicate that Failure is at the top level of the hierarchy. I will use ML’s none constructor as to represent the null pointer, and ML’s some(v) to represent a non-null pointer to v. Similarly, to create MyF ailure the compiler would allocate a new block of memory and store some(F ailure) in it.

To create the tagged value ep the compiler would create a pair consisting of Failure and the literal string. So the first 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} mktagged(e) : tagged

Γ ⊢_{S} e_{1} : tagged Γ ⊢_{S} e_{2} : tag(σ) Γ, x : σ ⊢_{S} b_{1} : τ Γ ⊢_{S} b_{2} : τ

Γ ⊢_{S} if tagof(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 2: Source Language Typing Rules

three examples might become:

let Failure = ⟨none⟩ in let MyFailure = ⟨some(Failure)⟩ in let ep = ⟨Failure, “unimplemented”⟩ in

To translate the last example, the compiler would extract the tag in ep, which is the address of some dynamic memory block, and compare it against Failure. If they are equal x would be bound to the second component of ep 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 = ep.1 in loop1 : if z = Failure then let x = ep.2 in b_{1}

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

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 ep is unknown, yet if the comparison z = Failure succeeds, the type of ep.2 is string, and this fact is needed to give x type string. What makes this difficult is that z and Failure are values unrelated to ep.2. In order to make this connection clear, 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 ep together, so that type information generated by the comparison will change ep’s type.

The solution to the second problem is to use type variables to link tags to values being tagged. For example, ep’s type could be ⟨tag(α), α⟩ for a yet to be determined type constructor tag(·) and some type variable α. Then comparing z, which has type tag(α), to Failure, which has type tag(string), will cause the type checker to change α to string in the successful branch, thus changing ep.2’s type to string also.

The solution to the first problem lies in the following observation. The compiler is using the address of the memory block allocated for Failure as a name for the type string. It never uses the same address as a name for two different types, so if two addresses are equal, the types they name must be equal. To reflect this behaviour the target type system must track which addresses are names for types, and which types they name. The compiler gives the target language type tag(τ_{t}, τ_{ds}) to these pointers. These types resemble the tagging language type tag(τ_{t}), as both are for tags for type τ_{t}. However, whereas tags were primitives in the tagging language, they are explicit datastructures in the target language, and τ_{ds} reflects the type of these datastructures. In particular, a value v is in the type tag(τ_{t}, τ_{ds}) if

Types  τ, σ ::= α | tag^{ϕ}(τ_{1}, τ_{2}) | rec α.τ | ∃α.τ | τ? | ⟨τ⃗⟩ | τ_{1} → τ_{2}
Variances ϕ ::= + | − | ∘
Terms  e, b ::= x | mktag(τ, ⟨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

Figure 3: Target Language Syntax

v also has type τ_{ds} and the programmer declared v to be a tag for type τ_{t}.

Now consider the datastructures used, and the type τ_{ds} for the examples. Failure is a linked list of Failure’s ancestors, and each pointer in this linked list is being used as a name for the type string. Linked lists have type rec β.⟨β?⟩ (where τ? is an option type). So Failure has type:

tag(string) = rec β.tag(string, ⟨β?⟩)

The tagged value ep is a pair of such a tag and a string except that string is abstracted over, thus ep has type ∃α.⟨tag(α), α⟩. To get the initial value of z, ep is unpacked introducing α into the type context, and giving z the type tag(α). If z = Failure succeeds then the type z tags and the type Failure tags must be the same, that is, α is string. The target type system will use this in type checking let x = ep.2 in b_{1}. Since ep.2 has type α, which is string, x will get type the correct type.

Two complications arise with this basic scheme. The first is ensuring that a pointer is used to name only one type. If the same pointer is used to name two different types, runtime type errors could occur. To see this, assume an operation mktag(τ, e) that declares that value e is a tag for τ, and consider the following malicious code:

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

The variables x_{1}, x_{2}, and x_{3} are all bound to the same pointer, which points to 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. Therefore 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 for 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 mktag(τ, 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 mktag(τ, e) only at points where new heap values are created. For example, ⟨e⃗⟩ creates a new heap value; the target operation mktag(τ, ⟨e⃗⟩) does the same thing but gives the result type tag(τ, ⟨τ⃗⟩) where e⃗ : τ⃗.

The other complication concerns the interaction between subtyping and tag types. In particular, if tag(τ_{1}, …) ≤ tag(τ_{2}, …) then what should be the relationship between τ_{1} and τ_{2} (the second position is covariant, i.e., τ_{1} ≤ τ_{2} implies tag(τ, τ_{1}) ≤ tag(τ, τ_{2})). As we shall see, different and conflicting relationships are required by the process of creating subtags and the process of destructing tagged values. The solution is to introduce a variance mechanism that states the relationship that holds. First some terminology, the value mktag(τ, e) is said to have been created as a tag for τ. For example, Failure was created as a tag for string. Now consider the creation of a subtag. For this example, string[10] will be the type of strings of length 10, and is a subtype of string. Joe User desires a subtag of Failure, MyFailure, that tags string[10]. Using the scheme above, the translated code for MyFailure is:

let MyFailure = mktag(string[10], ⟨some(Failure)⟩) in

Consider how this type checks. MyFailure should have have tag(string[10]), and the right hand side has this type if Failure has type tag(string[10]). In fact, Failure has type tag(string) so we require that tag(string) ≤ tag(string[10]), that is:

rec β.tag(string, ⟨β?⟩)

≤ rec β.tag(string[10], ⟨β?⟩)

This would hold if tag(string, …) ≤ tag(string[10], …), in other words, a contravariant subtyping rule: if τ_{1} ≤ τ_{2} then tag(τ_{2}, …) ≤ tag(τ_{1}, …).

However, now consider tagged value destruction, and the code from above:

z : rec β.tag(α, ⟨β?⟩), ep : ⟨rec β.tag(α, ⟨β?⟩), α⟩
if z = Failure then let x = ep.2 in b_{1} else … fi

Under the contravariant rule Failure subsumes to a tag type for string[10], so the type system could type check let x = ep.2 in b_{1} under the assumption that α is string[10]. Under this incorrect assumption, x has type string[10], but ep.2 is actually a thirteen character string. Thus for destruction, subtyping must not be contravariant.

I introduce a variance mechanism^{3} to track the subtyping rules used. Now a tag type has the form tag^{ϕ}(τ_{t}, τ_{ds}) where ϕ is a variance: either covariant +, contravariant −, or invariant ∘. A value is in this type if it has type τ_{ds} and was created to tag type σ. Furthermore, the variance states the relationship between τ_{t} and σ. For covariance τ_{t} is a supertype of σ, for contravariant τ_{t} is a subtype of σ, Syntax:

3Abadi and Cardelli [AC96] describe variances and their typing rules in detail.

Values  v ::= x | roll^{τ} (v) | pack[τ_{1}, v] as τ_{2} | none^{τ} | some(v) | fix f(x : τ_{1}) : τ_{2}.b
Contexts  E ::= [] | mktag(τ, ⟨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⃗⟩ | mktag(τ, ⟨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 mktag(τ, ⟨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 mktag(τ, 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

and for invariance τ_{t} is σ. Using this new form, we can revise the type for z to tag^{−}(α, …), and type for Failure to tag^{+}(string, …). Then if z equals Failure we know that the types these tags were created to tag are equal. If σ is this type, we further know that α ≤ σ since z has the contravariant tag type, and that σ ≤ string as Failure has the covariant tag type. So α ≤ string and it safe to assume x : string in b_{1}.

The key is the relationship between the static tag type and the runtime tag type. In creating tagged values and subtags, we want the static tag type to be a subtype of the runtime tag type, and for destructing tagged values, we want the runtime tag type to be a subtype of the static type so that the type system conservatively refines types. The variance mechanism tracks and ensures the correct relationships.

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 incorporates the keys ideas of the previous section, that is, tag types with a variance mechanism and physical pointer equality, with a typical typed lambda calculus. The syntax appears in Figure 3. The operation mktag(τ, ⟨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 ntuples and functions as before. In addition the translation will need recursive types, existentials, and option types. The 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. I also include a special let form let x_{1} = e_{1} and x_{2} = e_{2} in e. This expression first evaluates e_{1} to a value v_{1}, then evaluates e_{2} to a value v_{2}, and the evaluates e with v_{i} substituted for x_{i}. It makes the proof of operational correctness simpler.

The operational semantics is similar in spirit to the tagging language, and is given in Figure 4. Like in the tagging language, the heap is used to remember identities, in particular, the identities of the tuples created. Two tuples, or pointers, are equal if they have the same address, that is, if they are the same variable. Hence the rules for the if construct.

The target language is eraseable. The operation mktag(τ,

e) is equivalent to e, and the annotation mktag(τ, ·) on heap values is not needed at runtime.

The static semantics appears in Figures 5 and 6. Note that a typing context of the form Δ, α ≤ τ must have ftv(τ) ⊆ Δ. This syntactic restriction ensures that all typing contexts are well formed, which simplifies the proof of soundness. The static semantics is straightforward except for the tagging constructs. First, values in the type tag^{ϕ}(τ_{t}, τ_{ds}) also have type τ_{ds}, and the rule tag-sub reflects this specialised subsumption principle. This rule is used to manipulate the datastructure a type tag contains.

The two rules for tag comparison deserve mention.

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

Rule t1 is for comparing an unknown tag against a known one. This is the rule used to type the translation, which always unpacks an existentially quantified package, extracts from it a tag for the quantified type, and compares it to a known tag. The rule requires the unknown tag e_{1} to be a tag for a supertype of some type variable α, the known tag e_{2} to be a tag for a subtype of a closed type. I assume, 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.

However, rule t1 is not closed under type substitution. In particular, if a closed type is substituted for α then the expression compares two tags for known types, and the rule no longer applies. Thus to prove type substitution and thus type soundness, the rule t2 is used to type this case. It requires both e_{1} and e_{2} to be tags for known closed types σ_{1} and σ_{2} respectively. 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 the companion technical report [Gle99]. 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}. Then by rule t2 the then branch must type check. The other difference is the type substitution lemma mentioned earlier.

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 an existential abstracting over α a pair of a tag for α and an α. The operations newtag(τ), subtag(τ, e), and mktagged(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 presenting 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. These theorems are stated below and are proven in the companion technical report [Gle99]. Proving type preservation is a straightforward inductive proof. 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

\begin{matrix}Δ; Γ ⊢_{T} e : τ_{1} & Δ ⊢_{T} τ_{1} ≤ τ_{2} \\ Δ; Γ ⊢_{T} e : τ_{2} \end{matrix}  [rule tag-sub] {Δ; Γ ⊢_{T} e : tag^{ϕ}(τ, σ) \atop Δ; Γ ⊢_{T} e : σ}
Δ; Γ ⊢_{T} x : τ (Γ(x) = τ)

Δ; Γ ⊢_{T} e_{i} : τ_{i} Δ ⊢_{T} τ

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

[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} e_{1} : tag^{−}(σ_{1}, τ_{1}) ϵ ⊢_{T} σ_{1}
Δ; Γ ⊢_{T} e_{2} : tag^{+}(σ_{2}, τ_{2}) ϵ ⊢_{T} σ_{2}

(ϵ ⊢_{T} σ_{1} ≤ σ_{2} ⇒ Δ; Γ ⊢_{T} b_{1} : τ)

Δ; Γ ⊢_{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

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}  = mktag([[τ]]_{type}, ⟨roll^{tag′([[τ]]_{type})}(none^{tag(−,[[τ]]_{type})})⟩)
[[subtag(τ, e)]]_{exp}  = mktag([[τ]]_{type}, ⟨roll^{tag′([[τ]]_{type})}(some([[e]]_{exp}))⟩)
[[mktagged(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

[[if tagof(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}  = mktag([[τ]]_{type}, ⟨roll^{tag′([[τ]]_{type})}(none^{tag(−,[[τ]]_{type})})⟩)
[[(τ, x)]]_{hval}  = mktag([[τ]]_{type}, ⟨roll^{tag′([[τ]]_{type})}(some(x))⟩)
[[⟨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

simulation argument. Most of the work is in showing that tag checks are implemented properly.

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

Theorem 4.2 If ⊢_{S} P_{1} : τ and P_{1} ↦ P_{2} then [[P_{1}]]_{prog} ↦^{+} [[P_{2}]]_{prog}. (An appropriate converse also holds.)

5 Extensions and Implementation

The implementation given is quite naive, although it requires only constant space for each tag, it takes time linear in the height of the tag hierarchy for each tag check. Java implementations typically trade space for time, and represent a tag as an array of all of the tag’s ancestors. This implementation requires only one array subscript and one physical pointer equality test per tag check, but uses space proportional to the height of the tag hierarchy per tag. Also, this scheme is not suitable for multiple inheritance hierarchies. The companion technical report [Gle99] shows how to express this array scheme in a variant of the target language. I expect that most schemes for implementing multiple inheritance hierarchies that use pointer comparisons, could also be expressed in variants of the target language.

For expository purposes, I used a type lambda calculus as the target of the translation. However, the ideas could be applied to other languages. In fact, they were used to augment TALx86 [MCG^{+}99], a typed assembly language [MWCG98] for Intel’s IA32 architecture, to provide support for exceptions and downcasting in object oriented languages. This implementation was straightforward: 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. Furthermore, the array scheme mentioned above could be implemented in the augmented TALx86.

6 Related Work

Reppy and Riecke [RR96] describe an extension of SML with objects. Their language contains a class case mechanism, and they discuss the connections of this mechanism with hierarchy extensible sums and exceptions. Their paper includes a formalised core calculus, and a sketch of their implementation. There are three important differences between their system and the one presented in this paper. First, their tags are second class, whereas mine are first class. Second, their type system is named, whereas mine is structural. Third, they do not formalise their implementation nor discuss the typing issues that arise. Harper and Stone [HS97] formalise a non-hierarchical extensible sum for modelling exceptions in a type theoretic account of SML. Their extensible sum is like my tagging language without subtags. However, they do not discuss implementation issues.

Type dispatch in a structurally typed language was first discussed by Abadi et al. [ACPP91]. Harper and Morrisett [HM95, Mor95] discuss the related problem of type analysis, and formalise a type dispatch language for structural types without subtyping. Crary, Weirich, and Morrisett’s work on λ^{R} and LX [CWM98, CW99] shows how to do type analysis in a type erasure framework. Their work is the only work I know of that addresses the implementation of type dispatch for structural types. I know of no work that addresses structural types with subtyping.

I think it is worth spelling out the two key differences between the type analysis of structural types and my problem. 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. Second, my language is concerned with branded types whereas λ^{R} is concerned with the types themselves. Consider my informal coding of exceptions. In O’Caml 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.

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 type analysis of structural types, 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.

[ACPP91] Martín Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Progamming Languages and Systems, 13(2):237–268, April 1991.

[CGL95] Giuseppe Castanga, Giorgio Ghelli, and Guiseppe Longo. A calculus for overloaded functions with subtyping. Information and Computation, 117(1):115– 135, 1995.

[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. In 1999 ACM SIGPLAN International Conference on Functional Programming, Paris, France, September 1999. This volume.

[CWM98] Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type-erasure semantics. In 1998 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 1999 ACM SIG-PLAN Conference on Programming Language Design and Implementation, Atlanta, GA, USA, May 1999. 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.

[Gle99] Neal Glew. Type dispatch for named hierarchical types. Technical Report TR99-1738, Department of Computer Science, Cornell University, 4130 Upson Hall, Ithaca, NY 14853-7501, USA, April

1999. Available at http://www.cs.cornell.edu/
glew/paper-list.html.

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

[HS97] Robert Harper and Christopher Stone. An interpretation of Standard ML in type theory. Technical Report CMU-CS-97-147, Carnegie Mellon University, Pittsburgh, PA 15213, June 1997.

[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 typed assembly language. In ACM SIGPLAN Workshop on Compiler Support for System Software, volume 0228 of INRIA Research Reports, Atlanta, GA, USA, May 1999.

[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 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85– 97, San Diego California, USA, January 1998. ACM Press.

[RR96] John Reppy and Jon Riecke. Simple objects for Standard ML. In 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 171–180. ACM Press, 1996.

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