1

A Simple Soundness Proof for Dependent Object Types

arXiv:1706.03814v1 [cs.PL] 12 Jun 2017

MARIANNA RAPOPORT, IFAZ KABIR, PAUL HE, and ONDŘEJ LHOTÁK, University of Waterloo
Dependent Object Types (DOT) is intended to be a core calculus for modelling Scala. Its distinguishing feature is abstract type
members, fields in objects that hold types rather than values. Proving soundness of DOT has been surprisingly challenging,
and existing proofs are complicated, and reason about multiple concepts at the same time (e.g. types, values, evaluation).
To serve as a core calculus for Scala, DOT should be easy to experiment with and extend, and therefore its soundness proof
needs to be easy to modify.
This paper presents a simple and modular proof strategy for reasoning in DOT. The strategy separates reasoning about
types from other concerns. It is centred around a theorem that connects the full DOT type system to a restricted variant
in which the challenges and paradoxes caused by abstract type members are eliminated. Almost all reasoning in the proof
is done in the intuitive world of this restricted type system. Once we have the necessary results about types, we observe
that the other aspects of DOT are mostly standard and can be incorporated into a soundness proof using familiar techniques
known from other calculi.
Our paper comes with a machine-verified version of the proof in Coq.

1

INTRODUCTION

2016 was an exciting year for those who desire a formalism to understand and reason about the unique features
of Scala’s type system. Mechanized soundness results were published for the Dependent Object Types (DOT)
calculus and other related calculi (Amin et al. 2016; Amin and Rompf 2017; Rompf and Amin 2016). These proofs
were the culmination of an elusive search that spanned more than ten years. The chief subtleties and paradoxes
inherent in DOT and the Scala type system, which made the proof so challenging, were documented along the
way (Amin et al. 2012, 2014).
Since the DOT calculus exhibits such subtle and counterintuitive behaviour, and since the proofs are the result
of such a long effort, it is to be expected that the proofs must be complicated. The calculus is dependently typed,
so it is not surprising that the lemmas that make up the proofs reason about tricky relationships between types
and values. In some contexts, the type system admits typings that seem just plain wrong, and give no hope for
soundness, so it seems necessary to have lemmas that reason simultaneously about the intricate properties of
values, types, and the environments that they inhabit.
A core calculus needs to be easy to extend. Some extensions of DOT are necessary even just to model essential
Scala features. As a prominent example, types in Scala may depend on paths x .a 1 .···.an .A (where x is a variable,
ai are fields, and A is a type member), but types in the existing DOT calculi can depend only directly on variables
(x .A). Path-dependent types are needed to model essential features such as classes and traits (as members nested
in objects and packages) and the famous cake pattern (Odersky and Zenger 2005). Another important Scala
feature to be studied in DOT are implicit parameters. Moreover, language modifications and extensions are
the raison d’être of a core calculus. DOT enables designers to experiment with exciting new features that can
be added to Scala, to tweak them and reason about their properties before attempting to integrate them in the
compiler with the complexity of the full Scala language.
The complexity of the proof is a hindrance to such extension and experimentation. Over the past ten years,
DOT has been designed and re-designed to be just right, so that the brilliant lemmas that ensure its soundness
hold and can be proven. When the DOT calculus is disrupted by a modification, it is difficult to predict which
parts of the proof will be affected. Experimenting with modifications to DOT is difficult because each tweak
requires many lemmas to be re-proven.

1:2

• Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták

Our goal in this paper is a soundness proof that is simpler, more modular, and more intuitive. We aim to
separate the concepts of types, values, and operational semantics, and to reason about one concept at a time.
Then, if a language extension modifies only one concept, such as typing, the necessary changes are localized to
the parts of the proof that deal with types. We also aim to isolate most of the reasoning in a simpler system that
is immune to the paradox of bad bounds, the key challenge that plagued the long search for a soundness proof.
In this system, our reasoning can rely on intuitive notions from familiar object calculi without dependent object
types (Abadi and Cardelli 1996; Pierce 2002). The results of this reasoning are lifted to the full DOT type system
by a single, simple theorem.
The main focus of our proof is on types. Dependent object types are the one feature that distinguishes DOT, so
we aim to decouple that one feature, which mainly affects the static type system, from other concerns. We focus
on proving the properties that one expects of types, and deliberately keep the proof independent of other aspects,
such as operational semantics and runtime values, which are similar in DOT as in other object calculi. Of course,
a soundness proof must eventually speak about execution and values, but once we have the necessary theory to
reason about types, these other concerns can be handled separately, at the end of the proof, using standard proof
techniques. Our final soundness theorem is stated for the small-step operational semantics given by Amin et al.
(2016), but that is only the final conclusion; the theory that we develop about dependent object types would be
equally applicable in a proof for a big-step operational semantics.
In a sense, this paper moves in the opposite direction compared to other recent work related to DOT: this paper aims for a simpler proof of one specific calculus, while other work generalizes DOT with features from other
calculi. The most significant addition in Rompf and Amin (2016) is subtyping between recursive types, which requires sophisticated proof techniques and induction schemes, but is not needed to model Scala. Amin and Rompf
(2017) focuses on a family of calculi with some features similar to those in DOT, and on general proof techniques
applicable to the whole family. While it is useful to generalize and compare DOT to other calculi, that is not the
topic of this paper. This paper focuses inwards, on DOT itself, on only those features of DOT that are necessary
for modelling Scala, with an aim to make the soundness proof of those specific features as simple and modular
as possible.
The power of DOT is also its curse. DOT empowers a program to define a domain-specific type system with
a custom subtyping lattice inside the existing Scala type system. This power has been used to encode in plain
Scala expressive type systems that would otherwise require new languages to be designed. But this power also
enables typing contexts that make no sense, in which types cannot be trusted and thus become meaningless. For
example, a program could define typing contexts in which an object, which is not a function, nevertheless has
a function type. Since such “crazy” contexts are possible, a soundness proof needs to consider them (but prove
that they are harmless during execution).
Besides the general pursuit of modularity, the simplicity of our new proof depends on two main ingredients.
The first ingredient is inert types and inert typing contexts, which we will define in Section 3.2. The essential
property of an inert type is that if all variables have inert types, then no unexpected subtyping relationships
are possible, so types can be trusted, and none of the paradoxes are possible. We express this property more
formally in Section 3.2. An important part of the soundness proof is to ensure that a term cannot evaluate until
the types of all its free variables have been narrowed to inert types.
We define inertness as a concise, easily testable syntactic property of a type. The definition consists of only
two non-recursive inference rules, so it can be easily inverted when it occurs in a proof. By contrast, existing
DOT proofs achieve similar goals using properties that characterize types by the existence of values with specific
relationships to those types. The benefit of our inertness property is that it involves only a type, not any values,
and it is defined directly, not via existential quantification of some corresponding value.
The second ingredient is tight typing, a small restriction of the DOT typing rules with major consequences,
which we will discuss in Section 3.3. We did not invent tight typing; it appears as a technical definition in

A Simple Soundness Proof for Dependent Object Types • 1:3
the proof of Amin et al. (2016). Our contribution is to identify and demonstrate just how useful and important
tight typing is to a simple proof. Amin et al. (2016) use tight typing in a collection of technical lemmas mixed
with reasoning about other concerns, such as general typing (the full typing rules of DOT) and correspondences
between values and types. In our proof, however, tight typing takes centre stage; it is the main actor that enables
intuition and simplicity.
Tight typing neutralizes the two DOT type rules that enable a program to define custom subtyping relationships. Tight typing immunizes the calculus: even if a typing context contains a type that is not inert, tight typing
prevents it from doing any harm. The paradoxes that make it challenging to work with DOT disappear under
tight typing. Without those two typing rules, the calculus behaves very differently, like object calculi without
dependent object types, and our reasoning can rely on familiar properties that we are used to from these calculi.
Of course, DOT with tight typing is not at all the real DOT: it lacks the power to create customized type
systems, and it is uninteresting; it is just another calculus with predictable behaviour. Theorem 3.3 in Section 3.3
bridges the gap by showing that in inert contexts, tight typing has all the power of general typing. Therefore,
all the reasoning that we do in the intuitive environment of tight typing applies to the full power of DOT. Even
our proof of Theorem 3.3 itself reasons entirely with tight typing, without having to deal with the paradoxes of
general DOT typing, and without having to reason about relationships between types and values.
Combining these two ingredients, we contribute a unified general recipe that can be used whenever a proof
about DOT needs to deduce information about a term from its type. Many of our lemmas follow this recipe.
The first step of the recipe, which should be the first step of any reasoning about types in DOT, is to drop down
from general typing to tight typing using Theorem 3.3. The purpose of the remaining steps is to make inductive
reasoning as easy and systematic as possible.
Contributions. This paper presents a simplified and extensible soundness proof for the DOT calculus (Amin et al.
2016). We contribute the following:
– A modular proof that reasons about types, values, and operational semantics separately.
– The concept of inert typing contexts, a syntactic characterization of contexts that rule out any nonsensical subtyping that could be introduced by abstract type members.
– A simple proof recipe for deducing properties of terms from their types in full DOT while reasoning only
in a restricted, intuitive environment free from the paradoxes caused by abstract type members. Multiple
lemmas follow the same recipe, and following the recipe can facilitate the development of new lemmas
needed in future extensions for DOT.
– A Coq formalization of the DOT soundness proof presented in this paper.1
The rest of this paper is organized as follows. Section 2 describes the DOT type system and explains the
problem of bad bounds, which is responsible for the complexity in DOT soundness proofs. Section 3 presents a
detailed description of the simplified DOT soundness proof introduced in this paper. Section 4 explains how to
extend the proof with new DOT features. The section also continues the discussion of the bad-bounds problem.
Section 5 examines related work. We finish with concluding remarks in Section 6.

