Alias Types for Recursive Data Structures ^{∗} (Extended Version)

David Walker and Greg Morrisett

Cornell University

Abstract

Linear type systems permit programmers to deallocate or explicitly recycle memory, but they are severly restricted by the fact that they admit no aliasing. This paper describes a pseudo-linear type system that allows a degree of aliasing and memory reuse as well as the ability to define complex recursive data structures. Our type system can encode conventional linear data structures such as linear lists and trees as well as more sophisticated data structures including cyclic and doubly-linked lists and trees. In the latter cases, our type system is expressive enough to represent pointer aliasing and yet safely permit destructive operations such as object deallocation. We demonstrate the flexibility of our type system by encoding two common compiler optimizations: destination-passing style and Deutsch-Schorr-Waite or “link-reversal” traversal algorithms.

1 Introduction

Type-safe programming languages, such as Haskell, Java, and ML, do not give programmers control over memory management. In particular, these languages do not allow programmers to separate allocation and initialization of memory objects, nor do they allow explicit re-use of memory objects. Rather, allocation and initialization of objects are presented to the programmer as an atomic operation, and re-use of memory is achieved “under the covers” through garbage collection. In other words, memory management is achieved by meta-linguistic mechanisms that are largely outside the control of the programmer.

In type-unsafe languages such as C or C++, programmers have control over memory management so they can tailor routines for application-specific constraints, where the time and/or space overheads of general-purpose memory management mechanisms do not suffice. However, such languages have a far more complicated and error-prone programming model. In particular, neither the static type systems, the compilers, nor the run-time systems of these languages prevent the accidental use of uninitialized objects, or the accidental re-use of memory at an incompatible type. Such errors are extremely costly to diagnose and correct.

Our ultimate goal is to provide support for programmercontrolled memory management, without sacrificing typesafety, and without incurring significant overhead. In addition, we hope to discover general typing mechanisms and principles that allow greater lattitude in the design of lowlevel languages intended for systems applications or as the target of certifying compilers [22, 23]. In this paper, we take a step further towards these goals by developing a type system that gives fine-grained control over memory management, for a rich class of recursively defined datatypes. We demonstrate the power of the type system by showing how we can safely encode two important classes of optimization, destination-passing style and link-reversal traversals of data structures.

1.1 Background

One well-known principle for proving type safety is based upon type-invariance of memory locations. Simply put, this property says that, when allocated, a memory object should (conceptually) be stamped with its type, and that the type of the object should not change during evaluation. When this property is maintained, it is straightforward to prove a subject-reduction or type-preservation property (see for example [36, 11]), which is in turn crucial to establishing type-soundness. There are many examples from language design where this principle has been violated and resulted in an unsoundness. For instance, the naive treatment of polymorphic references in an ML-like language, or the covariant treatment of arrays in a Java-like language, both violate this basic principle.

From the type-invariance principle, it becomes clear why most type-safe languages do not support user-level initialization or memory recycling: the type τ of the memory object cannot change, so (1) it must initially have type τ and (2) must continue to have type τ after an evaluation step. Atomic allocation and initialization ensures the first invariant, and the lack of explicit re-cycling ensures the second. Thus, it appears that some meta-linguistic mechanism is necessary to achieve memory management when the typeinvariance principle is employed.

Linear type systems [35, 33] employ a different principle to achieve subject-reduction. In a linear setting, the crucial invariant is that memory objects must have exactly one reference — that is, no object can be aliased. Unlike the traditional approach, the type of a memory object can change over time and thus, explicit initialization and re-cycling can be performed in the language. Unfortunately, the inability to share objects through aliasing can have a steep cost: Many common and efficient data structures that use sharing or involve cycles cannot be implemented.

In recent previous work, we considered a generalization of linear types that supported a very limited degree of aliasing [29]. Like linear type systems, our alias types supported separation of allocation and initialization, and explicit reuse of memory, but unlike linear approaches, some objects could have more than one reference. To achieve subject reduction, we tracked aliasing in the type system by giving memory objects unique names, and maintained the invariant that the names were unique. We found that alias types unified a number of ad-hoc features in our Typed Assembly Language, including the treatment of initialization and control stacks. Furthermore, the alias type constructors were easy to add to our type checker for TALx86 [31].

∗This material is based on work supported in part by the AFOSR grant F49620-97-1-0013 and the National Science Foundation under Grant No. EIA 97-03470. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not reflect the views of these agencies.

Unfortunately, the named objects in our alias-type system were restricted to a “second-class” status; though named objects could be passed to and from functions, the type system prevented a programmer from placing these objects in a recursive datatype such as a list or tree. The problem is that our type system did not track aliasing beyond a certain compile-time “frontier”, and in this respect, was similar to the k-limiting approaches used in alias analysis [12]. As a result, we could not embed linear datatypes into our language, and the opportunities for user-level memory management were greatly reduced.

In this paper, we extend alias types to cover recursive datatypes in full generality. Our type system is powerful enough to encode linear variants of lists and trees, as well as richer data structures with complex shapes and aliasing relationships, such as cyclic or doubly-linked lists and trees. The critical addition to the type system is a mechanism for combining recursive type operators with first-class store abstractions that represent repeated patterns of aliasing. In this respect, our work is inspired by the more complex approaches to alias and shape analysis that have recently appeared in the literature [7, 9, 26].

The generalization to recursive datatypes opens the door for users or certifying compilers to have far more control over the memory management of complex data structures. To demonstrate this fact, we show how two classes of space optimization can be encoded in a language based on recursive alias types. The first optimization, called destinationpassing style [34, 16, 5] transforms algorithms that are “tailrecursive modulo allocation” into properly tail-recursive algorithms, thereby avoiding the space overheads of a control stack. The second optimization shows how we can safely encode Deutsch-Schorr-Waite algorithms [28] for traversing a tree using minimal additional space, based on link-reversal.

In the following section, we motivate the type structure of the language by introducing a series of type-theoretic abstraction mechanisms that enable suitable approximations of the store. We then show how these constructors may be used to encode a number of common data structures, without losing the ability to explicitly manage memory. Section 3 formalizes these ideas by presenting the syntax and static semantics of a programming language that includes instructions for allocating, deallocating, and overwriting memory objects. Section 4 shows how the destination-passing style and link-reversal optimizations can be safely encoded in the language. Section 5 presents an operational semantics for the language and states a type soundness theorem. We close in Section 6 by further discussing related work.

2 Types for describing store shapes

The linear type τ_{1} ⊗τ_{2} captures an extremely valuable memory management invariant: There is only one access path to any value with this type. Consequently, if x has type τ_{1} ⊗τ_{2} then once both its components have been extracted, it is safe to reuse x to store new values with incompatible types. Since the only way to access x’s data is through x itself, there is no chance that this reuse can introduce inconsistent views of the store and unsoundness into the system.

Unfortunately, the restriction to a single access path makes it impossible to construct a number of important data structures. Our goal is to lift this restriction and yet retain the capacity to reuse or deallocate memory when there is a pointer to it. Our approach is based on the intuition that a linear data structure may be decomposed into two parts, a piece of state and a pointer to that state. Destructive operations such as memory reuse alter only the state component and leave the pointer part unchanged. Consequently, if the goal is to ensure no inconsistencies arise, only the state component need be treated linearly. The pointer may be freely copied, making it possible to construct complex data structures with shared parts. Of course, in order to actually use a pointer, there must be some way to relate it to the state it points to. We make this relationship explicit in the type system by introducing locations, ℓ, that contain the state component, and by specializing the type of a pointer to indicate the location it points to. Consider again the linear pair τ_{1} ⊗ τ_{2}. We factor it into two parts:

• A type for the state, called an aliasing constraint or store description, that takes the form {ℓ ↦ ⟨τ_{1}, τ_{2}⟩}. This type states that at location ℓ there exists a memory block containing objects with types τ_{1} and τ_{2}.

• A type for a pointer to the location: ptr(ℓ). This type is a singleton type—any pointer described by this type is a pointer to the one location ℓ and to no other location.

This simple trick provides a tremendous flexibility advantage over conventional linear type systems because even though constraints may not alias one another, there is no explicit restriction on the way pointer types may be manipulated.

We build complicated data structures by joining a number of aliasing constraints together using the ⊗ constructor. For example, the following DAG may be specified by the constraints below.

[figure: 3; ℓ_{1}:; ℓ_{2}:; ℓ_{3}:]
{ℓ_{1} ↦ ⟨ptr(ℓ_{2}), ptr(ℓ_{3})⟩} ⊗
{ℓ_{2} ↦ ⟨ptr(ℓ_{3})⟩} ⊗
{ℓ_{3} ↦ ⟨int⟩}

In this type, the locations ℓ_{1}, ℓ_{2} and ℓ_{3} are necessarily distinct from one another because they all appear on left-hand sides in this collection of constraints. The type system maintains the invariant that if a store is described by constraints {ℓ_{1} ↦ τ_{1}} ⊗ ⋯ ⊗ {ℓ_{n} ↦ τ_{n}} then each of the locations ℓ_{i} must be different from one another. This invariant resembles invariants for the typing context of a standard linear type system. For example, the linear context x_{1}:τ_{1}, …, x_{n}:τ_{n} implies that the x_{i} are distinct values with linear types τ_{i}. However, the analogy is not exact because a linear type system prevents any of the x_{i} from being used more than once whereas our calculus allows pointers to the locations ℓ_{i} to be used over and over again and this flexibility makes it possible to represent aliasing: In the type above, there are two paths from location ℓ_{1} to location ℓ_{3}, one direct and one indirect through location ℓ_{2}.

One other important invariant is that although the ⊗ constructor is reminiscent of linear pairs, the ordering of the constraints joined by ⊗ is not important: {ℓ_{1} ↦ τ_{1}}⊗{ℓ_{2} ↦ τ_{2}} is equivalent to {ℓ_{2} ↦ τ_{2}} ⊗ {ℓ_{1} ↦ τ_{1}}. For the sake of brevity, we often abbreviate {ℓ_{1} ↦ τ_{1}} ⊗ {ℓ_{n} ↦ τ_{n}} with {ℓ_{1} ↦ τ_{1}, …, ℓ_{n} ↦ τ_{n}}.

2.1 Abstraction mechanisms

Any particular store can be represented exactly using these techniques^{1}, even stores containing cyclic data structures. For example, a node containing a pointer to itself may be represented with the type {ℓ ↦ ⟨ptr(ℓ)⟩}. However, the principle difficulty in describing aliasing relationships is not specifying one particular store but being able to specify a class of stores using a single compact representation. We use the following type-theoretic abstraction mechanisms to describe a wide class of pointer-rich data structures.

Location Polymorphism In general, the particular location ℓ that contains an object is inconsequential to the algorithm being executed. The relevant information is the connection between the location ℓ, the contents of the memory residing there, and the pointers ptr(ℓ) to that location. Routines that only operate on specific concrete locations are almost useless. If, for example, the dereference function could only operate on a single concrete location ℓ, we would have to implement a different dereference function for every location we allocate in the store! By introducing location polymorphism, it is possible to abstract away from the concrete location ℓ using a variable location ρ, but retain the necessary dependencies. We use the meta-variable η to refer to locations generically (either concrete or variable).

Store Polymorphism Any specific routine only operates over a portion of the store. In order to use that routine in multiple contexts, we abstract irrelevant portions of the store using store polymorphism. A store described by the constraints ϵ⊗{η ↦ τ} contains some store of unknown size and shape ϵ as well as a location η containing objects with type τ. We use the meta-variable C to range over aliasing constraints in general.

Unions Unlike polymorphic types, unions provide users with the abstraction of one of a finite number of choices. A memory block that holds either an integer or a pointer may be encoded using the type ⟨int⟩ ∪ ⟨ptr(η)⟩. However, in order to use the contents of the block safely, there must be some way to detect which element of the union the underlying value actually belongs to. There are several ways to perform this test: through a pointer equality test with an object of known type, by descriminating between small integers (including null/0) and pointers, or by distinguishing between components using explicit tags. All of these options will be useful in an implementation, but here we concentrate on the third option. Hence, the alternatives above will be encoded using the type ⟨S(1), int⟩∪⟨S(2), ptr(η)⟩ where S(i) is another form of singleton type — the type containing only the integer i.

