Type-Preserving Flow Analysis and Interprocedural Unboxing

arXiv:1203.1986v1 [cs.PL] 9 Mar 2012

Extended Version
Neal Glew

Leaf Petersen

Intel Labs
neal.glew@intel.com

Intel Labs
leaf.petersen@intel.com

Abstract
Interprocedural flow analysis can be used to eliminate otherwise
unnecessary heap allocated objects (unboxing), and in previous
work we have shown how to do so while maintaining correctness
with respect to the garbage collector. In this paper, we extend the
notion of flow analysis to incorporate types, enabling analysis and
optimization of typed programs. We apply this typed analysis to
specify a type preserving interprocedural unboxing optimization,
and prove that the optimization preserves both type and GC safety
along with program semantics. We also show that the unboxing
optimization can be applied independently to separately compiled
program modules, and prove via a contextual equivalence result
that unboxing a module in isolation preserves program semantics.

1. Introduction
Many languages and compilers use a uniform object representation
in which every source level object is represented at least initially
by a heap allocated object. Such a representation allows polymorphic functions to be compiled once and enables the implementation
of features that use runtime type information. In this representation machine integers and floating-point numbers are placed in a
single-field object, a box, and this operation is called boxing. Operations such as addition require first projecting the number from
the box (unboxing), followed by the actual addition, followed by
the creation of a new box for the result (boxing). Boxing and unboxing operations add considerable overhead, and thus it is highly
desirable to remove them when possible – e.g. when polymorphism
or features requiring runtime type information are not being used.
We refer to the general class of optimizations that attempt to remove unnecessary box and unbox operations as unboxing optimizations. We refer to unboxing optimizations that attempt to eliminate
boxing and unboxing across function boundaries as interprocedural unboxing. We also include in this latter category optimizations
(such as the one given in this paper) which attempt to unbox objects
written to and read from other objects in the heap.
Interprocedural unboxing presents additional challenges in a
typed setting, since type information must be updated to reflect
any unboxing. A box might flow to an argument in an application,
and the parameter of the called function might flow to an unbox
operation. If the optimization decides to remove the box and unbox

[Copyright notice will appear here once ’preprint’ option is removed.]

1

operations then it must also remove the box type on the parameter.
In other words, typed unboxing requires not just rewriting uses and
definitions in the traditional sense, but also rewriting intermediate
points in the program through which the unboxed values flow. At
a high level then, the optimization can be viewed as selecting a
set of box operations, unbox operations, and box types to remove.
Such a selection has a global consistency requirement—a box type
should only be removed if all boxes that flow to it are removed,
a box operation should only be removed if all unbox operations
it flows to are removed, and so on. Thus choosing a set of boxed
objects to eliminate and rewriting the program to reflect this choice
in a consistent manner requires knowing what things flow to what
points in the program, a question that flow analyses are designed
to answer. In this paper we use the results of flow analysis to
formulate correctness conditions for unboxing and then prove that
those conditions ensure correct optimization.
In previous work [8] we considered a simpler problem, that of
rewriting garbage-collector (GC) metadata rather than full types.
An accurate GC requires specifying for each field of each object
and each slot of each stack activation frame whether it contains
a pointer into the GC heap or not (contains a machine integer,
floating-point number, etc.). As with types, when interprocedurally
unboxing such metadata must be rewritten in a globally consistent
manner. Our previous paper showed how to do this rewriting correctly using the results of a flow analysis, in a whole program setting. In this paper we extend these ideas to develop a methodology
for dealing with interprocedural optimization of statically typed
languages (including universal polymorphism) in a type preserving
fashion. We also show that this methodology does not depend on
whole program compilation, and extends easily to support modular
compilation.
In the following sections, we begin by defining a core language
with a polymorphic type system that has box and unbox operations. As in our previous paper we formalize a notion of GC safety
for our language—that the GC metadata is currently correct—and
show that well-typed programs are GC safe throughout execution.
Next we specify a set of abstract conditions that a reasonably flow
analysis must satisfy, with the property that any flow analysis that
satisfies these conditions can be used in our framework to optimize
programs. The main section of the paper defines an unboxing optimization parameterized over a choice of objects to unbox, and
gives a set of correctness conditions under which such a choice
is guaranteed to preserve typing and preserve semantics. We show
that this set of correctness conditions is satisfiable by constructing a
simple unboxing algorithm which satisfies these conditions. Finally
we extend the system slightly by defining a notion of unboxing for
modules and show that it is correct in the sense that a module is
contextually equivalent to its unboxing.
While our paper is specifically about the concrete optimization
of unboxing, the ideas used here generalize naturally to other op-

2018/2/19

timizations that change the representation of objects in a non-local
fashion. For example, dead-field elimination and dead-parameter
elimination impose similar requirements for rewriting types and
GC metadata in a globally consistent fashion. Flow analyses can be
used to specify and implement these (and others), and we believe
(based on practical experience in our compiler) that the framework
presented here extends naturally to such optimizations. As far as we
know, this and our previous paper are the first to use a flow analysis
to rewrite types and GC metadata in a globally consistent fashion,
and to use a flow analysis to formulate correctness conditions for
this rewriting process and prove these conditions sound.

consequently it does not scale to typed core languages in which
one must be able to check the well-typedness (and hence the GC
safety) of programs before and after optimization[6]. In this paper,
we intend to develop a methodology for addressing this style of
optimization in a strongly typed setting.
2.1 Type safety
How does the problem of unboxing change in a typed setting?
Consider again the first example from this section using a still
informal but now typed notation:
let
f : box(int) → box(box(int)) = λx: box(int).(box x)
in unbox(unbox(f (box 3)))

2. A type and GC safe core language
Consider the following untyped program (using informal notation),
where box denotes a boxing operation that wraps its argument in
a heap-allocated structure, and unbox denotes its elimination form
that projects out the boxed item from the box:
let f = λx.(box x) in unbox(unbox(f (box 3)))
The only definition reaching the variable x is the boxed machine
integer 3. Information from an interprocedural analysis can be used
to rewrite this program to eliminate the boxing as follows:
let f = λx.x in f 3
This second version is much better in that it does less allocation,
and executes fewer instructions. In this optimized version of the
program however, an important property has changed that is not
reflected in this untyped synatax. Specifically, the GC status of
values reaching x has changed: whereas in the original program
all values reaching x are represented as heap allocated pointers,
in the second program all values reaching x are represented as
machine integers. From the standpoint of a garbage collector, a
garbage collection occuring while x is live must treat x as a root
in the first program, and must ignore x in the second program.
The question of which variables should be treated as roots by
the garbage collector is a subtle but crucial one for the purposes of
optimization and compiler correctness. Consider a modification of
the previous example in which the function f is used polymorphically:
let f = λx.(box x) in unbox(unbox((unbox(f f )) (box 3)))
In this variant, f is applied to itself and the boxed result (itself)
is unboxed and applied to a boxed integer. The resulting doubly
boxed integer is then unboxed. Assuming that functions are represented as heap-allocated objects, each variable in this program has a
concrete and statically known status as either a GC root or GC nonroot, since all objects passed to f are heap references. However,
an attempt to unbox this program as with the previous example results in f being applied to both heap references (f ) and non-heap
references (3).
let f = λx.x in(f f ) 3
Consequently, a correct optimizer must decline to unbox this program (at least in entirety) to avoid incorrect GC behavior 1 .
In our previous work[8] we developed a core language capturing
the essential issues of GC safety, along with an analysis and optimization framework for reasoning about and optimizing GC safe
programs in an untyped setting. This framework allows us to show
that given a GC safe program, our unboxing optimization will always produce a semantically equivalent GC safe program. However, the framework is essentially limited to untyped programs and
1 A conservative GC, or a GC implementation which tags pointers to distinguish them from non-pointers would not impose this restriction. See Section 2.2 for more discussion of the GC model.

2

As before, it is apparent that the only definition reaching the
variable x is the boxed machine integer 3, and as before we can
consider rewriting this program to eliminate (interprocedurally)
the boxing. However, simply rewriting the terms of the program
is inadequate from the standpoint of type preserving compilation,
since the result is not well-typed:
let
f : box(int) → box(box(int)) = λx: box(int).x
in f 3
The types of both the actual argument and the return value of f have
changed, and are no longer consistent with the type annotation for f
and x. In order to correctly unbox this program then, it is necessary
to rewrite not just the terms, but also the types:
let f :int → int = λx:int.x in f 3
This requirement is a more substantial change than might at first
be apparent. In the original (untyped) setting, it was sufficient to
have information only about the direct definitions (boxes) and uses
(unboxes) of objects. Rewriting the types in this fashion requires
information not just about the uses and definitions, but also about
intermediate program points (and other objects) through which the
boxed objects flow.
In addition to incurring these additional rewriting requirements,
the typed setting must still account for GC safety. Consider again
the polymorphic variant of the previous untyped example (naming
the first application of f for clarity).
let
f :∀α.α → box(α) = Λα.λx:α.(box x)
g: box(∀α.α → box(α)) = f [∀α.α → box(α)](f )
in unbox(unbox((unbox g)[box(int)](box 3)))
Here we have f applied to itself at a universal type to produce a
boxed version of itself (g), which is then unboxed and applied to a
boxed integer, at the boxed integer type. Attempting to unbox this
example (rewriting types as necessary) immediately illuminates the
problem.
let
f :∀α.α → α = Λα.λx:α.x
g:∀α.α → α = f [∀α.α → α](f )
in g[int](3)
The function f is instantiated directly at a universal function type,
and via its alias (g) at a machine integer type. As with the untyped
example in the previous section, the compiler cannot assign a concrete GC status to the variable x. For correctness then, the compiler
must not (fully) unbox this example, and must leave at least the
boxing operation on the integer parameter to f 2 .
2 It

is worth noting that an optimizing compiler might choose to duplicate
the body of f to make it monomorphic, and hence allow it to be unboxed.
It is also possible to use a runtime type passing interpretation to relax the

2018/2/19

Traceabilities
Labels
Type variables
Labeled Types
Types
Term variables
Constants
Labeled Terms
Terms
Values
Environments
States

t
i
τ
σ
e
m
v
ρ
M

::= b | r
::= 0, 1, . . .
α, β
::= σ i
::= α | B | ∀α.τ1 → τ2 | box(τ )
f, x, y, z
c
::= mi | v i
::= x | fix f [α](x:τ1 ):τ2 .e | e1 [τ ] e2 |
boxτ e | unbox e | ρ(e)
::= c | hρ, fix f [α](x:τ1 ):τ2 .ei | hv i :τ i
::= x1 :τ1 = v1 j1 , . . . , xn :τn = vn jn
::= (ρ, e)
Figure 1. Syntax

In the rest of this paper we make these issues concrete and formal, and we show how to deal with them issues by extending the
notion of flow analysis to incorporate types, thereby generating the
necessary flow information to correctly rewrite types and terms in
a consistent fashion. While we focus on a concrete optimization
(unboxing), we believe that these ideas are generally applicable to
flow analysis based representation optimizations in typed intermediate languages.
2.2 A core language for GC safety
In order to give a precise account of typed flow analysis and interprocedural unboxing, we begin by defining a type safe core language incorporating the essential features of GC safety. The motivation for the (small) idiosyncracies of this language lies in the
requirements of the underlying model of garbage collection. We assume that pointers cannot be intrinsically distinguished from nonpointers, and hence the compiler is required to statically annotate
the program with garbage collection meta-data such that at any
garbage collection point the garbage collector can reconstruct exactly which live variables are roots. Typically, this takes the form of
annotations on variables and temporaries indicating which contain
heap-pointers (the roots) and which do not (the non-roots), along
with information at every allocation site indicating which fields of
the allocated object contain traceable data. This approach is common in modern systems, and it is this approach that we target in
this paper.
Figure 1 defines the syntax of our core language. The essence of
the language is a standard polymorphic lambda calculus extended
with a fix point operator, implemented via an explicit environment
semantics. For the purposes of the semantics, we also include a
form of degenerate type information we call traceabilities. Traceabilities describe the GC status of variables: the traceability b (for
bits) indicates something that should be ignored by the garbage
collector, while the traceability r (for reference) indicates a GCmanaged pointer. The traceability b is inhabited by an unspecified
set of constants c while the traceability r is inhabited by functions
(anticipating their implementation by heap-allocated closures) and
by boxed objects. Anticipating the needs of the flow analysis, we
label each type, term, value, and variable binding site with an integer label. We do not assume that labels or variables are unique
within a program.
Types σ consist of type variables, the base type of constants,
B, function types, ∀α.τ1 → τ2 , and boxed types box(τ ). In order
to provide a concrete implementation strategy for the garbage colconstraints on the garbage collector sufficiently to permit this example[1].
These optimizations are orthogonal (but complementary) to the issues addressed by this paper.

3

lector, we insist that every type correspond to a traceability so that
we can extract the necessary garbage collection meta-data. Types
are mapped to traceabilities using the function tr (τ ), defined in
Figure 2. Polymorphic functions are restricted by well-formedness
rules to only be instantiated with types with the traceability r, and
consequently tr (α) = r. We define substitution of types in the
standard way and define τ [σ i /α] = τ [σ/α].
Expressions e consist of labeled terms mi and labeled values v i . The terms m consist of variables, functions, applications, box introductions, box eliminations, and frames. Functions
fix f [α](x:τ1 ):τ2 .e are polymorphic and recursive and variable
binding sites are decorated with types. We represent heap allocation in the language via the boxτ e term, which corresponds to
allocating a heap cell containing the value for e. The type τ is used
by the dynamic semantics to provide the meta-data with which the
heap-cell will be tagged, allowing the garbage collector to trace the
cell. However, only the top-level traceability of the type (given by
the tr () function in Figure 2) is actually required by the dynamic
semantics, and so the language can be erased into an untyped language in the obvious way. Objects can be projected out of an allocated object by the unbox e operation. Frames ρ(e) are discussed
further below.
Values consist of either constants, closures, or heap-allocated
boxes. We distinguish between the introduction form (boxτ e) and
the value form (hv i :τ i) for allocated objects. The introduction form
corresponds to the allocation instruction, whereas the value form
corresponds to the allocated heap value. This distinction is key for
the formulation of GC safety and the dynamic semantics. For the
purposes of the dynamic semantics we also distinguish between
functions (fix f [α](x:τ1 ):τ2 .e) and the heap allocated closures
that represent them at runtime (hρ, fix f [α](x:τ1 ):τ2 .ei).
For notational convenience, we will sometimes use the notation
vb to indicate that a value v is a non-heap-allocated value (i.e. a
constant c), and vr to indicate that a value v is a heap-allocated
value (i.e. either a function value or a boxed value). If t is a
traceability meta-variable, then we use vt to indicate that v is a
value of the same traceability as t.
In examples, we use a derived let expression, taking it to be
syntactic sugar for application in the usual manner. Environments
ρ map variables to values. The term ρ(e) executes e in the environment ρ rather than the outer environment – all of the free variables
of e are provided by ρ. The nested set of these environments at any
point can be thought of as the activation stack frames of the executing program. The traceability of the typing annotations on variables
in the environments play the role of stack-frame GC meta-data, indicating which slots of the frame are roots (traceability r). The environments buried in closures (hρ, fix f [α](x:τ1 ):τ2 .ei) similarly
provide the traceabilities of values reachable from the closure via
the type annotations on the variables in the environment, and hence
provide the GC meta-data for tracing through closures. While we
do not make the process of garbage collection explicit, it should
be clear how to extract the appropriate set of GC roots from the
environment and any active frames.
This core language contains the appropriate information to formalize a notion of GC safety consisting of two complementing
pieces. First we define a dynamic semantics in which reductions
that might lead to undefined garbage-collector behavior are explicitly undefined. Programs that take steps in this semantics do not
introduce ill-formed heap objects. Secondly, we define a notion
of a traceable program: one in which all heap values have valid
GC meta-data. Reduction steps in the semantics can then be shown
to maintain the traceability property in addition to the usual welltypedness property. The GC correctness criteria for a compiler optimization then becomes simply the usual one: that the optimization
map well-typed programs to semantically equivalent well-typed

2018/2/19

programs. By showing that typable programs are both traceable
programs and have well-defined semantics, we thereby show that
GC correctness for a compiler optimization can be achieved simply
by preserving well-typedness.
It is worth noting that in our implementation, the compiler intermediate language under consideration is substantially more lowlevel: a control-flow graph based, static single assignment intermediate representation. We believe however that all of the key issues
are captured faithfully in this higher-level representation, and with
greater clarity of presentation.

tr (σ i )
tr (α)
tr (B)
tr (∀α.τ1 → τ2 )
tr (box(τ ))

tr (σ)
r
b
r
r

x:τ = v j ∈ ρ
(ρ, xk ) 7−→ (ρ, v j )

(ρ, (fix f [α](x:τ1 ):τ2 .e)j ) 7−→
(ρ, hρ, fix f [α](x:τ1 ):τ2 .eij )

2.3 Operational semantics
We choose to use an explicit environment semantics rather than a
standard substitution semantics since this makes the GC meta-data
(implicit in the types) for stack frames and closures explicit in the
semantics. Thus a machine state (ρ, e) supplies an environment ρ
for e that provides the values of the free variables of e during execution. Environments contain typing annotations on each of the
variables mapped by the environment, which provide the traceabilities of the variables.
Reduction in this language is for the most part fairly standard.
We deviate somewhat in that we explicitly model the allocation of
heap objects as a reduction step—hence there is an explicit reduction mapping a function term fix f [α](x:τ1 ):τ2 .e to an allocated
closure hρ, fix f [α](x:τ1 ):τ2 .ei, and similarly for boxed objects
and values. More notably, beta-reduction is restricted to only permit
construction of a stack frame when the type for the parameter variable has an appropriate traceability for the actual argument value.
This captures the requirement that stack frames have correct metadata for the garbage collector. In actual practice, incorrect metadata for stack frames leads to undefined behavior (since incorrect
meta-data may cause arbitrary memory corruption by the garbage
collector)—similarly here in the meta-theory we leave the behavior of such programs undefined. In a similar fashion, we only define the reduction of the allocation operation to an allocated value
(boxτ vt 7−→ hvt :τ i) when the operation meta-data is appropriate
for the value (i.e. tr (τ ) = t).
It is important to note that this semantics does not model a
dynamically checked language, in which there is an explicit check
of the meta-data associated with these reductions. The point is
simply that the semantics only specifies how programs behave
when these conditions are met—in all other cases the behavior of
the program is undefined.

=
=
=
=
=

tr (τ ) = t
j

j

(ρ, (boxτ vt i ) ) 7−→ (ρ, hvt i :τ i )
(ρ, e1 ) 7−→ (ρ, e′1 )
i

(ρ, (e1 [τ ] e2 )i ) 7−→ (ρ, (e′1 [τ ] e2 ) )
(ρ, e2 ) 7−→ (ρ, e′2 )
j

j

(ρ, (v i [τ ] e2 ) ) 7−→ (ρ, (v i [τ ] e′2 ) )
vf = hρ′ , fix f [α](x:τ1 ):τ2 .ei τ ′ = (∀α.τ1 → τ2 )i
τ1′ = τ1 [τ /α] tr (τ1′ ) = t
k

(ρ, (vf i [τ ] vt j ) ) 7−→
k
(ρ, (ρ′ , f :τ ′ = vf i , x:τ1′ = vt j )(e[τ /α]) )
(ρ, e) 7−→ (ρ, e′ )
i

(ρ, (boxτ e)i ) 7−→ (ρ, (boxτ e′ ) )
(ρ, e) 7−→ (ρ, e′ )
i

(ρ, (unbox e)i ) 7−→ (ρ, (unbox e′ ) )
j k

(ρ, (unbox hv i :τ i ) ) 7−→ (ρ, v i )
(ρ′ , e) 7−→ (ρ′ , e′ )
i

i

(ρ, ρ′ (e) ) 7−→ (ρ, ρ′ (e′ ) )

j

(ρ, ρ′ (v i ) ) 7−→ (ρ, v i )

2.4 Traceability
The operational semantics ensures that no reduction step introduces
mis-tagged values. In order to make use of this, we define a judgment for checking that a program does not have a mis-tagged value
in the first place. Implicitly this judgement defines what a wellformed heap and activation stack looks like; however, since our
heap and stack are implicit in our machine states, it takes the form
of a judgement on terms, values, environments, and machine states.
The value judgement ⊢v v:t asserts that a value v is wellformed, and has traceability t. In this simple language, this corresponds to having the types on the variables in the environment
of each function value have traceabilities which are consistent with
the values to which they are bound, and the type on each boxed
value be consistent with the traceability of the object nested in the
box. An environment is consistent, ⊢ ρ tr, when the annotation on
each variable agrees with the traceability of the value it is bound to.
The term judgement ⊢ e tr and machine state judgement ⊢ M tr
simply check that all values and environments (and hence stack
frames) contained in the term or machine state are well-formed.

4

Figure 2. Operational Semantics
The key result for traceability is that it is preserved under reduction. That is, if a traceable term takes a well-defined reduction step,
then the resulting term will be traceable.
Lemma 1 (Preservation of traceability)
If ⊢ M tr and M 7−→ M ′ then ⊢ M ′ tr.
Proof: If ⊢ (ρ, e) tr then ⊢ ρ tr and ⊢ e tr. If (ρ, e) 7−→ (ρ, e′ )
then the result follows if we can show ⊢ e′ tr. The proof of that is
by induction on the derivation of (ρ, e) 7−→ (ρ, e′ ). Consider the
cases for the last rule used to derive it (the cases are in the same
order as in the figure):
• In this case, e = xk for some x and k, and e′ = v j where

x:τ = v j ∈ ρ for some τ , v, and j. Since ⊢ ρ tr then
⊢v v:tr (τ ), so by the traceability rules ⊢ v j tr as required.

2018/2/19

• In this case, e = (e1 [τ ] e2 )i for some e1 , τ , e2 , and i, e′ =

⊢ e tr

Labeled Terms
⊢ m tr

i

(e′1 [τ ] e2 ) for some e′1 , and (ρ, e1 ) 7−→ (ρ, e′1 ) is a subderivation. The first hypothesis is that ⊢ (e1 [τ ] e2 )i tr. There is
only one rule to derive this judgement and that rule requires
that ⊢ e1 [τ ] e2 tr, which in turn can only be derived by one
rule that requires both ⊢ e1 tr and ⊢ e2 tr. Thus, by the
induction hypothesis, ⊢ e′1 tr. Then, by the rules for traceability, ⊢ e′1 [τ ] e2 tr, and by the traceability rules again,
i
⊢ (e′1 [τ ] e2 ) tr, as we are required to prove.

⊢v v:t

i

⊢ v i tr

⊢ m tr

⊢ m tr

Terms
⊢ e tr
⊢ x tr
⊢ e1 tr

⊢ fix f [α](x:τ1 ):τ2 .e tr

⊢ e2 tr

j

• In this case, e = (v i [τ ] e2 ) for some v, i, τ , e2 , and j,

⊢ e tr

⊢ e1 [τ ] e2 tr

⊢ boxτ e tr

⊢ e tr

⊢ ρ tr

⊢ unbox e tr

⊢ e tr

⊢ ρ(e) tr
⊢v v:t

Values

l

e = (vf j [τ ] vt k )
vf = hρ′ , fix f [α](x:τ1 ):τ2 .e′′ i
l
e′ = ρ′′ (e′′ [τ /α])
′′
′
′
ρ = ρ , f :τ = vf j , x:τ1′ = vt k
τ ′ = (∀α.τ1 → τ2 )j
τ1′ = τ1 [τ /α]
tr (τ1′ ) = t
(6)

⊢v hv i :τ i:r
⊢ ρ tr

⊢ e tr