2

BACKGROUND

The proof in this paper proves type soundness of the variant of the DOT calculus defined by Amin et al. (2016).

2.1

DOT Syntax

We begin by describing the abstract syntax of the calculus, shown in Figure 1. The calculus defines two forms of
values:
1

The Coq proof can be found at https://git.io/simple-dot-proof

1:4

• Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták

Definition

dF
x, y, z

Variable

a, b, c

Term member
Type member

A, B, C
s, t, u F

Term

{a = t }

field definition

{A = T }

type definition

d ∧d

′

aggregate definition
Type

S, T , U F
∀(x : S)T

dependent function

x

variable

v

value

µ(x : T )

recursive type

x .a

selection

{a : T }

field declaration

xy

application

{A: S..T }

type declaration

let x = t in u

let binding

x .A
S ∧T

vF

Value

type projection
intersection

λ(x : T ).t

lambda

⊤

top type

ν (x : T )d

object

⊥

bottom type

Fig. 1. Abstract syntax of DOT (Amin et al. 2016)

– A lambda abstraction λ(x : T ).t is a function with parameter x of type T and a body consisting of the
term t.
– An object of type T with definitions d is denoted as ν (x : T )d. The body of the object consists of the
definitions d, which are a collection of field and type member definitions, connected through the intersection operator. The field definition {a = t } assigns a term t to a field labeled a, and the type definition
{A = U } defines the type label A as an alias for the type U . The object also explicitly declares a recursive
self, or “this”, variable x. As a result, both T and d can refer to x.
A DOT term is a variable x, value v, field selection x .a, function application x y, or let binding let x = t in u.
To keep the syntax simple, the DOT calculus uses administrative normal form (ANF); as a result, field selection
and function application can involve only variables, not arbitrary terms.
A DOT type can be one of the following:
– A dependent function type ∀(x : S)T is the type of a function with a parameter x of type S, and with the
return type T , which can refer to the parameter x.
– A recursive type µ(x : T ) declares an object type T which can refer to its self-variable x.
– A field declaration {a : T } states that the field labeled a has type T .
– A type declaration {A: S..T } specifies that an abstract type member A is a subtype of T and a supertype
of S.
– A type projection x .A is the type assigned to the type member labelled A of the object x (ANF allows type
projection only on variables).
– An intersection type S ∧ T is the most general subtype of both S and T .
– The bottom type ⊥ and the top type ⊤ correspond to the bottom and top of the subtyping lattice, and are
analogous to Scala’s Nothing and Any.
Examples of DOT programs and their Scala equivalents can be found in Amin et al. (2016).

A Simple Soundness Proof for Dependent Object Types • 1:5

2.2

DOT Typing Rules

For lack of space, the DOT typing rules (which we will call the “general” typing relation throughout this paper)
are presented in the appendix in Figure 7. However, the tight typing rules, which will be discussed in Section 3.3,
and are shown in Figures 2 and 3, are very similar. The general typing rules can be read from the tight typing rules
by ignoring all occurrences of the symbol #, and by replacing the two highlighted rules <:-Sel-# and Sel-<:-#
with the following ones:
Γ ⊢ x : {A: S..T }
Γ ⊢ S <: x .A

(<:-Sel)

Γ ⊢ x : {A: S..T }
Γ ⊢ x .A <: T

(Sel-<:)

Most of the type rules are unsurprising. The rules All-I and {}-I give types to values. An object ν (x : T )d has
the recursive type µ(x : T ), where the types T must match, and T must summarize the definitions d following
the definition typing rules in Figure 3. Note that due to Def-Typ, each of the type declarations in an object must
have equal lower and upper bounds (i.e. an object ν (x : {A: S..U }) {A = T } is only well-typed if S = U = T ).
The rules Var, All-E, {}-E, Let give types to the other four forms of terms, and are unsurprising. The recursion
introduction (Rec-I), recursion elimination (Rec-E), and intersection introduction (And-I) rules apply only to
variables, but the subsumption rule (Sub) applies to all terms. The subtyping rules establish the top and bottom
of the subtyping lattice (Top, Bot), define reflexivity and transitivity (Refl, Trans), and basic subtyping rules for
intersection types (And1 -<:, And2 -<:, <:-And). As is commonplace, dependent functions are covariant in the
return type and contravariant in the parameter type (All-<:-All). Field typing is covariant by the rule Fld-<:,
whereas type member declarations are contravariant in the lower bound and covariant in the upper bound via
Typ-<:. The most interesting rules that distinguish DOT are <:-Sel and Sel-<: above, which introduce an objectdependent type x .A and define subtyping between it and its bounds. As we will see, these rules are responsible
for much of the complexity of the safety proof.

2.3

Bad Bounds

The type selection subtyping rules <:-Sel and Sel-<: enable users to define a type system with a custom subtyping lattice. If a program defines a function λ(x : {A: S..U }).t, then t is typed in a context in which S is considered
a subtype of U , because S <: x .A <: U . The soundness proof must ensure that such a user-defined subtyping
lattice do not cause any harm, i.e., cannot cause a violation of type soundness of the overall calculus.
Let S be the object type {a : ⊤} and U be the function type ∀(z : ⊤)⊤. Then the following is a valid and
well-typed DOT term:
λ(x : {A: S..U }).let y = ν (y : S) {a = y.a} in y y
How is this possible? The inner term y y is a function application applying y to itself, but y is bound by the let to
an object, not a function. How can y appear in a function application when it is not a function? This is possible
because y has the object type S, and in the body of the lambda, we have the subtyping chain S <: x .A <: U . The
declaration of the lambda asserts that x .A is a supertype of S and a subtype of U , and therefore introduces the
new custom subtyping relationship S <: U . Inside the body of the lambda, the object type S is a subtype of the
function type U , so since the object y has type S, it also has the function type U . The function application of
object y to itself is therefore well-typed in this context.
This is crazy, the reader may be thinking. Indeed, in an environment in which subtyping can be arbitrarily
redefined, types cannot be trusted. In particular, we cannot conclude from the fact that y has the function type S
that it is indeed a function; actually, it is an object. The seemingly obvious fix is to require S to be a subtype of U
when the parameter x of the lambda is declared to have type {A: S..U }. But as we will discuss in Section 4.2, this
seemingly obvious fix does not work, and the struggle to try to make it work has caused much of the difficulty
in the ten-year struggle for a DOT soundness proof.

1:6

• Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták

Tight term typing
Γ(x) = T