Recursion As yet, we have defined no mechanism for describing regular repeated structure in the store. We use standard recursive types of the form μα.τ to capture this notion. However, recursion by itself is not enough. Consider an attempt to represent a store containing a linked list in the obvious way: {η ↦ μα.⟨S(1)⟩ ∪ ⟨S(2), α⟩}.^{2} An unfolding of this definition results in the type {η ↦ ⟨S(1)⟩ ∪ ⟨S(2), ⟨S(1)⟩ ∪ ⟨S(2), List⟩⟩}, rather than the type {η ↦ ⟨S(1)⟩ ∪ ⟨S(2), ptr(η′)⟩, η′ ↦ ⟨S(1)⟩ ∪ ⟨S(2), List⟩}. The former type describes a number of memory blocks flattened into the same location whereas the latter type describes a linked collection of disjoint nodes.

Encapsulation In order to represent linked recursive structures properly, each unfolding must encapsulate its own portion of the store. We use an existential type for this purpose. Hence, a sensible representation for linked lists is

μα.⟨S(1)⟩ ∪ ∃[ρ:Loc | {ρ ↦ α}].⟨S(2), ptr(ρ)⟩

The existential ∃[ρ:Loc | {ρ ↦ τ_{1}}].τ_{2} may be read “there exists some location ρ, different from all others in the program, such that ρ contains an object of type τ_{1}, and the value contained in this data structure has type τ_{2}. More generally, an existential has the form ∃[Δ | C].τ. It abstracts a sequence of type variables with their kinds, Δ, and encapsulates a store described by some constraints C. In our examples, we will omit the kinds from the sequence Δ as they are clear from context. A similar definition gives rise to trees:

\begin{matrix}μα.⟨S(1)⟩ ∪ ∃[ρ_{1}, ρ_{2} | \{ρ_{1} ↦ α, ρ_{2} ↦ α\}]. \\ ⟨S(2), ptr(ρ_{1}), ptr(ρ_{2})⟩ \end{matrix}

Notice that the existential abstracts a pair of locations and that both locations are bound in the store. From this definition, we can infer that the two subtrees are disjoint. For the sake of contrast, a DAG in which every node has a pair of pointers to a single successor is coded as follows. Here, reuse of the same location variable ρ indicates aliasing.

μα.⟨S(1)⟩ ∪ ∃[ρ | {ρ ↦ α}].⟨S(2), ptr(ρ), ptr(ρ)⟩

Cyclic lists and trees with leaves that point back to their roots also cause little problem—simply replace the terminal node with a memory block containing a pointer type back to the roots.

CircularList =
{ρ_{1} ↦ μα.⟨S(1), ptr(ρ_{1})⟩∪
∃[ρ_{2} | {ρ_{2} ↦ α}].⟨S(2), ptr(ρ_{2})⟩}
CircularT ree =
{ρ_{1} ↦ μα.⟨S(1), ptr(ρ_{1})⟩∪
∃[ρ_{2}, ρ_{3} | {ρ_{2} ↦ α, ρ_{3} ↦ α}].
⟨S(2), ptr(ρ_{2}), ptr(ρ_{3})⟩}

Parameterized Recursive Types One common data structure we are unable to encode with the types described so far is the doubly-linked list. Recursive types only “unfold” in one direction, making it easy to represent pointers from a parent “down” to its children, or all the way back up to the top-level store, but much more difficult to represent pointers that point back up from children to their parents, which is the case for doubly-linked lists or trees with pointers back to their parent nodes. Our solution to this problem is to use parameterized recursive types to pass a parent location down to its children. In general, a parameterized recursive type has the form rec α (β_{1}:κ_{1}, …, β_{n}:κ_{n}).τ and has kind (κ_{1}, …, κ_{n}) → Type. We will continue to use unparameterized recursive types μα.τ in examples and consider them to be an abbreviation for rec α ().τ[α ()/α]. Once again, kinds will be omitted when they are clear from the context. Trees in which each node has a pointer to its parent may be encoded as follows.

1We cannot represent a store containing a pointer into the middle of a memory block.

2Throughout we use the convention that union binds tighter than the recursion operator.

{ρ_{root} ↦ ⟨S(2), ptr(ρ_{L}), ptr(ρ_{R})⟩} ⊗
{ρ_{L} ↦ REC (ρ_{root}, ρ_{L})} ⊗
{ρ_{R} ↦ REC (ρ_{root}, ρ_{R})}

where

REC =
rec α (ρ_{prt}, ρ_{curr}).
⟨S(1), ptr(ρ_{prt})⟩∪
∃[ρ_{L}, ρ_{R} | {ρ_{L} ↦ α (ρ_{curr}, ρ_{L})}⊗
{ρ_{R} ↦ α (ρ_{curr}, ρ_{R})}].
⟨S(2), ptr(ρ_{L}), ptr(ρ_{R}), ptr(ρ_{prt})⟩

The tree has a root node in location ρ_{root} that points to a pair of children in locations ρ_{L} and ρ_{R}, each of which are defined by the recursive type REC. REC has two arguments, one for the location of its immediate parent ρ_{prt} and one for the location of the current node ρ_{curr}. Either the current node is a leaf, in which case it points back to its immediate parent, or it is an interior node, in which case it contains pointers to its two children ρ_{L} and ρ_{R} as well as a pointer to its parent. The children are defined recursively by providing the location of the current node (ρ_{curr}) for the parent parameter and the location of the respective child (ρ_{L} or ρ_{R}) for the current pointer.

Function Types Functions are polymorphic with type arguments Δ and they express the shape of the store (C) required by the function: ∀[Δ | C].(τ_{1}, …, τ_{n})→0. The underlying term language will be written in continuation-passing style and therefore functions never return, but instead call another function (the function’s continuation). We use the notation “→ 0” to indicate this fact. Continuation-passing style is extremely convenient in this setting because it makes the flow of control explicit in the language and the store shape varies from one control-flow point to the next.

2.2 Summary of Type Structure

The formal syntax for the type constructor language is defined in the table below. We distinguish a subset of the types, called small types, for which no additional storage need be allocated when they are copied. The small types contain objects such as integers, functions^{3} and data pointers. Function parameters are required to contain small types because function application is modeled by substitution, which copies values. Likewise, fields of memory blocks must be small because field projection copies values.

   kinds  κ ::= Loc | Store | Small | Type |

(κ_{1}, …, κ_{n}) → Type
con. vars  β ::= ρ | ϵ | α
con. ctxts  Δ ::= · | Δ, β:κ
constructors c ::= η | C | τ

locations  η ::= ρ | ℓ
constraints C ::= ∅ | C ⊗ {η ↦ τ} | C ⊗ ϵ
types  τ ::= α | σ | ⟨σ_{1}, …, σ_{n}⟩ |
τ_{1} ∪ τ_{2} | ∃[Δ | C].τ |
rec α (Δ).τ | c (c_{1}, …, c_{n})
small types σ ::= α | int | S(i) | ptr(η) |
∀[Δ | C].(σ_{1}, …, σ_{n}) → 0

A judgement Δ ⊢ c : κ states that a type is well-formed and has kind κ according to the assignment of free type variables to kinds given by Δ. Locations have kind Loc, aliasing constraints have kind Store, small types have the kind Small, but like the other types, may also be given kind Type. Recursive types have arrow kinds that can be eliminated through constructor application c (c_{1}, …, c_{n}). The judgement Δ ⊢ c_{1} = c_{2} : κ states that type constructors c_{1} and c_{2} are equivalent and well-formed with kind κ. Types are considered equivalent up to alpha-conversion of bound variables and constraints are considered equivalent up to reordering of the elements in the sequence. A recursive type is not considered equal to its unfolding. The formal rules for these judgements are straightforward and they appear in Appendix A.

We use the notation A[X/x] to denote the captureavoiding substitution of X for a variable x in A. Occasionally, we use the notation X[c_{1}, …, c_{n}/Δ] to denote captureavoiding substitution of constructors c_{1}, …, c_{n} for the corresponding type variables in the domain of Δ. Substitution is defined in the stardard way in all cases except for the substitution of constraints in constraints. Substitution of C′ for a constraint variable ϵ in C appends the list C′ to the list C. We use the notation C′@C to denote the result of appending C to C′ (notice that C ⊗ C′ is not syntactically well-formed). For example,

\begin{matrix}(∅ ⊗ a_{1} ⊗ ⋯ ⊗ a_{m})@(∅ ⊗ a′_{1} ⊗ ⋯ ⊗ a′_{n}) = \\ ∅ ⊗ a_{1} ⊗ ⋯ ⊗ a_{m} ⊗ a′_{1} ⊗ ⋯ ⊗ a′_{n} \end{matrix}

Formally, substitution for constraints is defined as follows.

(C ⊗ ϵ)[C′/ϵ] = (C[C′/ϵ])@C′

We will continue to omit the initial “∅” when a constraint is non-empty. For example, we write {η ↦ τ} instead of ∅ ⊗ {η ↦ τ}.

3 Term Structure

The term structure is split into three classes: values, instructions, and coercions. The grammar below describes the syntax of the language.

values  v ::= x | i | S(i) | v[c] |

fixf[Δ | C](x_{1}:σ_{1}, …, x_{n}:σ_{n}).ι

instruct’s ι ::= new ρ, x, i; ι | free v; ι |

let x = (v).i; ι | (v_{1}).i := v_{2}; ι | case v (inl ⇒ ι_{1} | inr ⇒ ι_{2}) | v(v_{1}, …, v_{n}) | halt v |

                                                                            coerce(γ); ι

coercions γ ::= union_{τ_{1}∪τ_{2}}(η) |

roll_{rec α (Δ).τ (c_{1},...,c_{n})}(η) |

                                                                            unroll(η) |

pack_{[c_{1},...,c_{n}|C]as ∃[Δ|C].τ} (η) |

                                                                            unpack η with Δ

3For the purposes of this paper, we ignore the space required by closures. The language is powerful enough to encode closure conversion in the style of Morrisett et al. [22]. If desired, closure environments can be represented as memory blocks and functions can be required to be closed.

Δ; Γ ⊢ v : τ

Δ; Γ ⊢ x : Γ(x)  Δ; Γ ⊢ i : int  Δ; Γ ⊢ S(i) : S(i)

Δ ⊢ ∀[Δ′ | C′].(σ_{1}, …, σ_{n}) → 0 = σ_{f} : Small ΔΔ′; C′; Γ, f:σ_{f} , x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ ι

Δ; Γ ⊢ fixf[Δ′ | C′](x_{1}:σ_{1}, …, x_{n}:σ_{n}).ι : σ_{f}

\begin{matrix}Δ; Γ ⊢ v : ∀[β:κ, Δ′ | C′].(σ_{1}, …, σ_{n}) → 0 & Δ ⊢ c : κ \\ Δ; Γ ⊢ v[c] : (∀[Δ′ | C′].(σ_{1}, …, σ_{n}) → 0)[c/β] \end{matrix}

Δ; Γ ⊢ v : σ′ Δ ⊢ σ′ = σ : Small

Δ; Γ ⊢ v : σ

Δ; Γ ⊢ v : τ′ Δ ⊢ τ′ = τ : Type
Δ; Γ ⊢ v : τ

Figure 1: Static Semantics: Values

Values Values consist of integers, singleton integers, and functions. Their typing judgements have the form Δ; Γ ⊢ v : τ where Γ is a finite partial map from value variables to small types. The rules are mostly standard and are presented in figure 1. Notice that functions may be recursive and contain a specification of the polymorphic variables Δ, the requirements on the store C and the types of the parameters. These preconditions are used to type the instruction sequence that forms the body of the function. The value v[c] denotes type application of the polymorphic function v to type constructor c. We often abbreviate successive type applications v[c_{1}] ⋯ [c_{n}] by v[c_{1}, …, c_{n}]. Later, when we give an operational semantics for the language, we will add other values (such as pointers and memory blocks), but these objects only appear at run time and so we omit them for now.

Instructions Figure 2 present the typing rules for the instructions. The judgement Δ; C; Γ ⊢ ι states that in type context Δ, a store described by C and value context Γ, the instruction sequence ι is well-formed.