⊢v hρ, fix f [α](x:τ1 ):τ2 .ei:r
⊢ ρ tr

Environments
⊢v v1 :tr (τ1 )

···

for some ρ′ , f , α, x, τ1 , τ2 , e′′ , j, τ , vt , k, and l. The first hyl
pothesis is that ⊢ (vf j [τ ] vt k ) tr. There is only one rule to derive that judgement and that rule requires that ⊢ vf j [τ ] vt k tr,
which in turn can only be derived by one rule that requires both
⊢ vf j tr and ⊢ vt k tr. Both of these latter derivations can only
be derived by one rule and those rules require that ⊢v vf :r (1)
and ⊢v vt :t (2) (a simple inspection reveals the traceabilities to
be r and t). Judgement 1 can only be derived by one rule and
that rule requires that ⊢ ρ′ tr (3) and ⊢ e′′ tr (4). By (3), (1),
tr (τ ′ ) = r, (2), and (6) we can derive ⊢ ρ′′ tr (5). By (5) and
(4) we can derive ⊢ ρ′′ (e′′ ) tr, and then ⊢ e′ tr, as required.

⊢v vn :tr (τn )

⊢ x1 :τ1 = v1 j1 , . . . , xn :τn = vn jn tr
⊢ M tr

Machine States
⊢ ρ tr

e′2 ,

• In this case:

⊢v v:tr (τ )
⊢v c:b

j
e′2 )

i