(Var-#)

Γ ⊢# x : T

Γ ⊢# t : T
(Γ, x : T ) ⊢ u : U
x < fv(U )
Γ ⊢# let x = t in u : U

(Γ, x : T ) ⊢ t : U

x < fv(T )

Γ ⊢# λ(x : T ).t : ∀(x : T )U
Γ ⊢# x : ∀(z : S)T
Γ ⊢# x y :

Γ ⊢# ν (x : T )d : µ(x : T )

Γ ⊢# x .a : T

(Rec-I-#)

Γ ⊢# x : µ(z : T )

(All-E-#)

(Rec-E-#)

Γ ⊢# x : [x/z ]T

(Γ, x : T ) ⊢ d : T

Γ ⊢# x : {a : T }

Γ ⊢# x : T
Γ ⊢# x : µ(x : T )

Γ ⊢# y : S
[y/z ]T

(All-I-#)

Γ ⊢# x : T

({}-I-#)

Γ ⊢# x : U

Γ ⊢# x : T ∧ U
Γ ⊢# t : T

({}-E-#)

(Let-#)

Γ ⊢# T <: U

Γ ⊢# t : U

(And-I-#)

(Sub-#)

Tight subtyping
Γ ⊢# T <: ⊤

(Top-#)

Γ ⊢# ⊥ <: T

(Bot-#)

Γ ⊢# T <: T

(Refl-#)

Γ ⊢# T ∧ U <: T (And1 -<:-#)

Γ ⊢# {a : T } <: {a : U }
(Fld-<:-Fld-#)
Γ ⊢# T ∧ U <: U (And2 -<:-#)

Γ ⊢# S <: T

Γ ⊢# S <: T

Γ ⊢# T <: U

Γ ⊢# S <: U
(Trans-#)
Γ ⊢# S 2 <: S 1
Γ ⊢# T1 <: T2
Γ ⊢# {A: S 1 ..T1 } <: {A: S 2 ..T2 }

Γ ⊢# T <: U

Γ ⊢# S <: U

Γ ⊢# S <: T ∧ U
(<:-And-#)

(Typ-<:-Typ-#)

Γ ⊢! x : {A: T ..T }
(<:-Sel-#)
Γ ⊢# T <: x .A
Γ ⊢! x : {A: T ..T }
(Sel-<:-#)
Γ ⊢# x .A <: T

Γ ⊢# S 2 <: S 1
(Γ, x : S 2 ) ⊢ T1 <: T2
Γ ⊢# ∀(x : S 1 )T1 <: ∀(x : S 2 )T2

(All-<:-All-#)

Fig. 2. Tight Typing Rules (Amin et al. 2016)

How can DOT be sound then, when it is so crazy? After all, the function application y y is well-typed but its
evaluation gets stuck, because y is not a function, so how can DOT be sound? The key is that the DOT semantics
is call-by-value. In order to invoke the body of the lambda, one must provide an argument value to pass for the
parameter x. This value must contain a type assigned to A that is both a supertype of U and a subtype of S. If no

A Simple Soundness Proof for Dependent Object Types • 1:7

Γ ⊢t: U
Γ ⊢ {a = t } : {a : U }
Γ ⊢ {A = T } : {A: T ..T }

(Def-Trm)
(Def-Typ)

Γ ⊢ d 1 : T1
Γ ⊢ d 1 : T2
dom(d 1 ), dom(d 2 ) disjoint
Γ ⊢ d 1 ∧ d 2 : T1 ∧ T2

(AndDef-I)

Fig. 3. Definition Typing Rules (Amin et al. 2016)

such type exists, then no such argument value can exist, so the lambda cannot be called, so its body containing
the crazy application y y cannot ever be executed. Therefore, this term is not a counterexample to the soundness
of the DOT type system.
Why should DOT have such a strange feature? The ability to define a custom subtyping lattice turns out to
be very useful. For example, we can define the term:
λ(x : {A: ⊥..⊤} ∧ {B : x .A..x .C} ∧ {C : ⊥..⊤}).t
In the body t of this lambda, we can make use of unspecified opaque types A, B, and C, making use of only the
condition that A <: B <: C. We can use this feature to define arbitrary type systems within the language. For
example, Scalas and Yoshida (2016) have implemented session types, a feature that usually requires a customdesigned language, inside plain Scala. As another example, Osvald et al. (2016) used this ability to define a lattice
of lifetimes within the Scala type system for categorizing values that cannot outlive different stack frames.
To reconcile a custom subtyping lattice with a sound language, we only need to force the programmer to
provide evidence that the custom lattice does not violate any familiar assumptions (e.g., it does not make object
types subtypes of function types). This evidence takes the form of an argument value that must be passed to the
lambda before the body that uses the custom type lattice can be allowed to execute. This value must be an object
that provides existing types that satisfy the specified custom subtyping constraints. In our example, this is easy:
it suffices to pass the same type, such as ⊤, for all three type parameters, since ⊤ <: ⊤ <: ⊤. However, the types
are opaque: when checking the body of the lambda, the type checker cannot use the fact that A = B = C = ⊤;
the body must type-check even under only the assumptions that A <: B <: C.
Since DOT programs can exhibit unexpected subtyping lattices in some contexts, and since this is unavoidable, an essential feature of a soundness proof is to clearly distinguish contexts in which types can be trusted,
because any custom subtyping relationships have been justified by actual type arguments, from contexts in
which types cannot be trusted, because they could have been derived from arbitrary unjustified custom subtyping relationships. In Section 3.2, we will formally define this property that types can be trusted, and define a
simple syntactic characterization of inert typing contexts that guarantee this property. In earlier DOT soundness proofs, the trusted types property was not precisely defined, and typing contexts in which there are no
bad bounds were defined more indirectly, not in terms of the types themselves, but in terms of the existence of
values having those types.

3 PROOF
3.1 Overview
We will first outline the general recipe that we use to reason throughout the proof about the meaning of a type.
The details of each step will be discussed in the following subsections. We present the overview on an example
proof of Lemma 3.9, which will be introduced in Section 3.5, but the specific example is unimportant; most of

1:8

• Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták

the reasoning throughout the proof follows the same steps, through the same typing relations, in the same order,
using the same reasoning techniques.
Usually, we know that some term has some type (e.g. Γ ⊢ x : {a : T }), and we seek to interpret what the type
tells us about the term, and to determine how the type of the term was derived. In this example, we seek more
detailed information about x, for example that the typing context Γ assigns it an object type Γ(x) = µ(x : ··· ∧
{a : T ′ } ∧ ···), or the shape of the value that it will hold at run time (e.g. an object ν (x : ··· ∧ {a : T ′ } ∧ ···)(··· ∧
{a = t ′ } ∧ ···)).
Each such derivation follows the same sequence of steps (although sometimes only a subsequence of the steps
is necessary):
inert Γ

Γ ⊢ x : {a : T }

inert Γ

Γ ⊢# x : {a : T }

inert Γ

Γ ⊢## x : {a : T }

inert Γ

Theorem 3.3 (⊢ to ⊢# )
Theorem 3.6 (⊢# to ⊢## )

Γ ⊢! x : {a : T ′ }

inert Γ

Γ ⊢ T ′ <: T

Γ(x) = µ(x : ··· ∧ {a : T ′ } ∧ ···)

Induction on ⊢##

Γ ⊢ T ′ <: T

Induction on ⊢!

Although there are four steps, each individual step is quite simple. More importantly, each step is modular,
independent of the other steps, and the proof techniques at each step are either directly reusable (theorems) or
easily adaptable (induction) to proofs of properties other than this specific lemma.
The derivation starts with general typing (Γ ⊢ x : {a : T }), the typing relation of the DOT calculus. The
key property that makes reasoning possible is that the typing context Γ is inert. Inert contexts will be defined
in Section 3.2. Inertness ensures that customized subtyping in the program does not introduce unexpected
subtyping relationships. If the context were not inert, any type could have been customized to have arbitrary
subtypes and be inhabited by arbitrary terms, so it would be impossible to draw any conclusions about a term
from its type.
Knowing that the typing context is inert, we apply Theorem 3.3 (⊢ to ⊢# ) to get a tight typing (Γ ⊢# x : {a : T }),
which will be discussed in Section 3.3. A tight typing is immune to any unexpected subtyping relationships that
the program may have defined, so our reasoning can now rely on familiar intuitions about what types ought to
mean about their terms.
However, the tight typing rules are not amenable to inductive proofs. Theorem 3.6 (⊢# to ⊢## ) gives invertible typing (Γ ⊢## x : {a : T }), which is specifically designed to make inductive reasoning as easy as possible.
Invertible typing will be discussed in Section 3.4.
By induction on invertible typing, we obtain a property of all of the precise types Γ ⊢! x : {a : T ′ } that could
have caused x to have the general type {a : T }. Informally, the precise typing means that the type Γ(x) given
to x by the typing context is an object type containing a field a of type T ′ . We will present precise typing in
Section 3.3. Precise typing is also amenable to straightforward induction proofs, so we can use one to obtain
Γ(x).

3.2

Inert Typing Contexts

Recall the function λ(x : {A: S..U }).t that we discussed in Section 2.3. If the function appears in a context Γ,
its body is type checked in an extended context (Γ, x : {A: S..U }). The extended context adds a new subtyping
relationship (Γ, x : {A: S..U }) ⊢ S <: U that might not have held in the original context Γ. In particular, the
extended context could introduce a subtyping relationship that does not make sense, such as ∀(x : S)T <: µ(x : U ),
or ⊤ <: ⊥. To control such unpredictable contexts, we define the notion of inert typing contexts and inert types.
Definition 3.1. A typing context Γ is inert if the type Γ(x) that it assigns to each variable x is inert.

A Simple Soundness Proof for Dependent Object Types • 1:9
Definition 3.2. A type U is inert if
– U is a dependent function type ∀(x : S)T , or
– U is a recursive type µ(x : T ), where T is an intersection of field declarations {a : S } and tight type
declarations {A: S..S }, and the type labels A of the tight type declarations are distinct. A type declaration
{A: S..U } is tight if its bounds S and U are the same.
An inert typing context has the following useful property.
Property 1 (Inert Context Guarantee). Let Γ be any inert typing context, t be a closed term and U be a
closed type. If Γ ⊢ t : U , then ∅ ⊢ t : U .
The significance of this property is that in an inert typing context, a term t does not have any “unexpected”
types that it would not have in an empty typing context. For example, we can be sure that in an inert typing
context, a function value will not have an object (recursive) type, and an object will not have a function type.
Though we do not directly apply the property in the proof, it is useful for intuitive reasoning about typing and
subtyping in inert typing contexts.
Every value has an inert type (as long as the value is well formed, i.e., as long as it has any type at all). This is
because the two base typing rules for values, (All-I) and ({}-I), and the definition typing rules that they depend
on, always assign an inert type to the value. The converse is not true: not every inert type is inhabited by a
value. For example, we cannot construct a value of type λ(x : ⊤).⊥.
Returning to the example, suppose now that the function is invoked with some value v bound to a variable
y: let y = v in (λ(x : {A: S..U }).t) y. Recall that the body t is typed with the assumption that S <: U . Type
checking the overall term ensures that the argument y provides evidence for that assumption. Specifically, the
value v has an inert type, so y has an inert type. The typing rule for function application requires subtyping
between the argument and parameter types, so the type of y must have a member {A: T ..T } with S <: T and
T <: U . (The bounds T of the type member must be tight because the type is inert.) The type T that y provides is
evidence that justifies the assumption S <: U under which the body t of the function was type checked. During
execution, when the function is called, all occurrences of x in the body t will be replaced by y before evaluation
of the body begins. In general, the semantics ensures that before it begins evaluating a term (such as t), the term
has a type in a context in which all non-inert types (such as the type of x) have been narrowed to inert types
(such as the type of y).

3.3

Tight Typing

Although inert contexts provide the assurance of Property 1 (Inert Context Guarantee), in our proofs, we often
need to reason even in contexts that are not inert. Moreover, even when we know that a context is inert, it would
be difficult to express the important consequences of the inert context in every proof that deals with the general
DOT typing and subtyping rules.
Tight typing (Amin et al. 2016) is a slight restriction of general typing that can bridge the gap between the
unpredictability of the general DOT typing rules in arbitrary typing contexts and the predictable assurances
of Property 1 in inert typing contexts. The tight typing rules are presented in Figure 2. They are almost the
same as the general DOT typing rules, except that the <:-Sel-# and Sel-<:-# rules have the restricted premise
Γ ⊢! x : {A: T ..T }, so they can be applied only when the bounds T of the type member A are tight. Precise
typing, denoted ⊢! , is defined in Figure 4. The precise type of a variable x is the type Γ(x) given to it by the
typing context Γ, possibly decomposed using the elimination rules, so that if Γ(x) is an object type such as
µ(x : ··· ∧ {A: T ..T } ∧ ···), then x also has just the type member {A: T ..T } as a precise type. For values, precise
typing applies only the base case rules All-I and {}-I from general typing. In premises of rules that extend the
typing context (All-I-#, Let-#, {}-I-#), tight typing reverts to general typing in the extended context.

1:10

• Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták

Precise variable typing
Γ(x) = T
Γ ⊢! x : T

(Var!)

Γ ⊢! x : µ(z : T )
Γ ⊢! x : [x/z ]T

(Rec-E!)

Γ ⊢! x : T ∧ U
Γ ⊢! x : T

(And1 -E!)

Γ ⊢! x : T ∧ U
Γ ⊢! x : U

(And2 -E!)

Precise value typing
(Γ, x : T ) ⊢ t : U

x < fv(T )

Γ ⊢! λ(x : T ).t : ∀(x : T )U

(All-I!)

(Γ, x : T ) ⊢ d : T
Γ ⊢! ν (x : T )d : µ(x : T )

({}-I!)

Fig. 4. Precise Typing Rules (Amin et al. 2016)

We observe two very useful properties of tight typing that together combine to make it especially convenient for reasoning about DOT typing. The first property is that tight typing extends the benefits of Property 1
(Inert Context Guarantee), to all typing contexts, not only inert ones:
Property 2 (Tight Typing Guarantee). Let Γ be any typing context, t be a closed term and U be a closed type.
If Γ ⊢# t : U , then ∅ ⊢# t : U and ∅ ⊢ t : U .
The general typing rules that enable DOT programs to define new user-defined subtyping relationships, <:-Sel
and Sel-<:, are restricted in tight typing to <:-Sel-# and Sel-<:-#, which allow only to give an alias to an existing
type, but not to introduce new subtyping between existing types.
Property 2 makes reasoning in tight typing easy: we never have to worry about unexpected custom subtyping
relationships being introduced by the program, and we do not need to reason about whether we are in an inert
typing context, because tight typing gives the guarantee in all contexts.
Although tight typing satisfies the desirable intuitive Property 2, it is not DOT. In particular, tight typing does
not, in general, enable a program to use a custom-defined subtyping lattice that is the key feature of dependent
object types. We would like the best of both worlds: to allow DOT programs to enjoy the full power of general
typing, yet to reason about our proofs with the intuitive tight typing. For this, we need the second property of
tight typing.
The second important property of tight typing is that in an inert typing context, tight typing is equivalent to
general DOT typing:
Theorem 3.3 (⊢ to ⊢# ). If Γ is an inert context, then Γ ⊢ t : T implies Γ ⊢# t : T , and Γ ⊢ S <: U implies
Γ ⊢# S <: U .
We delay giving the proof of the theorem until after some discussion.
These two properties motivate and justify our recommendation that tight typing should be at the core of
all reasoning about the meaning of types in DOT. Tight typing is predictable, like the type systems of familiar
calculi without dependent object types, yet in an inert typing context, it has the same power as general DOT
typing. Therefore, every proof with a premise involving general typing and an inert typing context should
immediately apply Theorem 3.3 (⊢ to ⊢# ) to drop down into the intuitive environment of tight typing for the rest
of the reasoning.
What if we do not have an inert context as a premise, and therefore cannot apply Theorem 3.3? In that case,
we should not reason about the meanings of types at all. As we saw in Section 2.3, in such a context, a term

A Simple Soundness Proof for Dependent Object Types • 1:11
could be given an arbitrary type by custom subtyping rules. Therefore, we cannot deduce anything about a term
from its type, and it would be futile to try.
In summary, inert contexts, tight typing, and Theorem 3.3 that justifies reasoning in tight typing should be
the cornerstones of any reasoning about the meaning of types in the DOT calculus.
How shall we prove Theorem 3.3, then? It is tempting to prove the theorem by trying to compare various
properties of the tight and general typing relations, the closures of the tight and general typing rules. This approach was taken in the proof of Amin et al. (2016) for a related theorem (with the same conclusion but different
premises). The typing relations are very different from each other (general typing is much more powerful), but
the rules that give rise to them are quite similar. It is much easier, therefore, to instead show that the rules are
equivalent in an inert context. The only rules in general typing missing from tight typing are the <:-Sel and
Sel-<: rules. Our goal is therefore to replace these rules with a lemma:
Lemma 3.4 (Sel-<: Replacement). If Γ is an inert context, then if Γ ⊢# x : {A: S..U }, then Γ ⊢# S <: x .A and
Γ ⊢# x .A <: U .
One nice property of this lemma is that it is stated entirely in terms of tight typing. Thus, to prove it, we can
ignore the unpredictable world of general typing, and work exclusively in the intuitive world of tight typing.
But how can we prove it? We would like to apply the <:-Sel# and Sel-<:# rules. Their premises are Γ ⊢!
x : {A: T ..T }. Therefore, we need to invert tight typing, to show the following:
Lemma 3.5 (Sel-<: −# Premise). If Γ is an inert context, then if Γ ⊢# x : {A: S..U }, then there exists a type T
such that Γ ⊢! x : {A: T ..T }, Γ ⊢# S <: T , and Γ ⊢# T <: U .
We will discuss how to invert tight typing to prove this lemma in Section 3.4.
Using Lemma 3.5 (Sel-<:-# Premise), proving Lemma 3.4 (Sel-<: Replacement) is easy:
Proof of Lemma 3.4 (Sel-<: Replacement). Apply Lemma 3.5 (Sel-<:-# Premise), then <:-Sel-# and Sel-<:-#,
to get Γ ⊢# S <: T <: x .A <: T <: U . The result follows by Trans-#.

Using Lemma 3.4 (Sel-<: Replacement), proving Theorem 3.3 (⊢ to ⊢# ) is now also quite easy.
Proof of Theorem 3.3 (⊢ to ⊢# ). The proof is by mutual induction on the tight typing and subtyping derivations of Γ ⊢ t : T and Γ ⊢ S <: U . In general, for each rule of general typing, we invoke the corresponding rule
of tight typing. The premises of the tight typing rules differ from those of the general typing rules in that they
require tight typing in rules that do not extend the context. Since the unextended context is inert, the general
premise implies the tight premise by the induction hypothesis. Premises that do extend the context use general typing, so nothing needs to be proven for them. The exception is the <:-Sel and Sel-<: rules. Lemma 3.4
(Sel-<: Replacement) is an exact replacement for these rules, so we just apply it. Despite the long explanation,
the proof in Coq is only two lines long.


3.4

Inversion of Tight Typing

Although reasoning with tight typing is intuitive because it obeys Property 2 (Tight Typing Guarantee), we often
need to invert the tight typing rules to prove properties such as Lemma 3.5 (Sel-<:-# Premise), which we used
in the proof of Lemma 3.4 (Sel-<: Replacement). More generally, we need to prove that if Γ ⊢# x : T , where T is
of a certain form, then Γ(x) = U , and there is a certain relationship between T and U .
The obvious approach to proving such inversion properties is by induction on the derivation of the tight typing.
This usually fails, however, because of cycles in the tight typing rules. Each language construct typically has both
an introduction and an elimination rule, and the two form a cycle. For example, if Γ ⊢# x : T , then Γ ⊢# x : µ(x : T )
by Rec-I-#, so again Γ ⊢# x : T by Rec-E-#. Such cycles block inductive proofs because a proposition Γ ⊢# x : T

1:12

• Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták

is justified by Γ ⊢# x : µ(x : T ), which in turn is justified by the original proposition Γ ⊢# x : T . The solution is to
define a set of acyclic, invertible rules on which induction is easy, and to prove that the invertible rules induce
the same typing relation as the cyclic tight typing rules.
The construction of the invertible typing rules is simplified by two restrictions:
(1) We only ever need to invert typing rules in inert typing contexts.
(2) We only ever need to invert typings of variables and values, not of arbitrary terms.
In the invertible rules, we can thus exclude rules that cannot apply to variables or values, and rules that cannot
apply to inert types or to types derived from inert types.
It remains to decide, when facing a cycle of two rules that introduce and eliminate a given language construct,
which one of the two rules to remove and which one to keep in the acyclic, invertible rule set. In general, because
a construct can be introduced an unbounded number of times in tight typing, we must keep the introduction rule.
For example, if x has type T , then x also has type µ(y : µ(y ′ : µ(y ′′ : T ))), and the invertible rules must generate
this type. On the other hand, the base case of the typing rules for variables, the rule Var-#, gives each variable
x the type Γ(x), which in an inert context is an inert type, and can therefore be a recursive type containing an
intersection type. Since the tight typing rules eliminate the recursion and the intersection, the invertible rules
must also eliminate them. It seems that we have reached a contradiction: the invertible rules must have both
introduction and elimination rules for recursive and intersection types.
The solution is to split the invertible rules into two phases. The first phase of rules contains all the elimination
rules. After all necessary eliminations have been performed, a second phase containing only introduction rules
can then perform all necessary introductions. By splitting the rules into two phases, we ensure that no derivation
can cycle between introductions and eliminations, so the rules are invertible. It turns out that we already have
rules for the first phase: the precise typing rules introduced in Section 3.3 already contain all of the elimination
rules that apply to variables and values, and eliminate from the type of a variable all constructs that can appear
in an inert type. (Note that even the general DOT typing rules remove recursive and intersection types only
from the types of variables, not values.) To construct the invertible introduction rules, we propose the following
recipe:
(1) Start with the tight typing rules.
(2) Inline the subsumption rule (inline the subtyping rules into the typing rules). This simplifies the construction, so we define only one relation instead of two separate typing and subtyping relations.
(3) Specialize the terms in all rules to variables and values, and remove all rules that cannot apply to variables
or values.
(4) Remove all elimination rules.
(5) Remove all rules that cannot apply in an inert context. Specifically, this means the Bot-# rule, because
it has Γ ⊢# x : ⊥ as a premise, but this typing cannot be derived by any of the other remaining rules
starting from an inert type given to a variable by the Var-# rule or to a value by the All-I-# and {}-I-#
rules.
By applying this recipe to the tight typing rules, we arrive at the invertible typing rules shown in Figure 5.
We must now prove that the typing relation induced by the invertible typing rules is equal to the typing relation
induced by the tight typing rules (restricted to inert contexts and to variables and values):
Theorem 3.6 (⊢# to ⊢## ). If Γ is an inert context, t is a variable or a value, and Γ ⊢# t : T , then Γ ⊢## t : T .
Proof. The proof is by induction on the tight subtyping and typing rules. Although we said that induction on
tight typing usually fails because the rules have cycles, in this specific case, the induction is quite straightforward
because invertible typing is part of the induction hypothesis. The inductive cases for elimination rules, which

A Simple Soundness Proof for Dependent Object Types • 1:13
Invertible Typing for Variables
Γ ⊢! x : T

(Var-##)

Γ ⊢## x : T
Γ ⊢## x : {a : T }

(All-I-##)

Γ ⊢## x : ∀(z : S ′)T ′

Γ ⊢# T <: U

(Fld-<:-##)

Γ ⊢## x : {a : U }
Γ ⊢## x : {A: T ..U }
Γ ⊢# T ′ <: T
Γ ⊢# U <: U ′
′

Γ ⊢## x : ∀(z : S)T
Γ ⊢# S ′ <: S
(Γ, y : S ′) ⊢ T <: T ′

′

Γ ⊢## x : {A: T ..U }

Γ ⊢## x : T

Γ ⊢## x : U

(And-I-##)

Γ ⊢## x : T ∧ U
(Typ-<:-##)

Γ ⊢## x : T

Γ ⊢## x : S

Γ ⊢## x : y.A
Γ ⊢## x : T

(Rec-I-##)

Γ ⊢## x : µ(x : T )

Γ ⊢! y : {A: S..S }

(Sel-##)

(Top-##)

Γ ⊢## x : ⊤

Invertible Typing for Values
Γ ⊢! v : T

Γ ⊢## v : T

(Val-##)

Γ ⊢## v : T

Γ ⊢## v : T ∧ U
Γ ⊢## v : S

′

Γ ⊢## v : ∀(z : S )T

′

Γ ⊢## v : T

(All-v-##)

(And-v-##)

Γ ⊢! y : {A: S..S }
Γ ⊢## v : y.A

′

Γ ⊢## v : ∀(z : S)T
Γ ⊢# S <: S
(Γ, y : S ′ ) ⊢ T <: T ′

Γ ⊢## v : U

Γ ⊢## v : ⊤

(Sel-v-##)

(Top-v-##)

Fig. 5. Invertible Typing Rules

would usually lead to cycles in the induction, are all discharged using the invertible typing in the induction
hypothesis.

With this theorem, inversion proofs such as the proof of Lemma 3.5 (Sel-<:-# Premise) become easy inductions
on the invertible typing rules:
Proof of Lemma 3.5 (Sel-<:-# Premise).
inert Γ
inert Γ
inert Γ

Γ ⊢# x : {A: S..U }
Γ ⊢## x : {A: S..U }

Γ ⊢! x : {A: T ..T }

Theorem 3.6 (⊢# to ⊢## )

Γ ⊢# S <: x .T

Γ ⊢# x .T <: U

Induction on ⊢##


We will see more lemmas that follow the same proof strategy in the next section.

1:14

• Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták

3.5

Extending to Values

In general, soundness proofs require canonical-forms lemmas that show that if a value has a given type, then it
is a particular form of value. Following our theme of a modular proof that deals with one concept at a time, we
do most of our work at the level of types, following the same general recipe.
Because the DOT syntax enforces ANF, before a value can be used for anything interesting, it must first be
assigned to a variable through a let expression. Suppose a variable x is bound to a value v by let x = v in t and
the variable x is used somewhere inside t. From the type U of the use of x, we would like to deduce the form of
the value v.
We proceed in two steps. First, from a type U such that Γ ′ ⊢ x : U , where Γ ′ is the typing context used to
type the use of x occurring inside t, we follow the proof recipe to deduce the type Γ ′(x) given to x by the typing
context. The typing context Γ ′ is constructed by the premises of the Let typing rule, which extends an existing
typing context Γ to the typing context Γ ′ by adding a binding (x : T ). Here, T is some type such that Γ ⊢ v : T .
Therefore, Γ ′(x) is this T , and we have, in general, that Γ ⊢ v : Γ ′(x) and thus also Γ ′ ⊢ v : Γ ′(x).
For the second step, we know Γ ′ ⊢ v : T , where the type T has been identified by the first step, and we wish
to deduce the precise type of v, and thence invert the precise value typing rules to obtain the form of v.
The following lemmas instantiate these two steps, first for dependent function types, and then for field member
types.
Lemma 3.7 (∀ to Γ(x)).
Γ ⊢ z : ∀(x : T )U

inert Γ
′

Γ(z) = ∀(x : T )U

′

Γ ⊢ T <: T ′

(Γ, x : T ) ⊢ U ′ <: U

Lemma 3.8 (∀ to λ).
Γ ⊢ v : ∀(x : T )U

inert Γ
′

Γ ⊢ T <: T ′

v = λ(x : T ).t

(Γ, x : T ) ⊢ t : U

Lemma 3.9 (µ to Γ(x)).
Γ ⊢ x : {a : T }

inert Γ

Γ(x) = µ(x : ··· ∧ {a : T ′ } ∧ ···)

Γ ⊢ T ′ <: T

Lemma 3.10 (µ to ν ).
inert Γ

Γ ⊢ v : µ(x : ··· ∧ {a : T } ∧ ···)

v = ν (x : ··· ∧ {a : T } ∧ ···)(··· ∧ {a = t } ∧ ···)

Γ ⊢t:T

The proofs of all of the lemmas follow the same general proof recipe that we introduced for Lemma 3.9 in
Section 3.1. We show the proof of Lemma 3.8 here, and proofs of the other three lemmas in the Appendix.
Proof of Lemma 3.8 (∀ to λ).
inert Γ

Γ ⊢ v : ∀(x : T )U

inert Γ

Γ ⊢# v : ∀(x : T )U

inert Γ

Γ ⊢## v : ∀(x : T )U

Γ ⊢! v : ∀(x : T ′ )U ′

inert Γ
v = λ(x : T ′ ).t

v = λ(x : T ′ ).t

Theorem 3.3 (⊢ to ⊢# )
Theorem 3.6 (⊢# to ⊢## )

Γ ⊢ T <: T ′

(Γ, x : T ′ ) ⊢ U ′ <: U

Induction on ⊢##

(Γ, x : T ′ ) ⊢ t : U ′

Γ ⊢ T <: T ′

(Γ, x : T ′ ) ⊢ U ′ <: U

(Γ, x : T ) ⊢ t : U ′

Γ ⊢ T <: T ′

(Γ, x : T ) ⊢ U ′ <: U

v = λ(x : T ′ ).t

(Γ, x : T ) ⊢ t : U

Γ ⊢ T <: T ′

Induction on ⊢!
Narrowing
Sub

A Simple Soundness Proof for Dependent Object Types • 1:15

Since the return type of a dependent function type depends on the parameter type, this proof and the proof
of Lemma 3.7 rely on a standard narrowing property, which states that making a typing context more precise
by substituting one of the types by its subtype preserves the typing and subtyping relations.
Lemma 3.11 (Narrowing). Suppose Γ(x) = T and Γ[x : T ′ ] ⊢ T ′ <: T . Then Γ ⊢ t : U implies Γ[x : T ′ ] ⊢ t : U ,
and Γ ⊢ S <: U implies Γ[x : T ′ ] ⊢ S <: U .
Narrowing is proved for DOT by Amin et al. (2016). The proof is standard, with no issues specific to DOT, by
induction on the typing and subtyping rules.

3.6

Operational Semantics

In general, a type soundness proof for a given operational semantics shows that if a term t has a type T , then
it steps to another term of the same type (in a small-step semantics), or it reduces to a value of the same type
(in a big-step semantics). In both cases, the first step of the proof is to deduce the form of the term from its
type. The second step is then to apply the evaluation relation to obtain a new term (or value), apply the typing
rules to obtain its type, and (hopefully) conclude that it has the original type T . The techniques presented in
the preceding sections solve the first step for DOT. The second step is then primarily direct application of the
evaluation and typing rules.
Although the soundness statement applies to the whole program t and requires it to have a type in an empty
typing context, the operational semantics typically defines evaluation of a complex term recursively in terms
of evaluation of its subterms u. The soundness proof typically uses induction on the structure of t, and it must
prove that if ∅ ⊢ t : T , then Γ ⊢ u : U , where the typing context Γ is carefully determined by the position of u in
t. This part is standard, and the DOT soundness proof depends on this property in the same way as soundness
proofs for other calculi.
The part that is unique to DOT is that the typing context Γ in which the subterm u is typed must also be inert,
so that we can use all of the theory developed in preceding sections. Thus, given that ∅ ⊢ t : T and a subterm u
of t to be reduced, we need a way to find an inert typing context Γ in which Γ ⊢ u : U . This is needed for any
sound semantics of DOT, whether big-step or small-step.
To summarize, usually, to prove a calculus sound, it must obey the property that if ∅ ⊢ t : T and u is a subterm
of t that may be evaluated during evaluation of t, then Γ ⊢ u : U for some carefully determined typing context Γ.
DOT adds a further requirement that Γ must be inert.
The variant of DOT that we have studied in this paper is from Amin et al. (2016), which defines the small-step
semantics with evaluation contexts shown in Figure 6. For a small-step semantics, the soundness theorem to
prove is:
Theorem 3.12 (Soundness). If ∅ ⊢ t : T , then t is a normal form or t → t ′ and ∅ ⊢ t ′ : T .
In the soundness proof, the program term t is decomposed into an evaluation context e containing a subterm u.
Each evaluation context is a sequence of let bindings that bind variables to values. As a specific example, consider
the case when u is a function application x y. We must show that t = e[x y] = e ′ [let x = λ(y : S ′′ ).s in e ′′ [x y]],
so that the corresponding reduction rule can be applied. Since ∅ ⊢ e[x y] : T and the evaluation context e is a
sequence of let terms that bind variables x i to values vi , we can invert the Let typing rule of each such binding.
The premises of the Let rule add to the typing context the binding (x i ,T ), where T is a type such that Γ ⊢ vi : T .
Thus, we obtain Γ ⊢ x y : U in a context Γ in which, for each i, Γ ⊢ vi : Γ(x i ). Since x occurs in a well-typed
function application, we would like to deduce that it must have a function type, and thence that the value v that
it is bound to must be a function. However, as we saw in Section 2.3, nothing can be deduced from the type of
a term in an unrestricted DOT typing context.

1:16

• Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták

e F [] | let x = [] in t | let x = v in e

Evaluation context

t 7−→ t ′
e[t] 7−→ e[t ′ ]
v = λ(z : T ).t
let x = v in e[x y] 7−→ let x = v in e[[y/z ] t]
v = ν (x : T ) . . . {a = t } . . .
let x = v in e[x .a] 7−→ let x = v in e[t]

(Term)

(Apply)

(Project)

let x = y in t 7−→ [y/x ] t

(Let-Var)

let x = let y = s in t in u 7−→ let y = s in let x = t in u

(Let-Let)

Fig. 6. DOT Operational Semantics (Amin et al. 2016)

In order to reason about x, we require a typing in an inert typing context. We know that Γ ⊢ vi : Γ(x i ), but
even though every value has an inert type (given by the precise typing rules for values), not every type of a
value is inert. Thus, Γ ⊢ vi : Γ(x i ) alone is not sufficient to conclude that Γ(x i ) is inert. One more small lemma is
necessary:
Lemma 3.13. If Γ ⊢ v : T , then there exists a type T ′ such that Γ ⊢! v : T ′ and Γ ⊢ T ′ <: T .
Proof (Amin et al. 2016). The proof is by induction on the derivation of Γ ⊢ v : T , and is short because few
of the typing rules apply to values, and because the lemma includes subtyping in its conclusion (and therefore
in the induction hypothesis).

Each type T ′ generated by the lemma is inert because it is the precise type of some value. Applying the lemma
to each type in the typing context Γ, we obtain an inert typing context Γ ′ such that for each x i , Γ ′ ⊢ Γ ′(x i ) <: Γ(x i ).
By narrowing, since Γ ⊢ x y : U , it is also the case that Γ ′ ⊢ x y : U in the inert typing context Γ ′.
From the typing rule that infers Γ ′ ⊢# x y : U , we determine that x has a function type Γ ′ ⊢ x : ∀(y : S)U . We can
then use Lemma 3.7 (∀ to Γ(x)) to show that Γ ′(x i ) = ∀(y : S ′ )U ′ with Γ ′ ⊢ S <: S ′ and (Γ ′, y : S) ⊢ U ′ <: U , and
Lemma 3.8 (∀ to λ) to show that the value v assigned to x in the evaluation context is λ(y : S ′′ ).s with Γ ′ ⊢ S <: S ′′ .
Similar reasoning applies when u is a field selection x .a (using Lemma 3.9 (µ to Γ(x)) and Lemma 3.10 (µ to ν )),
and simpler reasoning applies when u is a variable, value, or let binding.
Finally, we must check that each reduction step preserves the type of a term. The only non-trivial case is
function application, which reduces x y, where x is bound to a function λ(z : T ).t, to [y/z ] t. Proving preservation
requires a substitution lemma.
Lemma 3.14. If (Γ, x : S) ⊢ t : T and Γ ⊢ y : [y/x ] S then Γ ⊢ [y/x ] t : [y/x ]T .
The lemma is proven by Amin et al. (2016). The proof is standard, with no issues specific to DOT, by induction
on the typing and subtyping rules. Thanks to the use of A-normal form in the DOT syntax, function application
and therefore substitution is needed only for substituting variables for other variables.
Our paper comes with a Coq-formalized version of the presented proof. It is based on the original Coq proof
by Amin et al. (2016).

A Simple Soundness Proof for Dependent Object Types • 1:17

4 DISCUSSION
4.1 Modifications of the Calculus
The most common expected extensions of a calculus are the addition of new forms of values and terms, of new
forms of types and typing rules, and changes to the evaluation rules. Most extensions will change multiple
aspects (e.g., add a new form of value and an associated type), but we discuss each change individually.
The only part of our proof that deals with values are the canonical forms lemmas in Section 3.5 and the final
safety theorem. A new form of value will require an additional canonical forms lemma. The lemma can follow
the general recipe, so it does not need to reason with the general DOT typing rules, but only in invertible typing,
which is designed to make inductive reasoning easy.
The only part of the proof that deals with terms is the final safety theorem. The only non-trivial change
required when adding a new term is to add the evaluation semantics of the term to that theorem.
Adding a new form of type is a more significant change. Given general typing rules for the new type, we must
incorporate the changes into the tight, invertible, and precise typing. Tight typing differs from general typing
only in its handling of abstract type members and type projections, so changes unrelated to those features can be
incorporated directly into tight typing. A change involving abstract type members or type projections requires
corresponding modifications to tight typing. Property 2 (Tight Typing Guarantee) gives a modular specification
to guide the design of such modifications. Specifically, we know that as long as the modified tight typing rules
satisfy the property and we can prove Theorem 3.3 (⊢ to ⊢# ), then the proof recipe and the rest of the whole
soundness proof will continue to hold without requiring non-trivial changes. To incorporate the modifications
into invertible and precise typing, it suffices to follow the general recipe outlined in Section 3.4. Specifically, we
must classify the new tight typing rules as either introducing or eliminating a syntactic construct, and then add
them to either invertible or precise typing, respectively.
A change to the evaluation rules of the calculus does not affect any of the reasoning in Sections 3.1 to 3.5, since
those sections are independent of any particular evaluation semantics. In Section 3.6, we identified the crucial
property that any semantics must satisfy if it is to be sound: any subterm t that it evaluates must be typeable
in an inert context. This is another modular specification that can guide our design of any new operational
semantics. Provided that this property is satisfied, the only non-trivial modifications required in the proof are
localized to the final safety theorem.

4.2

The Struggle for “Good” Bounds

A recurring theme in previous work on DOT has been the struggle to enforce “good” bounds. A type member
declaration {A: S..U } is considered to have “good” bounds if S <: U . If all type members could be forced to
maintain “good” bounds, it would prevent an object of type µ(x : {A: S..U }) from introducing a new, possibly
non-sensical subtyping relationship S <: U from S <: x .A <: U and transitivity. Many of the challenges along
the way to defining a sound DOT calculus arose from the negative interaction between “good” bounds and other
properties, such as narrowing and transitivity. For example, although both {A: ⊥..⊥} and {A: ⊤..⊤} have “good”
bounds, the narrowed type {A: ⊥..⊥}∧{A: ⊤..⊤} causes trouble: in the function λ(x : {A: ⊥..⊥}∧{A: ⊤..⊤}).t,
the body t is type-checked in a typing context in which ⊤ <: x .A <: ⊥.
Not only do “good” bounds interact poorly with other desirable properties, but even defining precisely what
“good” bounds are is surprisingly elusive. Informally, bounds are “good” if S <: U . But in what typing context
should this subtyping relationship hold? In deciding whether the type µ(x : {A: S..U }) should be allowable, it
seems appropriate to respect the recursion implied by µ and use a context that includes x; that is, to require
that (Γ, x : {A: S..U }) ⊢ S <: U . But this statement is always true regardless of the types S and U because
it is self-justifying: (Γ, x : {A: S..U }) ⊢ S <: x .A <: U . If we decide instead to exclude the self-reference x
from the context used to decide whether S <: U , we exclude many desirable types from the definition of “good”

1:18

• Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták

bounds. For example, we consider “bad” the type µ(x : {A: ⊥..⊤} ∧ {B : x .A..x .C} ∧ {C : ⊥..⊤}) that innocently
defines three type members with A <: B <: C, because x .A cannot be a subtype of x .C without x in the context.
We also consider “bad” the following type that defines two type members A <: B constrained to be function
types: µ(x : {A: ⊥..∀(y : ⊥)⊤} ∧ {B : x .A..∀(y : ⊥)⊤}). Again, x .A cannot be a subtype of ∀(y : ⊥)⊤ without x in
the context. Finally, such a definition of “good” bounds restricts the applicability of type aliases: the following
type defines A and B as aliases for ⊤ and ⊥, respectively, but cannot use these aliases in the bounds of C because
x .B 6<: x .A in a context without x: µ(x : {A: ⊤..⊤}∧{B : ⊥..⊥}∧{C : x .B..x .A}). Although it would be possible to
come up with some definition of “good” bounds that handles these specific examples, the definition of what was
intended to be an obvious and intuitive concept would become very complicated, and other more sophisticated
counterexamples would probably continue to exist. Thus, it appears that trying to enforce “good” bounds, and
even trying to define what “good” bounds are, is a dead end.
By contrast, inert types obey a purely syntactic property that is easily defined and checked, without requiring
a subtyping judgement in some typing context that would have to be specified. The property provided by an
inert typing context can be stated precisely and formally (Property 1 (Inert Context Guarantee)).

5 RELATED WORK
5.1 DOT Soundness Proofs
The work most closely related to ours is Amin et al. (2016), which defines and proves sound the variant of the
DOT calculus for which we have developed our alternative soundness proof. That work also defines tight typing,
though it does not use it as pervasively as our proof does.
A central notion of that proof is store correspondence, a relationship between typing contexts and stores of
runtime values. A typing context Γ corresponds to a store s if for every variable x, Γ ⊢! s(x) : Γ(x). Typing and
subtyping in a context Γ that corresponds to some store s have similar predictable behaviour as they do in an
inert context. Part of the proof consists of lemmas that relate internal details of values in stores with internal
details of types in corresponding contexts. By contrast, the property of inert contexts is independent of values,
so our proof does not depend on such lemmas.
Another central notion is “possible types”: if a typing context Γ corresponds to some store s, and s assigns to
variable x the value v, then the possible types of the triple (Γ, x, v) include all types T such that Γ ⊢ x : T . Possible
types serve a similar purpose as our invertible typing rules, to facilitate induction proofs. Unlike invertible typing,
possible types depend on the runtime value v of x. The possible types lemma relates general typing in a context
with a corresponding store to possible types. It serves a similar purpose as our Theorem 3.6 (⊢# to ⊢## ) (which
relates tight to invertible typing), but its proof is more complicated, because it depends on sublemmas that relate
types to values in the context corresponding to the store, and on general typing.
Amin et al. (2016) also prove a similar result as Theorem 3.3 (⊢ to ⊢# ): the general to tight lemma states that
in a context Γ for which there exists some corresponding runtime store s, general typing implies tight typing.
We prove Theorem 3.6 (⊢# to ⊢## ) first, which makes proving Theorem 3.3 (⊢ to ⊢# ) easy. The proof of Amin et al.
(2016) does the analogous steps in the opposite order: it proves the general to tight lemma first, and the possible
types lemma afterwards, using the general to tight lemma in its proof. The proof of the general to tight lemma
is thus complicated because it cannot make use of possible types. Another complication is that the proof of the
general to tight lemma, like the proof of the possible types lemma, depends on sublemmas that relate types to
values in the context corresponding to the store.
Rompf and Amin (2016) define a variant of the DOT calculus with additional features, most significantly subtyping between recursive types. This adds significant complexity to the proof: Lemmas 6 to 11 are needed only
because of this feature. However, subtyping between recursive types is not needed to model Scala. Scala has
nominal subtyping between classes and traits that are explicitly declared to be subtypes using an extends clause.

A Simple Soundness Proof for Dependent Object Types • 1:19
A class or trait declaration in Scala corresponds in DOT to a type member declaration that gives a label A to
a recursive type. The recursive type is used to define the members of the class, and the recursion is necessary
so that members of the class can refer to the object of the class this. However, if this class A is declared to
be a subclass of a similarly declared superclass A′, the corresponding DOT definitions generate the following
subtyping relationships: A <: µA <: A <: A′ <: µA′ <: A′, where µA and µA′ represent the recursive types that
encode the sets of members of classes A and A′ , respectively. These definitions model the subtyping between
classes A and A′ without requiring a direct subtyping relationship between recursive types.
Unlike Amin et al. (2016) and our proof, the proof of Rompf and Amin (2016) does not use tight typing, the
typing relation that neutralizes the two type rules that enable a DOT program to introduce non-sensical subtyping relationships in a custom type system. Instead, the proof uses “precise subtyping”, a restriction of general
subtyping to relationships whose derivation does not end in the transitivity rule.

5.2

History of Scala Calculi

Odersky et al. (2003) introduce ν Obj, a calculus to formalize Scala’s path-dependent types. ν Obj includes abstract
type members, classes, compound (non-commutative) mixin composition, and singleton types, among other
features. However, the calculus lacks several essential Scala features, such as the ability to define custom lower
bounds for type members, and has no top and bottom types. Additionally, ν Obj, unlike Scala, has classes as
first-class values. ν Obj comes with a type soundness proof. The paper also shows that type checking for ν Obj is
undecidable. Cremet et al. (2006) propose Featherweight Scala, which is similar to ν Obj, but without classes as
first-class values. The paper shows that type inference in Featherweight Scala is decidable, but does not prove
type safety. Scalina, introduced by Moors et al. (2008), presents a formalization for higher-kinded types in Scala,
but also without a soundness proof.
Amin et al. (2012) present the first DOT. DOT has fewer syntax-level features than ν Obj: there are no classes,
mixins, or inheritance. However, some of the previously missing crucial Scala features are now present. The
calculus allows refinement of abstract type members through commutative intersections, combining nominal
with structural typing. Type members can have custom lower and upper bounds, and the type system contains
a bottom and top type. The paper comes without a type safety proof, but it explains the challenges and provides
counterexamples to preservation. The paper shows how the environment narrowing property makes proving
soundness complicated: replacing a type in the context with a more precise version can impose a new subtyping
relationship, which could disagree with the existing ones.
Amin et al. (2014) have the first mechanized soundness proof for µDOT, a simplified calculus that excludes
refinements, intersections, and the bottom and top types, and uses big-step semantics. The paper proposes the
idea to circumvent bad bounds by reasoning about types that correspond to runtime values.
Amin et al. (2016) and Rompf and Amin (2016) build on this store correspondence idea, to establish the first
mechanized soundness proofs for DOT calculi with support for type intersection and refinement, and top and
bottom types. The two calculi and soundness proofs were discussed in the previous section.

5.3

Other Related Calculi

Path-dependent types were first introduced in the context of family polymorphism by Ernst (2001). In family
polymorphism, groups of types can form families that correspond to a specific object. Two types from the same
class are considered incompatible if the types are associated with different runtime objects.
Family polymorphism is the foundation of virtual classes, which were introduced in the Beta programming
language (Madsen and Møller-Pedersen 1989) and further developed in gbeta (Ernst 1999). Virtual classes are
nested classes that can be extended or redefined (overridden), and are dynamically resolved through late binding.
Family polymorphism allows for a fine-grained distinction between classes that have the same static path, yet
belong to different runtime objects and can thus have different implementations.

1:20

• Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták

Virtual classes were first formalized and proved type safe in the vc calculus (Ernst et al. 2006). vc is a classbased, nominally-typed calculus with a big-step semantics. To create path-based types, the keyword out is used
to refer to an enclosing object. With its support for classes, inheritance, and mutation of variables, vc is more
complex than DOT, whose purpose is to serve as a simple core calculus for Scala. Additionally, Scala has no
support for virtual classes: the language does not allow class overriding, and its classes are resolved statically at
compile time.
Tribe by Clarke et al. (2007) is a simpler, more general calculus inspired by vc. One of the main distinctions
to vc is that variables, and not just enclosing objects (out), can be used as paths for path-dependent types.
This makes the calculus more general, as it can express subtyping relationships between classes with arbitrary
absolute paths. Tribe comes with a type-safety proof, which is based on a small-step semantics. Expanding
paths to allow variables brings Tribe closer to DOT. However, the complexity of the type system, resulting from
modeling classes and inheritance, and the modeling of virtual classes, which are not present in Scala, leaves DOT
more suitable as a core calculus for Scala.
Amin and Rompf (2017) offer a survey of mechanized soundness proofs for big-step, DOT-like calculi using
definitional interpreters. The paper explores a family of calculi ranging from System F to System D <:> and
general proof techniques that can be applied to this entire family. The paper discusses similarities and differences
between System D <:> and DOT.

6

CONCLUSION

DOT (Amin et al. 2016) is the result of a long effort to develop a core calculus for Scala. Now that there is a sound
version of the calculus, we would like to extend it with other Scala features, such as classes, mixin composition,
side effects, implicit parameters, etc. DOT can be also used as a platform for developing new language features
and for fixing Scala’s soundness issues (Amin and Tate 2016). But these applications are hindered by the complexity of the existing soundness proofs, which interleave reasoning about variables, types, and runtime values,
and their complex interactions.
We have presented a simplified soundness proof for the DOT calculus, formalized in Coq. The proof separates
the reasoning about types, typing contexts, and values from each other. The proof depends on the insight of inert
typing contexts, a syntactic characterization of contexts that rule out any non-sensical subtyping that could be
introduced by abstract type members. The central lemmas of the proof follow a general proof recipe for deducing
properties of terms from their types in full DOT while reasoning only in a restricted, intuitive environment free
from the paradoxes caused by abstract type members. The same recipe can be followed to prove similar lemmas
when the calculus is modified or extended. The result is a simple, modular proof that is well suited for developing
extensions.

REFERENCES
Martı́n Abadi and Luca Cardelli. 1996. A Theory of Objects. Springer.
Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. In A
List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Lecture Notes
in Computer Science), Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella (Eds.), Vol. 9600. Springer, 249–272. DOI:
http://dx.doi.org/10.1007/978-3-319-30936-1 14
Nada Amin, Adriaan Moors, and Martin Odersky. 2012. Dependent Object Types. In International Workshop on Foundations of Object-Oriented
Languages (FOOL 2012).
Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In Proceedings of the 44th ACM SIGPLAN Symposium
on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.).
ACM, 666–679. DOI:http://dx.doi.org/10.1145/3009837
Nada Amin, Tiark Rompf, and Martin Odersky. 2014. Foundations of path-dependent types. In Proceedings of the 2014 ACM International
Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA,
October 20-24, 2014, Andrew P. Black and Todd D. Millstein (Eds.). ACM, 233–249. DOI:http://dx.doi.org/10.1145/2660193.2660216

A Simple Soundness Proof for Dependent Object Types • 1:21
Nada Amin and Ross Tate. 2016. Java and Scala’s type systems are unsound: the existential crisis of null pointers. In Proceedings of the
2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part
of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, Eelco Visser and Yannis Smaragdakis (Eds.). ACM, 838–848.
DOI:http://dx.doi.org/10.1145/2983990.2984004
Dave Clarke, Sophia Drossopoulou, James Noble, and Tobias Wrigstad. 2007. Tribe: a simple virtual class calculus. In Proceedings of
the 6th International Conference on Aspect-Oriented Software Development, AOSD 2007, Vancouver, British Columbia, Canada, March
12-16, 2007 (ACM International Conference Proceeding Series), Brian M. Barry and Oege de Moor (Eds.), Vol. 208. ACM, 121–134. DOI:
http://dx.doi.org/10.1145/1218563.1218578
Vincent Cremet, François Garillot, Sergueı̈ Lenglet, and Martin Odersky. 2006. A Core Calculus for Scala Type Checking. In Mathematical
Foundations of Computer Science, 31st International Symposium, Slovakia.
Erik Ernst. 1999. gbeta – a Language with Virtual Attributes, Block Structure, and Propagating, Dynamic Inheritance. Ph.D. Dissertation.
Department of Computer Science, University of Aarhus, Århus, Denmark.
Erik Ernst. 2001. Family Polymorphism. In ECOOP 2001 - Object-Oriented Programming, 15th European Conference, Budapest, Hungary,
June 18-22, 2001, Proceedings (Lecture Notes in Computer Science), Jørgen Lindskov Knudsen (Ed.), Vol. 2072. Springer, 303–326. DOI:
http://dx.doi.org/10.1007/3-540-45337-7 17
Erik Ernst, Klaus Ostermann, and William R. Cook. 2006. A virtual class calculus. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, J. Gregory Morrisett and
Simon L. Peyton Jones (Eds.). ACM, 270–282. DOI:http://dx.doi.org/10.1145/1111037.1111062
Ole Lehrmann Madsen and Birger Møller-Pedersen. 1989. Virtual Classes: A Powerful Mechanism in Object-Oriented Programming. In
Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA’89), New Orleans, Louisiana, USA, October
1-6, 1989, Proceedings., George Bosworth (Ed.). ACM, 397–406. DOI:http://dx.doi.org/10.1145/74877.74919
Adriaan Moors, Frank Piessens, and Martin Odersky. 2008. Safe type-level abstraction in Scala. In International Workshop on Foundations of
Object-Oriented Languages (FOOL 2008).
Martin Odersky, Vincent Cremet, Christine Röckl, and Matthias Zenger. 2003. A Nominal Theory of Objects with Dependent Types. In
ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Darmstadt, Germany, July 21-25, 2003, Proceedings (Lecture Notes
in Computer Science), Luca Cardelli (Ed.), Vol. 2743. Springer, 201–224. DOI:http://dx.doi.org/10.1007/978-3-540-45070-2 10
Martin Odersky and Matthias Zenger. 2005. Scalable component abstractions. In Proceedings of the 20th Annual ACM SIGPLAN Conference
on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2005, October 16-20, 2005, San Diego, CA, USA, Ralph E.
Johnson and Richard P. Gabriel (Eds.). ACM, 41–57. DOI:http://dx.doi.org/10.1145/1094811.1094815
Leo Osvald, Grégory M. Essertel, Xilun Wu, Lilliam I. González Alayón, and Tiark Rompf. 2016. Gentrification gone too far? affordable 2ndclass values for fun and (co-)effect. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming,
Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016,
Eelco Visser and Yannis Smaragdakis (Eds.). ACM, 234–251. DOI:http://dx.doi.org/10.1145/2983990.2984009
Benjamin C. Pierce. 2002. Types and programming languages. MIT Press.
Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016,
Amsterdam, The Netherlands, October 30 - November 4, 2016, Eelco Visser and Yannis Smaragdakis (Eds.). ACM, 624–641. DOI:
http://dx.doi.org/10.1145/2983990.2984008
Alceste Scalas and Nobuko Yoshida. 2016. Lightweight Session Programming in Scala. In 30th European Conference on Object-Oriented
Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy (LIPIcs), Shriram Krishnamurthi and Benjamin S. Lerner (Eds.), Vol. 56. Schloss
Dagstuhl - Leibniz-Zentrum fuer Informatik, 21:1–21:28. DOI:http://dx.doi.org/10.4230/LIPIcs.ECOOP.2016.21

1:22

7

• Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták

APPENDIX
Proof of Lemma 3.7 (∀ to Γ(x)).
inert Γ

Γ ⊢ x : ∀(y : T )U

inert Γ

Γ ⊢# x : ∀(y : T )U

inert Γ

Γ ⊢## x : ∀(y : T )U

Theorem 3.6 (⊢# to ⊢## )
Induction on ⊢##

Γ ⊢! x : ∀(y : T ′ )U ′
Γ ⊢ T <: T ′
′
′
(Γ, y : T ) ⊢ U <: U

inert Γ
inert Γ

Theorem 3.3 (⊢ to ⊢# )

Γ ⊢! x : ∀(y : T ′ )U ′

Γ ⊢ T <: T ′

Γ(x) = ∀(y : T ′ )U ′

inert Γ

(Γ, y : T ) ⊢ U ′ <: U

Γ ⊢ T <: T ′

Narrowing
Induction on ⊢!

(Γ, y : T ) ⊢ U ′ <: U


Proof of Lemma 3.9 (µ to Γ(x)).
inert Γ

Γ ⊢ x : {a : T }

inert Γ

Γ ⊢# x : {a : T }

inert Γ

Γ ⊢## x : {a : T }

inert Γ
inert Γ

Theorem 3.3 (⊢ to ⊢# )
Theorem 3.6 (⊢# to ⊢## )

Γ ⊢! x : {a : T ′ }

Γ ⊢ T ′ <: T

Γ(x) = µ(x : ··· ∧ {a : T ′ } ∧ ···)

Induction on ⊢##

Γ ⊢ T ′ <: T

Induction on ⊢!


Proof of Lemma 3.10 (µ to ν ).
inert Γ

Γ ⊢ v : µ(x : ··· ∧ {a : T } ∧ ···)

inert Γ

Γ ⊢# v : µ(x : ··· ∧ {a : T } ∧ ···)

inert Γ

Γ ⊢## v : µ(x : ··· ∧ {a : T } ∧ ···)
inert Γ
inert Γ

Theorem 3.3 (⊢ to ⊢# )
Theorem 3.6 (⊢# to ⊢## )

Γ ⊢! v : µ(x : ··· ∧ {a : T } ∧ ···)

v = ν (x : ··· ∧ {a : T } ∧ ···)(··· ∧ {a = t } ∧ ···)

Induction on ⊢##

Γ ⊢t:T

Inversion of {}-I!



A Simple Soundness Proof for Dependent Object Types • 1:23
Term typing
Γ(x) = T

Γ ⊢t:T
(Γ, x : T ) ⊢ u : U
x < fv(U )

(Var)

Γ ⊢x:T

Γ ⊢ let x = t in u : U
(Γ, x : T ) ⊢ t : U

x < fv(T )

Γ ⊢ λ(x : T ).t : ∀(x : T )U
Γ ⊢ x : ∀(z : S)T

(Γ, x : T ) ⊢ d : T
Γ ⊢ ν (x : T )d : µ(x : T )
Γ ⊢ x : {a : T }
Γ ⊢ x .a : T
(Γ, z : T ) ⊢ t : U
Γ ⊢ {a = t } : {a : U }
Γ ⊢ {A = T } : {A: T ..T }

Γ ⊢x:T

(Rec-I)

Γ ⊢ x : µ(x : T )

Γ ⊢ y: S

Γ ⊢ x y : [y/z ]T

(All-I)

Γ ⊢ x : µ(z : T )

(All-E)

(Rec-E)

Γ ⊢ x : [x/z ]T
Γ ⊢x:T

({}-I)

Γ ⊢x: U

(And-I)

Γ ⊢ x: T ∧U
Γ ⊢t:T

({}-E)

Γ ⊢ T <: U

(Sub)

Γ ⊢t:U
Γ ⊢ d 1 : T1
Γ ⊢ d 1 : T2
dom(d 1 ), dom(d 2 ) disjoint

(Def-Trm)

Γ ⊢ d 1 ∧ d 2 : T1 ∧ T2

(Def-Typ)

(Let)

(AndDef-I)

Subtyping rules
Γ ⊢ T <: ⊤

(Top)

Γ ⊢ S <: T

Γ ⊢ x : {A: S..T }

Γ ⊢ S <: U

Γ ⊢ S <: T ∧ U
Γ ⊢ ⊥ <: T

Γ ⊢ S <: x .A
(<:-And)

(Bot)

Γ ⊢ T ∧ U <: T (And1 -<:)
Γ ⊢ T <: T

(Refl)

Γ ⊢ T <: U
Γ ⊢ {a : T } <: {a : U }
(Fld-<:-Fld)
Γ ⊢ S 2 <: S 1
Γ ⊢ T1 <: T2
Γ ⊢ {A: S 1 ..T1 } <: {A: S 2 ..T2 }

(<:-Sel)

Γ ⊢ T ∧ U <: U (And2 -<:)
Γ ⊢ S <: T

Γ ⊢ S <: U

Γ ⊢ x : {A: S..T }
Γ ⊢ x .A <: T
Γ ⊢ S <: T

Γ ⊢ S <: T ∧ U

Γ ⊢ T <: U

Γ ⊢ S <: U
(<:-And)

(Typ-<:-Typ)

(Sel-<:)

Γ ⊢ S 2 <: S 1
(Γ, x : S 2 ) ⊢ T1 <: T2
Γ ⊢ ∀(x : S 1 )T1 <: ∀(x : S 2 )T2

(Trans)

(All-<:-All)

Fig. 7. DOT Type Rules (Amin et al. 2016). Definition type assignment rules are shown in Figure 3.