The principle interest of the language is the typing of memory management instructions. Operationally, the new ρ, x, i instruction allocates a memory block of size i at a fresh location and substitutes the location for ρ and a pointer to that location for x in the remaining instructions.^{4} This operation is modeled in the type system by extending the store description with a memory type of length i. Initially, the fields of the memory block have type S(0) since we assume the allocator returns zeroed-out memory.^{5} Once a block has been allocated, it may be operated on by accessor functions let x = (v_{1}).i and (v_{1}).i := v_{2}, which project from or store into the i^{th} field of v_{1}. The projection operation is well-formed if v_{1} is a pointer to some location η and that location contains a object with type ⟨σ_{1}, …, σ_{n}⟩ (where i is less than n). In this case, the remaining instructions ι must be well-formed given the additional assumption that x has type σ_{i}. The update operation is similar in that v_{1} must be a pointer to a location containing a memory block. However, the remaining instructions are verified in a context where the type of the memory block has changed: The i^{th} field has type σ where σ is the type of the object being stored into that location, but is otherwise unconstrained. Although surprising at first, this rule is sound because the constraints behave linearly. Despite the fact that the type of a memory block at a location changes, each location can only appear once in the domain of a store type and therefore there is no opportunity to introduce inconsistencies into the store typing. Constraints such as {η ↦ τ} ⊗ {η ↦ τ′} will never describe a well-formed store. The instruction free v frees the memory block pointed to by v. This effect is reflected in the typing rule for free by requiring that the remaining instructions be well-formed in a context C′ that does not include the location η.

The typing of the case expression is also somewhat unusual. Operationally, case checks the first field of the memory block in the location pointed to by a value v. If the first field is a 1, execution continues with the first instruction sequence, and if it is a 2, execution continues with the second instruction sequence. However the memory type constructor ⟨⋯⟩ will not be the top-most type constructor (otherwise, the case would be unnecessary). The type system expects a union type to be the top-most and each alternative may contain some number (possibly zero) of existential quantifiers to abstract the store encapsulated in that alternative. The underlying memory value must have either tag 1 or tag 2 in its first field. As mentioned earlier, it is possible to formulate other union elimination constructs including pointer equality checks or discrimination between pointers and small integers (such as null implemented by 0).

Because the language has been defined in continuationpassing style, all instruction sequences are either terminated by a function call v(v_{1}, …, v_{n}) or a call to the terminal continuation halt, which requires an integer argument. Function calls are well-formed if the polymorphic function v has been fully instantiated, the constraints in the current context equal the constraints required by the function, and the argument types match the types of the function parameters.

The last instruction coerce(γ) applies a typing coercion to the store. Coercions, unlike the other instructions are for type-checking purposes only. Intuitively, coercions may be erased before executing a program and the run-

4For the purposes of alpha-conversion, ρ and x are considered bound by this instruction.

5If an allocator returns unzeroed, random memory, it is may be modelled by adding a Top type and returning a memory block with fields of type Top.

Δ; C; Γ ⊢ ι

Δ, ρ:Loc; C ⊗ \{ρ ↦ \overbrace{⟨S(0), …, S(0)⟩}^{i}\}; Γ, x:ptr(ρ) ⊢ ι

Δ; C; Γ ⊢ new ρ, x, i; ι

(x ∉ Dom(Γ), ρ ∉ Dom(Δ))

Δ; Γ ⊢ v : ptr(η) Δ ⊢ C = C′ ⊗ {η ↦ ⟨σ_{1}, …, σ_{n}⟩} : Store Δ; C′; Γ ⊢ ι
Δ; C; Γ ⊢ free v; ι

Δ; Γ ⊢ v : ptr(η)  Δ ⊢ C = C′ ⊗ {η ↦ ⟨σ_{1}, …, σ_{n}⟩} : Store  Δ; C; Γ, x:σ_{i} ⊢ ι

Δ; C; Γ ⊢ let x = (v).i; ι (\begin{matrix}1 ≤ i ≤ n \\ x ∉ Dom(Γ) \end{matrix})

Δ; Γ ⊢ v_{1} : ptr(η) Δ ⊢ C = C′ ⊗ {η ↦ ⟨σ_{1}, …, σ_{i}, …, σ_{n}⟩} : Store Δ; Γ ⊢ v_{2} : σ Δ; C′ ⊗ {η ↦ ⟨σ_{1}, …, σ, …, σ_{n}⟩}; Γ ⊢ ι

Δ; C; Γ ⊢ (v_{1}).i := v_{2}; ι (1 ≤ i ≤ n)

Δ; Γ ⊢ v : ptr(η) Δ ⊢ C = C′ ⊗ {η ↦ τ_{1} ∪ τ_{2}} : Store Δ ⊢ τ_{1} = ∃[Δ′_{1} | C′_{1}]. · · · ∃[Δ′_{j} | C′_{j}].⟨S(1), σ′_{1}, …, σ′_{k}⟩ : Type Δ ⊢ τ_{2} = ∃[Δ′′_{1} | C′′_{1}]. · · · ∃[Δ′′_{m} | C′′_{m}].⟨S(2), σ′′_{1}, …, σ′′_{n}⟩ : Type Δ; C′ ⊗ {η ↦ τ_{1}}; Γ ⊢ ι_{1} Δ; C′ ⊗ {η ↦ τ_{2}}; Γ ⊢ ι_{2}

Δ; C; Γ ⊢ case v (inl ⇒ ι_{1} | inr ⇒ ι_{2})

Δ; Γ ⊢ v : ∀[· | C].(σ_{1}, …, σ_{n}) → 0  Δ; Γ ⊢ v_{1} : σ_{1}  ⋯  Δ; Γ ⊢ v_{n} : σ_{n}

Δ; C; Γ ⊢ v(v_{1}, …, v_{n})

Δ; Γ ⊢ v : int

Δ; C; Γ ⊢ halt v

Δ; C ⊢ γ ⟹ Δ′; C′ Δ′; C′; Γ ⊢ ι

Δ; C; Γ ⊢ coerce(γ); ι

Figure 2: Static Semantics: Instructions

time behaviour will not be affected. The judgement form Δ; C ⊢ γ ⟹ Δ′; C′ indicates that a coercion is well-formed, extends the type context to Δ′, and produces new store constraints C′. These judgements are presented in figure 3.

Each coercion operates on a particular store location η. The union coercion lifts the object at η into a union type and the roll/unroll coercions witness the isomorphism between a recursive type and its unfolding. The coercion pack_{[c_{1},...,c_{n}|C′[c_{1},...,c_{n}/Δ′]]as ∃[Δ′|C′].τ} (η) introduces an existential type by hiding the type constructors c_{1}, …, c_{n} and encapsulating the store described by C′[c_{1}, …, c_{n}/Δ′]. The unpack coercion eliminates an existential type, augments the current constraints with the encapsulated C′, and extends the type context Δ with Δ′, the hidden type constructors.

4 Applications

In this section, we show how our language can be used to encode two common programming patterns, the destinationpassing style pattern, which constructs data structures efficiently and the Deutsch-Schorr-Waite or “link-reversal” patterns, which traverse data structures using minimal additional space.

4.1 Destination-Passing Style

An effective optimization for functional languages is the destination-passing style (DPS) transformation. Wadler [34] first realized that compilers could detect certain “almosttail-recursive” functions and automatically transform such functions into more efficient tail-recursive functions. Since then several other researchers have studied various facets of this problem [16, 5, 18]. Our contribution is to provide a type system that can be used in a type-preserving compiler and is capable of verifying that the code resulting from the transformation is safe.

Append is the canonical example of a function suitable for DPS:

Δ; C ⊢ γ ⟹ Δ′; C′

Δ ⊢ C = C′ ⊗ {η ↦ τ_{i}} : Store  Δ ⊢ τ_{1} : Type  Δ ⊢ τ_{2} : Type

Δ; C ⊢ union_{τ_{1}∪τ_{2}}(η) ⟹ Δ; C′ ⊗ {η ↦ τ_{1} ∪ τ_{2}}

(for i = 1 or 2)

Δ ⊢ τ = (rec α (Δ′).τ′) (c_{1}, …, c_{n}) : Type Δ ⊢ C = C′ ⊗ {η ↦ τ′[rec α (Δ′).τ′/α][c_{1}, …, c_{n}/Δ′]} : Store Δ; C ⊢ roll_{τ} (η) ⟹ Δ; C′ ⊗ {η ↦ τ}

Δ ⊢ C = C′ ⊗ {η ↦ τ} : Store Δ ⊢ τ = (rec α (Δ′).τ′) (c_{1}, …, c_{n}) : Type Δ; C ⊢ unroll(η) ⟹ Δ; C′ ⊗ {η ↦ τ′[rec α (Δ′).τ′/α][c_{1}, …, c_{n}/Δ′]}

Δ′ = β_{1}:κ_{1}, …, β_{n}:κ_{n} · ⊢ c_{i} : κ_{i} (for 1 ≤ i ≤ n) Δ ⊢ C = C′′ ⊗ {η ↦ τ[c_{1}, …, c_{n}/Δ′]} ⊗ C′[c_{1}, …, c_{n}/Δ′] : Store

Δ; C ⊢ pack_{[c_{1},...,c_{n}|C′[c_{1},...,c_{n}/Δ′]]as ∃[Δ′|C′].τ} (η) ⟹ Δ; C′′ ⊗ {η ↦ ∃[Δ′ | C′].τ}

Δ ⊢ C = C′′ ⊗ {η ↦ ∃[Δ′ | C′].τ} : Store Δ; C ⊢ unpack η with Δ′ ⟹ Δ, Δ′; C′′ ⊗ {η ↦ τ} @ C′

Figure 3: Static Semantics: Coercions

fun append (xs,ys) =
case xs of
[] -> []
| hd :: tl -> hd :: append (tl,ys)

Here, the second-last operation in the second arm of the case is a function call and the last operation constructs a cons cell. If the two operations were inverted, we would have an efficient tail-recursive function. In DPS, the function allocates a cons cell before the recursive call and passes the partially uninitialized value to the function, which computes its result and fills in the uninitialized part of the data structure. If the input list xs is linear, it will not be used in the future. In this case, it is possible to further optimize the program by reusing the input list cells for the output list. Our example performs both of these optimizations.

Before presenting the code for the optimized function, we will need to define a number of abbreviations. Such abbreviations not only aid readability, but also help compress typing information in a compiler [10]. First, recall the type of integer lists List and their unrolling List′:

\begin{aligned}List & = & μα.⟨S(1)⟩ ∪ ∃[ρ | \{ρ ↦ α\}].⟨S(2), int, ptr(ρ)⟩ \\ List′ & = & ⟨S(1)⟩ ∪ ∃[ρ | \{ρ ↦ List\}].⟨S(2), int, ptr(ρ)⟩ \end{aligned}

Given these list definitions, it will be useful to define the following composite coercion.

rollList ρ_{1} packing ρ_{2} =

pack_{[ρ_{2}|{ρ_{2}↦List}]as ∃[ρ_{2}|{ρ_{2}↦List}].⟨S(2),int,ptr(ρ_{2})⟩}(ρ_{1}); union_{List′}(ρ_{1}); roll_{List}(ρ_{1})

This coercion operates on a portion of the store with shape {ρ_{1} ↦ ⟨S(2), int, ptr(ρ_{2})⟩} ⊗ {ρ_{2} ↦ List}. It packs up ρ_{2} into an existential around ρ_{1}, lifts the resultant object up to a union type and finally rolls it up, producing a store with the shape {ρ_{1} ↦ List}.

The function append′, presented in figure 4, implements the inner loop of the optimized append function. A wrapper function must check for the case that the input list is empty. If not, it passes two pointers to the beginning of the first list (aliases of one another) to append′ for parameters prev and start. It also passes a pointer to the second element in that list for parameter xs and a pointer to the second list for parameter ys. Notice that the contents of location ρ_{s} are not described by the aliasing constraints. On the first iteration of the loop ρ_{s} is an alias of ρ_{p} and on successive iterations, it abstracted by ϵ. However, these facts are not explicit in the type structure and therefore ρ_{s} cannot be used during any iteration of the loop (cont will be aware that ρ_{s} equals ρ_{p} and may use the resultant list).

The first place to look to understand this code is at the aliasing constraints, which act as a loop invariant. Reading the constraints in the type from left to right reveals that the function expects a store with some unknown part (ϵ) as well as a known part. The known part contains a cons cell at location ρ_{p} that is linked to a List in location ρ_{xs}. Independent of either of these objects is a third location, ρ_{ys}, which also contains a List.