and (ρ, e2 ) 7−→ (ρ, e′2 ) is a
for some
e = (v [τ ]
j
subderivation. The first hypothesis is that ⊢ (v i [τ ] e2 ) tr.
There is only one rule to derive this judgement and that rule
requires that ⊢ v i [τ ] e2 tr, which in turn can only be derived
by one rule that requires both ⊢ v i tr and ⊢ e2 tr. Thus,
by the induction hypothesis, ⊢ e′2 tr. Then, by the rules for
traceability, ⊢ v i [τ ] e′2 tr, and by the traceability rules again,
j
⊢ (v i [τ ] e′2 ) tr, as we are required to prove.
′

⊢ e tr

⊢ (ρ, e) tr
Figure 3. Traceability

• In this case, e = (boxτ e′′ )i for some τ , e′′ , and i, e′ =
i

• In this case, e = (fix f [α](x:τ1 ):τ2 .e′′ )j for some f , α,
j

x, τ1 , τ2 , e′′ , and j, and e′ = hρ, fix f [α](x:τ1 ):τ2 .e′′ i .
j
The first hypothesis is that ⊢ (fix f [α](x:τ1 ):τ2 .e′′ ) tr.
There is only one rule to derive this judgement and that
rule requires that ⊢ fix f [α](x:τ1 ):τ2 .e′′ tr, which in turn
can only be derived by one rule that requires that ⊢ e′′ tr.
Then, and since ⊢ ρ tr, by the rules for traceability, ⊢v
hρ, fix f [α](x:τ1 ):τ2 .e′′ i:r, and by the traceability rules again
j
⊢ hρ, fix f [α](x:τ1 ):τ2 .e′′ i tr, as we are required to prove.
• In this case, e = (boxτ vt i )

j

for some τ , vt , i, and j,
e = hvt :τ i , and tr (τ ) = t. The first hypothesis is that
j
⊢ (boxτ vt i ) tr. There is only one rule to derive this judgement and that rule requires that ⊢ boxτ vt i tr, which in turn
can only be derived by one rule that requires that ⊢ vt i tr.
There is only one rule to derive the latter judgement and it requires that ⊢v vt :t′ for some t′ . By inspection of the rules for
value traceability, we see that t = t′ . Since tr (τ ) = t = t′ , by
the rules for traceability, ⊢v hvt i :τ i:r, and by the traceability
j
rules again ⊢ hvt i :τ i tr, as we are required to prove.
′

i

j

5

(boxτ e′′′ ) , and (ρ, e′′ ) 7−→ (ρ, e′′′ ) is a subderivation. The
i
first hypothesis is that ⊢ (boxτ e′′ ) tr. There is only one rule to
derive this judgement and that rule requires that ⊢ boxτ e′′ tr,
which in turn can only be derived by one rule that requires that
⊢ e′′ tr. Thus, by the induction hypothesis, ⊢ e′′′ tr. Then, by
the rules for traceability, ⊢ boxτ e′′′ tr, and by the traceability
i
rules again, ⊢ (boxτ e′′′ ) tr, as we are required to prove.
• In this case, e = (unbox e′′ )i for some e′′ and i, e′ =
i

(unbox e′′′ ) , and (ρ, e′′ ) 7−→ (ρ, e′′′ ) is a subderivation.
i
The first hypothesis is that ⊢ (unbox e′′ ) tr. There is only
one rule to derive this judgement and that rule requires that
⊢ unbox e′′ tr, which in turn can only be derived by one rule
that requires that ⊢ e′′ tr. Thus, by the induction hypothesis,
⊢ e′′′ tr. Then, by the rules for traceability, ⊢ unbox e′′′ tr,
i
and by the traceability rules again, ⊢ (unbox e′′′ ) tr, as we
are required to prove.
j k

• In this case, e = (unbox hv i :τ i ) for some τ , v, i, j, and k,
j k

and e′ = v i . The first hypothesis is that ⊢ (unbox hv i :τ i ) tr.
There is only one rule to derive this judgement and that rule
j
requires that ⊢ unbox hv i :τ i tr, which in turn can only be

2018/2/19

∆
Γ

::=
::=

∆; Γ ⊢ e : τ

α1 , . . . , αn
x1 :τ1 , . . . , xn :τn

x:τ ∈ Γ

∆ ⊢ τ wf

∆; Γ ⊢ xi : τ
ftv (τ ) ⊆ ∆

∆ ⊢ (∀α.τ1 → τ2 )i wf
∆, α; Γ, f :(∀α.τ1 → τ2 )i , x:τ1 ⊢ e : τ2

∆ ⊢ τ wf
⊢ τ1 = τ2

∆; Γ ⊢ (fix f [α](x:τ1 ):τ2 .e)i : (∀α.τ1 → τ2 )i
j

∆; Γ ⊢ e1 : (∀α.τ1 → τ ′ ) ∆; Γ ⊢ e2 : τ2
∆ ⊢ τ wf tr (τ ) = r ⊢ τ1 [τ /α] = τ2

⊢ Bi = Bj

⊢ αi = αj
⊢ τ11 = τ21

∆; Γ ⊢ (e1 [τ ] e2 )i : τ ′ [τ /α]

⊢ τ12 = τ22

∆ ⊢ τ wf

⊢ (∀α.τ11 → τ12 )i = (∀α.τ21 → τ22 )j

∆; Γ ⊢ e : τ ′

⊢ τ = τ′

⊢ τ1 = τ2

∆; Γ ⊢ (boxτ e)i : box(τ )i

⊢ box(τ1 )i = box(τ2 )j

∆; Γ ⊢ e : box(τ )j
∆; Γ ⊢ (unbox e)i : τ

⊢ρ:Γ
∅ ⊢ τ1 wf
∅; ∅ ⊢ v1 i1 : τ1′
⊢ τ1 = τ1′

···
···
···

∅ ⊢ τn wf
∅; ∅ ⊢ vn in : τn′
⊢ τn = τn′

⊢ ρ : Γ′

∅; Γ′ ⊢ e : τ

∆; Γ ⊢ ρ(e)i : τ

⊢ x1 :τ1 = v1 i1 , . . . , xn :τn = vn in : x1 :τ1 , . . . , xn :τn
∆; Γ ⊢ ci : Bi

⊢M :τ
⊢ρ:Γ

⊢ ρ : Γ′ ∅ ⊢ (∀α.τ1 → τ2 )i wf
α; Γ′ , f :(∀α.τ1 → τ2 )i , x:τ1 ⊢ e : τ2

∅; Γ ⊢ e : τ

⊢ (ρ, e) : τ

∆; Γ ⊢ hρ, fix f [α](x:τ1 ):τ2 .eii : (∀α.τ1 → τ2 )i

Figure 4. Type rules, other constructs
∅ ⊢ τ wf
j

derived by one rule that requires that ⊢ hv i :τ i tr. There is only
one rule to derive this latter judgement and that rule requires
that ⊢v hv i :τ i:t for some t, which in turn can only be derived
by one rule that requires that ⊢v v:tr (τ ). Then, by the rules for
traceability, ⊢ v i tr, as we are required to prove.
• In this case, e = ρ′ (e′′ )i for some ρ′ , e′′ and i, e′ = ρ′ (e′′′ )i

for some e′′′ , and (ρ′ , e′′ ) 7−→ (ρ′ , e′′′ ). The hypothesis ⊢ e tr
can only be derived in a certain way, unpacking that we see
that ⊢ ρ′ tr and ⊢ e′′ tr. Then by the induction hypothesis,
⊢ e′′′ tr. So applyling the rules, we derive that ⊢ ρ′ (e′′′ ) tr
and then ⊢ e′ tr, as required.
j

• In this case, e = ρ′ (v i ) for some ρ′ , v, i, and j, and e′ = v i .

The hypothesis, ⊢ e tr can only be derived in one way and
unpacking that we see that ⊢ v i tr, which is what we are
required to prove.
There is no corresponding progress property for our notion of
traceability, since in the absence of further guarantees, programs
can go wrong. However, typable programs are both traceable and
do not go wrong, as we will see in the next section, and so preserving typability ensures GC correctness.
2.5 Typing
The typing rules appear in Figures 4 and 5. They are for the most
part standard except for three modifications. First, as types are labelled, we must sometimes ignore the labels in typing. Judgement

6

∆; Γ ⊢ v j : τ ′

⊢ τ = τ′

i

∆; Γ ⊢ hv j :τ i : box(τ )i
Figure 5. Type rules, expressions

⊢ τ1 = τ2 states that types τ1 and τ2 are syntactically equivalent except that the labels on their sub-terms might differ. This is
important in (for example) the rule for application, where we require only that the parameter type τ1 and the actual argument type
τ2 satisfy ⊢ τ1 = τ2 rather than τ1 = τ2 ; similarly in the rule
for environments. Second, in the rules for boxes we require that
the traceability of the box equal the traceability of the type of the
thing being boxed. This is essential for showing that well-typedness
implies traceability. Finally, the instantiation rule for polymorphic
functions enforces the property that the type argument have traceability r.
One particularly important aspect of our language is that we
assume a type erasure semantics. For this interpretation to be correct, we must show that we can compute the correct GC metadata
when erasing types. The operational semantics have the application of a polymorphic function step to a frame where the annotation on the function’s parameter is a substituted type. We need that
the GC metadata for this substituted type equal the GC metadata
for the unsubstituted parameter type of the function. The requirement tr (τ ) = r in the typing rule for application is crucial to that
equality, and the following lemma proves it.

2018/2/19

• (Variable) In this case, e1 = xi , e2 = v j , and x:τ ′ = v j ∈ ρ

Lemma 2
If tr (τ ) = r then tr (τ ′ ) = tr (τ ′ [τ /α]).
Proof: The proof is by inspection of the definitions.
We can prove type safety for this language in the standard
way, via progress and preservations lemmas. First we need several
lemmas: that type equality is an equivalence relation, that equal
types have the same traceabilities, that a well-typed value has
the same traceability as its type, that type equality respects type
substitution, that value typing is independent of the typing context,
and a type substitution lemma.
Lemma 3
Type equality is an equivalence relation, that is, ⊢ τ = τ , ⊢ τ1 =
τ2 implies ⊢ τ2 = τ1 , and ⊢ τ1 = τ2 and ⊢ τ2 = τ3 implies
⊢ τ1 = τ3 .
Proof: The proof is by a simple induction on the structure of τ for
reflexivity or the structure of the derivation(s) for symmetry and
transitivity and inspection of the rules.

for some x, i, v, j, and τ ′ . The typing judgement can only be
derived with one rule and it requires that x:τ ∈ Γ. The typing
judgement (for ρ) can only be derived in one way and it requires
that τ = τ ′ , ∅; ∅ ⊢ v j : τ ′′ , and ⊢ τ = τ ′′ . Thus the desired τ2
is τ ′′ . We just need to show that ∅; Γ ⊢ v j : τ2 , which follows
by Lemma 7.

• (Fix expression) In this case, e1 = (fix f [α](x:τ1′ ):τ2′ .e′ )i
i

and e2 = hρ, fix f [α](x:τ1′ ):τ2′ .e′ i . The typing judgement
can only be derived with one rule and it requires that ∅ ⊢ τ1 wf ,
i
α; Γ, f :τ1 , x:τ1′ ⊢ e′ : τ2′ and τ1 = (∀α.τ1′ → τ2′ ) . Thus by
the typing rules, ∅; Γ ⊢ e2 : τ1 . By Lemma 3, ⊢ τ1 = τ1 , so
the result follows by setting τ2 = τ1 .
j

• (Box expression) In this case, e1 = (boxτ v i ) and e2 =
i

j

hv :τ i for some τ , v, i, and j. The typing judgement can
only be derived with one rule and it requires that ∅ ⊢ τ wf ,
∅; Γ ⊢ v i : τ ′ , ⊢ τ = τ ′ , and τ1 = box(τ )j . By the typing
rules, ∅; Γ ⊢ e2 : τ1 . By Lemma 3, ⊢ τ1 = τ1 , so the result
follows by setting τ2 = τ1 .
• (Application function) In this case, e1 = (e3 [τ ] e4 )i , e2 =

Lemma 4
If ⊢ τ1 = τ2 then tr (τ1 ) = tr (τ2 ).
Proof: The proof is by inspection of the last rule used.
Lemma 5
If ⊢ τ1 = τ2 then ⊢ τ1 [τ /α] = τ2 [τ /α].
Proof: The proof is by an easy induction on the derivation of
⊢ τ1 = τ2 .
Lemma 6
If ∆; Γ ⊢ vt i : τ then tr (τ ) = t.

(e5 [τ ] e4 )i , and (ρ, e3 ) 7−→ (ρ, e5 ) for some e3 , τ , e4 , and e5 .
The typing judgement can only be derived with one rule and it
j
requires that ∅; Γ ⊢ e3 : (∀α.τ3 → τ ′ ) , ∅; Γ ⊢ e4 : τ4 , ∅ ⊢
τ wf , tr (τ ) = r, ⊢ τ3 [τ /α] = τ4 , and τ = τ ′ [τ /α] for some
τ3 , τ ′ , j, and τ4 . By the induction hypothesis, ∅; Γ ⊢ e5 : τ5
j
and ⊢ (∀α.τ3 → τ ′ ) = τ5 for some τ5 . There is only one rule
to derive the latter and it requires that τ5 = (∀α.τ51 → τ52 )k ,
⊢ τ3 = τ51 , and ⊢ τ ′ = τ52 for some τ51 , τ52 , and k. By
Lemma 5, ⊢ τ3 [τ /α] = τ51 [τ /α] and ⊢ τ ′ [τ /α] = τ52 [τ /α].
By Lemma 3, ⊢ τ51 [τ /α] = τ4 . So by the typing rules, ∅; Γ ⊢
e2 : τ52 [τ /α]. The result follows by setting τ2 = τ52 [τ /α].

• (Application argument) In this case, e1 = (e3 [τ ] e4 )i , e2 =

Proof: The proof is by inspection of the three rules for value
typing.
Lemma 7
If ∆; Γ ⊢ v i : τ then ∆′ ; Γ′ ⊢ v i : τ for any ∆′ and Γ′ .
Proof: The proof is by any easy induction on the typing derivation
and inspection of the three rules for value typing.

(e3 [τ ] e5 )i , and (ρ, e3 ) 7−→ (ρ, e5 ) for some e3 , e4 , and e5 .
The typing judgement can only be derived with one rule and it
j
requires that ∅; Γ ⊢ e3 : (∀α.τ3 → τ ′ ) , ∅; Γ ⊢ e4 : τ4 , ∅ ⊢
τ wf , tr (τ ) = r, ⊢ τ3 [τ /α] = τ4 , and τ1 = τ ′ [τ /α] for some
τ3 , τ ′ , j, and τ4 . By the induction hypothesis, ∅; Γ ⊢ e5 : τ5
and ⊢ τ4 = τ5 . By Lemma 3, ⊢ τ3 [τ /α] = τ5 . So by the typing
rules, ∅; Γ ⊢ e2 : τ1 . By Lemma 3, ⊢ τ1 = τ1 , so the result
follows by setting τ2 = τ1 .

• (Application beta) In this case:

Lemma 8
If ∆, α, ∆′ ; Γ ⊢ e : τ , ∆ ⊢ τ ′ wf , and tr (τ ′ ) = r then
∆, ∆′ ; Γ[τ ′ /α] ⊢ e[τ ′ /α] : τ [τ ′ /α].
Proof: The proof is a straight forward induction over the derivation
of ∆, α, ∆′ ; Γ ⊢ e : τ . It uses Lemma 2 in the case of the rule for
application.
With all these lemmas we can prove Type Preservation and
Progress.

k

e1 = (v1 i [τ ] v2 j )
v1 = hρ′ , fix f [α](x:τ1′ ):τ2′ .e′ i
k
e2 = ρ′′ (e′ [τ /α])
′′
′
′
ρ = ρ , f :τ = v1 i , x:τ1′ [τ /α] = v2 j
i
τ ′ = (∀α.τ1′ → τ2′ )

Proof: Assume that ⊢ (ρ, e1 ) : τ1 and (ρ, e1 ) 7−→ (ρ, e2 ). We will
show by induction on the derivation of the latter that ⊢ (ρ, e2 ) : τ2
and ⊢ τ1 = τ2 for some τ2 . By the typing rules, ⊢ ρ : Γ and
∅; Γ ⊢ e1 : τ1 for some Γ. By the typing rules, we just need to
show that ∅; Γ ⊢ e2 : τ2 and ⊢ τ1 = τ2 for some τ2 . Consider the
cases, in the same rule as the figure, for the last rule used to derive
the reduction:

for some ρ′ , f , α, x, τ1′ , τ2′ , e′ , i, v2 , j, and k. Unpacking the
typing judgement, which can only be derived in one way, ∅; Γ ⊢
v1 i : τ ′ (1), ⊢ ρ′ : Γ′ (2), ∅ ⊢ τ ′ wf (12), α; Γ′ , f :τ ′ , x:τ1′ ⊢
e′ : τ2′ (3), τ1 = τ2′ [τ /α] (4), ∅; Γ ⊢ v2 j : τ1′′ (5), ⊢
τ1′ [τ /α] = τ1′′ (6), ∅ ⊢ τ wf , and tr (τ ) = r for some
Γ′ and τ2′′ . By (1) and Lemma 7, ∅; ∅ ⊢ v1 i : τ ′ (7). By
Lemma 3, ⊢ τ ′ = τ ′ (8). By (5) and Lemma 7, ∅; ∅ ⊢
v2 j : τ2′′ (9). By (2), (7), (8), (9), and (6), the typing rules
give ⊢ ρ′′ : Γ′ , f :τ ′ , x:τ1′ [τ /α] (10). By (3) and Lemma 8,
∅; (Γ′ , f :τ ′ , x:τ1′ )[τ /α] ⊢ e′ [τ /α] : τ2′ [τ /α] (11). By (2)
and (12), by inspection of the typing rules, Γ′ [τ /α] = Γ′
and τ ′ [τ /α] = τ ′ . Thus, ∅; Γ′ , f :τ ′ , x:τ1′ [τ /α] ⊢ e′ [τ /α] :
τ2′ [τ /α] (13). By (10) and (13), the typing rules give ∅; Γ ⊢

7

2018/2/19

Lemma 9 (Type Preservation)
If ⊢ M1 : τ1 and M1 7−→ M2 then ⊢ M2 : τ2 and ⊢ τ1 = τ2 for
some τ2 .

k

ρ′′ (e′ [τ /α]) : τ2′ [τ /α] (14). By (4), the result follows by
setting τ2 = τ2′ [τ /α].

induction hypothesis, either e1 is a value or reduces, and e2 is a
value or reduces. There are three subcases:

• (Box argument) In this case, e1 = (boxτ e)i , e2 = (boxτ e′ )i ,

Case 1, e1 reduces: In this case there is e′1 such that
(ρ, e1 ) 7−→ (ρ, e′1 ). Then by the application function rule,
i
(ρ, e) 7−→ (ρ, (e′1 [τ ′ ] e2 ) ), as required.

′

′

and (ρ, e) 7−→ (ρ, e ) for some τ , e, i, and e . The typing
judgement can only be derived with one rule and it requires that
∅ ⊢ τ wf , ∅; Γ ⊢ e : τ ′ , ⊢ τ = τ ′ and τ1 = box(τ )i for some
τ ′ . By the induction hypothesis, ∅; Γ ⊢ e′ : τ ′′ and ⊢ τ ′ = τ ′′
for some τ ′′ . By Lemma 3, ⊢ τ = τ ′′ . By the typing rules,
∅; Γ ⊢ e2 : box(τ )i . By Lemma 3, ⊢ τ1 = τ1 , so the result
follows by setting τ2 = τ1 .
• (Unbox argument) In this case, e1 = (unbox e)i , e2 =
i

(unbox e′ ) , and (ρ, e) 7−→ (ρ, e′ ) for some e, i, and e′ . The
typing judgement can only be derived with one rule and it requires that ∅; Γ ⊢ e : box(τ1 )j for some j. By the induction
hypothesis, ∅; Γ ⊢ e′ : τ ′ and ⊢ box(τ1 )j = τ ′ for some τ ′ .
The latter can only be derived with one rule and it requires that
k
τ ′ = box(τ ′′ ) and ⊢ τ1 = τ ′′ for some τ ′′ and k. By the
typing rules, ∅; Γ ⊢ e2 : τ ′′ , so the result follows by setting
τ2 = τ ′′ .
j k

• (Unbox beta) In this case, e1 = (unbox hv i :τ i ) and e2 = v i

for some τ , v, i, j, and k. The typing judgement can only be
j
derived with one rule and it requires that ∅; Γ ⊢ hv i :τ i :
l
box(τ1 ) for some l. The latter can only be derived with one
rule and it requires τ = τ1 , ∅; Γ ⊢ v i : τ ′ , and ⊢ τ = τ ′ . So
the result follows by setting τ2 = τ ′ .
• (Frame step) In this case, e1 = ρ′ (e)i , e2 = ρ′ (e′ )i , and

(ρ′ , e) 7−→ (ρ′ , e′ ) for some ρ′ , e, i, and e′ . The typing judgement can only be derived with one rule and it requires that
ρ′ ⊢ Γ′ : and ∅; Γ′ ⊢ e : τ1 for some Γ′ . By the induction
hypothesis, ∅; Γ′ ⊢ e′ : τ ′ and ⊢ τ1 = τ ′ for some τ ′ . By
the typing rules, ∅; Γ ⊢ e2 : τ ′ , so the result follows by setting
τ2 = τ ′ .
j

• (Frame return) In this case, e1 = ρ′ (v i ) and e2 = v i for some

ρ′ , v, i, and j. The typing judgement can only be derived with
one rule and it requires that ρ′ ⊢ Γ′ : and ∅; Γ′ ⊢ v i : τ1 . By
Lemma 7, ∅; Γ ⊢ v i : τ1 . By Lemma 3, ⊢ τ1 = τ1 , so the result
follows by setting τ2 = τ1 .

Case 2, e1 is a value and e2 reduces: In this case there is
e′2 such that (ρ, e2 ) 7−→ (ρ, e′2 ). Then by the application
i
function rule, (ρ, e) 7−→ (ρ, (e1 [τ ′ ] e′2 ) ), as required.
Case 3, e1 = v1 k and e2 = v2 l for some v1 , k, v2 , and l:
There is only one typing rule to derive (1) and it requires that
v1 have the form hρ′ , fix f [α](x:τ1 ):τ3 .e′ i for some ρ′ , f ,
x, and e′ . Let t be the traceability of v2 . By Lemma 6 and
(2), tr (τ2 ) = t. By Lemma 4 and (3), tr (τ1 [τ ′ /α]) = t.
Then by the application beta rule:
(ρ, e) 7−→
i
(ρ, (ρ′ , f :τ ′ = v1 k , x:τ1 [τ ′ /α] = v2 l )(e′ [τ ′ /α]) )
where τ ′ = (∀α.τ1 → τ3 )k , as required.
• (Box expression) In this case, e = (boxτ ′ e′ )i for some τ ′ ,
i

e′ , and i. The typing rule requires that τ = box(τ ′ ) , ∅; Γ ⊢
e′ : τ ′′ (1), and ⊢ τ ′ = τ ′′ (2) for some τ ′′ . By the induction
hypothesis, either e′ is a value or reduces:
If e′ = vt j then by Lemma 6 and (1), tr (τ ′′ ) = t. By (2)
and Lemma 4, tr (τ ′ ) = t. So by the box reduction rule,
i
(ρ, e) 7−→ (ρ, hvt′ j :τ ′ i ), as required.
i

If (ρ, e′ ) 7−→ (ρ, e′′ ) then (ρ, e) 7−→ (ρ, (boxτ ′ e′′ ) ), as
required.
• (Unbox) In this case, e = (unbox e′ )i for some e′ and i. The

typing rule requires that ∅; Γ ⊢ e′ : box(τ )j (1) for some j. By
the induction hypothesis, e′ is a value or reduces:
If e′ = v k then (1) can be derived by only one rule and
l
it requires that v = hv ′ :τ ′ i for some v ′ , l, and τ ′ . By the
l
unbox beta rule, (ρ, e) 7−→ (ρ, v ′ ), as required.
If (ρ, e′ ) 7−→ (ρ, e′′ ) then by the unbox argument rule,
i
(ρ, e) 7−→ (ρ, (unbox e′′ ) ), as required.
• (Frame) In this case, e = ρ′ (e′ )i for some ρ′ , e′ , and i. The

Lemma 10 (Progress)
If ⊢ M : τ then either M has the form (ρ, v i ) or M 7−→ M ′ for
some M ′ .
Proof: The result follows from: If ⊢ ρ : Γ and ∅; Γ ⊢ e : τ then
either e has the form v i or (ρ, e) 7−→ (ρ, e′ ) for some e′ . We will
prove this by induction on the typing derivation for e. Consider
the last rule, in the same order as the figure, used to derive the
judgement:
• (Variable) In this case e = xi and x:τ ∈ Γ. There is only one

rule to derive ⊢ ρ : Γ and it requires that x:τ = v j ∈ ρ and
other conditions for some v and j. Then by the variable rule,
(ρ, e) 7−→ v j , as required.

• (Fix expression) In this case e = (fix f [α](x:τ1 ):τ2 .e′ )i .

Clearly by the fix expression rule:

typing rule requires that ⊢ ρ′ : Γ′ and ∅; Γ′ ⊢ e′ : τ for some
Γ′ . By the induction hypothesis, e′ is a value or reduces:
If e′ = v j then by the frame return rule, (ρ, e) 7−→ (ρ, v j ),
as required.
If (ρ, e′ ) 7−→ (ρ, e′′ ) then by the frame step rule, (ρ, e) 7−→
i
(ρ, ρ′ (e′′ ) ), as required.

• (Constant) In this case e = ci for some c and i and is clearly a

value.
• (Fix value) In this case e = hρ′ , fix f [α](x:τ1 ):τ2 .e′ ii for

some ρ′ , f , x, τ1 , τ2 , e′ and i and is clearly a value.
j

• (Box value) In this case e = hv i :τ ′ i for some τ ′ , v, i, and j

and is clearly a value.
We can also prove that typability implies traceability and thus
typable programs are GC safe and remain so throughout execution.

i

(ρ, e) 7−→ (ρ, hρ, fix f [α](x:τ1 ):τ2 .e′ i )
• (Application) In this case, e = (e1 [τ ′ ] e2 )i . The typing rule

requires that ∅; Γ ⊢ e1 : (∀α.τ1 → τ3 )j (1), ∅; Γ ⊢ e2 : τ2
(2), and ⊢ τ1 [τ ′ /α] = τ2 (3) for some τ1 , j, and τ2 . By the

8

Lemma 11
• If ⊢ M : τ then ⊢ M tr.
• If ⊢ ρ : Γ then ⊢ ρ tr.
• If ∆; Γ ⊢ e : τ then ⊢ e tr.

2018/2/19

• If ∆; Γ ⊢ v i : τ then ⊢v v:tr (τ ).

Proof: The results are proven simultaneously by induction on the
structure of the typing derivation. The cases for the last rule used,
in the same order as the figure, are:
• (Variable) In this case clearly ⊢ e tr.
• (Fix expression) In this case e = (fix f [α](x:τ1 ):τ2 .e′ )i

for some x, α, τ1 , τ2 , e′ , and i. Then by the typing rule,
∆, α; Γ, f :τ, x:τ1 ⊢ e′ : τ2 is a subderivation. By the induction
hypothesis, ⊢ e′ tr. So by the rules for traceability, ⊢ e tr, as
required.

• (Application) In this case e = (e1 [τ ′ ] e2 )i for some e1 , τ ′ , e2 ,

and i. By the typing rule, ∆; Γ ⊢ e1 : τ1 and ∆; Γ ⊢ e2 : τ2
for some τ1 and τ2 . By the induction hypothesis, ⊢ e1 tr and
⊢ e2 tr. By the rules for traceability ⊢ e tr, as required.
• (Box expression) In this case e = (boxτ ′ e′ )i for some τ ′ , e′ ,

and i. By the typing rule, ∆; Γ ⊢ e′ : τ ′′ for some τ ′′ . By
the induction hypothesis, ⊢ e′ tr. By the rules for traceability,
⊢ e′ tr, as required.

• (Unbox) In this case e = (unbox e′ )i for some e′ and i. By

the typing rule, ∆; Γ ⊢ e′ : τ ′ for some τ ′ . By the induction
hypothesis, ⊢ e′ tr. By the rules for traceability, ⊢ e tr, as
required.

• (Frame) In this case, e = ρ(e′ )i for some ρ, e′ , and i. By the

typing rule, ⊢ ρ : Γ′ and ∅; Γ′ ⊢ e′ : τ for some Γ′ . By the
induction hypothesis, ⊢ ρ tr and ⊢ e′ tr. By the rules for
traceability, ⊢ e tr, as required.

• (Constant) In this case e = ci . By the typing rule, τ = Bi and so

clearly tr (τ ) = b. By the rules for traceability, ⊢v c:b, proving
the fourth result. By the rules for traceability again, ⊢ e tr,
proving the third result.
• (Fix value) In this case e = hρ, fix f [α](x:τ1 ):τ2 .e′ ii for

some ρ, f , α, x, τ1 , τ2 , e′ , and i. By the typing rule, ⊢ ρ : Γ′
and α; Γ′ , f :τ, x:τ1 ⊢ e′ : τ2 for some Γ′ . Also by the typing
rules, τ is a function type, so tr (τ ) = r. By the induction
hypothesis, ⊢ ρ tr and ⊢ e′ tr. By the rules for traceability,
⊢v hρ, fix f [α](x:τ1 ):τ2 .e′ i:r, proving the fourth result. By
the rules for traceability again, ⊢ e tr, proving the third result.

grams. There is a vast body of literature on interprocedural analysis and optimization, and it is generally fairly straightforward to
use these approaches to obtain information about what terms flow
to what use sites. This paper is not intended to provide any contribution to the algorithmic side of this body of work, which we
will broadly refer to as flow analysis. Our contribution in this paper
lies in showing how to extend flow analysis to the type level, and
showing that any generic flow analysis so extended can be used to
implement an unboxing optimization that preserves type safety.
In order to do this, we must provide some framework for describing what information a flow analysis must provide. For the
purposes of our unboxing optimization, we are interested in findi
ing (interprocedurally) for every (unbox v j ) operation the set of
(boxτ e)k terms that could possibly reach v. Under appropriate
conditions, we can then eliminate both the box introductions and
the box elimination, thereby improving the program. The core language defined in Section 2 provides labels serving as proxies for
the terms, types, and variables on which they occur – the question
above can therefore be re-stated as finding the set of labels k that
reach the position labeled with j.
More generally, following previous work we begin by defining
an abstract notion of analysis. We say that an analysis is a pair
(C, ̺). Binding environments ̺ simply serve to map variables to
the label of their binding sites. The mappings are, as usual, global
for the program. Consequently, a given environment may not apply
to alpha-variants of a term. We do not require that labels be unique
within a program—as usual however, analyses will be more precise
if this is the case. Variables are also not required to be unique
(since reduction may duplicate terms and hence binding sites).
However, duplicate variable bindings in a program must be labeled
consistently according to ̺ or else no analysis of the program
can be acceptable according to our definition. This can always be
avoided by alpha-varying or relabeling appropriately.
A cache C is a mapping from labels to sets of shapes. Shapes
are given by the grammar:
Shapes:

s

::=

ci | (∀i.j → k)lv | (boxt i)jv |
l
j
Bi | (∀i.j → k)t | (box i)t

Our original motivation for this work was to apply interprocedural
analysis to the problem of eliminating unnecessary boxing in pro-

There are two classes of shapes—term shapes and type shapes.
The idea behind term shapes is that each shape provides a proxy
for a set of terms that might flow to a given location, describing
both the shape of the values that might flow there and the labels of
the sub-components of those values. For example, for an analysis
(C, ̺), ci ∈ C(k) indicates that (according to the analysis) the
constant c, labeled with i, might flow to a location labeled with
k
k. Similarly, if (∀i′ .i → j)v ∈ C(l), then the analysis specifies
that among the values flowing to locations labeled with l might
be functions labeled with k, whose type parameter is labeled with
i′ , parameter type is labeled with i, and whose bodies are labeled
with j. If (boxt k)iv ∈ C(l) then among the values that might flow
to l (according to the analysis) are boxed values labeled with i,
with meta-data t and whose bodies are labeled by some j such that
C(j) ⊆ C(k).
Where term shapes provide a proxy for the set of values that
might flow to a given location, type shapes provide a proxy for
the types of the locations that values might flow through to get to
a given location. For example, for an analysis (C, ̺), Bi ∈ C(k)
indicates that (according to the analysis) objects that reach location
k might flow through a variable or term of type B, labeled with i.
The function type and box type shapes similarly correspond to the
flow of values through locations labeled with function or box types.
It is important to note that the shapes in the cache may not
correspond exactly to the terms in the program, since reduction may
change program terms (e.g. by instantiating variables with values).

9

2018/2/19

j

• (Box value) In this case e = hv i :τ ′ i . By the typing rule,
i

′′

′

′′

∆; Γ ⊢ v : τ and ⊢ τ = τ for some τ ′′ . Also by the
typing rule, τ is a box type, so tr (τ ) = r. By the induction
hypothesis, ⊢v v:tr (τ ′′ ). By Lemma 4, ⊢v v:tr (τ ′ ). By the
rules for traceability, ⊢v hv i :τ ′ i:r, proving the third result. By
the rules for traceability again, ⊢ e tr, as required.
• (Environment) In this case ρ = x1 :τ1 = v1 i1 , . . . , xn :τn =

vn in . By the typing rule, ∅; ∅ ⊢ vj ij : τj′ and ⊢ τj = τj′
for 1 ≤ j ≤ n and some τj′ s. By the induction hypothesis,
⊢v vj :tr (τj′ ) for 1 ≤ j ≤ n. By Lemma 4, tr (τj ) = tr (τj′ )
for 1 ≤ j ≤ n. Thus ⊢v vj :tr (τj ) for 1 ≤ j ≤ n. By the
traceability rules, ⊢ ρ tr, as required.

• (Machine state) In this case M = (ρ, e). By the typing rule,

⊢ ρ : Γ and ∅; Γ ⊢ e : τ for some Γ. By the induction
hypothesis, ⊢ ρ tr and ⊢ e tr. By the rules for traceability,
⊢ M tr, as required.

3. Flow analysis

However, reduction does not change the outer shape and labeling
of values—it is this reduction invariant information that is captured
by shapes.
Clearly, not every choice of analysis pairs is meaningful for program optimization. While in general it is reasonable (indeed, unavoidable) for an analysis to overestimate the set of terms associated with a label, it is unacceptable for an analysis to underestimate
the set of terms that flow to a label—most optimizations will produce incorrect results, since they are designed around the idea that
the analysis is telling them everything that could possibly flow to
them. In order to capture the notion of when an analysis pair gives
a suitable approximation of the flow of values in a program we
follow the general spirit of Nielson et al. [7], and define a notion
of an acceptable analysis. That is, we give a declarative specification that gives sufficient conditions for specifying when a given
analysis does not underestimate the set of terms flowing to a label,
without committing to a particular analysis. We arrange the subsequent meta-theory such that our results apply to any analysis that is
acceptable. In this way, we completely decouple our optimization
from the particulars of how the analysis is computed.
Our acceptable-analysis relation is given in Figures 6 and 7—
the judgement C; ̺ ⊢ (ρ, e) determines that an analysis pair (C, ̺)
is acceptable for a machine state (ρ, e), and similarly for the environment and expression forms of the judgement. We use the notation lbl(e) to denote the outermost label of e: that is, i where e is of
the form mi or v i . The acceptability judgement generally indicates
for each syntactic form what the flow of values is. For example,
in the application rule, the judgment insists that for every function
value that flows to the applicand position, the set of shapes associated with the parameter of that function is a super-set of the set of
shapes associated with the argument of the application; and that the
set of shapes associated with the result of the function is a sub-set
of the set of shapes associated with the application itself.
The judgement C; ̺ ⊢ τ determines that an analysis pair (C, ̺)
is acceptable for a labeled type τ . In particular, if a function flows
to a function type ∀τ1 .τ2 → then the set of values that flow to the
function’s parameter can flow to the argument type τ1 , and the set
of values that can flow from the result of the function can flow to
the result type τ2 . And similarly for box types.
Given this definition, we can show that the acceptability relation
is preserved under reduction. First we show that the cache is only
refined by reduction.

funC (i, j, k, l) boxC (i, j)
funC (i, j, k, l) =
i′
∧ ∀(∀j ′ .k′ → l′ )v ∈ C(i) :
′
C(j) = C(j ) ∧ C(k) ⊆ C(k′ ) ∧ C(l′ ) ⊆ C(l)
i′
∧ ∀(∀j ′ .k′ → l′ )t ∈ C(i) :
′
C(j) = C(j ) ∧ C(k) ⊆ C(k′ ) ∧ C(l′ ) ⊆ C(l)
boxC (i, j) =
i′
∧ ∀(boxt j ′ )v ∈ C(i) : C(j ′ ) ⊆ C(j)
′
i
∧ ∀(box j ′ )t ∈ C(i) : C(j ′ ) ⊆ C(j)
C; ̺ ⊢ e
C(̺(x)) ⊆ C(i)
C; ̺ ⊢ xi
̺(f ) = i ̺(x) = lbl(τ1 ) C; ̺ ⊢ (∀α.τ1 → τ2 )i
C; ̺ ⊢ e (∀̺(α).lbl(τ1 ) → lbl(e))iv ∈ C(i)
C; ̺ ⊢ (fix f [α](x:τ1 ):τ2 .e)i
C; ̺ ⊢ e1 C; ̺ ⊢ τ C; ̺ ⊢ e2
funC (lbl(e1 ), lbl(τ ), lbl(e2 ), i)
C; ̺ ⊢ (e1 [τ ] e2 )i
C; ̺ ⊢ box(τ )i C; ̺ ⊢ e
(boxtr (τ ) j)iv ∈ C(i) C(lbl(e)) ⊆ C(j)
C; ̺ ⊢ (boxτ e)i
C; ̺ ⊢ e boxC (lbl(e), i)
C; ̺ ⊢ (unbox e)i
C; ̺ ⊢ ρ

• (Variable instantiation.) In this case, e1 = xk , e2 = v j , and

x:τ = v j ∈ ρ. The assumption C; ̺ ⊢ ρ requires that C(j) ⊆
C(lbl(τ )) and ̺(x) = lbl(τ ). The assumption C; ̺ ⊢ e1
requires that C(̺(x)) ⊆ C(k). Thus C(j) ⊆ C(k). Clearly,
lbl(e1 ) = k and lbl(e2 ) = j and the result follows.

• (Fix introduction.) In this case, clearly lbl(e1 ) = lbl(e2 ) and

the result immediately follows.

C(lbl(e)) ⊆ C(i)

C; ̺ ⊢ ρ(e)i

Lemma 12 (Cache refinement under reduction)
If C; ̺ ⊢ ρ, C; ̺ ⊢ e1 , and (ρ, e1 ) 7−→ (ρ, e2 ) then C(lbl(e1 )) ⊇
C(lbl(e2 )).
Proof: The proof is by induction on the derivation of (ρ, e1 ) 7−→
(ρ, e2 ). Consider the cases for the last rule used to it (the cases are
in the same order as in the figure):

C; ̺ ⊢ e

C; ̺ ⊢ Bi

ci ∈ C(i)

C; ̺ ⊢ ci
̺(x) = lbl(τ1 ) C; ̺ ⊢ (∀α.τ1 → τ2 )i
C; ̺ ⊢ ρ C; ̺ ⊢ e
(∀̺(α).lbl(τ1 ) → lbl(e))iv ∈ C(i)

̺(f ) = i

C; ̺ ⊢ hρ, fix f [α](x:τ1 ):τ2 .eii
C; ̺ ⊢ box(τ )i C; ̺ ⊢ v j
(boxtr (τ ) k)iv ∈ C(i) C(j) ⊆ C(k)
C; ̺ ⊢ hv j :τ i

i

• (Box introduction.) In this case, clearly lbl(e1 ) = lbl(e2 ) and

the result immediately follows.

Figure 6. Acceptable Analysis, Expressions

• (Application left.) In this case, clearly lbl(e1 ) = lbl(e2 ) and

the result immediately follows.
• (Application right.) In this case, clearly lbl(e1 ) = lbl(e2 ) and

the result immediately follows.

10

2018/2/19

Lemma 13
If C; ̺ ⊢ τ and C(lbl(τ )) = C(̺(α)) then:

C; ̺ ⊢ τ
C(̺(α)) = C(i)

•
•
•
•

i

C; ̺ ⊢ α

Bj ∈ C(i)
C; ̺ ⊢ Bi

Proof: The proof is by induction on the derviation of the C; ̺ ⊢ τ ′
and C; ̺ ⊢ e. Consider the cases for the rules used to derive it (in
the same order as in the figures):

C; ̺ ⊢ τ1 C; ̺ ⊢ τ2
(∀̺(α).lbl(τ1 ) → lbl(τ2 ))jt ∈ C(i)
funC (i, ̺(α), lbl(τ1 ), lbl(τ2 ))

• The cases for expressions are straight forward.
• (Type variable) In this case τ ′ = β i . If β 6= α then τ ′ [τ /α] =

C; ̺ ⊢ (∀α.τ1 → τ2 )i
C; ̺ ⊢ τ

(box lbl(τ ))jt ∈ C(i)

If C; ̺ ⊢ τ ′ then C; ̺ ⊢ τ ′ [τ /α].
If C; ̺ ⊢ Γ then C; ̺ ⊢ Γ[τ /α].
If C; ̺ ⊢ e then C; ̺ ⊢ e[τ /α].
If C; ̺ ⊢ ρ then C; ̺ ⊢ ρ[τ /α].

τ ′ and the result is immediate. Otherwise, by the rules for
acceptability, C(̺(α)) = C(i). If τ = σ j then τ ′ [τ /α] = σ i .
Consider the cases for σ:

boxC (i, lbl(τ ))

i

C; ̺ ⊢ box(τ )

Subcase 1, σ = α′ : Then by the rules for acceptability,
C(̺(α′ )) = C(j). Since C(j) = C(̺(α)) = C(i),
i
C(̺(α′ )) = C(i), and thus C; ̺ ⊢ α′ , as required.

∀1 ≤ j ≤ n : ̺(xj ) = lbl(τj ) ∧ C; ̺ ⊢ τj

Subcase 2, σ = ∀α′ .τ1 → τ2 : Since C; ̺ ⊢ τ , the rules
require:

C; ̺ ⊢ Γ

C; ̺ ⊢ x1 :τ1 , . . . , xn :τn

C; ̺ ⊢ τ1
C; ̺ ⊢ τ2
k
(∀̺(α′ ).lbl(τ1 ) → lbl(τ2 ))t ∈ C(j)
′
funC (j, ̺(α ), lbl(τ1 ), lbl(τ2 ))

C; ̺ ⊢ ρ
C; ̺ ⊢ x1 :τ1 , . . . , xn :τn
∀1 ≤ j ≤ n : C(ij ) ⊆ C(lbl(τj )) ∧ C; ̺ ⊢ vk ik

(1)
(2)
(3)
(4)

By (3) and C(j) = C(i):

C; ̺ ⊢ x1 :τ1 = v1 i1 , . . . , xn :τn = vn in

k

(∀̺(α′ ).lbl(τ1 ) → lbl(τ2 ))t ∈ C(i)

C; ̺ ⊢ M

(5)

By (4) and C(j) = C(i):
C; ̺ ⊢ ρ C; ̺ ⊢ e

funC (i, ̺(α′ ), lbl(τ1 ), lbl(τ2 )) (6)

C; ̺ ⊢ (ρ, e)

By (1), (2), (5), and (6), by the rules for acceptability,
C; ̺ ⊢ σ i .

Figure 7. Acceptable Analysis, Other Constructs

Subcase 3, σ = box(τ ′′ ): Since C; ̺ ⊢ τ , the rules require:
C; ̺ ⊢ τ ′′
k
(box lbl(τ ′′ ))t ∈ C(j)
boxC (j, lbl(τ ′′ ))

• (Application beta.) In this case, clearly lbl(e1 ) = lbl(e2 ) and

the result immediately follows.
• (Under box.) In this case, clearly lbl(e1 ) = lbl(e2 ) and the

k

By (2) and C(j) = C(i), (box lbl(τ ′′ ))t ∈ C(i) (4). By
(3) and C(j) = C(i), boxC (i, lbl(τ ′′ )) (5). By (1), (4), and
(5), by the rules for acceptability, C; ̺ ⊢ σ i , as required.

result immediately follows.
• (Under unbox.) In this case, clearly lbl(e1 ) = lbl(e2 ) and the

result immediately follows.
j k

i

• (Base type) In this case τ ′ [τ /α] = τ and the result is immedii

• (Unbox beta.) In this case, e1 = (unbox hv :τ i ) and e2 = v .

The first hypothesis can be derived only by one rule and it
j
requires that C; ̺ ⊢ hv i :τ i (1), and boxC (j, k) (2). Judgement
1 can only be derived by one rule and it requires that C; ̺ ⊢ v i
j
(4), (boxtr (τ ) i′′ )v ∈ C(j) (5) for some i′′ , and C(i) ⊆ C(i′′ )
(6). Instantiating Fact 2 with Fact 5 we get that C(i′′ ) ⊆ C(k)
(7). Combining Facts 6 and 7, C(i) ⊆ C(k), as we are required
to prove.
• (Under frame.) In this case, clearly lbl(e1 ) = lbl(e2 ) and the

result immediately follows.
• (Frame return.) In this case, e1 = ρ′ (v i )

j

(1)
(2)
(3)

i

and e2 = v .
The assumption C; ̺ ⊢ e1 requires that C(i) ⊆ C(j). Since
lbl(e1 ) = j and lbl(e2 ) = i, the result is immediate.

Next we show a type substitution lemma for acceptability.

ate.
• (Function type) In this case τ ′ = (∀α′ .τ1 → τ2 )i . The rules for

acceptability require:
C; ̺ ⊢ τ1
C; ̺ ⊢ τ2
k
(∀̺(α′ ).lbl(τ1 ) → lbl(τ2 ))t ∈ C(i)
funC (i, ̺(α′ ), lbl(τ1 ), lbl(τ2 ))

(1)
(2)
(3)
(4)

By (1), (2), and the induction hypothesis:
C; ̺ ⊢ τ1 [τ /α]
C; ̺ ⊢ τ2 [τ /α]

(5)
(6)

Since lbl(τ1 [τ /α]) = lbl(τ1 ) and lbl(τ1 [τ /α]) = lbl(τ1 ):
k

(∀̺(α′ ).lbl(τ1 [τ /α]) → lbl(τ2 [τ /α]))t ∈ C(i)
funC (i, ̺(α′ ), lbl(τ1 [τ /α]), lbl(τ2 [τ /α]))

(7)
(8)

Since lbl(τ ′ [τ /α]) = i, by (5), (6), (7), and (8), C; ̺ ⊢
τ ′ [τ /α], as required.

11

2018/2/19

• (Box type) In this case, τ ′ = box(τ ′′ )i . The rules for accept-

ability require:
C; ̺ ⊢ τ ′′
k
(box lbl(τ ′′ ))t ∈ C(i)
boxC (i, lbl(τ ′′ ))

(1)
(2)
(3)

By (1) and the induction hypothesis:
C; ̺ ⊢ τ ′′ [τ /α]

(2), and funC (j, lbl(τ ), lbl(e2 ), i) (3). By the induction hypothesis and Judgement 1, C; ̺ ⊢ e′2 (4). By Lemma 12,
C(lbl(e′2 )) ⊆ C(lbl(e2 )) (5). Combining Facts 3 and 5,
funC (j, lbl(τ ), lbl(e′2 ), i) (6). Combining Facts 1, 7, 4, and
6, and using the rules for acceptable analysis, we see that
i
C; ̺ ⊢ (v j [τ ] e′2 ) , as we are required to prove.
• In this case:

(4)
l

e = (v1 j [τ ] v2 k )
v1 = hρ′ , fix f [α](x:τ1 ):τ2 .e′′ i
l
e′ = ρ′′ (e′′ [τ /α])
′′
′
′
ρ = ρ , f :τ = v1 j , x:τ1 [τ /α] = v2 k
τ ′ = (∀α.τ1 → τ2 )j

Since lbl(τ ′′ [τ /α]) = lbl(τ ′′ ):
k

(box lbl(τ ′′ [τ /α]))t ∈ C(i)
boxC (i, lbl(τ ′′ [τ /α]))

(5)
(6)

Since lbl(τ ′ [τ /α]) = i, by (4), (5), and (6), C; ̺ ⊢ τ ′ [τ /α], as
required.
• The cases for type and value environments are straight forward.

With these lemmas we can prove that reduction preserves acceptability of the flow analysis.
Lemma 14 (Preservation of acceptability under reduction)
If C; ̺ ⊢ M and M 7−→ M ′ then C; ̺ ⊢ M ′ .
Proof: If C; ̺ ⊢ (ρ, e) then C; ̺ ⊢ ρ and C; ̺ ⊢ e. If (ρ, e) 7−→
(ρ, e′ ) then the result follows if we show that C; ̺ ⊢ e′ . The proof
of the latter is by induction on the derivation of (ρ, e) 7−→ (ρ, e′ ).
Consider the cases for the last rule used to derive it (the cases are
in the same order as in the figure):
• In this case e = xk , e′ = v j , and x:τ = v j ∈ ρ. The

assumption C; ̺ ⊢ ρ requires that C; ̺ ⊢ v j , which is what
we need to prove.
′′ j

• In this case e = (fix f [α](x:τ1 ):τ2 .e ) for some f , α, x,
j

τ1 , τ2 , e′′ , and j, and e′ = hρ, fix f [α](x:τ1 ):τ2 .e′′ i . Let
i = lbl(τ1 ). The first hypothesis can only be derived by one
rule and it requires that ̺(f ) = j, ̺(x) = i, C; ̺ ⊢ τ where
j
τ = (∀α.τ1 → τ2 )j , C; ̺ ⊢ e′′ , and (∀̺(α).i → lbl(e′′ ))v ∈
C(j). Then, and noting C; ̺ ⊢ ρ by assumption, by the rules
j
for acceptable analysis, C; ̺ ⊢ hρ, fix f [α](x:τ1 ):τ2 .e′′ i , as
we are required to prove.
• In this case e = (boxτ v i )

j

for some τ , v, i, and j, and
j
e′ = hv i :τ i . The first hypothesis can only be derived by
one rule and it requires that C; ̺ ⊢ box(τ )j , C; ̺ ⊢ v i ,
(boxtr (τ ) k)jv ∈ C(j) for some k, and C(i) ⊆ C(k). Then
j
by the rules for acceptable analysis, C; ̺ ⊢ hv i :τ i , as we are
required to prove.

• In this case e = (e1 [τ ] e2 )i for some e1 , τ , e2 , and i,
i

e′ = (e′1 [τ ] e2 ) , and (ρ, e1 ) 7−→ (ρ, e′1 ) is a subderivation.
The first hypothesis can only be derived by one rule and it
requires that C; ̺ ⊢ e1 (1), C; ̺ ⊢ τ (7), C; ̺ ⊢ e2 (2),
and funC (lbl(e1 ), lbl(τ ), lbl(e2 ), i) (3). By the induction hypothesis and Judgement 1, C; ̺ ⊢ e′1 (4). By Lemma 12,
C(lbl(e′1 )) ⊆ C(lbl(e1 )) (5). Combining Facts 3 and 5,
funC (lbl(e′1 ), lbl(τ ), lbl(e2 ), i) (6). Combining Facts 4, 7, 2,
and 6, and using the rules for acceptable analysis, we see that
i
C; ̺ ⊢ (e′1 [τ ] e2 ) , as we are required to prove.

for some ρ′ , f , α, x, τ1 , τ2 , e′′ , j, τ , v2 , k, and l. The first
hypothesis can only be derived by one rule and it requires
that C; ̺ ⊢ v1 j (1), C; ̺ ⊢ τ (2), C; ̺ ⊢ v2 k (3), and
funC (j, lbl(τ ), k, l) (4). Let i = lbl(τ1 ). Judgement 1 can
only be derived by one rule and it requires that ̺(f ) = j
(5), ̺(x) = i (6), C; ̺ ⊢ τ ′ (7), C; ̺ ⊢ e′′ (8), and
j
(∀i.̺(α) → lbl(e′′ ))v ∈ C(j) (9). Instantiating Fact 4 with
Fact 9, C(lbl(τ )) = C(̺(α)) (10), C(k) ⊆ C(i) (11), and
C(lbl(e′′ )) ⊆ C(l) (12). Judgement 7 requires that C; ̺ ⊢ τ1
(13). By (13), (2), and (10), by Lemma 13, C; ̺ ⊢ τ1 [τ /α] (14).
Since C; ̺ ⊢ ρ, (5), (7), C(j) ⊆ C(j), (1), lbl(τ1 [τ /α]) =
lbl(τ1 ) = i and (6), (14), (11), and (3), we can derive C; ̺ ⊢ ρ′′
(15). By (13), (2), and (10), by Lemma 13, C; ̺ ⊢ e′′ [τ /α]
(16). By (15), (16), and lbl(e′′ [τ /α]) = lbl(e′′ ) and (12), we
can derive C; ̺ ⊢ e′ , as required.
• In this case e = (boxτ e1 )i for some t, e1 , and i, e′ =

(boxτ e2 )i for some e2 , and (ρ, e1 ) 7−→ (ρ, e2 ) is a subderivation. The first hypothesis can only be derived by one rule and it
requires that C; ̺ ⊢ box(τ )i (7), C; ̺ ⊢ e1 (1), (boxtr (τ ) j)iv ∈
C(i) (2) for some j, and C(lbl(e1 )) ⊆ C(j) (3). By the induction hypothesis and Judgement 1, C; ̺ ⊢ e2 (4). By Lemma 12,
C(lbl(e2 )) ⊆ C(lbl(e1 )) (5). Combining Facts 3 and 5 gives
C(lbl(e2 )) ⊆ C(j) (6). Then by Facts 7, 4, 2, and 6, and using
the rules for acceptable analysis, C; ̺ ⊢ (boxτ e2 )i , as we are
required to prove.

• In this case e = (unbox e1 )i for some e1 and i, e′ =

(unbox e2 )i for some e2 , and (ρ, e1 ) 7−→ (ρ, e2 ) is a subderivation. The first hypothesis can only be derived by one rule
and it requires that C; ̺ ⊢ e1 (1) and boxC (lbl(e1 ), i) (2). By
Judgement (1) and the induction hypothesis, C; ̺ ⊢ e2 (3). By
Lemma 12, C(lbl(e2 )) ⊆ C(lbl(e1 )) (4). Combining Facts 4
and 2, boxC (lbl(e2 ), i) (5). Combining Facts 3 and 5, by the
rules for acceptable analysis, C; ̺ ⊢ (unbox e2 )i , as we are
required to prove.
j k

• In this case e = (unbox hv i :τ i ) for some τ , v, i, j, and k,
′

i

and e = v . The first hypothesis can only be derived by one
j
rule and it requires that C; ̺ ⊢ hv i :τ i , which in turn can only
be derived by one rule that requires that C; ̺ ⊢ v i , as we are
required to prove.
• In this case e = ρ′ (e′′ )i , e′ = ρ′ (e′′′ )i , and (ρ′ , e′′ ) 7−→

e = (v [τ ]
and (ρ, e2 ) 7−→ (ρ, e′2 ) is a subderivation. The first hypothesis can only be derived by one rule
and it requires that C; ̺ ⊢ v j (1), C; ̺ ⊢ τ (7), C; ̺ ⊢ e2

(ρ′ , e′′′ ) is a subderivation. Assumption C; ̺ ⊢ e requires that
C; ̺ ⊢ ρ′ (1), C; ̺ ⊢ e′′ (2), and C(lbl(e′′ )) ⊆ C(i) (3).
By (1), (2), and the induction hypothesis, C; ̺ ⊢ e′′′ (4). By
Lemma 12, C(lbl(e′′′ )) ⊆ C(lbl(e′′ )) (5). Combining (3) and
(5), C(lbl(e′′′ )) ⊆ C(i) (6). Using (1), (4), and (6) we derive
i
C; ̺ ⊢ ρ′ (e′′′ ) , as required.

12

2018/2/19

i

• In this case e = (v j [τ ] e2 ) for some v, j, τ , e2 , and i,
′

j

i
e′2 ) ,

j

• In this case e = ρ′ (v i ) and e′ = v i . The assumption C; ̺ ⊢ e
i

unpacks to requiring that C; ̺ ⊢ v , as required.

• (Fix value) In this case, e = hρ, fix f [α](x:τ1 ):τ2 .e′ ii , τ =

(∀α.τ1 → τ2 )i . The first part holds as lbl(e) = lbl(τ ). The
second part is required by C; ̺ ⊢ e.
i

• (Box value) In this case e = hv j :τ ′ i and τ = box(τ ′ )i . The

first part holds as lbl(e) = lbl(τ ). The second part is required
by C; ̺ ⊢ e.

Lemma 15 (Many-step reduction preserves acceptability)
If C; ̺ ⊢ M and M 7−→∗ M ′ then C; ̺ ⊢ M ′ .
Proof: The proof is by a straightforward induction on the length
of the reduction sequence and Lemma 14.
We can also show an important connection between typing and
acceptable flow analysis—namely that the cache of an expression’s
type is a contained in the cache of that expression.
Lemma 16
If ∆; Γ ⊢ e : τ , C; ̺ ⊢ Γ, and C; ̺ ⊢ e then C(lbl(τ )) ⊆
C(lbl(e)) and C; ̺ ⊢ τ .
Proof: The proof is by induction on the derivation of Γ ⊢ e : τ .
Consider the cases for the last rule used (in same order as figure):
• (Variable) In this case e = xi and x:τ ∈ Γ. By the rules for

acceptable analysis, ̺(x) = lbl(τ ) (1), C; ̺ ⊢ τ (2), and
C(̺(x)) ⊆ C(i) (3). By (1) and (3), C(lbl(τ )) ⊆ C(i) (4).
The result is (4) and (2).
• (Fix expression) In this case, e = (fix f [α](x:τ1 ):τ2 .e′ )i

and τ = (∀α.τ1 → τ2 )i . The first part is immediate since
lbl(τ ) = lbl(e). The second part is required by C; ̺ ⊢ e.

• (Application) In this case:
i

e = (e1 [τ ′ ] e2 )
∆; Γ ⊢ e1 : (∀α.τ1 → τ3 )j
τ = τ3 [τ ′ /α]

(1)

By the rules for acceptability, C; ̺ ⊢ e1 (2), C; ̺ ⊢ τ ′ (3),
C; ̺ ⊢ e2 , and funC (lbl(e1 ), lbl(τ ′ ), lbl(e2 ), i) (4). By (1),
(2), and the induction hypothesis, C(j) ⊆ C(lbl(e1 )) (5) and
C; ̺ ⊢ (∀α.τ1 → τ3 )j (6). By (6) and the rules for acceptability, C; ̺ ⊢ τ3 (7) and (∀̺(α).lbl(τ1 ) → lbl(τ3 ))kt ∈ C(j)
(8). By (5), instantiating (4) with (8), C(lbl(τ ′ )) = C(̺(α))
(9) and C(lbl(τ3 )) ⊆ C(i), so since lbl(τ ) = lbl(τ3 ),
C(lbl(τ )) ⊆ C(i) (10). By (3), (7), and (9), C; ̺ ⊢ τ3 [τ ′ /α]
(11). The result is (10) and (11).
• (Box expression) In this case e = (boxτ ′ e′ )i and τ

=
i
box(τ ′ ) . The first part holds as lbl(e) = lbl(τ ). The second
part is required by C; ̺ ⊢ e.

• (Unbox) In this case e = (unbox e′ )i and ∆; Γ ⊢ e′ : box(τ )j

(1) is a subderivation. By the rules for acceptability, C; ̺ ⊢
e′ (2) and boxC (lbl(e′ ), i) (3). By (1), (2), and the induction hypothesis, C(j) ⊆ C(lbl(e′ )) (4) and C; ̺ ⊢ box(τ )j
(5). By (5) and the rules for acceptability, C; ̺ ⊢ τ (6) and
(box lbl(τ ))kt ∈ C(j) (7). By (4), instantiating (3) with (7),
C(lbl(τ )) ⊆ C(i) (8). The result is (8) and (6).
• (Frame) In this case e = ρ(e′ )i , ⊢ ρ : Γ′ (1), and ∅; Γ′ ⊢ e′ : τ

(2). By the rules for acceptability, C; ̺ ⊢ ρ (3), C; ̺ ⊢ e′ (4),
and C(lbl(e′ )) ⊆ C(i) (5). By (1), (3), the rules for typing,
and the rules for acceptability, C; ̺ ⊢ Γ′ (6). By (6), (2), (4),
and the induction hypothesis, C(lbl(τ )) ⊆ C(lbl(e′ )) (7) and
C; ̺ ⊢ τ (8). By (7) and (5), C(lbl(τ )) ⊆ C(i) (9). The result
is (9) and (8).

4. Unboxing
The goal of the unboxing optimization is to use the information provided by a flow analysis to replace a boxed object with the contents
of the box. Doing so may change the traceability, since the object in
the box may not be a GC-managed reference. Moreover, the object
in the box may itself be a candidate for unboxing; consequently,
determining the traceability of boxed objects depends on exactly
which objects are unboxed. Function parameters may be instantiated with objects from multiple different definition sites, some of
which may be unboxed and some of which may not.
Consider again the first example from Section 2, written out
with explicit type information and labels:
let
3 4
1
8
fix f [](x:box(B0 ) ):box(box(B2 ) ) .(boxbox(B5 )6 x7 )
10 11
z1 = (boxB9 3 )
13
z2 = f [](z1 12 )
16 17
in (unbox (unbox z2 15 ) )
It is fairly easy to see that this program is unboxable. The binding
site for x is only reached by the term labeled with 11 (the outer
box introduction), and hence there should be no problems with
changing its type annotation. Each box elimination is reached only
by a single box introduction, and hence the box/unbox pairs in this
program should be eliminable, yielding an optimized program:
let
fix f [](x:B0 ):B2 .x7
z1 = 310
13
z2 = f [](z1 12 )
15
in z2
Notice that in order to rewrite the program, we have had to change
the types of both f and x, since we have eliminated the box
introductions on the argument and in the body of f . The change
in type of x has changed its traceability from r to b. If we choose
(perhaps because of limitations on the precision of the analysis, or
perhaps because of other constraints) to only eliminate the outer
box/unbox pair, then we must similarly adjust types on the the
remaining box introduction (labeled with 8).
let
3
8
fix f [](x:B0 ):box(B2 ) .(boxB5 x7 )
10
z1 = 3
13
z2 = f [](z1 12 )
15 16
in (unbox z2 )

clearly holds as lbl(e) = lbl(τ ). The second part is required
by C; ̺ ⊢ e.

Clearly then, to optimize these programs in a type preserving
fashion, we must rewrite types along with the terms in the program. In the rest of this section, we first develop a framework for
specifying an unboxing assignment regardless of any correctness
concerns, and then separately define a judgement specifying when
such an assignment is a reasonable one.

13

2018/2/19

• (Constant) In this case e = ci and τ = Bi . The first part

ficient conditions for ensuring correctness of an unboxing, without
specifying a particular method of choosing such an unboxing. By
using analyses of different precisions or choosing different optimization strategies we may end up with quite different choices of
unboxings; however, so long as they satisfy our notion of acceptability we can be sure that they will preserve correctness.
Informally, a choice of an unboxing set is reasonable if it meets
two criteria. Firstly, it must make uniform choices in the sense
that if a box introduction is eliminated, then all of the types and
elimination forms to which it flows must also be unboxed, and
vice versa. Secondly, we must ensure that types remain consistent
with their uses in polymorphic instantiations, since we do not allow
polymorphism over base types.

⇃τ ⇂Υ
⇃αi ⇂Υ
⇃Bi ⇂Υ
⇃(∀α.τ1 → τ2 )i ⇂Υ
⇃box(τ )i ⇂Υ
⇃box(τ )i ⇂Υ

=
=
=
=
=

αi
Bi
(∀α.⇃τ1 ⇂Υ → ⇃τ2 ⇂Υ )i
⇃τ ⇂Υ
box(⇃τ ⇂Υ )i

i∈Υ
i∈
/Υ

⇃Γ⇂Υ
⇃x1 :τ1 , . . . , xn :τn ⇂Υ = x1 :⇃τ1 ⇂Υ , . . . , xn :⇃τn ⇂Υ
⇃e⇂Υ

Υ

⇃xi ⇂Υ
⇃mi ⇂Υ

=
=
i

⇃(e1 [τ ] e2 ) ⇂Υ
⇃(boxτ e)i ⇂Υ
⇃(unbox e)i ⇂Υ
i

⇃ρ(e) ⇂Υ
⇃ci ⇂Υ
⇃v i ⇂Υ
i

⇃hv j :τ i ⇂Υ

=
=
=
=
=
=
=
=
=
=

xi
(fix f [α](x:⇃τ1 ⇂Υ ):⇃τ2 ⇂Υ .⇃e⇂Υ )i
where m = fix f [α](x:τ1 ):τ2 .e
(⇃e1 ⇂Υ [⇃τ ⇂Υ ] ⇃e2 ⇂Υ )i
⇃e⇂Υ
i∈Υ
(box⇃τ ⇂Υ ⇃e⇂Υ )i
i∈
/Υ
⇃e⇂Υ
lbl(e) ∈ Υ
(unbox ⇃e⇂Υ )i
lbl(e) ∈
/Υ
⇃ρ⇂Υ (⇃e⇂Υ )i
ci
h⇃ρ⇂Υ , fix f [α](x:⇃τ1 ⇂Υ ):⇃τ2 ⇂Υ .⇃e⇂Υ ii
where v = hρ, fix f [α](x:τ1 ):τ2 .ei
⇃v j ⇂Υ
i∈Υ
i
h⇃v j ⇂Υ :⇃τ ⇂Υ i
i∈
/Υ

⇃ρ⇂Υ

We use the notation i ≃ j to indicate when an unboxing agrees
at two labels i and j.
Υ

i≃j

iff

either i, j ∈ Υ or i, j ∈
/Υ

The first requirement is then specified via the cache consistency
judgement, which enforces that for any label i, the unboxing set
must agree on i and the labels of any shapes in the cache of i.
Υ

∀i, s : s ∈ C(i) =⇒ i ≃ lbl(s)
C⊢Υ
The second requirement is specified via the consistent unboxing
judgement of Figure 9. The type rules determine the traceability of
the unboxed type: that is, the judgement Υ ⊢ τ : t indicates that
unboxing τ with Υ will result in a type of traceability t. The key use
of the type judgement is in the term level polymorphic instantiation
rule, which requires that the traceability of the unboxed type be r.
4.3 Type Preservation

⇃x1 :τ1 = v1 j1 , . . . , xn :τn = vn jn ⇂Υ =
x1 :⇃τ1 ⇂Υ = ⇃v1 j1 ⇂Υ , . . . , xn :⇃τn ⇂Υ = ⇃vn jn ⇂Υ

Our goal is to show that the unboxing function induced by any
acceptable unboxing is in some sense correct as an optimization.
The first part of this is to show that unboxing preserves typing. One
key property is that types have non-empty caches.

⇃M ⇂Υ
⇃(ρ, e)⇂Υ = (⇃ρ⇂Υ , ⇃e⇂Υ )

Lemma 17 (Type Inhabitance)
If τ is not a type variable and C; ̺ ⊢ τ then C(lbl(τ )) 6= ∅.

Figure 8. Unboxing

4.1 The unboxing optimization
We specify a particular choice of unboxing via an unboxing set Υ
which contains the set of labels of terms and types to be unboxed.
A choice of a particular Υ then induces an unboxing function as defined in Figure 8. The unboxing function is defined in a straightforward compositional manner. Box introductions are dropped when
their labels are in the unboxing set, box type constructors are
dropped when their labels are in the unboxing set, box eliminations
are dropped when the labels of their arguments are in the unboxing
set, and all other terms and types are left unchanged.
An important observation about the unboxing optimization as
we have defined it is unlike many previous interprocedural approaches (Section 7), it only improves programs and never introduces instructions or allocation. This is easy to see, since the unboxing function only removes boxes (which allocate and have an
instruction cost), and unboxes (which have an instruction cost) and
never introduces any new operations at all.

Proof: The proof is by inspection of the rules for acceptability.
We also need several technical properties: labels agree when
their caches intersect, unboxing preserves type well formedness,
type traceability, and type equality, and unboxing commutes with
type subsitution.
Lemma 18 (Agreement)
Υ
If C ⊢ Υ and C(i) ∩ C(j) 6= ∅ then i ≃ j .
Proof: The proof is by inspection of the rules for cache consistency.
Lemma 19
If ∆ ⊢ τ wf then ∆ ⊢ ⇃τ ⇂Υ wf .
Proof: The proof is a straight forward induction on the structure
of τ .
Lemma 20
If C; ̺ ⊢ τ2 and C(lbl(τ2 )) = C(̺(α)) then:

4.2 Acceptable unboxings
While any choice of Υ defines an unboxing, not every unboxing
set is reasonable in the sense that it defines a type and semantics
preserving optimization. Just as we defined a notion of acceptable
analysis in Section 3, we will define a judgement that captures suf-

14

• If C; ̺ ⊢ τ1 then ⇃τ1 [τ2 /α]⇂Υ = ⇃τ1 ⇂Υ [⇃τ2 ⇂Υ /α].
• If C; ̺ ⊢ e then ⇃e[τ2 /α]⇂Υ = ⇃e⇂Υ [⇃τ2 ⇂Υ /α].

Proof:

2018/2/19

i

Case 3, τ1 = (∀α′ .τ3 → τ4 ) : Then C; ̺ ⊢ τ1 requires
C; ̺ ⊢ τ3 and C; ̺ ⊢ τ4 . By the induction hypothesis, ⇃τ3 [τ2 /α]⇂Υ = ⇃τ3 ⇂Υ [⇃τ2 ⇂Υ /α] and ⇃τ4 [τ2 /α]⇂Υ =
⇃τ4 ⇂Υ [⇃τ2 ⇂Υ /α]. Thus:

Υ⊢τ :t
Υ ⊢ Bi : b

Υ ⊢ αi : r

=
=
=
=
=

Υ ⊢ (∀α.τ1 → τ2 )i : r
i∈Υ

Υ⊢τ :t

i∈
/Υ

i

Υ ⊢ box(τ )i : r

Υ ⊢ box(τ ) : t

Case 4, τ1 = box(τ )i : Then C; ̺ ⊢ τ1 requires C; ̺ ⊢ τ .
The induction hypothesis is ⇃τ [τ2 /α]⇂Υ = ⇃τ ⇂Υ [⇃τ2 ⇂Υ /α].
If i ∈ Υ then ⇃τ1 ⇂Υ = ⇃τ ⇂Υ and ⇃τ1 [τ2 /α]⇂Υ =
⇃τ [τ2 /α]⇂Υ , as required. If i ∈
/ Υ then:

Υ⊢e
Υ⊢e
Υ ⊢ xi

Υ ⊢ (fix f [α](x:τ1 ):τ2 .e)i
Υ ⊢ e1

Υ ⊢ e2

=
=
=
=
=

Υ⊢τ :r

Υ ⊢ (e1 [τ ] e2 )i
Υ⊢e

Υ⊢e
i

Υ ⊢ (boxτ e)

⇃τ1 [τ2 /α]⇂Υ
i
⇃(∀α′ .τ3 [τ2 /α] → τ3 [τ2 /α]) ⇂Υ
i
′
(∀α .⇃τ3 [τ2 /α]⇂Υ → ⇃τ3 [τ2 /α]⇂Υ )
i
′
(∀α .⇃τ3 ⇂Υ [⇃τ2 ⇂Υ /α] → ⇃τ4 ⇂Υ [⇃τ2 ⇂Υ /α])
i
(∀α′ .⇃τ3 ⇂Υ → ⇃τ4 ⇂Υ ) [⇃τ2 ⇂Υ /α]
⇃τ1 ⇂Υ [⇃τ2 ⇂Υ /α]

⇃τ1 [τ2 /α]⇂Υ
⇃box(τ [τ2 /α])i ⇂Υ
box(⇃τ [τ2 /α]⇂Υ )i
box(⇃τ ⇂Υ [⇃τ2 ⇂Υ /α])i
box(⇃τ ⇂Υ )i [⇃τ2 ⇂Υ /α]
⇃τ1 ⇂Υ [⇃τ2 ⇂Υ /α]

• The proof is a straight forward induction on the structure of e.

Υ ⊢ (unbox e)i

Υ⊢ρ Υ⊢e
Υ ⊢ ρ(e)i

Lemma 21
If Υ ⊢ τ : t then tr (⇃τ ⇂Υ ) = t.

Υ ⊢ ci

Υ⊢ρ Υ⊢e

Υ ⊢ vi

Υ ⊢ hρ, fix f [α](x:τ1 ):τ2 .eii

Υ ⊢ hv i :τ i

Proof: The proof is a straight forward induction on the derivation
of Υ ⊢ τ : t.

j

Lemma 22
If ⊢ τ1 = τ2 , C ⊢ Υ, C; ̺ ⊢ τ1 , C; ̺ ⊢ τ2 , and either
C(lbl(τ1 )) ⊆ C(lbl(τ2 )) or C(lbl(τ2 )) ⊆ C(lbl(τ1 )) then ⊢
⇃τ1 ⇂Υ = ⇃τ2 ⇂Υ .

Υ⊢ρ
∀1 ≤ j ≤ n : Υ ⊢ vj ij
Υ ⊢ x1 :τ1 = v1 i1 , . . . , xn :τn = vn in

Proof: The proof is by induction on the derivation of ⊢ τ1 = τ2 .
Consider the last rule used (in the same order as the figure):

Υ⊢M

• (Type variable) In this case τ1 = αi and τ2 = αj . By definition,

Υ⊢ρ Υ⊢e

⇃τ1 ⇂Υ = τ1 and ⇃τ2 ⇂Υ = τ2 , and the result is immediate.
• (Base) In this case τ1 = Bi and τ2 = Bj . By definition,

Υ ⊢ (ρ, e)

⇃τ1 ⇂Υ = τ1 and ⇃τ2 ⇂Υ = τ2 , and the result is immediate.
Figure 9. Consistent unboxing

• (Function) In this case:

• The proof is by induction on the structure of τ1 . Consider the

cases for τ1 :
k

Case 1, τ1 = αi : If τ2 = σ j and ⇃σ j ⇂Υ = σ ′ then
τ1 [τ2 /α] = σ i , thus ⇃τ1 [τ2 /α]⇂Υ = ⇃σ i ⇂Υ , and also
i
⇃τ1 ⇂Υ [⇃τ2 ⇂Υ /α] = σ ′ . Thus I need to show that ⇃σ i ⇂Υ =
′i
σ . When σ is not a box type, this condition follows easily
from the definitions. When σ is a box type, this condition
Υ

follows if i ≃ j. By C; ̺ ⊢ τ2 and Lemma 17, C(j) 6= ∅.
By C; ̺ ⊢ τ1 , C(lbl(τ2 )) = C(̺(α)), and the rules for
Υ

acceptability, C(i) = C(j). By Lemma 18, i ≃ j, as
required.

τ1 = (∀α.τ11 → τ12 )i1
τ2 = (∀α.τ21 → τ22 )i2
⊢ τ11 = τ21
⊢ τ12 = τ22

(1)
(2)

WLOG, assume C(i1 ) ⊆ C(i2 ) (3). By the rules for acceptability:
C; ̺ ⊢ τ11
C; ̺ ⊢ τ12
(∀̺(α).lbl(τ11 ) → lbl(τ12 ))jt ∈ C(i1 )
C; ̺ ⊢ τ21
C; ̺ ⊢ τ22
funC (i2 , ̺(α), lbl(τ21 ), lbl(τ22 ))

(4)
(5)
(6)
(7)
(8)
(9)

Case 2, τ1 = β i and α 6= β: In this case τ1 [τ2 /α] = τ1 ,
⇃τ1 ⇂Υ = τ1 , and the result is immediate.

By (6), (3), and (9), C(lbl(τ21 )) ⊆ C(lbl(τ11 )) (10) and
C(lbl(τ12 )) ⊆ C(lbl(τ22 )) (11). By (1), (4), (7), (10), and the
induction hypothesis, ⊢ ⇃τ11 ⇂Υ = ⇃τ21 ⇂Υ (12). By (2), (5), (8),
(11), and the induction hypothesis, ⊢ ⇃τ12 ⇂Υ = ⇃τ22 ⇂Υ (13).

15

2018/2/19

• (Application) In this case, e = (e1 [τ ′ ] e2 )i . The typing rule,

By (12), (13), and the typing rules:

C; ̺ ⊢ e, and Υ ⊢ e require that:

⊢ (∀α.⇃τ11 ⇂Υ → ⇃τ12 ⇂Υ )i1 = (∀α.⇃τ21 ⇂Υ → ⇃τ22 ⇂Υ )i2
By definition:
⊢ ⇃(∀α.τ11 → τ12 )i1 ⇂Υ = ⇃(∀α.τ21 → τ22 )i2 ⇂Υ
as required.
• (Box) In this case τ1 = box(τ1′ )i1 , τ2 = box(τ2′ )i2 , and

⊢ τ1′ = τ2′ (1). WLOG, assume C(i1 ) ⊆ C(i2 ) (2). By the
j
rules for acceptability, C; ̺ ⊢ τ1′ (3), (box lbl(τ1′ ))t ∈ C(i1 )
′
′
(4), C; ̺ ⊢ τ2 (5), and boxC (i2 , lbl(τ2 )) (6). By (4), (2), and
(6), C(lbl(τ1′ )) ⊆ C(lbl(τ2′ )) (7). By (1), (3), (5), (7), and the
induction hypothesis, ⊢ ⇃τ1′ ⇂Υ = ⇃τ2′ ⇂Υ (8). By Lemmas 17
Υ

and 18, i1 ≃ i2 . There are two cases:
Case 1, i1 ∈ Υ: In this case, ⇃τ1 ⇂Υ = ⇃τ1′ ⇂Υ , ⇃τ2 ⇂Υ =
⇃τ2′ ⇂Υ , and the result is (8).
i

Case 2, i2 ∈
/ Υ: In this case, ⇃τ1 ⇂Υ = box(⇃τ1′ ⇂Υ ) 1 ,
i
⇃τ2 ⇂Υ = box(⇃τ2′ ⇂Υ ) 2 , and the result follows from (8) and
the typing rules.

(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(10)
(11)
(12)

for some τ1 , τ3 , j, and τ2 . By (1), (5), (10), (2), (7), (11), and
the induction hypothesis:
∆; ⇃Γ⇂Υ ⊢ ⇃e1 ⇂Υ : ⇃(∀α.τ1 → τ )j ⇂Υ
∆; ⇃Γ⇂Υ ⊢ ⇃e2 ⇂Υ : ⇃τ2 ⇂Υ

(13)
(14)

By definition ⇃(∀α.τ1 → τ3 )j ⇂Υ = (∀α.⇃τ1 ⇂Υ → ⇃τ3 ⇂Υ )j .
By (3) and Lemma 19, ∆ ⊢ ⇃τ ′ ⇂Υ wf (15). By (12) and
Lemma 21, tr (⇃τ ′ ⇂Υ ) = r (16). By (1), (2), and Lemma 16:
C(j) ⊆ C(lbl(e1 ))
C; ̺ ⊢ (∀α.τ1 → τ3 )j
C(lbl(τ2 )) ⊆ C(lbl(e2 ))
C ⊢ τ2

Now we can prove that unboxing preserves typing.

(17)
(18)
(19)
(20)

By (18) and the rules for acceptability:

Theorem 1 (Consistent unboxings preserve typing)
If C ⊢ Υ then:
• If ∆; Γ ⊢ e : τ , C; ̺ ⊢ Γ, C; ̺ ⊢ e, and Υ ⊢ e then

∆; ⇃Γ⇂Υ ⊢ ⇃e⇂Υ : ⇃τ ⇂Υ .
• If ⊢ ρ : Γ, C; ̺ ⊢ ρ, and Υ ⊢ ρ then ⊢ ⇃ρ⇂Υ : ⇃Γ⇂Υ .
• If ⊢ M : τ , C; ̺ ⊢ M , and Υ ⊢ M then ⊢ ⇃M ⇂Υ : ⇃τ ⇂Υ .

Proof: The proof is by induction on the structure of the typing
judgement. Consider the cases, in the same order as the figure, for
the last rule used in the derivation:
• (Variable) In this case e = xi and x:τ ∈ Γ. Then ⇃e⇂Υ = xi

and clearly x:⇃τ ⇂Υ ∈ ⇃Γ⇂Υ , so the result follows by the typing
rules.
′ i

• (Fix expression) In this case e = (fix f [α](x:τ1 ):τ2 .e ) .
i

The typing rule requires that both τ = (∀α.τ1 → τ2 ) and
∆; Γ, f :τ, x:τ1 ⊢ e′ : τ2 . The assumption C; ̺ ⊢ e requires
̺(f ) = i, ̺(x) = lbl(τ1 ), C ⊢ τ , and C; ̺ ⊢ e′ . From C ⊢ τ
and the rules for acceptability, C ⊢ τ1 . From these facts, C; ̺ ⊢
Γ, f :τ, x:τ1 . The assumption Υ ⊢ e requires that Υ ⊢ e′ . By
the induction hypothesis, ∆; ⇃Γ, f :τ, x:τ1 ⇂Υ ⊢ ⇃e′ ⇂Υ : ⇃τ2 ⇂Υ .
Since:
⇃Γ, f :τ, x:τ1 ⇂Υ = ⇃Γ⇂Υ , f :(∀α.⇃τ1 ⇂Υ → ⇃τ2 ⇂Υ )i , x:⇃τ2 ⇂Υ
by the typing rules:
i

∆; ⇃Γ⇂Υ ⊢ (fix f [α](x:⇃τ1 ⇂Υ ):⇃τ2 ⇂Υ .⇃e′ ⇂Υ ) :
(∀α.⇃τ1 ⇂Υ → ⇃τ2 ⇂Υ )i
The result follows since:
⇃e⇂Υ = (fix f [α](x:⇃τ1 ⇂Υ ):⇃τ2 ⇂Υ .⇃e′ ⇂Υ )
⇃τ ⇂Υ = (∀α.⇃τ1 ⇂Υ → ⇃τ2 ⇂Υ )i

∆; Γ ⊢ e1 : (∀α.τ1 → τ3 )j
τ = τ3 [τ ′ /α]
∆; Γ ⊢ e2 : τ2
∆ ⊢ τ ′ wf
⊢ τ1 [τ ′ /α] = τ2
C; ̺ ⊢ e1
C; ̺ ⊢ τ ′
C; ̺ ⊢ e2
funC (lbl(e1 ), lbl(τ ), lbl(e2 ), i)
Υ ⊢ e1
Υ ⊢ e2
Υ ⊢ τ′ : r

i

16

C; ̺ ⊢ τ1
C; ̺ ⊢ τ3
(∀̺(α).lbl(τ1 ) → lbl(τ3 ))kt ∈ C(j)

(21)
(22)
(23)

By (23), (17), and (8), C(lbl(τ ′ )) = C(̺(α)) (24) and
C(lbl(e2 )) ⊆ C(lbl(τ1 )). Hence by (19), C(lbl(τ2 )) ⊆
C(lbl(τ1 )). Since lbl(τ1 [τ ′ /α]) = lbl(τ1 ), C(lbl(τ2 )) ⊆
C(lbl(τ1 [τ ′ /α])) (25). By (21), (6), (24), and Lemma 13,
C; ̺ ⊢ τ1 [τ ′ /α] (26). By (4), (26), (20), (25), and Lemma 22,
⊢ ⇃τ1 [τ ′ /α]⇂Υ = ⇃τ2 ⇂Υ . By (21), (6), (24), and Lemma 20,
⊢ ⇃τ1 ⇂Υ [⇃τ ′ ⇂Υ /α] = ⇃τ2 ⇂Υ (27). Thus by (13), (14), (15), (16),
i
(27), and the typing rules, ∆; ⇃Γ⇂Υ ⊢ (⇃e1 ⇂Υ [⇃τ ′ ⇂Υ ] ⇃e2 ⇂Υ ) :
′
⇃τ3 ⇂Υ [⇃τ ⇂Υ /α]. By definition, (22), (6), (24), and Lemma 20,
i
∆; ⇃Γ⇂Υ ⊢ ⇃(e1 [τ ′ ] e2 ) ⇂Υ : ⇃τ ⇂Υ , as required.
• (Box expression) In this case, e = (boxτ ′′ e′ )i for some e′ and
i

i. The typing rule requires that τ = box(τ ′′ ) , ∆ ⊢ τ ′′ wf ,
∆; Γ ⊢ e′ : τ ′ , and ⊢ τ ′′ = τ ′ for some τ ′ . The assumption
C; ̺ ⊢ e requires that C ⊢ τ and C; ̺ ⊢ e′ . The assumption
Υ ⊢ e requires that Υ ⊢ e′ . By the induction hypothesis,
∆; ⇃Γ⇂Υ ⊢ ⇃e′ ⇂Υ : ⇃τ ′ ⇂Υ . There are two subcases:
If i ∈ T then ⇃e⇂Υ = ⇃e′ ⇂Υ and ⇃τ ⇂Υ = ⇃τ ′ ⇂Υ and the
result is immediate.
i

If i ∈
/ T then ⇃e⇂Υ = (box⇃τ ′′ ⇂Υ ⇃e′ ⇂Υ ) and ⇃τ ⇂Υ =
i
box(⇃τ ′ ⇂Υ ) . The result follows by the typing rules if
∆ ⊢ ⇃τ ′ ⇂Υ wf , which holds by Lemma 19, and ⊢
⇃τ ′′ ⇂Υ = ⇃τ ′ ⇂Υ , which holds by Lemma 22 if its other
three premises hold. Since C ⊢ τ , by the rules for acceptability, boxC (i, lbl(τ ′′ )) (1) and C ⊢ τ ′′ , showing
the first premise. Since ∆; Γ ⊢ e′ : τ ′ , by Lemma 16,
C(lbl(τ ′ )) ⊆ C(lbl(e′ )) (2) and C ⊢ τ ′ , showing the
j
second premise. By C; ̺ ⊢ e, (boxtr (τ ′ ) lbl(e′ ))v ∈
′
′′
C(i). Thus by (1), C(lbl(e )) ⊆ C(lbl(τ )), so by (2),
C(lbl(τ ′ )) ⊆ C(lbl(τ ′′ )), showing the third premise, as
required.

2018/2/19

• (Unbox) In this case, e = (unbox e′ )i for some e′ and i. The

typing rule requires that ∆; Γ ⊢ e′ : box(τ )j for some j.
The assumption C; ̺ ⊢ e requires C; ̺ ⊢ e′ . The assumption
Υ ⊢ e requires Υ ⊢ e′ . By the induction hypothesis, ∆; ⇃Γ⇂Υ ⊢
⇃e′ ⇂Υ : ⇃box(τ )j ⇂Υ . By Lemma 16, C(j) ⊆ C(lbl(e′ )). By
Υ

Lemmas 17 and 18, j ≃ lbl(e′ ). There are two subcases:
If j ∈ Υ then ⇃e⇂Υ = ⇃e′ ⇂Υ and ⇃box(τ )j ⇂Υ = ⇃τ ⇂Υ and
the result is immediate.
i

If j ∈
/ Υ then ⇃e⇂Υ = (unbox ⇃e′ ⇂Υ ) and ⇃box(τ )j ⇂Υ =
box(⇃τ ⇂Υ )j . The result then follows by the typing rules.
• (Frame) In this case, e = ρ′ (e′ )i for some ρ′ , e′ , and i. The

typing rule requires that ⊢ ρ′ : Γ′ and ∆; Γ′ ⊢ e′ : τ for
some Γ′ . The assumption C; ̺ ⊢ e requires that C; ̺ ⊢ ρ′ and
C; ̺ ⊢ e′ . The former requires that C; ̺ ⊢ Γ′ . The assumption
Υ ⊢ e requires Υ ⊢ e′ . By the induction hypothesis, ⊢ ⇃ρ′ ⇂Υ :
⇃Γ′ ⇂Υ and ∆; ⇃Γ′ ⇂Υ ⊢ ⇃e′ ⇂Υ : ⇃τ ⇂Υ . So by the typing rules,
i
∆; ⇃Γ⇂Υ ⊢ ⇃ρ′ ⇂Υ (⇃e′ ⇂Υ ) : ⇃τ ⇂Υ . The result follows since
i
′
′
⇃e⇂Υ = ⇃ρ ⇂Υ (⇃e ⇂Υ ) .

• (Constant) In this case e = ci for some c and i. The typing rule

requires that τ = Bi . Clearly, ⇃e⇂Υ = ci , ⇃τ ⇂Υ = Bi , and the
result follows by the typing rules.

• (Fix value) In this case e = hρ, fix f [α](x:τ1 ):τ2 .e′ ii . The

typing rule require that τ = (∀α.τ1 → τ2 )i , ⊢ ρ : Γ′ , and
∆, α; Γ′ , f :τ, x:τ1 ⊢ e′ : τ2 . The assumption C; ̺ ⊢ e requires
C; ̺ ⊢ ρ, from which C; ̺ ⊢ Γ′ , ̺(f ) = i, ̺(x) = lbl(τ1 ),
C ⊢ τ , and C; ̺ ⊢ e′ . From C ⊢ τ and the rules for
acceptability, C ⊢ τ1 . From these facts, C; ̺ ⊢ Γ′ , f :τ, x:τ1 .
The assumption Υ ⊢ e requires Υ ⊢ e′ . By the induction
hypothesis, ⊢ ⇃ρ⇂Υ : ⇃Γ′ ⇂Υ and ∆, α; ⇃Γ′ , f :τ, x:τ1 ⇂Υ ⊢
⇃e′ ⇂Υ : ⇃τ2 ⇂Υ . Since:
′

i

′

⇃Γ , f :τ, x:τ1 ⇂Υ = ⇃Γ ⇂Υ , f :(∀α.⇃τ1 ⇂Υ → ⇃τ2 ⇂Υ ) , x:⇃τ2 ⇂Υ
by the typing rules:
i

∆; ⇃Γ⇂Υ ⊢ h⇃ρ⇂Υ , fix f [α](x:⇃τ1 ⇂Υ ):⇃τ2 ⇂Υ .⇃e′ ⇂Υ i :
(∀α.⇃τ1 ⇂Υ → ⇃τ2 ⇂Υ )i
The result follows since:
⇃e⇂Υ = h⇃ρ⇂Υ , fix f [α](x:⇃τ1 ⇂Υ ):⇃τ2 ⇂Υ .⇃e′ ⇂Υ i
⇃τ ⇂Υ = (∀α.⇃τ1 ⇂Υ → ⇃τ2 ⇂Υ )i

i

i

• (Box value) In this case, e = hv j :τ ′′ i for some v, i, and j. The
′′ i

typing rule requires that τ = box(τ ) , ∆ ⊢ τ ′′ wf , ∆; Γ ⊢
v j : τ ′ , and ⊢ τ ′′ = τ ′ for some τ ′ . The assumption C; ̺ ⊢ e
requires that C ⊢ τ and C; ̺ ⊢ v j . The assumption Υ ⊢ e
requires Υ ⊢ v j . By the induction hypothesis, ∆; ⇃Γ⇂Υ ⊢
⇃v j ⇂Υ : ⇃τ ′ ⇂Υ . There are two subcases:
If i ∈ T then ⇃e⇂Υ = ⇃v j ⇂Υ and ⇃τ ⇂Υ = ⇃τ ′ ⇂Υ and the
result is immediate.
i

If i ∈
/ T then ⇃e⇂Υ = h⇃v j ⇂Υ :⇃τ ′′ ⇂Υ i and ⇃τ ⇂Υ =
i
box(⇃τ ′ ⇂Υ ) . The result follows by the typing rules if
∆ ⊢ ⇃τ ′′ ⇂Υ wf , which holds by Lemma 19, and ⊢
⇃τ ′′ ⇂Υ = ⇃τ ′ ⇂Υ , which holds by Lemma 22 if its other three
premises hold. Since C ⊢ τ , by the rules for acceptability,
boxC (i, lbl(τ ′′ )) (1) and C ⊢ τ ′′ , showing the first premise.
Since ∆; Γ ⊢ v j : τ ′ , by Lemma 16, C(lbl(τ ′ )) ⊆ C(j)
(2) and C ⊢ τ ′ , showing the second premise. By C; ̺ ⊢ e,
(boxtr (τ ′ ) j)kv ∈ C(i). Thus by (1), C(j) ⊆ C(lbl(τ ′′ )),
so by (2), C(lbl(τ ′ )) ⊆ C(lbl(τ ′′ )), showing the third
premise, as required.

17

• (Environment) In this case ρ = x1 :τ1 = v1 i1 , . . . , xn :τn =

vn in and Γ = x1 :τ1 , . . . , xn :τn . The typing rule requires that
∅; ∅ ⊢ vj ij : τj′ and ⊢ τj = τj′ for 1 ≤ j ≤ n and some τj′ s.
The assumption C; ̺ ⊢ ρ requires C; ̺ ⊢ τj and C; ̺ ⊢ vj ij
for 1 ≤ j ≤ n. Clearly C; ̺ ⊢ Γ′ where Γ′ is empty. The
assumption Υ ⊢ ρ requires Υ ⊢ vj ij for 1 ≤ j ≤ n. By
the induction hypotheis, ∅; ∅ ⊢ ⇃vj ij ⇂Υ : ⇃τj′ ⇂Υ for 1 ≤
j ≤ n. By the rules for acceptability, C(ij ) ⊆ C(lbl(τj ))
for 1 ≤ j ≤ n. By Lemma 16, C(τj′ ) ⊆ C(ij ) and C ⊢ τj′
for 1 ≤ j ≤ n. Thus C(τj′ ) ⊆ C(τj ) for 1 ≤ j ≤ n.
By Lemma 22, ⊢ ⇃τj ⇂Υ = ⇃τj′ ⇂Υ for 1 ≤ j ≤ n. Then
by the typing rules ⊢ x1 :⇃τ1 ⇂Υ = ⇃v1 i1 ⇂Υ , . . . , xn :⇃τn ⇂Υ =
⇃vn in ⇂Υ : x1 :⇃τ1 ⇂Υ , . . . , xn :⇃τn ⇂Υ . The result follows since
⇃ρ⇂Υ = x1 :⇃τ1 ⇂Υ = ⇃v1 i1 ⇂Υ , . . . , xn :⇃τn ⇂Υ = ⇃vn in ⇂Υ and
⇃Γ⇂Υ = x1 :⇃τ1 ⇂Υ , . . . , xn :⇃τn ⇂Υ .

• (Machine state) In this case M = (ρ, e). By the typing rule,

⊢ ρ : Γ and ∅; Γ ⊢ e : τ for some Γ. The assumption C; ̺ ⊢ M
requires both C; ̺ ⊢ ρ and C; ̺ ⊢ e. The former requires
C; ̺ ⊢ Γ. The assumption Υ ⊢ M requires Υ ⊢ ρ and Υ ⊢ e.
By the induction hypothesis, ⊢ ⇃ρ⇂Υ : ⇃Γ⇂Υ and ∅; ⇃Γ⇂Υ ⊢
⇃e⇂Υ : ⇃τ ⇂Υ . So by the typing rules, ⊢ (⇃ρ⇂Υ , ⇃e⇂Υ ) : ⇃τ ⇂Υ .
The result follows since ⇃M ⇂Υ = (⇃ρ⇂Υ , ⇃e⇂Υ ).
A consequence of type preservation is that unboxed well typed
programs are traceable.
Theorem 2
If ⊢ M : τ , C ⊢ Υ, and C; ̺ ⊢ M then ⊢ ⇃M ⇂Υ tr.
Proof: The proof follows from Theorem 1 and Lemma 11.
4.4 Coherence
The other part of proving correctness is to show that unboxing
preserves semantics in some appropriate sense. That requires two
key lemmas—that a step of the program can be matched by zero
or more steps of the unboxed program and that consistency is
preserved under reduction.
To show the first lemma, we need three technical lemmas—that
a value’s cache is nonempty, that reduction preserves the unboxing
or not of the outermost label, and a multistep compositionality
property.
Lemma 23 (Inhabitance)
If C; ̺ ⊢ v k then ∃s ∈ C(k) such that lbl(s) = k.
Proof: By inspection of the acceptable analysis and acceptable
instantiation rules.
Lemma 24 (Unboxing set preservation)
If C; ̺ ⊢ ρ, C; ̺ ⊢ e, C ⊢ Υ, and (ρ, e1 ) 7−→ (ρ, e2 ) then
Υ

lbl(e) ≃ lbl(e′ ).
Proof: All of the cases for which lbl(e1 ) = lbl(e2 ) follow
immediately. For the remaining cases:
• If (ρ, xk ) 7−→ (ρ, v j ) where x:τ = v j ∈ ρ then by the as-

sumptions we have that ̺(x) = lbl(τ ) (1), C(j) ⊆ C(lbl(τ ))
(2) and C(̺(x)) ⊆ C(k) (3), so by transitivity we have C(j) ⊆
C(k) (4). By Inhabitance (Lemma 23) we have an s ∈ C(j) (5)
such that lbl(s) = j (6), and so by Agreement (Lemma 18)
Υ

we have k ≃ j. Since lbl(e) = k and lbl(e′ ) = j, the result
follows.

2018/2/19

j k

• If (ρ, (unbox hv i :ti ) ) 7−→ (ρ, v i ) then we must show that
Υ

k ≃ i. By Inhabitance we have s ∈ C(i) with lbl(s) = i, so by
Agreement, it suffices to show that C(i) ⊆ C(k). By the box
rule for an acceptable analysis, there is a s = (boxt l)jv ∈ C(j)
such that C(i) ⊆ C(l). Since s ∈ C(j), by the rule for unbox,
C(l) ⊆ C(k), so C(i) ⊆ C(k) and we’re done.
Υ

j

• If (ρ, ρ′ (v i ) ) 7−→ (ρ, v i ) then we must show that j ≃ i. By

Inhabitance, there is an s ∈ C(i), and by the acceptable analysis
rule for frames we have that C(i) ⊆ C(j), so by Agreement we
Υ

have that j ≃ i.

By definition of C; ̺ ⊢ M we have that C; ̺ ⊢ ρ and C; ̺ ⊢ e1 .
Hence we have that C; ̺ ⊢ (ρ, e1 ). By the typing rules we also
have that ⊢ ρ : Γ and ∅; Γ ⊢ e1 : τ1 for some Γ and τ1 ,
so ⊢ (ρ, e1 ) : τ1 . By the rules for consistency, Υ ⊢ ρ and
Υ ⊢ e1 , so Υ ⊢ (ρ, e1 ). Hence by induction we have that
(⇃ρ⇂Υ , ⇃e1 ⇂Υ ) 7−→∗ (⇃ρ⇂Υ , ⇃e′1 ⇂Υ ).
By Lemma 25
j
(⇃ρ⇂Υ , (⇃e1 ⇂Υ [⇃τ ′ ⇂Υ ] ⇃e2 ⇂Υ ) ) 7−→∗
j
′
′
(⇃ρ⇂Υ , (⇃e1 ⇂Υ [⇃τ ⇂Υ ] ⇃e2 ⇂Υ ) )
By definition of unboxing
j
j
(⇃ρ⇂Υ , ⇃(e1 [τ ′ ] e2 ) ⇂Υ ) 7−→∗ (⇃ρ⇂Υ , ⇃(e′1 [τ ′ ] e2 ) ⇂Υ )
• If (ρ, (e1 [τ ′ ] e2 )j ) 7−→ (ρ, (e1 [τ ′ ] e′2 )j ) then the argument

follows by the symmetric argument to the previous case.
Lemma 25 (Many step compositionality)
If (ρ, e1 ) 7−→∗ (ρ, e2 ) then:

l

• If (ρ, (vf j [τ ′ ] vt k ) ) 7−→ (ρ, ρ′′ (e′′ [τ ′ /α])l ) where:

vf = hρ′ , fix f [α](x:τ1 ):τ2 .e′′ i
ρ′′ = ρ′ , f :τ = vf j , x:τ1′ = vt k
τ = (∀α.τ1 → τ2 )j
τ1′ = τ1 [τ ′ /α]

• (ρ, (e1 e)i ) 7−→∗ (ρ, (e2 e)i )
i

i

• (ρ, (v j e1 ) ) 7−→∗ (ρ, (v j e2 ) )
• (ρ, (boxτ e1 )i ) 7−→∗ (ρ, (boxτ e2 )i )
• (ρ, (unbox e1 )i ) 7−→∗ (ρ, (unbox e2 )i )

then:
By definition of unboxing we have that:

• (ρ, ρ′ (e1 )i ) 7−→∗ (ρ, ρ′ (e2 )i )

Proof: The proof is by an easy induction on the length of the
reduction sequences.
Theorem 3 (Single step reduction coherence)
If ⊢ M : τ , C; ̺ ⊢ M , C ⊢ Υ, Υ ⊢ M , and M 7−→ M ′ then
⇃M ⇂Υ 7−→∗ ⇃M ′ ⇂Υ .
Proof: The proof is by induction on the derivation of M 7−→ M ′ ,
consider the cases for the last rule used to derive it:
• If (ρ, xk ) 7−→ (ρ, v j ) where x:τ = v j ∈ ρ then by definition

⇃M ⇂Υ = (⇃ρ⇂Υ , xk ), ⇃M ′ ⇂Υ = (⇃ρ⇂Υ , ⇃v j ⇂Υ ), and x:⇃τ ⇂Υ =
⇃v j ⇂Υ ∈ ⇃ρ⇂Υ . Thus ⇃M ⇂Υ 7−→ ⇃M ′ ⇂Υ by the same rule.

⇃e⇂Υ
vf′
′
vt′ k
⇃e′ ⇂Υ

=
=
=
=

l

(⇃ρ⇂Υ , ⇃e⇂Υ ) 7−→ (⇃ρ⇂Υ , ρ′′′ (e′′′ ) )
where:

′

then the unboxings of the e and e are of the same form, and the
same reduction step applies.
j

j

• If (ρ, (boxτ ′ vt i ) ) 7−→ (ρ, hvt i :τ ′ i ) where tr (τ ′ ) = t then:

If j ∈
/ Υ then:
k j

By the definition of unboxing, ⇃e⇂Υ = (box⇃τ ′ ⇂Υ vt′ ′ )
k
where vt′ ′ = ⇃vt i ⇂Υ .
By hypothesis, ⊢ ρ : Γ, ; Γ ⊢ vt i : τ ′′ and ⊢ τ ′ = τ ′′ for
some τ ′′ . By hypothesis, Υ ⊢ vt i . By Theorem 1, ∅; ⇃Γ⇂Υ ⊢
k
vt′ ′ : ⇃τ ′′ ⇂Υ . The proof of that theorem also showed that ⊢
′
⇃τ ⇂Υ = ⇃τ ′′ ⇂Υ , so by Lemma 4, tr (⇃τ ′ ⇂Υ ) = tr (⇃τ ′′ ⇂Υ ).
By Lemma 6, tr (⇃τ ′′ ⇂Υ ) = t′ , so tr (⇃τ ′ ⇂Υ ) = t′ .
k j
By definition of reduction (⇃ρ⇂Υ , (box⇃τ ′ ⇂Υ vt′ ′ ) ) 7−→
k

′ l

By hypothesis, ⊢ ρ : Γ, ∅; Γ ⊢ vt k : τ1′′ , and ⊢ τ1′ = τ1′′ .
′
By Theorem 1, ∅; ⇃Γ⇂Υ ⊢ vt′ k : ⇃τ1′′ ⇂Υ . The proof of that
′
theorem also showed that ⊢ ⇃τ1 ⇂Υ = ⇃τ1′′ ⇂Υ . By Lemma 4,
tr (⇃τ1′ ⇂Υ ) = tr (⇃τ1′′ ⇂Υ ). By Lemma 6, tr (⇃τ1′′ ⇂Υ ) = t′ . Thus
tr (⇃τ1′ ⇂Υ ) = t′ . So by the application beta rule:

• If:

(ρ, (fix f [α](x:τ1 ):τ2 .e1 )j ) 7−→
(ρ, hρ, fix f [α](x:τ1 ):τ2 .e1 ij )

j

(vf′ [⇃τ ′ ⇂Υ ] vt′ k )
h⇃ρ′ ⇂Υ , fix f [α](x:⇃τ1 ⇂Υ ):⇃τ2 ⇂Υ .⇃e′′ ⇂Υ i
⇃vt k ⇂Υ
′
j
(⇃ρ′ ⇂Υ , f :⇃τ ⇂Υ = vf′ , x:⇃τ1′ ⇂Υ = vt′ k )
(⇃e′′ [τ ′ /α]⇂Υ )l

j

(⇃ρ⇂Υ , hvt′ ′ :⇃τ ′ ⇂Υ i ).

ρ′′′
τ ′′
τ1′′
e′′′

=
=
=
=

j

⇃ρ⇂Υ , f :τ ′′ = vf′ , x:τ1′′ = vt′ k
(∀α.⇃τ1 ⇂Υ → ⇃τ2 ⇂Υ )j
⇃τ1 ⇂Υ [⇃τ ′ ⇂Υ /α]
⇃e′′ ⇂Υ [⇃τ ′ ⇂Υ /α]

′

By definition of unboxing, τ ′′ = ⇃τ ⇂Υ . The proof of the
theorem above also showed that C; ̺ ⊢ τ1 , C; ̺ ⊢ τ ′ , and
C(lbl(τ ′ )) = C(̺(α)). By the rules for acceptability, clearly
C; ̺ ⊢ e′′ . By Lemma 20, τ1′′ = ⇃τ1′ ⇂Υ and e′′′ = ⇃e′′ [τ ′ /α]⇂Υ .
l
Putting that altogether, ρ′′′ (e′′′ ) = ⇃e′ ⇂Υ , as required.
• If (ρ, (boxτ ′ e)j ) 7−→ (ρ, (boxτ ′ e′ )j ) then: By definition of

acceptability C; ̺ ⊢ ρ and C; ̺ ⊢ e, so C; ̺ ⊢ (ρ, e). By
the typing rules, ⊢ ρ : Γ and ∅; Γ ⊢ e : τ ′′ for some Γ and
τ ′′ , so ⊢ (ρ, e) : τ ′′ . By the rules for consistency, Υ ⊢ ρ
and Υ ⊢ e, so Υ ⊢ (ρ, e). So by the induction hypothesis,
(⇃ρ⇂Υ , ⇃e⇂Υ ) 7−→∗ (⇃ρ⇂Υ , ⇃e′ ⇂Υ ).
If j ∈ Υ then:
By definition of unboxing
⇃(boxτ ′ e)j ⇂Υ = ⇃e⇂Υ
By definition of unboxing
j
⇃(boxτ ′ e′ ) ⇂Υ = ⇃e′ ⇂Υ
By induction
(⇃ρ⇂Υ , ⇃e⇂Υ ) 7−→∗ (⇃ρ⇂Υ , ⇃e′ ⇂Υ )

If j ∈ Υ then:
By definition of unboxing
k
k
⇃e⇂Υ = vt′ ′ where vt′ ′ = ⇃vt i ⇂Υ
By definition of reduction
k
k
(⇃ρ⇂Υ , vt′ ′ ) 7−→∗ (⇃ρ⇂Υ , vt′ ′ )
• If (ρ, (e1 [τ ′ ] e2 )j ) 7−→ (ρ, (e′1 [τ ′ ] e2 )j ) then:

18

2018/2/19

If j ∈
/ Υ then:
By definition of unboxing:
⇃(boxτ ′ e)j ⇂Υ
j
⇃(boxτ ′ e′ ) ⇂Υ

=
=

(box⇃τ ′ ⇂Υ ⇃e⇂Υ )j
j
(box⇃τ ′ ⇂Υ ⇃e′ ⇂Υ )

Hence by the induction hypothesis and Lemma 25 we have
that:
(⇃ρ⇂Υ , (box⇃τ ′ ⇂Υ ⇃e⇂Υ )j ) 7−→∗
j
(⇃ρ⇂Υ , (box⇃τ ′ ⇂Υ ⇃e′ ⇂Υ ) )
• If (ρ, (unbox e)j ) 7−→ (ρ, (unbox e′ )j ) then let i = lbl(e) and
Υ

i′ = lbl(e′ ). By Lemma 24 we have that i ≃ i′ . By the rules
for acceptability, C; ̺ ⊢ ρ and C; ̺ ⊢ e, so C; ̺ ⊢ (ρ, e).
By the typing rules, ⊢ ρ : Γ and ∅; Γ ⊢ e : τ ′ for some Γ
and τ ′ , so ⊢ (ρ, e) : τ ′ . By the rules for consistency, Υ ⊢ ρ
and Υ ⊢ e, so Υ ⊢ (ρ, e). So by the induction hypothesis,
(⇃ρ⇂Υ , ⇃e⇂Υ ) 7−→∗ (⇃ρ⇂Υ , ⇃e′ ⇂Υ ).
If i, i′ ∈ Υ then:
By definition of unboxing
⇃(unbox e)j ⇂Υ = ⇃e⇂Υ
By definition of unboxing
j
⇃(unbox e′ ) ⇂Υ = ⇃e′ ⇂Υ
By induction
(⇃ρ⇂Υ , ⇃e⇂Υ ) 7−→∗ (⇃ρ⇂Υ , ⇃e′ ⇂Υ )

By definition of unboxing
j
j
⇃ρ′ (v i ) ⇂Υ = ⇃ρ′ ⇂Υ (⇃v i ⇂Υ )
Unboxed value is a value, so by reduction rules
j
(⇃ρ⇂Υ , ⇃ρ′ ⇂Υ (⇃v i ⇂Υ ) ) 7−→ (⇃ρ⇂Υ , ⇃v i ⇂Υ )
To show preservation of consistency we need a type substitution
lemma.

• If Υ ⊢ τ ′ : r and C; ̺ ⊢ τ ′ then Υ ⊢ τ ′ [τ /α] : r.
• If Υ ⊢ e and C; ̺ ⊢ e then Υ ⊢ e[τ /α].
• If Υ ⊢ ρ and C; ̺ ⊢ ρ then Υ ⊢ ρ[τ /α].

Proof: The proof is by simultaneous induction on the derivation
of Υ ⊢ τ ′ : t, Υ ⊢ e, and Υ ⊢ ρ. The cases for expressions and
environments are straight forward. Consider the cases for types:
• Case 1, τ ′ = αi : If τ = σ j then τ ′ [τ /α] = σ i . Since

C; ̺ ⊢ τ ′ , C(i) = C(̺(α)), so C(i) = C(j). By Lemmas 17
Υ

and 18, i ≃ j. Then by inspection of the rules, Υ ⊢ σ i : r as
Υ ⊢ σ j : r.
• Case 2, τ ′ = β i and α 6= β: Then τ ′ [τ /α] = τ ′ and the result

is immediate.
• Case 3, τ ′ = Bi : Then Υ ⊢ τ ′ : r is not possible.

j k

• If (ρ, (unbox hv i :τ i ) ) 7−→ (ρ, v i ) then:

• Case 4, τ ′ = (∀β.τ1 → τ2 )i : Then Υ ⊢ τ ′ [τ /α] : r, as

required.

If j ∈ Υ then:
By definition of unboxing

• Case 5, τ ′ = (box(τ ′′ ))i , i ∈ Υ: By the rule, Υ ⊢ τ ′′ : r.

j k

Assumption C; ̺ ⊢ τ ′ requires C; ̺ ⊢ τ ′′ . By the induction hypothesis, Υ ⊢ τ ′′ [τ /α] : r. By the consistency rules,
i
Υ ⊢ box(τ ′′ [τ /α]) : r. By definition of substitution, Υ ⊢
′′ i
box(τ ) [τ /α] : r, as required.

j

⇃(unbox hv i :τ i ) ⇂Υ = ⇃hv i :τ i ⇂Υ = ⇃v i ⇂Υ
So in zero steps
j k

(⇃ρ⇂Υ , ⇃(unbox hv i :τ i ) ⇂Υ ) 7−→∗ (⇃ρ⇂Υ , ⇃v i ⇂Υ )
If j ∈
/ Υ then:
By definition of unboxing

• Case 6, τ ′ = (box(τ ′′ ))i , i ∈
/ Υ: Then Υ ⊢ τ ′ [τ /α] : r, as

required.

j k

i

j

k

⇃(unbox hv :τ i ) ⇂Υ = (unbox ⇃hv :τ i ⇂Υ )
By definition of unboxing
j

j

• If (ρ, ρ′ (v i ) ) 7−→ (ρ, v i ) then:

Lemma 26
If C ⊢ Υ, Υ ⊢ τ : r, τ is not a type variable, and C(lbl(τ )) =
C(̺(α)) then:

If i, i′ ∈
/ Υ then:
By definition of unboxing
⇃(unbox e)j ⇂Υ = (unbox ⇃e⇂Υ )j
By definition of unboxing
j
j
⇃(unbox e′ ) ⇂Υ = (unbox ⇃e′ ⇂Υ )
By induction
(⇃ρ⇂Υ , ⇃e⇂Υ ) 7−→∗ (⇃ρ⇂Υ , ⇃e′ ⇂Υ )
By Lemma 25
(⇃ρ⇂Υ , ⇃(unbox e)j ⇂Υ ) 7−→∗
j
(⇃ρ⇂Υ , ⇃(unbox e′ ) ⇂Υ )

i

By definition of unboxing
i
i
⇃ρ′ (e1 ) ⇂Υ = ⇃ρ′ ⇂Υ (⇃e1 ⇂Υ )
By definition of unboxing
i
i
⇃ρ′ (e2 ) ⇂Υ = ⇃ρ′ ⇂Υ (⇃e2 ⇂Υ )
By induction
(⇃ρ′ ⇂Υ , ⇃e1 ⇂Υ ) 7−→∗ (⇃ρ′ ⇂Υ , ⇃e2 ⇂Υ )
By Lemma 25
i
i
(⇃ρ⇂Υ , ⇃ρ′ ⇂Υ (⇃e1 ⇂Υ ) ) 7−→∗ (⇃ρ⇂Υ , ⇃ρ′ ⇂Υ (⇃e2 ⇂Υ ) )

k

Lemma 27
If Υ ⊢ M1 , C ⊢ Υ, C; ̺ ⊢ M1 , ⊢ M1 : τ , and M1 7−→ M2 then
Υ ⊢ M2 .

j k

(unbox ⇃hv i :τ i ⇂Υ ) = (unbox h⇃v i ⇂Υ :⇃τ ⇂Υ i )
By definition of reduction
j k

(⇃ρ⇂Υ , (unbox h⇃v i ⇂Υ :⇃τ ⇂Υ i ) ) 7−→
(⇃ρ⇂Υ , ⇃v i ⇂Υ )
• If (ρ, ρ′ (e1 )i ) 7−→ (ρ, ρ′ (e2 )i ) then:

By the rules for acceptability, C; ̺ ⊢ ρ′ and C; ̺ ⊢ e1 , so
C; ̺ ⊢ (ρ′ , e1 ). By the typing rules, ⊢ ρ′ : Γ′ and ∅; Γ′ ⊢ e1 : τ
for some Γ′ , so ⊢ (ρ′ , e1 ) : τ . By the rules for consistency,
Υ ⊢ ρ′ and Υ ⊢ e1 , so Υ ⊢ (ρ′ , e1 ). So by the induction
hypothesis, (⇃ρ′ ⇂Υ , ⇃e1 ⇂Υ ) 7−→∗ (⇃ρ′ ⇂Υ , ⇃e2 ⇂Υ ).
19

Proof: The proof is by induction on the derivation of M1 7−→ M2 .
Let M1 = (ρ, e1 ) and M2 = (ρ, e2 ). By the rules for consistency,
Υ ⊢ ρ and Υ ⊢ e1 . The result follows if Υ ⊢ e2 . The typing rules
require ⊢ ρ : Γ and ∅; Γ ⊢ e1 : τ ′ for some Γ and τ ′ . Assumption
C; ̺ ⊢ M requires C; ̺ ⊢ ρ and C; ̺ ⊢ e1 . Consider the cases for
the last rule used (in the same order as the figure):
• (Variable) In this case: e1 = xi , e2 = v j , and x:τ ′ = v j ∈ ρ.

By Υ ⊢ ρ, Υ ⊢ v j , as required.

2018/2/19

• (Fix expression) In this case: e1 = (fix f [α](x:τ1 ):τ2 .e)i and

e2 = hρ, fix f [α](x:τ1 ):τ2 .eii . Then Υ ⊢ e1 requires Υ ⊢ e,
then since Υ ⊢ ρ, Υ ⊢ e2 , as required.
i j

• (Box expression) In this case: e1 = (boxτ v ) and e2 =
j

hv i :τ i . Then Υ ⊢ e1 requires Υ ⊢ v i , so Υ ⊢ e2 , as required.
• (Application left) In this case, we have e1 = (e3 [τ ] e4 )i ,

e2 = (e5 [τ ] e4 )i , and (ρ, e3 ) 7−→ (ρ, e5 ) is a subderivation.
Then Υ ⊢ e1 requires Υ ⊢ e3 , Υ ⊢ e4 , and Υ ⊢ τ : r;
∅; Γ ⊢ e1 : τ ′ requires ∅; Γ ⊢ e3 : τ ′′ for some τ ′′ ; C; ̺ ⊢ e1
requires C; ̺ ⊢ e3 . By the induction hypothesis, Υ ⊢ e5 , so by
the consistency rules, Υ ⊢ e2 , as required.

• (Application right) In this case: e1 = (e3 [τ ] e4 )i , e2 =

(e3 [τ ] e5 )i , and (ρ, e3 ) 7−→ (ρ, e5 ) is a subderivation. Then
Υ ⊢ e1 requires Υ ⊢ e3 , Υ ⊢ e4 , and Υ ⊢ τ : r; ∅; Γ ⊢ e1 : τ ′
requires ∅; Γ ⊢ e4 : τ ′′ for some τ ′′ ; C; ̺ ⊢ e1 requires
C; ̺ ⊢ e4 . By the induction hypothesis, Υ ⊢ e5 , so by the
consistency rules, Υ ⊢ e2 , as required.

• (Application beta) In this case:

e1
v1
e2
ρ′′
τ′
τ1′

=
=
=
=
=
=

k

(v1 i [τ ] v2 j )
hρ′ , fix f [α](x:τ1 ):τ2 .ei
k
ρ′′ (e[τ /α])
′
′
ρ , f :τ = v1 i , x:τ1′ = v2 j
(∀α.τ1 → τ2 )i
τ1 [τ /α]

By Υ ⊢ e1 and the rules for consistency, Υ ⊢ v1 i , Υ ⊢ ρ′ ,
Υ ⊢ e, Υ ⊢ τ : r, and Υ ⊢ v2 j . Thus by the rules for
consistency, Υ ⊢ ρ′′ . By the typing rule ∅ ⊢ τ ′ wf , so τ ′
cannot be a type variable. Assumption C; ̺ ⊢ M requires
C; ̺ ⊢ e and, as in previous proofs, C(lbl(τ )) = C(̺(i)). By
Lemma 26, Υ ⊢ e[τ /α]. By the rules for consistency, Υ ⊢ e2 ,
as required.
• (Under box) Similar to application left.
• (Under unbox) Similar to appliction left.

By Theorem 1
⊢ M′ : τ′
By Lemma 15
C; ̺ ⊢ M ′
By Lemma 27
Υ ⊢ M′
By induction
⇃M ′ ⇂Υ 7−→∗ (⇃ρ⇂Υ , ⇃v i ⇂Υ )
By the defininition of many step reduction
⇃M ⇂Υ 7−→∗ (⇃ρ⇂Υ , ⇃v i ⇂Υ )
• In the operational semantics, there are six leaf reductions. Two

of them take expression forms to value forms, but otherwise
leave the term unchanged. One of the them takes unbox of box
of a value to that value. One of them takes a frame of a value
to that value. Thus if we measure a term by adding its size,
number of lambda expressions, and number of box expressions,
then this metric strictly decreases for these three leaf reductions.
Therefore, in any infinite reduction sequence, there must be
an infinite number of steps whose leaf reduction is a variable
reduction or an application beta reduction. Then observe in the
proof of Theorem 3 that the unboxing of a variable redex or
of an application beta redex will always take a step, and that
Lemma 25 preserves this. Thus the unboxing will also take an
infinite number of steps.
Theorem 4 shows that if two terms are related by reduction,
then their images under the unboxing function are also related by
the many step reduction relation given that the unboxing pair is
acceptable; and that if a term diverges under reduction, then its
image under the unboxing function also diverges. In other words,
for an acceptable analysis and an acceptable unboxing, the induced
unboxing function preserves the semantics of the original program
up to elimination of boxes. Since the semantics of the core language
only defines reduction steps that preserve GC safety, this theorem
implies that the image of a GC safe program under unboxing is also
GC safe.

j k

• (Unbox beta) In this case: e1 = (unbox hv i :τ i ) and e2 = v i .
i

5. Construction of an acceptable unboxing

Then Υ ⊢ e1 requires Υ ⊢ v , as required.
• (Under frame) Similar to application left.

2. If M 7−→∗ (ρ, v i ) in n steps, then by definition, M 7−→
M ′ and M ′ 7−→∗ (ρ, v i ) in n − 1 steps.
By Theorem 3
⇃M ⇂Υ 7−→ ⇃M ′ ⇂Υ

The previous section gives a declarative specification for when an
unboxing set Υ is correct but does not specify how such a set
might be chosen. In this section we give a simple algorithm for
constructing an acceptable unboxing given an arbitrary acceptable
flow analysis.
The idea behind the algorithm is that given a program and an
acceptable flow analysis for it, we use the results of the flow analysis to construct the connected components of the interprocedural flow graph of the program. All of the elements of a connected
component will then either be unboxed together, or not unboxed at
all. Any such choice of unboxing (as we will show) satisfies the
cache coherence property. The only remaining requirement is that
the choice of unboxing set be consistent, which is easily satisfied
by ensuring that any connected component which includes a type
passed to a polymorphic function is only unboxed if the unboxing
of the type argument still has traceability r. In the rest of the section, we make this informal algorithm concrete and show that the
choice of unboxing that it produces is in fact acceptable.
For the purposes of this section we ignore environments and the
j
intermediate forms ρ(e), hρ, fix f [α](x:τ1 ):τ2 .eij and hv i :ti .
These constructs are present in the language solely as mechanisms
to discuss the dynamic semantics—in this sense they can be thought
of as intermediate terms, rather than source terms. It is straightforward to incorporate these into the algorithm if desired.

20

2018/2/19

j

• (Frame return) In this case: e1 = ρ′ (v i ) and e2 = v i . Then

Υ ⊢ e1 requires Υ ⊢ v i , as required.

With these lemmas we can prove our semantics preservation
result.
Theorem 4 (Coherence)
• If ⊢ M : τ , C; ̺ ⊢ M , C ⊢ Υ, Υ ⊢ M , and M 7−→∗ (ρ, v i )
then ⇃M ⇂Υ 7−→∗ (⇃ρ⇂Υ , ⇃v i ⇂Υ ).
• If ⊢ M : τ , C; ̺ ⊢ M , C ⊢ Υ, Υ ⊢ M , and M 7−→ · · · then
⇃M ⇂Υ 7−→ · · · .
Proof:
• By induction on reduction derivations, using Theorem 3.

1. If M 7−→∗ (ρ, v i ) in zero steps, then the result follows
immediately.

Given a flow analysis (C, ̺) and program e such that C; ρ ⊢ e,
we define the induced undirected flow graph FG as an undirected
graph with a node for every label in C, and edges as follows:
• For every label i and every shape s ∈ C(i), we add an edge

between i and lbl(s).
The edges simply connect up each program point with all of its
reaching definitions.
Given a flow graph FG, we can find the connected components
in the usual way. Let CC be a mapping which maps labels to the
connected component in which they occur. Note that by definition
each label occurs in exactly one connected component. It is easy to
show that any connected component is cache consistent.
Lemma 28 (Cache consistency of a connected component)
Given any acceptable analysis (C, ̺) with induced flow graph FG ,
and any connected component S of FG , S is cache consistent: that
is, C ⊢ S .
Proof: To show that C ⊢ S we must show that ∀i, s : s ∈
S
C(i) =⇒ i ≃ lbl(s). But note that by the construction of
the induced flow graph FG, whenever s ∈ C(i) there is an edge
between i and lbl(s), and consequently by definition of a connected
component, i and lbl(s) must be in the same connected component.
Since every label occurs in exactly one connected component,
either both i and lbl(s) are in S or both are not in S. By definition
S

then, i ≃ lbl(s).
It is also easy to show that the union of any two disjoint cache
consistent sets is also cache consistent.
Lemma 29 (Cache consistency (unary) closure)
Given any acceptable analysis (C, ̺) and disjoint label sets S1 and
S2 , then if C ⊢ S1 and C ⊢ S2 then C ⊢ S1 ∪ S2
Proof: To show that C ⊢ S1 ∪ S2 we must show that ∀i, s : s ∈
S1 ∪S2

C(i) =⇒ i ≃ lbl(s). Consider an abitrary label i. If i is
not in S1 ∪ S2 , then we have that i is not in S1 and not in S2 , and
hence by assumption, lbl(s) is not in S1 and not in S2 , and hence
we have agreement. If i is in S1 ∪ S2 , then it must be in either S1 or
S1

S2 . WLOG, assume that i ∈ S1 . By assumption, i ≃ lbl(s), and so
lbl(s) ∈ S1 , and hence lbl(s) ∈ S1 ∪ S2 and we have agreement.
Consequently, we can show that any set consisting of a union of
connected components of the induced flow graph is cache consistent.
Lemma 30 (Cache consistency closure)
Given any acceptable analysis (C, ̺) with induced flow
S graph FG ,
and any set SS of connected components of FG , SS is cache
consistent.
Proof: By Lemma 28, each connected component is cache consistent. By definition, any two connected components are disjoint, and
so by Lemma 29 the union of any two connected components are
cache consistent, and are disjoint
S from any other connected component. The cache consistency of SS follows directly by induction.
5.1 The algorithm
Given the set of connected components for the induced flow graph,
the algorithm begins with an initial unboxing set Υ consisting of
the union of all of the connected components. By Lemma 30, we
have that C ⊢ Υ. The algorithm then proceeds by considering in
turn each application sub-term e1 [τ ]e2 as follows:

21

- For each sub-term of e of the form e1 [τ ]e2 :
- if lbl(τ ) ∈ Υ, and if Υ ⊢ τ : b, then:
- Υ ← Υ − CC(lbl(τ )).
That is, for any application for which the current unboxing results
in the type argument being unboxed to a non-reference type, we
remove the connected component for the type from the unboxing
set. Note that after removing a connected component from Υ,
the new unboxing set Υ is still cache consistent since it is still a
union of connected components (just a union of one less connected
component).
With the help of some technical lemmas, it is straightforward to
show that the final unboxing set Υ computed by the algorithm is an
acceptable unboxing for the program.
To begin with, we observe that if a type’s label is not in the unboxing set Υ, then it is consistent and its traceability is unchanged
by the unboxing.
Lemma 31 (Type consistency)
For any unboxing set Υ and type τ , if lbl(τ ) ∈
/ Υ then Υ ⊢ τ :
tr (τ ).
Proof: By inspection.
• (Variable) tr (αi ) = r, and Υ ⊢ αi : r.
• (Base type) tr (Bi ) = b, and Υ ⊢ Bi : b.
• (Fun type) tr (∀α.τ1 → τ2 i ) = r, and Υ ⊢ ∀α.τ1 → τ2 i : r.
• (Box type) tr (box(τ ′ )i ) = r, and by assumption i ∈
/ Υ, so we
i

have that Υ ⊢ box(τ ′ ) : r.
It is also the case that the consistent type judgement defines a
total function on types, and hence for any type we either have that
it is consistent at traceability r or that it is consistent at traceability
b.
Lemma 32 (Type consistency is a total function)
For any unboxing set Υ and type τ , either Υ ⊢ τ : b, or Υ ⊢ τ : r.
Proof: By induction on types. All of the cases follow immediately
i
except when τ = box(τ ′ ) and i ∈ Υ. In that case, by induction we
′
have that either Υ ⊢ τ : b, or Υ ⊢ τ ′ : r, and so by construction
either Υ ⊢ τ : b, or Υ ⊢ τ : r.
Theorem 5
If ∆; Γ ⊢ e : τ , C; ̺ ⊢ Γ, and C; ̺ ⊢ e and if Υ is the unboxing set
computed by the algorithm in this section, then Υ is an acceptable
unboxing for e. That is, C ⊢ Υ and Υ ⊢ e.
Proof: The conclusion that C ⊢ Υ follows almost immediately
from Lemma 30. The initial choice of Υ is a union of connected
components, and hence is cache consistent. At every step of the algorithm, we may remove a single connected component from Υ.
The result is still a union of connected components (since connected components are disjoint), and hence the result of removing
a connected component is still cache consistent by Lemma 30.
The conclusion that Υ ⊢ e follows by induction on the structure
of the typing derivation.
• (Variable) In this case, e = xi , consistency is immediate.
• (Fix) In this case e = (fix f [α](x:τ1 ):τ2 .e′ )i . To get con-

sistency, we must show that Υ ⊢ e′ . The last rule applied in
the typing judgement must have been the fix rule, and by its
premises we have that ∆ ⊢ ∀α.τ1 → τ2 i wf (1), and that

2018/2/19

∆, α; Γ, f :∀α.τ1 → τ2 i , x:τ1 ⊢ e′ : τ2 (2). The last rule applied in the acceptable analysis judgement must also have been
the fix rule, and by its premises we have that C; ̺ ⊢ e′ (3).
To apply the induction hypothesis, we need (1), (3), and that
C; ̺ ⊢ Γ, f :∀α.τ1 → τ2 i , x:τ1 (4). To show (4), it is sufficient
to show that:
̺(f ) = i which is a premise of the acceptable analysis
derivation

⊢ (Γ ⇒ e : τ ) wf
∅ ⊢ Γ wf

⊢ (Γ ⇒ e : τ ) wf
C; ̺ ⊢ (Γ ⇒ e : τ )

C; ̺ ⊢ ∀α.τ1 → τ2 i which is a premise of the acceptable
analysis derivation

C; ̺ ⊢s Γ

̺(x) = lbl(τ1 ) which is a premise of the acceptable analysis derivation
C; ̺ ⊢ τ1 which is a sub-premise of the derivation of
C; ̺ ⊢ ∀α.τ1 → τ2 i .

we need that Υ ⊢ e1 (1), Υ ⊢ e2 (2), and Υ ⊢ τ : r
(3). Inverting the typing derivation and the acceptable analysis
derivation immediately gives us the premises we need to apply
the induction hypothesis to get (1) and (2). To prove (3), note
that a premise of the typing derivation gives us that tr (τ ) = r
(4). If lbl(τ ) ∈
/ Υ, then by Lemma 31 we have that Υ ⊢ τ :
tr (τ ) and so by (4) we’re done. If lbl(τ ) ∈ Υ, then by the
definition of the algorithm, we must have that Υ ⊢ τ : b does
not hold (since otherwise the algorithm would have removed
the connected component containing lbl(τ ) from Υ), and so by
Lemma 32 we must have that Υ ⊢ τ : r and we’re done.
• (Box) All of the premises need to apply the induction hypothe-

sis are available immediately by inverting the typing derivation
and the acceptable analysis derivation.

C; ̺ ⊢s τ

⇃(Γ ⇒ e : τ )⇂Υ
⇃(Γ ⇒ e : τ )⇂Υ = (Γ ⇒ ⇃e⇂Υ : τ )
Υ ⊢ τ not unboxed
i∈
/Υ

i∈
/Υ
i

i

Υ ⊢ α not unboxed

Υ ⊢ B not unboxed

i∈
/Υ

Υ ⊢ τ2 not unboxed

Υ ⊢ τ1 not unboxed

Υ ⊢ (∀α.τ1 → τ2 )i not unboxed
i∈
/ Υ Υ ⊢ τ not unboxed
Υ ⊢ box(τ )i not unboxed
Υ ⊢ Γ not unboxed
∀1 ≤ j ≤ n : Υ ⊢ τj not unboxed

• (Unbox) All of the premises need to apply the induction hypoth-

esis are available immediately by inverting the typing derivation
and the acceptable analysis derivation.

C; ̺ ⊢s e

C; ̺ ⊢ (Γ ⇒ e : τ )

So by (1), (3), and (4), we have by induction that Υ ⊢ e′ .
• (Application) In this case e = (e1 [τ ]e2 )i . To prove consistency,

∅; Γ ⊢ e : τ

Υ ⊢ x1 :τ1 , . . . , xn :τn not unboxed
Υ ⊢ (Γ ⇒ e : τ )

• (Constant) Follows immediately.

Υ ⊢ Γ not unboxed
Thus we have shown by construction that the specification defined in Section 4 is a useful one in the sense that it is satisfiable.

Υ⊢e

Υ ⊢ τ not unboxed

Υ ⊢ (Γ ⇒ e : τ )
Figure 10. Judgements for modules

6. Open Terms
The paper so far has considered whole-program optimization and
proved that unboxing in that setting is correct. We would like to
be able to optimize program fragments where we have part of the
program but know nothing about the rest of the program. Such
a setting adds one more correctness criteria—since we are not
optimizing the rest of the program, anything that flows across the
boundary to or from the rest of the program must remain as boxed
as it originally was. We can ensure this requirement by simply
requiring that nothing on the boundary is in the unboxing set. This
section formalizes these ideas and proves them correct.
For our purposes, a program fragment is a module, which is
a triple (Γ ⇒ e : τ ). Γ specifies the imports of the module, e
specifies the body of the module, which exports only one thing—
the value that e evaluates to, and τ specifies the type of the export.
We wish to optimize modules without making any assumptions
about the code that the module is linked to. In particular that means
we cannot unbox any of the imports nor unbox anything exported.
This requirement can be achieved by not unboxing any subterm of
any type in Γ nor in τ .
We can extend the definitions of well typedness, acceptability of
flow analysis, unboxing, and consistency of unboxing to modules,

22

C; ̺ ⊢s τ
s ∈ C(i)

C(̺(α)) = C(i)
s

i

C; ̺ ⊢ α
C; ̺ ⊢s e
C; ̺ ⊢s box(τ )i

C; ̺ ⊢s e (boxtr (τ ) lbl(e))iv ∈ C(i)
C; ̺ ⊢s (boxτ e)i

C; ̺ ⊢s box(τ )i

C; ̺ ⊢s v j

(boxtr (τ ) j)iv ∈ C(i)
i

C; ̺ ⊢s hv j :τ i

Figure 11. Stronger Analysis

2018/2/19

and the formal judgements appear in Figure 10. The acceptability
of a flow analysis for modules is stronger than that for programs.
The rules for type variables, box expressions, and box values are
replaced with those in Figure 11, the other rules remain the same.
The rules for boxes require a more precise shape in the cache, any
actual flow analysis would use such a shape, so this requirement
is not a burden. The rules for programs are weaker as the stronger
conditions are not closed under reduction whereas the weaker conditions are. The stronger condition for type variables is required to
ensure consistency for type variables, and is also not a burden.
The goal is to show that unboxing is correct for modules. A
suitable notion of correctness is that a module and its unboxing
are contextually equivalent. Rather than define contextual equivalence directly, we will use a notion that is usually proven equivalent
to contextually equivalence as our definition. Namely, two expressions are equivalent if in any environment that closes them and any
elimination context for their type they are observable equivalent
then they are contextually equivalent. The formal definition is in
Figure 12.
The strategy is that we will take the context and alpha vary it and
relabel it so that it is sufficiently distinct from the module. Then we
will argue that we can modify the flow analysis and unboxing to
cover the context without unboxing any of it. Then by coherence
the module in context will behave the same as the unboxing of the
module in context, which because the context is not unboxed, will
act the same as the unboxed module in context.
First we formalize and prove that the operational semantics is
insensitive to the alpha variant and labels used. Let x ∼s y mean
that x and y are alpha variants and possibly relabelled.
Lemma 33
If M1 ∼s M2 and M1 7−→ M3 then there exists M4 such that
M3 ∼s M4 and M2 7−→ M4 .
Proof: The proof is by a straight forward induction on the derivation of M1 7−→ M3 .
Next we prove three lemmas about unboxing preservation. In
the first two we show that something’s unboxing is that something
because either the not unboxed judgement (the first lemma) or the
labels in the something are not in the unboxing set (the second
lemma). In the third we show the unboxing of an expression is the
same if the unboxing set is the same on the labels in the expression.
To state and prove these and subsequent lemmas we need a function
to return all the labels in an expressions, type, or environment. It is
defined in Figure 13.
Lemma 34
• If Υ ⊢ τ not unboxed then ⇃τ ⇂Υ = τ .
• If Υ ⊢ Γ not unboxed then ⇃Γ⇂Υ = Γ.
Proof:

• If Γ = x1 :τ1 , . . . , xn :τn then: Υ ⊢ Γ not unboxed requires

Υ ⊢ τj not unboxed for 1 ≤ j ≤ n. So by the first item,
⇃τj ⇂Υ = τj for 1 ≤ j ≤ n. Then by definition, ⇃Γ⇂Υ = Γ, as
required.

Lemma 35
• If lbls(ρ) ∩ Υ = ∅ then ⇃ρ⇂Υ = ρ.
• If lbls(E) ∩ Υ = ∅ then ⇃E⇂Υ = E .
Proof: The proof is a straight forward induction on the structure
of ρ and E.
Lemma 36
If Υ1 ∩ lbls(e) = Υ2 ∩ lbls(e) then ⇃e⇂Υ1 = ⇃e⇂Υ2 .
Proof: The proof is a staight forward induction on the structure of
e.
Next we state and prove our main technical lemma. This lemma
states that we can rewrite the context and flow analysis to have
certain desirable properties, namely that the flow analysis covers
the context and the module, that the context is not unboxed, that
the module is unboxed as before, and the unboxing set and flow
analysis remain consistent and consistent with the module and
context.
Lemma 37
If:
∅ ⊢ Γ wf
∅; Γ ⊢ e : τ
C; ̺ ⊢ Γ
C; ̺ ⊢ e
C; ̺ ⊢ τ
C⊢Υ
Υ ⊢ Γ not unboxed
Υ⊢e
Υ ⊢ τ not unboxed
⊢ρ:Γ
Γ ⊢ E : Bi hτ i

then there exists ρ′ , E ′ , C′ , ̺′ , and Υ′ such that:
ρ ∼s ρ ′
E ∼s E ′
⊢ ρ′ : Γ
Γ ⊢ E ′ : Bj hτ i
C′ ; ̺′ ⊢ (ρ′ , E ′ hei)
C′ ⊢ Υ′
Υ′ ⊢ (ρ′ , E ′ hei)
lbls(ρ′ ) ∩ Υ′ = ∅
lbls(E ′ ) ∩ Υ′ = ∅
Υ ∩ lbls(e) = Υ′ ∩ lbls(e)

• The proof is by induction on the structure of τ . Consider the

Case 4, τ = box(τ ′ ) : Then Υ ⊢ τ not unboxed requires
i∈
/ Υ and Υ ⊢ τ ′ not unboxed . By the induction hypothesis, ⇃τ ′ ⇂Υ = τ ′ . By definition, ⇃τ ⇂Υ = τ , as required.

Proof: Let V be the set of variables that occur in e. Let A be the
set of type variables that occur in Γ, e, or τ . Both these sets are
finite.
The derivation of C; ̺ ⊢ Γ, C; ̺ ⊢ e, and C; ̺ ⊢ τ will for each
type that is not a type variable require a particular type shape with
some label on it in the cache of the label of that type, similarly for
each box expression and box value require a box shape with some
label of its contents in the cache. Let L be one such label for each
such type and such box as well as ̺(V )∪̺(A)∪lbls(Γ)∪lbls(e)∪
lbls(τ ). Note that L is a finite set.
Let ̺′ be ̺ on V and A and on every other variable or type
variable let it map to a fresh label (distinct from each other and

23

2018/2/19

cases:
Case 1, τ = αi : Then by definition ⇃τ ⇂Υ = τ , as required.
Case 2, τ = Bi : Then by definition ⇃τ ⇂Υ = τ , as required.
Case 3, τ = (∀α.τ1 → τ2 )i : Then Υ ⊢ τ not unboxed
requires Υ ⊢ τ1 not unboxed and Υ ⊢ τ2 not unboxed .
By the induction hypothesis, ⇃τ1 ⇂Υ = τ1 and ⇃τ2 ⇂Υ = τ2 .
By definition, ⇃τ ⇂Υ = τ , as required.
i

E ::= hi | (E[τ ] e)i | (unbox E)i

Γ ⊢ hi : τ hτ i
Γ ⊢ E : (∀α.τ1 → τ2 )j hτ i ∅ ⊢ τ wf

tr (τ ) = r

∅; Γ ⊢ e : τ1′

⊢ τ1 [τ /α] = τ1′

Γ ⊢ (E[τ ] e)i : τ2 [τ /α]hτ i
j

Γ ⊢ E : box(τ ′ ) hτ i
Γ ⊢ (unbox E)i : τ ′ hτ i
obs

M1 ≡ M2
Γ ⊢ e1 ≡ e2 : τ

def
def

=
=

(∀c, i : (M1 7−→∗ ci ⇔ M2 7−→∗ ci )) ∧ (M1 7−→ · · · ⇔ M2 7−→ · · · )
∅; Γ ⊢ e1 : τ ∧ ∅; Γ ⊢ e2 : τ ∧

⊢ (Γ1 ⇒ e1 : τ1 ) ≡ (Γ2 ⇒ e2 : τ2 )

def

∀ρ, E : ⊢ ρ : Γ ∧ Γ ⊢ E : Bi hτ i =⇒ (ρ, Che1 i) ≡ (ρ, Che2 i)
Γ1 = Γ2 ∧ τ1 = τ2 ∧ (Γ1 ⊢ e1 ≡ e2 : τ1 )

obs

=

Figure 12. Contextual Equivalence
lbls(σ i )
lbls(α)
lbls(B)
lbls(∀α.τ1 → τ2 )
lbls(box(τ ))
lbls(mi )
lbls(v i )
lbls(x)
lbls(fix f [α](x:τ1 ):τ2 .e)
lbls(e1 [τ ] e2 )
lbls(boxτ e)
lbls(unbox e)
lbls(ρ(e))
lbls(c)
lbls(hρ, fix f [α](x:τ1 ):τ2 .ei)
lbls(hv i :τ i)
lbls(x1 :τ1 = v1 i1 , . . . , xn :τn = vn in )

=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=

{i} ∪ lbls(σ)
∅
∅
lbls(τ1 ) ∪ lbls(τ2 )
lbls(τ )
{i} ∪ lbls(m)
{i} ∪ lbls(v)
∅
lbls(τ1 ) ∪ lbls(τ2 ) ∪ lbls(e)
lbls(e1 ) ∪ lbls(τ ) ∪ lbls(e2 )
lbls(τ ) ∪ lbls(e)
lbls(e)
lbls(ρ) ∪ lbls(e)
∅
lbls(ρ) ∪ lbls(τ1 ) ∪ lbls(τ2 ) ∪ lbls(e)
lbls(τ ) ∪ lbls(v i )
∪1≤i≤n lbls(τj ) ∪ lbls(vj ij )

Figure 13. The labels in an type, expression, or environment
from L). Define:

{s | s ∈ C(i) ∧ lbls(s) ⊆ L}
C′′ (i) =
∅

• (Application) In this case e = (e1 [τ ] e2 )i , C; ̺ ⊢ e1 , C; ̺ ⊢

i∈L
i∈
/L

Claim: C′′ ; ̺′ ⊢ Γ, C′′ ; ̺′ ⊢ e, and C′′ ; ̺′ ⊢ τ . The proof is by
induction on the derivation, consider the last rule used:
• (Variable) In this case e = xi and C(̺(x)) ⊆ C(̺(x)).

τ , C; ̺ ⊢ e2 , and funC (lbl(e1 ), lbl(τ ), lbl(e2 ), i). By the
induction hypothesis, C′ ; ̺′ ⊢ e1 , C′ ; ̺′ ⊢ τ , and C′ ; ̺′ ⊢ e2 .
Since lbl(e1 ) ∈ L, lbl(τ ) ∈ L, lbl(e2 ) ∈ L, and i ∈ L, it is
easy to see that funC (lbl(e1 ), lbl(τ ), lbl(e2 ), i) (for C′′ ). Thus
by the same rule, C′′ ; ̺′ ⊢ e, as required.
• Other cases are similar . . .

′

Since x ∈ V , ̺ (x) = ̺(x) and ̺(x) ∈ L. Also i ∈ L.
Therefore, C′′ (̺′ (x)) ⊆ C′′ (i), as required. Thus by the same
rule, C′′ ; ̺′ ⊢ e, as required.
̺(f ) = i, ̺(x) = lbl(τ1 ), C; ̺ ⊢ (∀α.τ1 → τ2 )i , C; ̺ ⊢ e′ ,
∈
and (∀̺(α).lbl(τ1 ) → lbl(e′ ))v C(i). Since f, x ∈ V and α ∈
′
′
A, ̺ (f ) = ̺(f ), ̺ (x) = ̺(x), ̺′ (α) = ̺(α), and ̺(α) ∈ L.
By the induction hypothesis, C′′ ; ̺′ ⊢ (∀α.τ1 → τ2 )i and
C′′ ; ̺′ ⊢ e′ . Since ̺′ (α) ∈ L, lbl(τ1 ) ∈ L, lbl(e) ∈ L, and
∈
i ∈ L, (∀̺′ (α).lbl(τ1 ) → lbl(e′ ))v C′′ (i). Thus by the same
rule, C′′ ; ̺′ ⊢ e, as required.

Let A′ be the set of type variables that appear in Γ and τ . We
construct ρ′ and E ′ as alpha variants and relabellings of ρ and E
as follows. Since ⊢ ρ : Γ, ρ contains Γ, so we keep that part
the same. Type variables that are in A′ we keep the same. All
other type variables and variables we pick an alpha variant that is
fresh (distinct from each other and from A respectively V ). The
outermost label on types on variables we relabel to the binding label
for that variable. All other labels we relabel to be fresh. Clearly
ρ ∼s ρ′ and E ∼s E ′ .
Claim: ⊢ ρ′ : Γ and Γ ⊢ E ′ : Bj hτ i for some j. The proof is a
straight forward induction on the structure of ρ′ and E ′ .

24

2018/2/19

• (Fix expression) In this case e = (fix f [α](x:τ1 ):τ2 .e′ )i ,

Now we need to build a C′ such that C′ ; ̺′ ⊢ (ρ′ , E ′ hei). We
start from C′′ . First we add into the caches, shapes required directly
for the rules for C′ ; ̺′ ⊢ ρ′ and C′ ; ̺′ ⊢ E ′ (such things are already
there for e). In the case of types we add shapes using the label of
the type as the label of the shape. In the case of box expressions
and values we use the label of the contents of the box as the label
of the contents of the shape. What remains is a bunch of subset and
equalty constraints between cache entries, so we pick C′ to be the
smallest larger cache that satisfies these constraints. Clearly such a
C′ exists and by construction, C′ ; ̺′ ⊢ (ρ′ , E ′ hei).
Set Υ′ = Υ ∩ L. Clearly, Υ ∩ lbls(e) = Υ′ ∩ lbls(e) as
lbls(e) ⊆ L. By construction, the labels of ρ′ and E ′ are in the
labels of Γ or τ or are not in L. Since Υ ⊢ Γ not unboxed and
Υ ⊢ τ not unboxed , the labels of Γ and τ are not in Υ. Therefore,
lbls(Γ) ∩ Υ′ = ∅ and lbls(τ ) ∩ Υ′ = ∅. In fact, if A′′ is a set of
type variables in ρ′ and E ′ then ̺′ (A′′ ) ∩ Υ′ = ∅ too.
Claim: any flow from the interface to a boxC (i, j) condition has
a box type at the interface (**), and similarly for funC (i, j, k, l).
The proof is by induction on the flow conditions noting that in all
cases the two end points have the same type.
Claim: C′ ⊢ Υ′ . Let s and i be such that s ∈ C′ (i). If s ∈ C′′ (i)
then s ∈ C(i), i ∈ L, and lbls(s) ⊆ L, and in particular,
Υ

lbl(s) ∈ L. Since C ⊢ Υ, i ≃ lbl(s). Since Υ′ = Υ ∩ L,
Υ′

i ∈ L, and lbl(s) ∈ L, i ≃ lbl(s), as required. Otherwise, we
claim that i, lbl(s) ∈
/ Υ′ . Let LC = lbls(ρ′ ) ∪ lbls(E ′ ) ∪ ̺′ (A′′ ),
LI = lbls(Γ) ∪ lbls(τ ), LM = L − LC , and LA = LC ∪ L.
First notice that C′′ has entries only for labels in L and with shapes
whose labels are in L. The first part of computing C′ added shapes
to cache entries for labels in LC with shapes whose labels are in
LC . The second part of computing C′ only propagates existing
shapes from one cache entry to another, and only from/to cache
entries in LA or in labels in shapes in the cache entries. Thus,
the cache entries of C′ are only for LA with shapes with labels
in LA . If lbl(s) ∈ LC then by previous argument lbl(s) ∈
/ Υ′ , as
required. If lbl(s) ∈ LM then we will show that s ∈ C′′ (j) for
some j ∈ LI . Then s ∈ C(j), and since C ⊢ Υ and j ∈
/ Υ,
lbl(s) ∈
/ Υ so lbl(s) ∈
/ Υ′ , as required. If i ∈ LC then by
previous argument i ∈
/ Υ′ , as required. If i ∈ LM then we will
show that C′′ (j) ⊆ C′′ (i) for some j ∈ LI . Then since C′′ (j)
is inhabited because it labels a type checked in C′′ ; ̺′ ⊢ Γ or
C′′ ; ̺′ ⊢ τ , and since that required type shape has labels in L,
∅ =
6 C(j) ⊆ C(i). Then since C ⊢ Υ and j ∈
/ Υ, i ∈
/ Υ, so
i ∈
/ Υ′ , as required. It remains to show the two conditions we
claimed. Since C′ was computed using a least fixed point, we prove
these claims by induction on when s was added to C′ (i). Consider
the cases:
• Case 1, s was added to i because s ∈ C′ (j), s ∈
/ C′ (i),

and C′ (j) ⊆ C(i) is required by the rules for variables, box
expressions, frames, box values, or environments. In this case, i
and j have to come from the same term, that is, either i, j ∈ LC
or i, j ∈ L. If lbl(s) ∈ LM then s must have been added to
C(j) previously in the second phase of constructing C′ , so by
the induction hypothesis, lbl(s) ∈ C′′ (k) for some k ∈ LI .
If i ∈ LM then j ∈ L. First note that the condition on j
and i is also required to show that C′′ ; ̺′ ⊢ Γ, C′′ ; ̺′ ⊢ e,
or C′′ ; ̺′ ⊢ τ , so C′′ (j) ⊆ C′′ (i). If j ∈ LI then we have
what we need. Otherwise j ∈ LM , so s was added to C′ (j)
previously in the second phase of constructing C′ (j), so by the
induction hypothesis, C′′ (k) ⊆ C′′ (j) for some k ∈ LI . Then
C′′ (k) ⊆ C′′ (i), as required.

• Case 3, s was added to i because boxC (j, i) is required, either
j′

j′

(boxt i′ )v ∈ C′ (j) or (box i′ )t ∈ C′ (j), and s was already
in C(i′ ). In this case, i and j have to come from the same term,
that is, either i, j ∈ LC or i, j ∈ L. Note that the labels in
any shape under consideration come from the same term, that
is, either they are all in L or they are all in LC .
If lbl(s) ∈ LM then:
− If s was added to C′ (i′ ) previously in the second phase
of constructing C′ then by the induction hypothesis,
s ∈ C′′ (k) for some k ∈ LI .
− Otherwise s ∈ C′′ (i′ ) and i′ , j ′ ∈ L. Since s was not
already in C′ (i) then the box shape was added to C′ (j)
previously in the second phase of constructing C′ , so by
the induction hypothesis, the box shape is in C′′ (k) for
some k ∈ LI . By (**), k labels a box type. By the rules
for acceptability, boxC (k, k′ ) for C′′ for some k′ ∈ LI .
Thus, C′′ (i′ ) ⊆ C′′ (k′ ). Thus s ∈ C′′ (k′ ), as required.
If i ∈ LM then j ∈ L and boxC (j, i) holds for C′′ .
− If the box shape was added to C′ (j) previously in the
second phase of the constructing C′ then by the induction hypothesis, C′′ (k) ⊆ C′′ (j) for some k ∈ LI .
By (**), k labels a box type. Then by the rules for acj ′′
ceptability, (box i′′ )t ∈ C′′ (k) for some i′′ ∈ LI , so
′′
j
(box i′′ )t ∈ C′′ (j). By boxC (j, i), C′′ (i′′ ) ⊆ C′′ (i),
as required.
− Otherwise, the box shape was in C′′ (j) and i′ , j ′ ∈ L.
By boxC (j, i), C′′ (i′ ) ⊆ C′′ (i). Since s was not already
in C′ (i) then it was previously added to C′ (i′ ) in the
second phase of constructing C′ , so by the induction
hypothesis, C′′ (k) ⊆ C′′ (i′ ) for some k ∈ LI . Then
by transitivity C′′ (k) ⊆ C′′ (i), as required.
• Case 4, s was added because a funC (j1 , j2 , j3 , j4 ) is required.

Similar to Case 3.
Claim: Υ′ ⊢ (ρ′ , E ′ hei). The proof is by a straight forward
induction on the structure of (ρ′ , E ′ hei). The only interesting case
is application. In that case, we have (e1 [τ ] e2 )i . By the induction
hypothesis we get Υ′ ⊢ e1 and Υ′ ⊢ e2 . We just need to show that
Υ′ ⊢ τ : r. If the application came from e then since the labels
of τ are in L, the result follows from Υ ⊢ τ : r, which holds by
assumption (Υ ⊢ e). Otherwise, the labels of τ are not in Υ′ so
clearly Υ′ ⊢ τ tr (τ ). Then tr (τ ) = r holds by the typing rules.
We these definitions we can prove that unboxing for modules is
correct.

Theorem 6
If ⊢ (Γ ⇒ e : τ ) wf , C; ̺ ⊢ (Γ ⇒ e : τ ), C ⊢ Υ, and
Υ ⊢ (Γ ⇒ e : τ ) then ⊢ (Γ ⇒ e : τ ) ≡ ⇃(Γ ⇒ e : τ )⇂Υ .

by the rule for type variables, did not hold and s ∈ C(̺′ (α)).
Similar to Case 1.

Proof: By definition, ⇃(Γ ⇒ e : τ )⇂Υ = (Γ ⇒ ⇃e⇂Υ : τ ). Clearly
Γ = Γ and τ = τ , so it remains to show that Γ ⊢ e ≡ ⇃e⇂Υ : τ .
By ⊢ (Γ ⇒ e : τ ) wf , ∅ ⊢ Γ wf and Γ ⊢ e : τ . By
C; ̺ ⊢ (Γ ⇒ e : τ ), C; ̺ ⊢ Γ, C; ̺ ⊢ e, and C; ̺ ⊢ τ .
By Υ ⊢ (Γ ⇒ e : τ ), Υ ⊢ Γ not unboxed , Υ ⊢ e, and
Υ ⊢ τ not unboxed . By Theorem 1, ⇃Γ⇂Υ ⊢ ⇃e⇂Υ : ⇃τ ⇂Υ . By
Lemma 34, Γ ⊢ ⇃e⇂Υ : τ . Let ρ and E be such that ⊢ ρ : Γ and
Γ ⊢ E : Bi hτ i. Then by Lemma 37, there exists ρ′ , E ′ , C′ , ̺′ , and

25

2018/2/19

• Case 2, s was added to i because C(̺′ (α)) = C(i), required

Υ′ such that:
′

ρ ∼s ρ
E ∼s E ′
⊢ ρ′ : Γ
′
Γ ⊢ E ′ : Bi hτ i
C′ ; ̺′ ⊢ (ρ′ , E ′ hei)
C′ ⊢ Υ′
Υ′ ⊢ (ρ′ , E ′ hei)
lbls(ρ′ ) ∩ Υ′ = ∅
lbls(E ′ ) ∩ Υ′ = ∅
Υ ∩ lbls(e) = Υ′ ∩ lbls(e)
Since the operational semantics is deterministic, we just need to
show that (ρ, Eh⇃e⇂Υ i) matches (ρ, Ehei) in behaviour. There are
two cases:
• If (ρ, Ehei) 7−→∗ (ρ, cj ) then by Lemma 33, (ρ′ , E ′ hei) 7−→∗
′

(ρ′ , cj ) for some j ′ . By Theorem 4, ⇃(ρ′ , E ′ hei)⇂Υ′ 7−→∗
′
⇃(ρ′ , cj )⇂Υ′ . By both Lemma 35 and definition of unbox′
ing, (ρ′ , E ′ h⇃e⇂Υ′ i) 7−→∗ (ρ′ , cj ). Hence by Lemma 36,
′
(ρ′ , E ′ h⇃e⇂Υ i) 7−→∗ (ρ′ , cj ). Therefore by Lemma 33 again,
′′
(ρ, Eh⇃e⇂Υ i) 7−→∗ (ρ′ , cj ), for some j ′′ . It is not too hard to
′′
see that j = j , as required.
• If (ρ, Ehei) 7−→ · · · then by Lemma 33, (ρ′ , E ′ hei) 7−→

· · · . By Theorem 4, ⇃(ρ′ , E ′ hei)⇂Υ′ 7−→ · · · . By Lemma 35,
(ρ′ , E ′ h⇃e⇂Υ′ i) 7−→ · · · . By Lemma 36, (ρ′ , E ′ h⇃e⇂Υ i) 7−→
· · · . By Lemma 33, (ρ, Eh⇃e⇂Υ i) 7−→ · · · , as required.

of optimality explicitly does not correspond in any way to reduced
allocation or reduced instruction count and does not seem to provide uniform improvement over Leroy’s approach.
The MLton compiler [11] largely avoids the issue of a uniform
object representation by completely monomorphizing programs before compilation. This approach requires whole-program compilation. More limited monomorphization schemes could be considered
in an incremental compilation setting. Monomorphization does not
eliminate the need for boxing in the presence of dynamic type tests
or reflection. Just in time compilers (e.g. for .NET) may monomorphize dynamically at runtime.
The TIL compiler [1, 10] uses intensional type analysis in a
whole-program compiler to allow native data representations without committing to whole-program compilation. As with the Leroy
coercion approach, polymorphic uses of objects require conditionals and boxing coercions to be inserted at use sites, and consequently there is the potential to slow down, rather than speed up,
the program.
Serrano and Feeley [9] described a flow analysis for performing unboxing substantially similar in spirit to our approach. Their
algorithm attempts to find a monomorphic typing for a program
in which object representations have not been made explicit, which
they then use selectively to choose whether to use a uniform or nonuniform representation for each particular object. Their approach
differs in that they define a dedicated analysis rather than using a
generic reaching definitions analysis. They assume a conservative
garbage collector and hence do not need to account for the requirements of GC safety, and they do not prove a correctness result.

References
7. Related work

[1] R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Twenty-Second ACM Symposium on Principles of Programming Languages, pages 130–141, San Francisco, CA,
January 1995.

This paper provides a modular approach to showing correctness
of a realistic compiler optimization that rewrites the structure of
program data structures in significant ways. Our approach uses an
arbitrary inter-procedural reaching definitions analysis to eliminate
unnecessary heap allocation in an intermediate representation in
which object representation has been made explicit. Our optimization can be staged freely with other optimizations. Unlike any previous work that we are aware of, we account for correctness with
respect to the meta-data requirements of the garbage collector. For
presentational purposes, we have restricted our attention to the core
concern of GC safety, but additional issues such as value size, dynamic type tests, etc. are straightforward to incorporate.
There has been substantial previous work addressing the problem of unboxing. Peyton Jones [3] introduced an explicit distinction
between boxed and unboxed objects to provide a linguistic account
of unboxing, and hence to allow a high-level compiler to locally
eliminate unboxes of syntactically apparent box introduction operations. Leroy [4] defined a type-driven approach to adding coercions into and out of specialized representations. The type driven
translation represented monomorphic objects natively (unboxed, in
our terminology), and then introduced wrappers to coerce polymorphic uses into an appropriate form. To a first-order approximation,
instead of boxing at definition sites this approach boxes objects
at polymorphic use sites. This style of approach has the problem
that it is not necessarily beneficial, since allocation is introduced
in places where it would not otherwise be present. This is reflected
in the slowdowns observed on some benchmarks described in the
original paper. This approach also has the potential to introduce
space leaks. In a later paper [5] Leroy argued that a simple untyped
approach gives better and more predictable results.
Henglein and Jørgensen [2] defined a formal notion of optimality for local unboxings and gave two different choices of coercion
placements that satisfy their notion of optimality. Their definition

[10] D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee.
Til: a type-directed, optimizing compiler for ml. SIGPLAN Not., 39:
554–567, April 2004. ISSN 0362-1340.

26

2018/2/19

[2] F. Henglein and J. Jørgensen. Formally optimal boxing. In Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of
programming languages, POPL ’94, pages 213–226, New York, NY,
USA, 1994. ACM. ISBN 0-89791-636-0.
[3] S. L. P. Jones and J. Launchbury. Unboxed values as first class citizens
in a non-strict functional language. In Proceedings of the 5th ACM
conference on Functional programming languages and computer architecture, pages 636–666. Springer-Verlag New York, Inc., 1991.
[4] X. Leroy. Unboxed objects and polymorphic typing. In Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of
programming languages, POPL ’92, pages 177–188, New York, NY,
USA, 1992. ACM. ISBN 0-89791-453-8.
[5] X. Leroy. The effectiveness of type-based unboxing. Technical report,
Boston College, Computer Science Department, 1997.
[6] G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to
typed assembly language. ACM Trans. Program. Lang. Syst., 21:527–
568, May 1999. ISSN 0164-0925.
[7] F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program
Analysis. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1999.
ISBN 3540654100.
[8] L. Petersen and N. Glew. GC-safe interprocedural unboxing. In Proceedings of the 21st International Conference on Compiler Construction, CC 2012, 2012.
[9] M. Serrano and M. Feeley. Storage use analysis and its applications.
In Proceedings of the first ACM SIGPLAN international conference
on Functional programming, ICFP ’96, pages 50–61, New York, NY,
USA, 1996. ACM. ISBN 0-89791-770-7.

[11] S. Weeks. Whole-program compilation in MLton. In Proceedings of
the 2006 workshop on ML, ML ’06, pages 1–1, New York, NY, USA,
2006. ACM. ISBN 1-59593-483-9.

27

2018/2/19