The first instruction in the function unrolls the recursive type of the object at ρ_{xs} to reveal that it is a union and can be eliminated by a case statement. In the first branch of the case, xs must point to null. The code frees the null cell, resulting in a store at program point 1 that can be described by the constraints ϵ ⊗ {ρ_{p} ↦ ⟨S(2), int, ptr(ρ_{xs})⟩} ⊗ {ρ_{ys} ↦ List}. Observe that the cons cell at ρ_{p} contains a dangling pointer to memory location ρ_{xs}, the location that has just been freed and no longer appears in the constraints. Despite the dangling pointer, the code is perfectly safe: The typing rules prevent the pointer from being used.

Next, the second list ys is banged into the cons cell at ρ_{p}. fix append′ [ϵ, ρ_{xs}, ρ_{ys}, ρ_{p}, ρ_{s} |

ϵ ⊗ {ρ_{p} ↦ ⟨S(2), int, ptr(ρ_{xs})⟩, ρ_{xs} ↦ List, ρ_{ys} ↦ List}]. (xs : ρ_{xs}, ys : ρ_{ys}, prev : ptr(ρ_{p}), start : ptr(ρ_{s}),

cont : τ_{c}[ϵ, ρ_{p}, ρ_{s}]).

unroll(ρ_{xs});
case xs
( inl ⟹
free xs;  % 1.

(prev).3 := ys; % 2.

rollList ρ_{p} packing ρ_{ys}; % 3.

cont(start)

| inr ⟹
unpack ρ_{xs} with ρ_{tl};  % 4.

let tl = (xs).3; % 5. append′

[ϵ ⊗ {ρ_{p} ↦ ⟨S(2), int, ptr(ρ_{xs})⟩}, ρ_{tl}, ρ_{ys}, ρ_{xs}, ρ_{s}] (tl, ys, xs, start, cont′))

where τ_{c}[ϵ, ρ_{p}, ρ_{s}] = ∀[· | ϵ ⊗ {ρ_{p} ↦ List}].(ptr(ρ_{s})) → 0

Figure 4: Optimized Append

Hence, at program point 2, the store has a shape described by ϵ⊗{ρ_{p} ↦ ⟨S(2), int, ptr(ρ_{ys})⟩}⊗{ρ_{ys} ↦ List}. The type of the cons cell at ρ_{p} is different here than at 1, reflecting the new link structure of store. The tail of the cell no longer points to location ρ_{xs}, but to ρ_{ys} instead. After packing and rolling using the composite coercion, the store can be described by ϵ ⊗ {ρ_{p} ↦ List}. This shape equals the shape expected by the continuation (see the definition of τ_{c}), so the function call is valid.

In the second branch of the case, xs must point to a cons cell. The existential containing the tail of the list is unpacked and at program point 4, the store has shape ϵ⊗{ρ_{p} ↦ ⟨S(2), int, ptr(ρ_{xs})⟩}⊗{ρ_{xs} ↦ ⟨S(2), int, ptr(ρ_{tl})⟩}⊗{ρ_{tl} ↦ List} ⊗ {ρ_{ys} ↦ List}. It is now possible to project the tail of xs. To complete the loop, the code uses polymorphic recursion. At the end of the second branch, the constraint variable ϵ for the next iteration of the loop is instantiated with the current ϵ and the contents of location ρ_{p}, hiding the previous node in the list. The location variables ρ_{xs} and ρ_{p} are instantiated to reflect the shift to the next node in the list. The locations ρ_{ys} and ρ_{s} are invariant around the loop and therefore are instantiated with themselves.

The last problem is how to define the continuation cont′ for the next iteration. The function should be tailrecursive, so we would like to use the continuation cont. However, close inspection reveals that the next iteration of append requires a continuation with type τ_{c}[ϵ ⊗ {ρ_{p} ↦ ⟨S(2), int, ptr(ρ_{xs})⟩}, ρ_{xs}, ρ_{s}] but that the continuation cont has type τ_{c}[ϵ, ρ_{p}, ρ_{s}]. The problem is that this iteration of the recursion has unrolled and unpacked the recursive data structure pointed to by xs, but before “returning” by calling the continuation, the list must be packed and rolled back up again. Therefore, the appropriate definition of cont′ is cont ∘ (rollList ρ_{p} packing ρ_{xs}). Once the continuation packs ρ_{xs} and rolls the contents of location ρ_{p} into a List, the constraints satisfy the requirements of the continuation cont. Semantically, cont′ is equivalent to the following function. fix [· | ϵ ⊗ {ρ_{p} ↦ ⟨S(2), int, ptr(ρ_{xs})⟩}{ρ_{xs} ↦ List}]

(start:ptr(ρ_{s})).

      rollList ρ_{p} packing ρ_{xs};

cont(start) However, because coercions can be erased before running a program, it is simple to arrange for cont′ to be implemented by cont.

4.2 Deutsch-Schorr-Waite Algorithms

Deutsch-Schorr-Waite or “link reversal” algorithms, are well-known algorithms for traversing data structures while incurring minimal additional space overhead. These algorithms were first developed for executing the mark phase of a garbage collector [28]. During garbage collection, there is little or no extra space available for storing control information, so minimizing the overhead of the traversal is a must. Recent work by Sobel and Friedman [30] has shown how to automatically transform certain continuation-passing style programs, those generated by anamorphisms [17], into linkreversal algorithms. Here we give an example how to encode a link-reversal algorithm in our calculus.

For this application, we will use the definition of trees from section 2.

T ree =

μα.⟨S(1)⟩ ∪ ∃[ρ_{L}, ρ_{R} | {ρ_{L} ↦ α, ρ_{R} ↦ α}].
⟨S(2), ptr(ρ_{L}), ptr(ρ_{R})⟩

T ree′ =

⟨S(1)⟩ ∪ ∃[ρ_{L}, ρ_{R} | {ρ_{L} ↦ T ree, ρ_{R} ↦ T ree}].
⟨S(2), ptr(ρ_{L}), ptr(ρ_{R})⟩

The code for the algorithm appears in figure 5. The trick to the algorithm is that when recursing into the left subtree, it uses space normally reserved for a pointer to that subtree to point back to the parent node. Similarly, when recursing into the right subtree, it uses the space for the right pointer. In both cases, it uses the tag field of the data structure to store a continuation that knows what to do next (recurse into right subtree or follow the parent pointers back up the tree). Before ascending back up out of the tree, the algorithm restores the link structure to a proper tree shape and the type system checks this is done properly. Notice that all of the functions and continuations are closed, so there is no stack hiding in the closures.

5 Operational Semantics and Type Soundness

In this section, we define the syntax and static semantics of the values manipulated at run-time, including pointers, memory blocks and the store and give an operational semantics for the language. The type system is sound with respect to this semantics.

Run-time Values The run-time values consist of all the values defined in previous sections as well as pointers ptr(ℓ), memory blocks ⟨v_{1}, …, v_{n}⟩ and witnessed values ς(v). Witnessed values are introduced by coercions. For example, the union coercion introduces a union witness and similarly for roll and pack coercions. Notice that these values are always type checked in an empty type context and empty value context (evaluation of open terms is nonsensical).

%  Traverse a tree node

letrec walk[ϵ, ρ_{1}, ρ_{2} | ϵ ⊗ {ρ_{1} ↦ T ree}]

(t : ptr(ρ_{1}), up : ptr(ρ_{2}), cont : τ_{c}[ϵ, ρ_{1}, ρ_{2}]).

unroll(ρ_{1});
case t of
   ( inl ⟹

union_{T ree′}(ρ_{1}); roll_{T ree}(ρ_{1}); cont(t, up)

   | inr ⟹
      unpack ρ_{1} with ρ_{L}, ρ_{R};
      % store cont in tag position

(t).1 := cont; let left = (t).2;

      % store parent pointer as left subtree

(t).2 := up; walk[ϵ⊗

{ρ_{1} ↦ ⟨τ_{c}[ϵ, ρ_{1}, ρ_{2}], ptr(ρ_{2}), ptr(ρ_{R})⟩}⊗

{ρ_{R} ↦ T ree}, ρ_{L}, ρ_{1}]
(left, t, rwalk[ϵ, ρ_{1}, ρ_{2}, ρ_{L}, ρ_{R}]))

%  Walk the right-hand subtree

and rwalk[ϵ, ρ_{1}, ρ_{2}, ρ_{L}, ρ_{R} | ϵ⊗ {ρ_{1} ↦ ⟨τ_{c}[ϵ, ρ_{1}, ρ_{2}], ptr(ρ_{2}), ptr(ρ_{R})⟩}⊗ {ρ_{L} ↦ T ree}⊗ {ρ_{R} ↦ T ree}] (left : ptr(ρ_{L}), t : ptr(ρ_{1})).

let up = (t).2;

% restore left subtree

(t).2 := left; let right = (t).3;

% store parent pointer as right subtree

(t).3 := up; walk[ϵ⊗

{ρ_{1} ↦ ⟨τ_{c}[ϵ, ρ_{1}, ρ_{2}], ptr(ρ_{L}), ptr(ρ_{2})⟩}⊗ {ρ_{L} ↦ T ree}, ρ_{R}, ρ_{1}] (right, t, finish[ϵ, ρ_{1}, ρ_{2}, ρ_{L}, ρ_{R}])

%  Reconstruct tree node and return

and finish[ϵ, ρ_{1}, ρ_{2}, ρ_{L}, ρ_{R} | ϵ⊗ {ρ_{1} ↦ ⟨τ_{c}[ϵ, ρ_{1}, ρ_{2}], ptr(ρ_{L}), ptr(ρ_{2})⟩}⊗

{ρ_{L} ↦ T ree}⊗
{ρ_{R} ↦ T ree}]
(right : ptr(ρ_{R}), t : ptr(ρ_{1})).

let up = (t).3;

% restore right subtree

(t).3 := right; let cont = (t).1;

% restore tag

(t).1 := S(2); pack_{ρ_{L},ρ_{R}}(ρ_{1}); union_{T ree′}(ρ_{1}); roll_{T ree}(ρ_{1}); cont(t, up)

where τ_{c}[ϵ, ρ_{1}, ρ_{2}] = ∀[· | ϵ ⊗ {ρ_{1} ↦ T ree}].(ptr(ρ_{1}), ptr(ρ_{2})) → 0

Figure 5: Deutsch-Schorr-Waite tree traversal with constant space overhead

values  v ::= ⋯ | ptr(ℓ) | ⟨v_{1}, …, v_{n}⟩ | ς(v)
witnesses ς ::= union_{τ_{1}∪τ_{2}} |
pack_{[c_{1},...,c_{n}|S]as∃[Δ|C].τ} |
roll_{(rec α (Δ).τ) (c_{1},...,c_{n})}

· ⊢ τ_{1} ∪ τ_{2} : Type ·; · ⊢ v : τ_{1} or ·; · ⊢ v : τ_{2}

·; · ⊢ union_{τ_{1}∪τ_{2}}(v) : τ_{1} ∪ τ_{2}
· ⊢ τ = (rec α (Δ).τ′) (c_{1}, …, c_{n}) : Type
·; · ⊢ v : τ′[rec α (Δ).τ′/α][c_{1}, …, c_{n}/Δ]
·; · ⊢ roll_{τ} (v) : τ

\begin{matrix}Δ = β_{1}:κ_{1}, …, β_{n}:κ_{n}  · ⊢ c_{i} : κ_{i} (for 1 ≤ i ≤ n) \\ ⊢ S : C[c_{1}, …, c_{n}/Δ]  ·; · ⊢ v : τ[c_{1}, …, c_{n}/Δ] \end{matrix}
·; · ⊢ pack_{[c_{1},...,c_{n}|S]as∃[Δ|C].τ} (v) : ∃[Δ | C].τ

The pack coercion encapsulates a portion of the store, S, which is a finite partial mapping from concrete locations to values. We treat stores equivalent up to reordering of their elements and use the notation S{ℓ ↦ v} to denote the extension of S to include the mapping {ℓ ↦ v}. The notation is undefined if ℓ ∈ Dom(S). The store well-formedness judgement is written ⊢ S : C and is given below.

S = {ℓ_{1} ↦ v_{1}, …, ℓ_{n} ↦ v_{n}}
· ⊢ C = {ℓ_{1} ↦ τ_{1}, …, ℓ_{n} ↦ τ_{n}} : Store
·; · ⊢ v_{i} : τ_{i} (for 1 ≤ i ≤ n)
⊢ S : C

There are no duplicate locations in the domain of a store (otherwise, it would not be a finite partial map). However, we will require a stronger property of stores to prove that program evaluation cannot get stuck. Informally, there can be no duplication of locations in the domain of the store or in any encapsulated store. We call this property Global Uniqueness.

Definition 1 (Global Uniqueness) GU(S) if and only if there are no duplicate locations in L(S).

Definition 2 (Global Store Locations) L(S) is the multi-set given by the following definition.

L({ℓ_{1} ↦ v_{1}, …, ℓ_{n} ↦ v_{n}})

= {ℓ_{1}, …, ℓ_{n}} ⊎ L(v_{1}) ⊎ ⋯ ⊎ L(v_{n})

L(pack_{[c_{1},...,c_{n}|S]asτ} (v))

= L(S) ⊎ L(v)

L(x) = L(x_{1}) ⊎ ⋯ ⊎ L(x_{n})

for any other term construct x

where x_{1}, …, x_{n} are the subcomponents of x.

A program is a store paired with an instruction stream. A program is well-formed, written ⊢ (S, ι), under the following circumstances.

Definition 3 (Well-formed Program) ⊢ (S, ι) iff

1. The store adheres to global uniqueness GU(S).

2. There exists constraints C such that ⊢ S : C.

3. The instructions are well-formed with the given constraints: ·; C; · ⊢ ι.

(S, ι) ⟼_{P} (S, ι)

(S, new ρ, x, i; ι)  ⟼_{P} (S{ℓ ↦ v}, ι[ℓ/ρ][ptr(ℓ)/x])

where ℓ ∉ S, ι and v = \overbrace{⟨S(0), …, S(0)⟩}^{i}

(S{ℓ ↦ ⟨v_{1}, …, v_{n}⟩}, freeptr(ℓ); ι)  ⟼_{P} (S, ι)
(S{ℓ ↦ ⟨v_{1}, …, v_{n}⟩}, let x = (ptr(ℓ)).i; ι)  ⟼_{P} (S{ℓ ↦ ⟨v_{1}, …, v_{n}⟩}, ι[v_{i}/x])

where 1 ≤ i ≤ n

(S{ℓ ↦ ⟨v_{1}, …, v_{i}, …, v_{n}⟩}, (ptr(ℓ)).i := v′; ι) ⟼_{P} (S{ℓ ↦ ⟨v_{1}, …, v′, …, v_{n}⟩}, ι)

where 1 ≤ i ≤ n

(S{ℓ ↦ v}, caseptr(ℓ) (inl ⇒ ι_{1} | inr ⇒ ι_{2})) ⟼_{P} (S{ℓ ↦ v′}, ι_{i})
where \begin{aligned}i & = & 1 or 2 \\ v & = & union_{τ_{1}∪τ_{2}}(ς_{1}(⋯ ς_{m}(⟨S(i), v_{1}, …, v_{n}⟩) ⋯)) \\ v′ & = & ς_{1}(⋯ ς_{m}(⟨S(i), v_{1}, …, v_{n}⟩) ⋯) \end{aligned}

(S, v(v_{1}, …, v_{n}))  ⟼_{P} (S, θ(ι))
where \begin{aligned}v & = & v′[c_{1}, …, c_{m}] \\ v′ & = & fixf[Δ | C](x_{1}:σ_{1}, …, x_{n}:σ_{n}).ι \\ θ & = & [c_{1}, …, c_{m}/Δ][v′/f][v_{1}, …, v_{n}/x_{1}, …, x_{n}] \end{aligned}

(S, coerce(γ); ι)  ⟼_{P} (S′, θ(ι))

where γ(S) ⟼_{γ} S′, θ

Figure 6: Operational Semantics: Programs

Operational Semantics The small-step operational semantics for the language is given by a function P ⟼_{P} P′. The majority of the operational rules are entirely standard and formalize the intuitive rules described earlier in the paper. The operational rule for the coerce instruction depends upon a separate semantics for coercions that has the form S ⟼_{γ} S′, θ where θ is a substitution of type constructors for type constructors variables. Inspection of these rules reveals that coercions do not alter the association between locations and memory blocks; they simply insert witnesses that alter the typing derivation so that it is possible to prove a type soundness result. The rules for program and coercion operational semantics may be found in figures 6 and 7.

Type Soundness We now have all the pieces necessary to state and prove that execution of a program in our language “can’t get stuck.” A stuck program is a program that is not in the terminal configuration halt i and for which no operational rule applies.

Theorem 4 (Type Soundness) If ⊢ (S, ι) and (S, ι) ⟼_{P}^{∗} (S′, ι′) then (S′, ι′) is not stuck.

The proof itself uses standard Subject Reduction and Progress lemmas in the style popularized by Wright and Felleisen [36] and is mostly mechanical. The proof can be found in Appendix B.

6 Related Work

Our type system builds upon the foundational work by other groups on syntactic control of interference [25] and linear type systems in functional programming languages [35, 33, 2]. We also owe much to researchers in alias analysis for imperative languages [12, 15, 7, 9, 26].

Our type system appears most closely related to the shape analysis developed by Sagiv, Reps, and Wilhelm (SRW) [26]. Although the precise relationship is currently unknown to us, it is clear that several of the key features that make SRW shape analysis more effective than similar alias analyses can be expressed in our type system. More specifically:

1. Unlike some other analyses, SRW shape nodes do not contain information about concrete locations or the site where the node was allocated. Our type system drops information about concrete locations using location polymorphism.

2. SRW shape nodes are named with the set of program variables that point to that node. Our type system can only label a node with a single name, but we are able to express the fact that a set of program variables point to that node using the same singleton type for each program variable in the set.

3. SRW shape nodes may be flagged as unshared. Linear types account for unshared shape nodes.

4. A single SRW summary node describes many memory blocks, but through the process of materialization a summary node may split off a new, separate shape node. Summary nodes may be represented as recursive types in our framework and materialization can be explained by the process of unrolling and unpacking a recursive and existential type.

γ(S) ⟼_{γ} S′, θ

union_{τ_{1}∪τ_{2}}(ℓ)(S{ℓ ↦ v})  ⟼_{γ} S{ℓ ↦ union_{τ_{1}∪τ_{2}}(v)}, [ ]
roll_{τ} (ℓ)(S{ℓ ↦ v})  ⟼_{γ} S{ℓ ↦ roll_{τ} (v)}, [ ]
unroll(ℓ)(S{ℓ ↦ roll_{τ} (v)})  ⟼_{γ} S{ℓ ↦ v}, [ ]
pack_{[c_{1},...,c_{n}|C]as τ} (ℓ)(S{ℓ ↦ v}S′)  ⟼_{γ} S{ℓ ↦ pack_{[c_{1},...,c_{n}|S′]asτ} (v)}, [ ]
where C = {ℓ_{1} ↦ τ_{1}, …, ℓ_{m} ↦ τ_{m}} and S′ = {ℓ_{1} ↦ v_{1}, …, ℓ_{m} ↦ v_{m}}
unpack ℓ with Δ (S{ℓ ↦ pack_{[c_{1},...,c_{n}|S′]as∃[Δ|C].τ} (v)}) ⟼_{γ} SS′{ℓ ↦ v}, [c_{1}, …, c_{n}/Δ]

Figure 7: Operational Semantics: Coercions

One of the advantages to our approach is that our language makes it straightforward to create dependencies between functions and data using store or location polymorphism. For example, in our implementation of the Deutsch-Schorr-Waite algorithm, we manipulate continuations that know how to reconstruct a well-formed tree from the current heap structure and we are able to express this dependence in the type system. Explicit manipulation of continuations is necessary in sufficiently low-level typed languages such as Typed Assembly Language when return addresses are interpreted as continuations [21].

Other work has focused on developing expressive pointer logics for describing the shape of the store [20, 13, 27, 3]. Some of these logics can express more sophisticated pointer relationships than the type structure described in this paper. For example, Benedikt et al. [3] provide a complex logic that includes path equality and inequality relations, allocation constraints, reachability constraints and other connectives. Our type system is built by starting with the concept of a finite partial map to describe the store and then using a combination of standard type constructors such as singleton, union, polymorphic, existential and recursive types. These type constructors can be reused for a variety of different purposes within a type-preserving compiler from representing closures [19] to data-flow analysis [8] to object encodings [24] to source-level polymorphism and existential types. From an engineering perspective, there are definite advantages to reusing as much type structure as possible.

Several other authors have considered alternatives to pure linear type systems that increase their flexibility. For example, Kobayashi [14] extends standard linear types with data-flow information and Minamide [18] uses a linear type discipline to allow programmers to manipulate “data structures with a hole.” Minamide’s language allows users to write programs that are compiled into destination-passing style. However, Minamide’s language is still quite high-level; he does not show how to verify explicit pointer manipulation. Moreover, neither of these type systems provide the ability to represent cyclic data structures.

Tofte, Talpin, and others [32, 4, 1, 6] have explored the use of region-based memory management. In their work, objects are allocated into one of several regions of memory. When a region is deallocated, all the objects in that region are deallocated too. Region-based memory management performs extremely well in many circumstances, but unlike systems based on linear types, space is not, in general, reused on a per-object basis. Moreover, regions cannot be encapsulated inside recursive data structures. However, we believe that some of the techniques we have developed here may be adapted to the region setting and we are eager to investigate a combined framework that can take advantage of both forms of typed memory management.

Acknowledgements

Fred Smith worked with us on the predecessor to this research and the many stimulating discussions we had together contributed to the current paper. Neal Glew made helpful comments on an earlier draft of this paper.

References

[1] Alexander Aiken, Manuel Fähndrich, and Raph Levien. Better static memory management: Improving region-based analysis of higher-order languages. In ACM Conference on Programming Language Design and Implementation, pages 174–185, La Jolla, California, 1995.

[2] Erik Barendsen and Sjaak Smetsers. Conventional and uniqueness typing in graph rewrite systems (extended abstract). In Thirteenth Conference on the Foundations of Software Technology and Theoretical Computer Science, pages 41–51, Bombay, 1993. In Shyamasundar, ed., Springer-Verlag, LNCS 761.

[3] Michael Benedikt, Thomas Reps, and Mooly Sagiv. A decidable logic for describing linked data structures. In European Symposium on Programming, pages 2–19, Amsterdam, March 1999.

[4] Lars Birkedal, Mads Tofte, and Magnus Vejlstrup. From region inference to von Neumann machines via region representation inference. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 171–183, St. Petersburg, January 1996.

[5] Perry Cheng and Chris Okasaki. Destination-passing style and generational garbage collection. Unpublished., November 1996.

[6] Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 262–275, San Antonio, January 1999.

[7] Alain Deutsch. Interprocedural may-alias analysis for pointers: Beyond k-limiting. In ACM Conference on Programming Language Design and Implementation, pages 230–241, Orlando, June 1994.

[8] Allyn Dimock, Robert Muller, Franklyn Turbak, and J. B. Wells. Strongly typed flow-directed representation transformations. In ACM International Conference on Functional Programming, pages 85–98, Amsterdam, June 1997.

[9] Rakesh Ghiya and Laurie J. Hendren. Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 1–15, St. Petersburg Beach, Florida, January 1996.

[10] Dan Grossman and Greg Morrisett. Scalable certification of native code: Experience from compiling to TALx86. Technical Report TR2000-1783, Cornell University, February 2000.

[11] Robert Harper. A simplified account of polymorphic references. Information Processing Letters, 51(4):201–206, August 1994.

[12] Neil D. Jones and Steven Muchnick, editors. Flow analysis and optimization of Lisp-like structures. Prentice-Hall, 1981.

[13] Nils Klarlund and Michael Schwartzbach. Graph types. In Twentieth ACM Symposium on Principles of Programming Languages, pages 196–205, Charleston, January 1993.

[14] Naoki Kobayashi. Quasi-linear types. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 29–42, San Antonio, January 1999.

[15] James R. Larus and Paul N. Hilfinger. Detecting conflicts between structure accesses. In ACM Conference on Programming Language Design and Implementation, pages 24– 31, June 1988.

[16] James Richard Larus. Restructuring Symbolic Programs for Concurrent Execution on Multiprocessors. PhD thesis, University of California at Berkeley, May 1989. Available as Berkeley technical report UCB/CSD 89/502.

[17] Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes, and barbed wire. In ACM Conference on Functional Programming and Computer Architecture, 1991. Also published in Lecture Notes in Computer Science, 523, Springer-Verlag.

[18] Y. Minamide. A functional representation of data structures with a hole. In Twenty-Fifth ACM Symposium on Principles of Programming Languages, pages 75–84, San Diego, January 1998.

[19] Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 271–283, St. Petersburg, January 1996.

[20] Bernhard Möller. Towards pointer algebra. Science of Computer Programming, 21:57–90, 1993.

[21] Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based Typed Assembly Language. In Second International Workshop on Types in Compilation, pages 95–117, Kyoto, March 1998. Published in Xavier Leroy and Atsushi Ohori, editors, Lecture Notes in Computer Science, volume 1473, pages 28-52. Springer-Verlag, 1998.

[22] Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. In Twenty-Fifth ACM Symposium on Principles of Programming Languages, pages 85–97, San Diego, January 1998.

[23] George Necula and Peter Lee. The design and implementation of a certifying compiler. In ACM Conference on Programming Language Design and Implementation, pages 333 – 344, Montreal, June 1998.

[24] Benjamin Pierce and David Turner. Simple type-theoretic foundations for object-oriented programming. Journal of functional programming, 4:207–247, 1994.

[25] John C. Reynolds. Syntactic control of interference. In Fifth ACM Symposium on Principles of Programming Languages, pages 39–46, Tucson, 1978.

[26] Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems, 20(1):1–50, January 1998.

[27] Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 105–118, San Antonio, January 1999.

[28] H. Schorr and W. M. Waite. An efficient machineindependent procedure for garbage collection in various list structures. Communications of the ACM, 10(8):501–506, August 1967.

[29] Frederick Smith, David Walker, and Greg Morrisett. Alias types. In European Symposium on Programming, March 2000. To appear. Available at http://www.cs.cornell.edu/talc/papers.html.

[30] Johnathan Sobel and Daniel Friedman. Recycling continuations. In ACM International Conference on Functional Programming, pages 251–260, Baltimore, September 1998.

[31] TALx86. See http://www.cs.cornell.edu/talc for an implementation of Typed Assembly Language based on Intel’s IA32 architecture.

[32] Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Twenty-First ACM Symposium on Principles of Programming Languages, pages 188–201, Portland, Oregon, January 1994.

[33] David N. Turner, Philip Wadler, and Christian Mossin. Once upon a type. In ACM International Conference on Functional Programming and Computer Architecture, San Diego, CA, June 1995.

[34] Philip Wadler. Listlessness is Better than Laziness. PhD thesis, Carnegie Mellon University, August 1985. Available as Carnegie Mellon University technical report CMU-CS-85-171.

[35] Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Progarmming Concepts and Methods, Sea of Galilee, Israel, April 1990. North Holland. IFIP TC 2 Working Conference.

[36] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994.

A Type Well-formedness

Δ ⊢ c : κ

Δ ⊢ ℓ : Loc  Δ ⊢ ρ : Δ(ρ)

                                                             Δ ⊢ ∅ : Store

                                                                            Δ ⊢ C : Store Δ ⊢ η : Loc Δ ⊢ τ : Type

Δ ⊢ C ⊗ {η ↦ τ} : Store

Δ ⊢ ϵ : Δ(ϵ)

                                                                                 Δ ⊢ C : Store Δ ⊢ ϵ : Store

Δ ⊢ C ⊗ ϵ : Store

Δ ⊢ α : Δ(α)

                                                                                         Δ ⊢ σ : Small
                                                                                         Δ ⊢ σ : Type

Δ ⊢ σ_{1} : Small ⋯ Δ ⊢ σ_{n} : Small
Δ ⊢ ⟨σ_{1}, …, σ_{n}⟩ : Type

Δ ⊢ τ_{1} : Type Δ ⊢ τ_{2} : Type
Δ ⊢ τ_{1} ∪ τ_{2} : Type

Δ, Δ′ ⊢ C : Store Δ, Δ′ ⊢ τ : Type

(Dom(Δ) ∩ Dom(Δ′) = ∅) Δ ⊢ ∃[Δ′ | C].τ : Type

Δ, α:(κ_{1}, …, κ_{n}) → Type, β_{1}:κ_{1}, …, β_{n}:κ_{n} ⊢ τ : Type

(for 1 ≤ i ≤ n.β_{i} ∉ Dom(Δ))

Δ ⊢ rec α (β_{1}:κ_{1}, …, β_{n}:κ_{n}).τ : (κ_{1}, …, κ_{n}) → Type

Δ ⊢ c : (κ_{1}, …, κ_{n}) → Type Δ ⊢ c_{1} : κ_{1} ⋯ Δ ⊢ c_{n} : κ_{n}

Δ ⊢ c (c_{1}, …, c_{n}) : Type

Δ ⊢ int : Small Δ ⊢ S(i) : Small

Δ ⊢ η : Loc Δ ⊢ ptr(η) : Small

Δ, Δ′ ⊢ C : Store

Δ, Δ′ ⊢ σ_{1} : Small ⋯ Δ, Δ′ ⊢ σ_{n} : Small

(Dom(Δ) ∩ Dom(Δ′) = ∅) Δ ⊢ ∀[Δ′ | C].(σ_{1}, …, σ_{n}) → 0 : Small

Δ ⊢ a_{1} = a_{2} : Atom

Δ ⊢ η : Loc Δ ⊢ τ = τ′ : Type

Δ ⊢ {η ↦ τ} = {η ↦ τ′} : Atom

Δ ⊢ ϵ : Store

Δ ⊢ ϵ = ϵ : Atom

Δ ⊢ c_{1} = c_{2} : κ

Δ ⊢ a_{1} = a′′_{1} : Atom  ⋯  Δ ⊢ a_{n} = a′′_{n} : Atom

a′_{1}, …, a′_{n} is a permutation of a′′_{1}, …, a′′_{n} Δ ⊢ ∅ ⊗ a_{1} ⊗ ⋯ ⊗ a_{n} = ∅ ⊗ a′_{1} ⊗ ⋯ ⊗ a′_{n} : Store

Add all congruence rules.

B Type Soundness

Lemma 5 If Δ ⊢ c : κ then FV(c) ⊆ Dom(Δ).

Proof: By induction on the kinding and equality derivations.

Lemma 6 (Properties of Type Equality)

1. (Well-formedness) If Δ ⊢ c_{1} = c_{2} : κ then Δ ⊢ c_{1} : κ and Δ ⊢ c_{2} : κ.

2. (Symmetry) If Δ ⊢ c_{1} = c_{2} : κ then Δ ⊢ c_{2} = c_{1} : κ

3. (Transitivity) If Δ ⊢ c_{1} = c_{2} : κ and Δ ⊢ c_{2} = c_{3} : κ then Δ ⊢ c_{1} = c_{3} : κ

Proof: By induction on the equality derivation.

Lemma 7 If Δ ⊢ c : κ and α ∉ Dom(Δ) then Δ, α:κ′ ⊢ c : κ

Proof: By induction on the kinding derivation.

Lemma 8 (Type Substitution) If · ⊢ c : κ and θ = [c/α] then 1. if Δ, α:κ, Δ′; Γ ⊢ v : τ then Δ, Δ′; θ(Γ) ⊢ θ(v) : θ(τ).

2. if Δ, α:κ, Δ′; C; Γ ⊢ ι then Δ, Δ′; θ(C); θ(Γ) ⊢ θ(ι)

Proof: By induction on the typing derivation.

Lemma 9 (Value Substitution) If ·; · ⊢ v : τ and θ = [v/x] then 1. if Δ; Γ, x:τ, Γ′ ⊢ v′ : τ′ then Δ; Γ, Γ′ ⊢ θ(v′) : τ′

2. if Δ; C; Γ, x:τ, Γ′ ⊢ ι then Δ; C; Γ, Γ′ ⊢ θ(ι)

Proof: By induction on the typing derivation.

Lemma 10 If for all x ∈ Dom(Γ), Δ ⊢ Γ(x) : Small and Δ; Γ ⊢ v : τ and Δ; Γ ⊢ v : τ′ then Δ ⊢ τ = τ′ : Type

Proof: By induction on the typing derivation.

Lemma 11 If for all x ∈ Dom(Γ), Δ ⊢ Γ(x) = Γ′(x) : Small and Δ ⊢ C = C′ : Store then

1. if Δ; Γ ⊢ v : τ then Δ; Γ′ ⊢ v : τ

2. if Δ; C; Γ ⊢ ι then Δ; C′; Γ′ ⊢ ι

Proof: By induction on the typing derivation.

Lemma 12 (Canonical Value Forms) If ·; · ⊢ v : τ then 1. if τ = int then v = i.

2. if τ = S(i) then v = S(i)

3. if τ = ptr(ℓ) then v = ptr(ℓ)

4. if τ = ⟨σ_{1}, …, σ_{n}⟩ then (a) v = ⟨v_{1}, …, v_{n}⟩

(b) ·; · ⊢ v_{i} : σ_{i}

5. if τ = τ_{1} ∪ τ_{2} then (a) v = union_{τ′_{1}∪τ′_{2}}(v′)

(b) ·; · ⊢ v′ : τ_{i} where i = 1 or 2

(c) · ⊢ τ_{1} = τ′_{1} : Type

(d) · ⊢ τ_{2} = τ′_{2} : Type

6. if τ = rec α (Δ).τ′ (c_{1}, …, c_{n}) then (a) v = roll_{τ′′}(v′)

(b) ·; · ⊢ v′ : τ′[rec α (Δ).τ′/α][c_{1}, …, c_{n}/Δ]

(c) · ⊢ τ = τ′′ : Type

7. if τ = ∃[Δ | C].τ′ then (a) v = pack_{[c_{1},...,c_{n}|S]asτ′′}(v′)

(b) · ⊢ τ = τ′′ : Type

(c) Δ = α_{1}:κ_{1}, …, α_{n}:κ_{n}

(d) for 1 ≤ i ≤ n, · ⊢ c_{i} : κ_{i}

(e) ·; · ⊢ v′ : τ′[c_{1}, …, c_{n}/Δ]

(f) ⊢ S : C[c_{1}, …, c_{n}/Δ]

8. if τ = ∀[Δ | C].(σ_{1}, …, σ_{n}) → 0 then

(a) v = v′[c′_{1}, …, c′_{n}] and

v′ = fixf[Δ′, Δ | C′](x_{1}:σ′_{1}, …, x_{n}:σ′_{n}).ι

(b) Δ′ = α_{1}:κ_{1}, …, α_{n}:κ_{n}

(c) for 1 ≤ i ≤ n, · ⊢ c′_{i} : κ_{i}

(d) · ⊢ fixf[Δ′, Δ | C](x_{1}:σ_{1}, …, x_{n}:σ_{n}).ι : τ

(e) · ⊢ (∀[Δ | C′].(σ′_{1}, …, σ′_{n}) → 0)[c_{1}, …, c_{n}/Δ′] =

(∀[Δ | C].(σ_{1}, …, σ_{n}) → 0) :

Proof: By induction on the typing derivation.

Lemma 13 (Canonical Store Forms) If ⊢ S : C and · ⊢ C = C′ ⊗ {ℓ ↦ τ} : Store then

1. S = S′{ℓ ↦ v}

2. ⊢ S′ : C′

3. ·; · ⊢ v : τ Proof:

The typing derivation ⊢ S : C has the form

S = {ℓ_{1} ↦ v_{1}, …, ℓ_{n} ↦ v_{n}}
· ⊢ C = {ℓ_{1} ↦ τ_{1}, …, ℓ_{n} ↦ τ_{n}} : Store
·; · ⊢ v_{i} : τ_{i} (for 1 ≤ i ≤ n)
⊢ S : C

By Lemma 6 and Lemma 5, C′ can contain no free variables and therefore may be written {ℓ′_{1} ↦ v′_{1}, …, ℓ′_{k} ↦ v′_{k}}. By transitivity of equality,

\begin{matrix}· ⊢ \{ℓ′_{1} ↦ τ′_{1}, …, ℓ′_{k} ↦ τ′_{k}, ℓ ↦ τ\} = \\ \{ℓ_{1} ↦ τ_{1}, …, ℓ_{n} ↦ τ_{n}\} : Store \end{matrix}

By inspection of the definition of constructor equality, we know that

1. for 1 ≤ i ≤ k, · ⊢ τ′_{i} = τ′′_{i} : Type and

2. · ⊢ τ = τ′′ : Type and

3. ℓ′_{1} ↦ τ′′_{1}, …, ℓ′_{k} ↦ τ′′_{k}, ℓ ↦ τ′′ is a permutation of ℓ_{1} ↦ τ_{1}, …, ℓ_{n} ↦ τ_{n}

In order for the two sequences to be permutations of one another k must be n − 1. Moreover, for some i, ℓ_{i} ↦ τ_{i} must be ℓ ↦ τ′′ and without loss of generality, we will assume that i is n. Therefore, ℓ′_{1} ↦ τ′′_{1}, …, ℓ′_{k} ↦ τ′′_{k} is a permutation of ℓ_{1} ↦ τ_{1}, …, ℓ_{n−1} ↦ τ_{n−1}. Consequently,

· ⊢ C′ = {ℓ_{1} ↦ τ_{1}, …, ℓ_{n−1} ↦ τ_{n−1}} : Store

Let S′ be {ℓ_{1} ↦ v_{1}, …, ℓ_{n−1} ↦ v_{n−1}} and let v be v_{n}. We have S = S′{ℓ ↦ v}. We can also conclude from the judgement ⊢ C : S that for 1 ≤ i ≤ n − 1, ·; · ⊢ v_{i} : τ_{i}. Therefore, we have

S′ = {ℓ_{1} ↦ v_{1}, …, ℓ_{n−1} ↦ v_{n−1}}
· ⊢ C′ = {ℓ_{1} ↦ τ_{1}, …, ℓ_{n−1} ↦ τ_{n−1}} : Store
·; · ⊢ v_{i} : τ_{i} (for 1 ≤ i ≤ n − 1)
⊢ S′ : C′

From the judgement ⊢ S : C, we also know that ·; · ⊢ v_{n} : τ_{n} and since v is v_{n} and τ is τ_{n}, we have ·; · ⊢ v : τ.

Lemma 14 If ⊢ S′{ℓ ↦ v} : C and · ⊢ C = C′⊗{ℓ ↦ τ} : Store then

1. ⊢ S′ : C′

2. ·; · ⊢ v : τ

Proof: Corollary of Canonical Store Forms.

Lemma 15 If

1. ⊢ S′{ℓ ↦ v} : C

2. · ⊢ C = C′ ⊗ {ℓ ↦ τ} : Store

3. ·; · ⊢ v′ : τ′

then ⊢ S′{ℓ ↦ v′} : C′ ⊗ {ℓ ↦ τ′}

Proof:

By (1), (2), and Lemma 14, ⊢ S′ : C′. Hence, by (3) and inspection of the store typing judgement, ⊢ S′{ℓ ↦ v′} : C′ ⊗ {ℓ ↦ τ′}

Lemma 16 If Dom(S)∩Dom(S′) = ∅ and ⊢ S : C and ⊢ S′ : C′ then ⊢ SS′ : C@C′

Proof:

Since Dom(S) ∩ Dom(S′) = ∅, we know that SS′ is a store. Inspection of the store typing judgement and examination of the definition of equality provides the result.

Lemma 17

1. If Δ; Γ ⊢ v : σ then L(v) = 0.

2. If Δ; C; Γ ⊢ ι then L(ι) = 0.

Proof: By induction on the typing derivations.

Lemma 18 (Preservation) If ⊢ (S, ι) and (S, ι) ⟼_{P} (S′, ι′) then ⊢ (S′, ι′)

Proof:

By cases on the operational rule that applied.

• Operational Rule:

(S, new ρ, x, i; ι) ⟼_{P} (S{ℓ ↦ v}, ι[ℓ/ρ][ptr(ℓ)/x])

where ℓ ∉ S, ι and v = _{⟨S(0), …, S(0)⟩}^{i}

Typing Assumption:

1. GU(S)

2. ⊢ S : C.

3. ·; C; · ⊢ new ρ, x, i; ι. First, we know GU(S{ℓ ↦ v}) since GU(S) and ℓ ∉ S. Second, we can conclude:

·; · ⊢ v : _{⟨S(0), …, S(0)⟩}^{i}

Consequently, by inspection of the store typing judgement,

⊢ S{ℓ ↦ v} : C ⊗ {ℓ ↦ _{⟨S(0), …, S(0)⟩}^{i}}

Third, the premise of the instruction typing judgement is

ρ:Loc; C ⊗ {ρ ↦ _{⟨S(0), …, S(0)⟩}^{i}}; x:ptr(ρ) ⊢ ι

By Type and Value Substitution Lemmas,

·; C ⊗ {ℓ ↦ _{⟨S(0), …, S(0)⟩}^{i}}; · ⊢ ι[ℓ/ρ][ptr(ℓ)/x]

Consequently, ⊢ (S{ℓ ↦ v}, ι[ℓ/ρ][ptr(ℓ)/x])

• Operational Rule:

(S{ℓ ↦ ⟨v_{1}, …, v_{n}⟩}, freeptr(ℓ); ι) ⟼_{P} (S, ι)

Typing Assumption:

1. GU(S{ℓ ↦ ⟨v_{1}, …, v_{n}⟩})

2. ⊢ S{ℓ ↦ ⟨v_{1}, …, v_{n}⟩} : C.

3. ·; C; · ⊢ freeptr(ℓ); ι. From 1, we have GU(S). The instruction judgement 3 must have the form:

·; · ⊢ v : ptr(ℓ)
· ⊢ C = C′ ⊗ {ℓ ↦ ⟨σ_{1}, …, σ_{n}⟩} : Store
·; C′; · ⊢ ι
·; C; · ⊢ free v; ι

Hence, by Lemma 14, we can deduce that ⊢ S : C′.

Moreover, we have ·; C′; · ⊢ ι directly.

Therefore, ⊢ (S, ι).

• Operational Rule:

\begin{matrix}(S\{ℓ ↦ ⟨v_{1}, …, v_{n}⟩\}, let x = (ptr(ℓ)).i; ι) ⟼_{P} \\ (S\{ℓ ↦ ⟨v_{1}, …, v_{n}⟩\}, ι[v_{i}/x]) \end{matrix}

where 1 ≤ i ≤ n Typing Assumption:

1. GU(S{ℓ ↦ ⟨v_{1}, …, v_{n}⟩})

2. ⊢ S{ℓ ↦ ⟨v_{1}, …, v_{n}⟩} : C.

3. ·; C; · ⊢ let x = (ptr(ℓ)).i; ι. Where the instruction derivation has the following form:

·; · ⊢ ptr(ℓ) : ptr(ℓ)
· ⊢ C = C′ ⊗ {ℓ ↦ ⟨σ_{1}, …, σ_{n}⟩} : Store
·; C; x:σ_{i} ⊢ ι
·; C; · ⊢ let x = (ptr(ℓ)).i; ι

The instruction derivation contains the fact ·; C; x:σ_{i} ⊢ ι and by Lemma 14, we can conclude that ·; · ⊢ ⟨v_{1}, …, v_{n}⟩ : ⟨σ_{1}, …, σ_{n}⟩. By Canonical Forms, we can conclude that ·; · ⊢ v_{i} : σ_{i}. Hence, from the Value Substitution Lemma, we know that ·; C; · ⊢ ι[v_{i}/x]. From this judgement and (1) and (2), we can conclude ⊢ (S{ℓ ↦ ⟨v_{1}, …, v_{n}⟩}, ι[v_{i}/x])

• Operational Rule:

\begin{matrix}(S\{ℓ ↦ ⟨v_{1}, …, v_{i}, …, v_{n}⟩\}, (ptr(ℓ)).i := v′; ι) ⟼_{P} \\ (S\{ℓ ↦ ⟨v_{1}, …, v′, …, v_{n}⟩\}, ι) \end{matrix}

Typing Assumption:

1. GU(S{ℓ ↦ ⟨v_{1}, …, v_{i}, …, v_{n}⟩})

2. ⊢ S{ℓ ↦ ⟨v_{1}, …, v_{i}, …, v_{n}⟩} : C.

3. ·; C; · ⊢ (ptr(ℓ)).i := v′; ι. The instruction typing judgement has the form:

·; · ⊢ ptr(ℓ) : ptr(ℓ)
·; · ⊢ v′ : σ
· ⊢ C = C′ ⊗ {ℓ ↦ ⟨σ_{1}, …, σ_{i}, …, σ_{n}⟩} : Store
·; C′ ⊗ {ℓ ↦ ⟨σ_{1}, …, σ, …, σ_{n}⟩}; · ⊢ ι
· ⊢ (ptr(ℓ)).i := v′; ι

By Lemma 14 we can conclude that

·; · ⊢ ⟨v_{1}, …, v_{n}⟩ : ⟨σ_{1}, …, σ_{n}⟩

By Canonical Value Forms, we can deduce that (4) for all 1 ≤ i ≤ n

·; · ⊢ v_{j} : σ_{j}

From the instruction typing judgement, we also have the fact that (5)

·; · ⊢ v′ : σ

By Lemma 17, L(v_{i}) = L(v′) = 0. Consequently, since GU(S{ℓ ↦ ⟨v_{1}, …, v_{i}, …, v_{n}⟩}), we know (6)

GU(S{ℓ ↦ ⟨v_{1}, …, v′, …, v_{n}⟩})

By Lemma 14 we can also conclude that ⊢ S : C′. From (4), (5), and the typing rule for tuples, we can conclude that (7)

·; · ⊢ ⟨v_{1}, …, v′, …, v_{n}⟩ : ⟨σ_{1}, …, σ, …, σ_{n}⟩

Therefore, from (2), (7), and the constraint equality judgement from the instruction typing judgement, we can conclude by Lemma 15 that

\begin{matrix}⊢ S\{ℓ ↦ ⟨v_{1}, …, v′, …, v_{n}⟩\} : \\ C′ ⊗ \{ℓ ↦ ⟨σ_{1}, …, σ, …, σ_{n}⟩\} \end{matrix}

These facts and the instruction typing judgement imply that ⊢ (S{ℓ ↦ ⟨v_{1}, …, v′, …, v_{n}⟩}, ι)

• Operational Rule

(S{ℓ ↦ v}, caseptr(ℓ) (inl ⇒ ι_{1} | inr ⇒ ι_{2})) ⟼_{P}

(S{ℓ ↦ v′}, ι_{i})

where

\begin{aligned}i & = & 1 or 2 \\ v & = & union_{τ_{1}∪τ_{2}}(v′) \\ v′ & = & ς_{1}(⋯ ς_{m}(⟨S(i), v_{1}, …, v_{n}⟩) ⋯) \end{aligned}

Typing Assumption:

1. GU(S{ℓ ↦ v})

2. ⊢ S{ℓ ↦ v} : C.

3. ·; C; · ⊢ caseptr(ℓ) (inl ⇒ ι_{1} | inr ⇒ ι_{2}).

Where the instruction typing judgement has the form:

· ⊢ ptr(ℓ) : ptr(ℓ)
· ⊢ C = C′ ⊗ {ℓ ↦ τ_{1} ∪ τ_{2}} : Store
· ⊢ τ_{1} = τ′_{1} : Type
· ⊢ τ_{2} = τ′_{2} : Type
·; C′ ⊗ {ℓ ↦ τ_{1}}; · ⊢ ι_{1}
·; C′ ⊗ {ℓ ↦ τ_{2}}; · ⊢ ι_{2}
·; C; · ⊢ caseptr(ℓ) (inl ⇒ ι_{1} | inr ⇒ ι_{2})

Where τ′_{1} is

∃[Δ′_{1} | C′_{1}]. · · · ∃[Δ′_{j} | C′_{j}].⟨S(1), σ′_{1}, …, σ′_{k}⟩

and τ′_{2} is

∃[Δ′′_{1} | C′′_{1}]. · · · ∃[Δ′′_{m} | C′′_{m}].⟨S(2), σ′′_{1}, …, σ′′_{n}⟩

First, by inspection of the definition of L(·), we can conclude that L(v′) = L(v) and therefore that L(S{ℓ ↦ v′}) = L(S{ℓ ↦ v}). Since GU(S{ℓ ↦ v}) we can conclude GU(S{ℓ ↦ v′}). Second, from (2) and by Canonical Store Forms and Canonical Value Forms, we can conclude that

·; · ⊢ v′ : τ_{i}

Hence, by Lemma 15, we can deduce that

⊢ S{ℓ ↦ v′} : C′ ⊗ {ℓ ↦ τ_{i}}

From the instruction typing judgement, we have

·; C′ ⊗ {ℓ ↦ τ_{i}}; · ⊢ ι_{i}

Therefore, we can conclude that ⊢ (S{ℓ ↦ v′}, ι_{i}).

• Operational Rule

(S, v(v_{1}, …, v_{n})) ⟼_{P} (S, θ(ι))

where

\begin{aligned}v & = & v′[c_{1}, …, c_{m}] \\ v′ & = & fixf[Δ | C](x_{1}:σ_{1}, …, x_{n}:σ_{n}).ι \\ θ & = & [c_{1}, …, c_{m}/Δ][v′/f][v_{1}, …, v_{n}/x_{1}, …, x_{n}] \\ Δ & = & β_{1}:κ_{1}, …, β_{m}:κ_{m} \end{aligned}

Typing Assumption:

1. GU(S)

2. ⊢ S : C.

3. ·; C; · ⊢ v(v_{1}, …, v_{n}).

Where the instruction typing judgement has the form:

\begin{matrix}·; · ⊢ v : ∀[· | C].(σ_{1}, …, σ_{n}) → 0 \\ ·; · ⊢ v_{1} : σ_{1}  ⋯  ·; · ⊢ v_{n} : σ_{n} \end{matrix} ; ·; C; · ⊢ v(v_{1}, …, v_{n})

By Canonical Value Forms,

Δ; C′; f:∀[Δ | C′].(σ′_{1}, …, σ′_{n}) → 0, x_{1}:σ′_{1}, …, x_{n}:σ′_{n} ⊢ ι

and

\begin{matrix}· ⊢ θ(∀[· | C′].(σ′_{1}, …, σ′_{n}) → 0) = \\ ∀[· | C].(σ_{1}, …, σ_{n}) → 0 : Small \end{matrix}

By definition of equality · ⊢ θ(C′) = C : Store and also, for 1 ≤ i ≤ m,

· ⊢ c_{i} : κ_{i}

From the instruction typing judgement, each value v_{i} is well-formed with type σ_{i}. Consequently, by Type and Value Substitution, we know that

·; θ(C′); · ⊢ θ(ι)

By Lemma 11 and the fact that · ⊢ θ(C′) = C : Store, we have

·; C; · ⊢ θ(ι)

From this fact (1) and (2), we can conclude ⊢ (S, θ(ι)).

• Operational Rule

(S, coerce(γ); ι) ⟼_{P} (S′, θ(ι))

where γ(S) ⟼_{γ} S′, θ and γ = union_{τ_{1}∪τ_{2}}(ℓ) or roll_{τ} (ℓ) or unroll(ℓ) is similar to the case for the instruction (v).i := v′.

• Operational Rule

\begin{matrix}(S\{ℓ ↦ v\}, coerce(γ); ι) ⟼_{P} \\ (SS′\{ℓ ↦ v′\}, θ(ι)) \end{matrix}

where

v = pack_{[c_{1},...,c_{n}|S′]as∃[Δ|C].τ} (v′)

         γ = unpack ℓ with Δ

θ = [c_{1}, …, c_{n}/Δ]
Δ = β_{1}:κ_{1}, …, β_{n}:κ_{n}

Typing Assumption:

1. GU(S{ℓ ↦ v})

2. ⊢ S{ℓ ↦ v} : C.

3. ·; C; · ⊢ coerce(γ); ι.

Where the coercion typing judgement is

· ⊢ C = C′′ ⊗ {ℓ ↦ ∃[Δ | C′].τ} : Store
·; C ⊢ unpack ℓ with Δ ⟹ Δ; C′′ ⊗ {ℓ ↦ τ}@C′

and the instruction typing judgement implies ι is wellformed:

Δ; C′′ ⊗ {ℓ ↦ τ} ⊗ C′; · ⊢ ι

By inspection of the definition of L(·), we can deduce that L(S{ℓ ↦ v}) = L(SS′{ℓ ↦ v′}) Therefore, since GU(S{ℓ ↦ v}), we can conclude that GU(SS′{ℓ ↦ v′}). By (2), the coercion typing judgement and Lemma 14 we can deduce that · ⊢ v : ∃[Δ | C′].τ. Consequently, by Canonical Value Forms, we can conclude that ·; · ⊢ v′ : θ(τ). From this fact, (2), and the equality from the coercion typing judgement, using Lemma 15, we can conclude that

⊢ S{ℓ ↦ v′} : C′′ ⊗ {ℓ ↦ θ(τ)}

By Canonical Value forms, we also know that

⊢ S′ : θ(C′)

Therefore, by Lemma 16 we can conclude that

⊢ S{ℓ ↦ v′}S′ : C′′ ⊗ {ℓ ↦ θ(τ)}@θ(C′)

Hence the equivalent store is also well-formed:

⊢ SS′{ℓ ↦ v′} : C′′ ⊗ {ℓ ↦ θ(τ)}@θ(C′)

Canonical Value Forms also implies that for 1 ≤ i ≤ n,

· ⊢ c_{i} : κ_{i}

Now using the instruction typing judgement and the Type Substitution Lemma we can deduce that

·; C′′ ⊗ {ℓ ↦ θ(τ)}@θ(C′); · ⊢ θ(ι)

Consequently, ⊢ (SS′{ℓ ↦ v′}, θ(ι)).

• Operational Rule:

(SS′{ℓ ↦ v}, coerce(γ); ι) ⟼_{P} (S{ℓ ↦ v′}, ι)

where

v′  = pack_{[c_{1},...,c_{n}|S′]as∃[Δ|C′].τ} (v)
γ  = pack_{[c_{1},...,c_{n}|θ(C′)]as ∃[Δ|C′].τ} (ℓ)
θ  = [c_{1}, …, c_{n}/Δ]
S′  = {ℓ_{1} ↦ v_{1}, …, ℓ_{m} ↦ v_{m}}
θ(C′) = {ℓ_{1} ↦ τ_{1}, …, ℓ_{m} ↦ τ_{m}}

Typing Assumption:

1. GU(SS′{ℓ ↦ v})

2. ⊢ SS′{ℓ ↦ v} : C.

3. ·; C; · ⊢ coerce(γ); ι.

Where the coercion typing judgement is

Δ = β_{1}:κ_{1}, …, β_{n}:κ_{n} · ⊢ c_{i} : κ_{i} (for 1 ≤ i ≤ n)

· ⊢ C = C′′ ⊗ {ℓ ↦ θ(τ)} ⊗ θ(C′) : Store
·; C ⊢ pack_{[c_{1},...,c_{n}|θ(C′)]as ∃[Δ|C′].τ} (ℓ) ⟹
·; C′′ ⊗ {ℓ ↦ ∃[Δ | C′].τ}

and the instruction typing judgement implies ι is wellformed:

·; C′′ ⊗ {ℓ ↦ ∃[Δ | C′].τ}; · ⊢ ι

By inspection of the definition of L(·), we can deduce that L(SS′{ℓ ↦ v}) = L(S{ℓ ↦ v′}). Therefore, since GU(SS′{ℓ ↦ v}), we can conclude that (4) GU(S{ℓ ↦ v′}). From the definitions above, we know that

SS′{ℓ ↦ v} = S{ℓ_{1} ↦ v_{1}, …, ℓ_{m} ↦ v_{m}, ℓ ↦ v}

Moreover, the constraint equality judgement in the coercion typing judgement with the definition of θ(C′) implies that

· ⊢ C = C′′ ⊗ {ℓ_{1} ↦ τ_{1}, …, ℓ_{m} ↦ τ_{m}, ℓ ↦ θ(τ)} : Store

Now from (2) and by induction on m and Lemma 14, we can conclude the following facts:

6. ·; · ⊢ v : θ(τ)

7. for 1 ≤ i ≤ m, ·; · ⊢ v_{i} : τ_{i}

8. ⊢ S : C′′ From (7), we can prove ⊢ S′ : θ(C′) using the store typing rule. Consequently, we can show that v′ is well-formed:

\begin{matrix}Δ = β_{1}:κ_{1}, …, β_{n}:κ_{n}  · ⊢ c_{i} : κ_{i} (for 1 ≤ i ≤ n) \\ ⊢ S′ : θ(C′)  ·; · ⊢ v : θ(τ) \end{matrix}
·; · ⊢ pack_{[c_{1},...,c_{n}|S′]as∃[Δ|C′].τ} (v) : ∃[Δ | C′].τ

Since ⊢ S : C′′ and ·; · ⊢ v′ : ∃[Δ | C′].τ, we can conclude by the store typing judgement that (8)

⊢ S{ℓ ↦ v′} : C′′ ⊗ {ℓ ↦ ∃[Δ | C′].τ}

Finally, using (4), (5), (8), we can conclude that ⊢ (S{ℓ ↦ v′}, ι).

Lemma 19 (Progress) If ⊢ (S, ι) then either ι = halt i or (S, ι) ⟼_{P} (S′, ι′).

Proof: By cases on the syntax of the first instruction of ι. The proof follows from Canonical Value Forms and Canonical Store Forms. Here, we show a couple of representative cases.

• (S, new ρ, x, i; ι). This program always steps to

(S{ℓ ↦ _{⟨S(0), …, S(0)⟩}^{i}}, ι[ℓ/ρ][ptr(ℓ)/x])

where ℓ is some location not present in S.

• (S, free v; ι).

Typing Assumption:

1. GU(S)

2. ⊢ S : C.

3. ·; C; · ⊢ free v; ι.

The instruction typing judgement must have the form:

·; · ⊢ v : ptr(ℓ)
· ⊢ C = C′ ⊗ {ℓ ↦ ⟨σ_{1}, …, σ_{n}⟩} : Store
·; C′; · ⊢ ι
·; C; · ⊢ free v; ι

By Canonical Value Forms, v must be ptr(ℓ). By Canonical Store Forms, S = S′{ℓ ↦ v′} and ·; · ⊢ v′ : ⟨σ_{1}, …, σ_{n}⟩. By Canonical Value Forms again, v′ must be ⟨v_{1}, …, v_{n}⟩. Therefore this program meets the precondition for the operational rule for free and it steps to (S′, ι).

• halt v. This program is not considered stuck if v is an integer i. By inspection of the typing rule for halt, we see that

·; · ⊢ v : int

By Canonical Value Forms, v must be an integer i.

• (S, coerce(γ); ι) where γ = unpack ℓ with Δ Typing Assumption:

1. GU(S)

2. ⊢ S : C.

3. ·; C; · ⊢ coerce(γ); ι.

Where the coercion typing judgement has the form:

· ⊢ C = C′′ ⊗ {ℓ ↦ ∃[Δ | C′].τ} : Store
·; C ⊢ unpack ℓ with Δ ⟹ Δ; C′′ ⊗ {ℓ ↦ τ}@C′

and the instruction typing judgement implies ι is wellformed:

Δ; C′′ ⊗ {ℓ ↦ τ}@C′; · ⊢ ι

By Canonical Store Forms, S = S′{ℓ ↦ v} and

·; · ⊢ v : ∃[Δ | C′].τ

By Canonical Value Forms,

v = pack_{[c_{1},...,c_{n}|S′′]as∃[Δ|C′].τ} (v′)

By inspection of the definition of GU(S), we can conclude that (Dom(S′)∪{ℓ})∩Dom(S′′) = ∅. Therefore, S′S′′{ℓ ↦ v} is a store. Canonical Value Forms also implies that Δ = β_{1}:κ_{1}, …, β_{n}:κ_{1} and therefore [c_{1}, …, c_{n}/Δ] is a substitution. Therefore,

(S, coerce(γ); ι) ⟼_{P} (S′S′′{ℓ ↦ v′}, ι[c_{1}, …, c_{n}/Δ])

Definition 20 (Stuck Program) A program (S, ι) is stuck if no operational rule applies and ι is not halt i.

Theorem 21 (Type Soundness) If ⊢ (S, ι) and

(S, ι) ⟼_{P}^{∗} (S′, ι′) then (S′, ι′) is not stuck.

Proof: By induction on the length of the evaluation sequence. Uses Progress and Preservation.