Type Soundness for Dependent Object Types (DOT)

Tiark Rompf ∗ Nada Amin†

tifact
∗ Ar t * Complete
Purdue University, USA: {firstname}@purdue.edu

*
en

O O * C on *

AE ll Doc Ev
*
t
sis
PSL A

We
†

C *
EPFL, Switzerland: {first.last}@epfl.ch

se

um
eu

e
nt R
ed
* Easy toalu
*
at e d

Abstract the DOT (Dependent Object Types) [4] family was finally
presented in 2014 [5].
Scala’s type system unifies aspects of ML modules, object-
The calculus proved sound by Amin et al. [5] is µDOT, a
oriented, and functional programming. The Dependent Ob-
core calculus that distills the essence of Scala’s objects that
ject Types (DOT) family of calculi has been proposed as a
may contain type members in addition to methods and fields,
new theoretic foundation for Scala and similar expressive
along with path-dependent types, which are used to access
languages. Unfortunately, type soundness has only been es-
such type members. µDOT models just these two features–
tablished for restricted subsets of DOT. In fact, it has been
records with type members and type selections on variables–
shown that important Scala features such as type refinement
and nothing else. This simple system already captures some
or a subtyping relation with lattice structure break at least
essential programming patterns, and it has a clean and in-
one key metatheoretic property such as environment narrow-
tuitive theory. In particular, it satisfies the intuitive and mu-
ing or invertible subtyping transitivity, which are usually re-
tually dependent properties of environment narrowing and
quired for a type soundness proof.
subtyping transitivity, which are usually key requirements
The main contribution of this paper is to demonstrate
for a soundness proof.
how, perhaps surprisingly, even though these properties are
Alas, Amin et al. also showed that adding other important
lost in their full generality, a rich DOT calculus that includes
Scala features such as type refinement, mixin composition,
recursive type refinement and a subtyping lattice with in-
or just a bottom type breaks at least one of these properties,
tersection types can still be proved sound. The key insight
which makes a soundness proof much harder to come by.
is that subtyping transitivity only needs to be invertible in
The main contribution of this paper is to demonstrate
code paths executed at runtime, with contexts consisting en-
how, perhaps surprisingly, even though these properties are
tirely of valid runtime objects, whereas inconsistent subtyp-
lost in their full generality, a richer DOT calculus that in-
ing contexts can be permitted for code that is never executed.
cludes both recursive type refinement and a subtyping lat-
Categories and Subject Descriptors D.3.3 [Programming tice with full intersection and union types can still be proved
Languages]: Language Constructs and Features sound. The key insight is that proper subtyping transitivity
Keywords dependent object types, DOT, Scala, soundness only needs to hold for types assigned to runtime objects, but
not for arbitrary code that is never executed.
1. Introduction The paper is structured around the main contributions as
Modern expressive programming languages such as Scala follows:
integrate and generalize concepts from functional program-
ming, object oriented programming and ML-style module • We present the first sound calculus of the DOT family
systems [32]. While most of these features are understood that includes recursive type refinement and a subtyping
on a theoretical level in isolation, their combination is not, lattice with intersection and union types: first informally
and the gap between formal type theoretic models and what with examples (Section 2), then formally (Section 3).
is implemented in realistic languages is large. • We discuss the key properties that make a soundness
In the case of Scala, developing a sound formal model proof difficult (Section 4).
that captures a relevant subset of its type system has been • We present our soundness result. First, we give a small-
an elusive quest for more than a decade. After many false
step operational semantics (Section 5). Then we explain
starts, the first mechanized soundness proof for a calculus of
the proof strategy and key lemmas in details (Section 6).
• We offer some perspective on how foundational type-
theoretic work influences practice (Section 7).
This is the author’s version of the work. It is posted here for your personal use. Not for
redistribution. The definitive version was published in the following publication: We discuss related work in Section 8 and offer conclud-
OOPSLA’16, November 2–4, 2016, Amsterdam, Netherlands ing remarks in Section 9. Our mechanized Coq proofs are
ACM. 978-1-4503-4444-9/16/11... available from http://oopsla16.namin.net.
http://dx.doi.org/10.1145/2983990.2984008

624
2. Types in Scala and DOT The actual List type is defined inside a container listModule,
which we can think of as a first-class module. In an ex-
Scala is a large language that combines features from func-
tended DOT calculus error may signify an ‘acceptable’ run-
tional programming, object-oriented programming and mod-
time error or exception that aborts the current execution and
ule systems. Scala unifies many of these features (e.g. ob-
transfers control to an exception handler. In the case that we
jects, functions, and modules) [32] but still contains a large
study, without such facilities, we can model the abortive be-
set of distinct kinds of types. These can be broadly classified
havior of error as a non-terminating function, for example
[28] into modular types:
def error(): Bot = error().
named type: scala.collection.BitSet
compound type: Channel with Logged
refined type: Channel { def close(): Unit }
And functional types : Nominality through Ascription In most other settings
parameterized type: List[String]
(e.g. object-oriented subclassing, ML module sealing), nom-
existential type: List[T] forSome { type T } inality is enforced when objects are declared or constructed.
higher-kinded type: List Here we can just assign a more abstract type to our list mod-
While this variety of types enables programming styles ule:
appealing to programmers with different backgrounds (Java, type ListAPI = { m =>
type List <: { this =>
ML, Haskell, ...), not all of them are essential. Further uni-
type Elem
fication and an economy of concepts can be achieved by re-
def head(): this.Elem
ducing functional to modular types as follows: def tail(): m.List & { type Elem <: this.Elem }
class List[Elem] {} ❀ class List { type Elem } }
List[String] ❀ List { type Elem = String } def nil(): List & { type Elem = Bot }
List[T] forSome { type T } ❀ List def cons[T]: T =>
List ❀ List m.List & { type Elem <: T } =>
This unification is the main thrust of the calculi of the m.List & { type Elem <: T }
DOT family. A further thrust is to replace Scala’s compound }
types A with B with proper intersection types A & B. It is Types List and Elem are abstract, and thus exhibit nominal
worth noting that the correspondence between higher-kinded as opposed to structural behavior. Since modules are just ob-
types and existential types suggested above is not exact, in jects, it is perfectly possible to pick different implementa-
particular with respect to well-kindedness constraints and tions of an abstract type based on runtime parameters.
partial application to type arguments. Before presenting our val mapImpl = if (size < 100) ListMap else HashMap
DOT variant in a formal setting in Section 3, we introduce
the main ideas with some high-level programming examples.
Objects and First Class Modules In Scala and in DOT, ev- Polymorphic Methods In the code above, we have still
ery piece of data is conceptually an object and every opera- used the functional notation cons[T](...) for parametric
tion a method call. This is in contrast to functional languages methods. We can desugar the type parameter T into a proper
in the ML family that are stratified into a core language and a method parameter x with a modular type, and at the same
module system. Below is an implementation of a functional time desugar the multi-argument function into nested anony-
list data structure: mous functions:
val listModule = new { m => def cons(x: { type A }) = ((hd: x.A) => ... )
type List = { this =>
References to T are replaced by a path-dependent type x.A.
type Elem
def head(): this.Elem
We can further desugar the anonymous functions into objects
def tail(): m.List & { type Elem <: this.Elem }
with a single apply method:
} def cons(x: { type A }) = new {
def nil() = new { this => def apply(hd: x.A) = new {
type Elem = Bot def apply(tl: m.List & { type Elem <: x.A }) =
def head() = error() new { this =>
def tail() = error() type Elem = x.A
} def head() = hd
def cons[T](hd: T)(tl: m.List & { type Elem <: T }) = def tail() = tl
new { this => }}}
type Elem = T More generally, with these desugarings, we can encode
def head() = hd the polymorphic λ-calculus System F [20, 35] and its exten-
def tail() = tl
sion with subtyping, System F<: [9], by defining a pointwise
}}
mapping over types and terms:

625
 Intersection and Union Types At the end of the day, we
X ❀ x.A want only one centralized configuration for our system, and
we can create one by assigning an intersection type:
∀(X <: S)T ❀ { def apply(x: { type A <: S }): T }
val globalConf: DBConfig & AuthConfig = new {
Λ(X <: S)t ❀ new { def apply(x: { type A <: S }) = t } def getDB = "myDB"
def getAuth = "myAuth"
t[U ] ❀ t.apply({ type A = U })
}
Since globalConf corresponds to both DBConfig and AuthConfig,
Apart from the translation of type variables into term we can use it to initialize both services:
variables with type members, another difference is that F<: dbs.init(globalConf)
supports only upper bounded type variables, while Scala and auths.init(globalConf)
DOT allow both lower and upper bounds. This gives rise But we would like to abstract even more.
to very fine grained choices of translucency, i.e. how much With the List definition presented earlier, we can build a
implementation details are revealed for a partially abstract list of services (using :: as syntactic sugar for cons):
type, and also allows a precise modelling of covariance and val services = auths::dbs::nil()
contravariance. We will see an example of a lower bounded
We define an initialization function for a whole list of ser-
type member { type Config >: T} below.
vices:
It is easy to see that while path-dependent types can
def initAll[T](xs:List[Service { type Config >: T }])(c: T) =
encode System F, the reverse is not likely true. For example,
xs.foreach(_ init c)
the following function is expressible in Scala and DOT but
does not have a System F equivalent: λ(x : { type A }).x Which we can then use as:
initAll(services)(globalConf)
How do the types play out here? The definition of List
and cons makes the type member Elem covariant. Thus, the
Path-Dependent Types Let us consider another example to type of auths::dbs::nil() corresponds to
illustrate path-dependent types: a system of services, each List & {
with a specific type of configuration object. Here is the type Elem = Service & {
type Config: (DBConfig & AuthConfig) ..
abstract interface:
(DBConfig | AuthConfig)
type Service {
}
type Config
}
def default: Config
def init(data: Config): Unit The notation type T: S..U denotes that type member T is
} lower bounded by S and upper bounded by U. Here, Config is
We now create a system consisting of a database and an lower bounded by the greatest lower bound (the intersection,
&) and upper bounded by the least upper bound (the union, |)
authentication service, each with their respective configura-
tion types: of the types DBConfig and AuthConfig. Since the Config mem-
type DBConfig { def getDB: String }
ber is lower bounded by DBConfig & AuthConfig, passing an
type AuthConfig { def getAuth: String } object of that type to init is legal.
val dbs = new Service { Records and Refinements as Intersections Subtyping al-
type Config = DBConfig lows us to treat a type as a less precise one. Scala provides
def default = new DBConfig { ... }
a dual mechanism that enables us to create a more precise
def init(d:Config) = ... d.getDB ...
}
type by refining an existing one.
val auths = new Service { type PersistentService = Service { a =>
type Config = AuthConfig def persist(config: a.Config)
def default = new AuthConfig { ... } }
def init(d:Config) = ... d.getAuth ... To express the type PersistentService by desugaring the
} refinement into an intersection type, we need a “self” vari-
We can initialize dbs with a new DBConfig, and auths with able (here a) to close over the intersection type, in order to
a new AuthConfig, but not vice versa. This is because each refer to the abstract type member Config of Service:
object has its own specific Config type member and thus, type PersistentService = { a => Service & {
dbs.Config and auths.Config are distinct path-dependent def persist(config: a.Config)
types. Likewise, if we have a service lam: Service with- }}
out further refinement of its Config member, we can still call Our variant of DOT uses intersection types also to model
lam.init(lam.default) but we cannot create a lam.Config the type of records with multiple type, value, or method
value directly, because Config is an abstract type in Service. members:

626
{ def foo(x: S1): U1 ; def bar(y: S2): U2 } ❀ rection as shown in the following example, which fails with
{ def foo(x: S1): U1 } & { def bar(y: S2): U2 } a runtime cast exception:
With this encoding of records, we benefit again from an trait A { type L >: Any}
economy of concepts. def id1(a: A, x: Any): a.L = x
val p: A { type L <: Nothing } = null
Soundness? Our aim for DOT is a strong type soundness def id2(x: Any): Nothing = id1(p, x)
result of the form “well-typed programs don’t go wrong”, id2("boom!")
i.e. to show the total absence of runtime errors. Clearly we The problem is that id2 is a “safe” cast from Any to Nothing,
cannot expect the same strong result to hold for Scala, as which we cannot support in a sound language. The subtyping
Scala includes unsafe features like null values and unsafe lattice collapses through a null path with bad bounds. The
casts. Especially null values make a strong soundness result issue is described in more detail by Amin and Tate [6], who
impossible as they violate the key canonical forms property: show that – remarkably – the same problem also exists in
a value that has a given type might not actually be a proper Java, even though Java does not have path-dependent types.
object of this type at runtime, but it might instead be null. Since this example uses an explicit null, one might be
A more realistic notion of soundness needs to include the tempted to dismiss the issue by saying “null is unsound
possibility of benign runtime failures. A desirable guarantee anyways”. But what is disturbing is that the result is not a
in this setting is that modules that do not introduce null val- NullPointerException but a ClassCastException, even though
ues cannot be blamed for NullPointerExceptions, and mod- no “unsafe” casts are used. Also, no pointer is dereferenced,
ules that do not perform unsafe casts cannot be blamed for so while a NullPointerException could be more easily ratio-
ClassCastExceptions. nalized (e.g. as a “type-level” null deferencing), it would still
In this light, it is important to note that Scala has some be unexpected, even for weak notions of soundness.
fundamental soundness bugs related to path-dependent types, The use of null is also not crucial, as we show in Sec-
even with respect to these weaker notions of soundness. tion 7.1. The issue is deeper, and the take-away is that paths
Some manifestations of these bugs have been known for a always need to refer to proper objects, which are guaranteed
long time (the Scala issue tracker lists unfixed soundness to have “good bounds” by construction, and thus serve as
problems dating back at least to 2008 [40]), but they have constructive evidence, i.e. witnesses for the subtyping rela-
been properly understood only recently, during the course of tions they introduce via transitivity. As we discuss in Sec-
this work. We discuss the general issue next, with a particu- tion 4, attempting to incorporate “good bounds” into well-
lar example related to null values [6]. formedness of types is not sufficient, as “good bounds” are
The key soundness challenge with path-dependent types not preserved under narrowing. Because they do not pro-
is to avoid “bad bounds”, i.e. type members like type T: S..U vide any actual witness ensuring that the subtyping relations
where S is not a subtype of U, e.g. type T: String..Int. If an added are valid, null values, unevaluated lazy vals, mutable
object x were allowed to have such a type member, we could variables, as well as arbitrary (non-terminating) term depen-
use it to safely treat a String first as type x.T, and then as Int, dencies need to be excluded from paths. The core DOT cal-
but of course this would be unsound: any attempt to treat a culus presented in this paper does not include these features,
String as an Int will lead to a cast exception at runtime! but we discuss potential avenues of extension in Section 7.2.
The formalization effort behind DOT has shown that pre- Our work on DOT helped identify and clarify these
venting such “bad bounds” is harder than previously thought soundness issues, and identify potential fixes. In the case
(see Section 4.3), and that the mechanisms implemented in of null, there are no easy fixes: the DOT effort has under-
the Scala compiler are not sufficient. More precisely, it is lined the necessity for future versions of Scala and similar
necessary to enforce constraints on type members and their languages to consider nullability explicitly in the type sys-
bounds at object creation time (see Section 4.5). The canon- tem.
ical forms property ensures that an object that is supposed
to have a type member T: S..U was indeed created with type 3. Formal Model of DOT
member T set to a type inbetween S and U – thus provid-
ing constructive evidence that S <: U. However, null is in- Figure 1 shows the syntax and static semantics of the DOT
compatible with canonical forms: null is assignable to any calculus we study. For readability, we omit well-formedness
other type, but it does not have any members on which con- requirements from the rules, and assume all types to be syn-
straints could be enforced. Thus it is clear that we can cre- tactically well-formed in the given environment. We write
ate a problem with type selections x.T when x is null. The T x when x is free in T . The type assignment syntax is over-
potential danger of this has been realized early on in the his- loaded: we use Γ ⊢ t : T for the usual term type assignment
tory of Scala, and the Scala compiler has ad-hoc checks to and Γ ⊢ t :! T for a path type assignment used in subtyp-
prevent direct uses of null. However, with the new observa- ing of type selections, specifically rules (S EL 1) and (S EL 2).
tion that “good bounds” are not preserved by narrowing (see We use Γ ⊢ t :(!) T for rules that are defined for both cases,
Section 4.3), it becomes easy to thwart those checks via indi- specifically rules (VAR ), (VARU NPACK ), and (S UB ).

627
Syntax

S, T, U ::= Type
⊤ top type t, u ::= Term
x, y, z Variable ⊥ bottom type x variable reference
L Type label L : S..U type member {z ⇒ d} new instance
m Method label m(x : S) : U x method member t.m(t) method invocation
x.L type selection d ::= Initialization
Γ ::= ∅ | Γ, x : T Context {z ⇒ T z } recursive self type L=T type initialization
T ∧T intersection type m(x) = t method initialization
T ∨T union type

Subtyping Γ ⊢ S <: U Type assignment Γ ⊢ t :(!) T

Lattice structure Variables, self packing/unpacking
Γ ⊢ ⊥ <: T (B OT ) Γ ⊢ T <: ⊤ (T OP ) Γ(x) = T
(VAR )
Γ ⊢ T1 <: T Γ ⊢ T <: T1 Γ ⊢ x :(!) T
(A ND 11) (O R 21)
Γ ⊢ T1 ∧ T2 <: T Γ ⊢ T <: T1 ∨ T2
Γ ⊢ x : Tx Γ ⊢ x :(!) {z ⇒ T z }
(VAR PACK ) (VARU NPACK )
Γ ⊢ T2 <: T Γ ⊢ T <: T2 Γ ⊢ x : {z ⇒ T } z
Γ ⊢ x :(!) T x
(A ND 12) (O R 22)
Γ ⊢ T1 ∧ T2 <: T Γ ⊢ T <: T1 ∨ T2

Γ ⊢ T <: T1 , T <: T2 Γ ⊢ T1 <: T , T2 <: T

(A ND 2) (O R 1)
Γ ⊢ T <: T1 ∧ T2 Γ ⊢ T1 ∨ T2 <: T Subsumption

Γ ⊢ t :(!) T1 , T1 <: T2
Type and method members (S UB )
Γ ⊢ t :(!) T2
Γ ⊢ S2 <: S1 , U1 <: U2
(T YP )
Γ ⊢ L : S1 ..U1 <: L : S2 ..U2
Γ ⊢ S2 <: S1 Method invocation
Γ, x : S2 ⊢ U1x <: U2x
(F UN ) Γ ⊢ t : (m(x : T1 ) : T2x ) , y : T1
Γ ⊢ m(x : S1 ) : U1x <: m(x : S2 ) : U2x (TA PP VAR )
Γ ⊢ t.m(y) : T2y
Path selections
Γ ⊢ t : (m(x : T1 ) : T2 ) , t2 : T1
Γ ⊢ x.L <: x.L (S EL X)
Γ ⊢ t.m(t2 ) : T2
(TA PP )

Γ[x] ⊢ x :! (L : T..⊤) Γ[x] ⊢ x :! (L : ⊥..T )

(S EL 2) (S EL 1)
Γ ⊢ T <: x.L Γ ⊢ x.L <: T
Object creation

Recursive self types (labels disjoint)

Γ, z : T1z ⊢ T1z <: T2z Γ, x : T1x ∧ . . . ∧ Tnx ⊢ di : Tix ∀i, 1 ≤ i ≤ n
(TN EW )
Γ ⊢ {z ⇒ T1z } <: {z ⇒ T2z }
(B IND X)
Γ ⊢ {x ⇒ d1 . . . dn } : {z ⇒ T1z ∧ . . . ∧ Tnz }

Γ, z : T1z ⊢ T1z <: T2 Member initialization Γ ⊢ d:T

(B IND 1)
Γ ⊢ {z ⇒ T1z } <: T2
Γ ⊢ T <: T
(DT YP )
Transitivity Γ ⊢ (L = T ) : (L : T..T )
Γ ⊢ T1 <: T2 , T2 <: T3
(T RANS ) Γ, x : T1 ⊢ t : T2
Γ ⊢ T1 <: T3 (DF UN )
Γ ⊢ (m(x) = t) : (m(x : T1 ) : T2 )

Figure 1. DOT Syntax and Type System

628
 Compared to the original DOT proposal [4], which used signment, the rules for variable packing and unpacking,
several auxiliary judgements such as membership and ex- (VAR PACK ) and (VARU NPACK ), serve as introduction and
pansion, the presentation here is vastly simplified, and uses elimination rules, enabling recursive types to be compared
only subtyping to access function and type members. Com- to other types as well. Since types can be recursive, and
pared to µDOT [5], the calculus is much more expressive, since subtype comparisons may introduce temporary bind-
and includes key features like intersection and union types, ings that may need to be unpacked, there are two contractive-
which are absent in µDOT. ness restrictions on type selections that ensure well-founded
The Scala syntax used above maps to the formal notation induction in the proofs (Section 6.2). First, the typing as-
in a straightforward way: signment judgement used in type selections, Γ ⊢ x :! T ,
{ type T = Elem } ❀ T : Elem..Elem forbids (VAR PACK ). Note that this typing is used to match
{ type T >: S <: U } ❀ T : S..U an unpacked type member type, anyways. Second, type se-
{ def m(x: T) = t } ❀ m(x) = t lections restrict the environment to disregard bindings in-
A & B, A | B ❀ A ∧ B, A ∨ B troduced after the self. In general, environments have the
In addition, top-level definitions of vals and types desugar form Γ = y : T , z : T , with proper term bindings y fol-
to local definitions, by the usual desugaring of let-bindings lowed by bindings z introduced by subtype comparisons.
into applications. Intersection and union types, along with The notation Γ[x] in rules (S EL 1) and (S EL 2) signifies that
the ⊥ and ⊤ types, provide a full subtyping lattice. all z : T bindings to the right of x are dropped from Γ,
Note that each kind of object member, i.e. a type member where x can be either a proper term binding y or a z bind-
L = T or a method member m(x) = t, includes its specific ing. While these restrictions are necessary for the proofs,
label L or m, respectively. The same holds for the corre- they do not limit expressiveness of the type system in any
sponding types. A sensible alternative would be to decou- significant way. Similar, and in many cases more impeding,
ple object membership and the underlying primitive types restrictions are standard in type systems with recursive types
for methods (having dependent function types instead) and [33]. Intuitively, note that the transitivity rule can always
types (having “type tag” types instead that can be derefer- be used to relate type selections across the context. Note as
enced as types). Because objects are recursive in their self well that there is no (B IND 2) rule, symmetric to (B IND 1),
type, we find coupling the labels more intuitive in terms of which is another kind of contractiveness restriction. We con-
reasoning. jecture that these contractiveness restrictions could be lifted
When typing object creation, rules (TN EW ) and (DT YP ) without breaking soundness, since we can always construct
ensure syntactically that object values have “good bounds”, explicit conversion functions that use rules (VAR PACK ) and
avoiding soundness issues due to lattice collapsing (which (VARU NPACK ) on proper term bindings. However, remov-
we explain in Section 4.3). First, labels are disjoint. Sec- ing these contractiveness restrictions would likely require
ond, type member initialization requires exact aliases, not different and harder to mechanize proof techniques such as
bounds. Finally, to avoid circular reasoning, the checking of a coinductive interpretation of subtyping.
member initialization is done without subsumption on the In the version of DOT presented here, we make the tran-
self type. sitivity rule (T RANS ) explicit, although, as we will see in
In subtyping, members of the same label and kind can Section 4, we will sometimes need to ensure that we can
be compared via rules (T YP ) and (F UN ). The type member eliminate uses of this rule from subtyping derivations so that
upper bound, and method result type are covariant while the the last rule is a structural one.
type member lower bound and the method parameter type The aim of DOT is to be a simple, foundational calculus
are contravariant – as is standard. In rule (F UN ), we allow in the spirit of FJ [22], without committing to specific deci-
some dependence between the parameter type and the return sions for nonessential things. Hence, implementation inheri-
type of a method, when the argument is a variable. This is tance, mixin strategy, and prototype vs class dispatch are not
another difference to previous versions of DOT [4, 5], which considered.
did not have such dependent method types.
If a variable x can be assigned a type member L, then 4. Static Properties of DOT
the type selection x.L is valid, and can be compared with
any upper bound when it is on the left, and with any lower Having introduced the syntax and static semantics of DOT,
bound when it is on the right, via rules (S EL 1) and (S EL 2). we turn to its metatheoretic properties. Our main focus of in-
Furthermore, a type selection is reflexively a subtype of itself terest will be type safety: establishing that well-typed DOT
via rule (S EL X). This rule is explicit, so that even abstract programs do not go wrong. Of course, type safety is only
type members can be compared to themselves. meaningful with respect to a dynamic semantics, which we
Finally, recursive self types can be compared to each will discuss in detail in Section 5. Here, we briefly touch
other via (B IND X). They can also be dropped if the self some general static properties of DOT and then discuss spe-
identifier is not used, via rule (B IND 1). During type as- cific properties of the subtyping relation, which (or their ab-
sence!) makes proving type safety a challenge.

629
Decidability Type assignment and subtyping are undecid- the argument and result types from a given subtype relation
able in DOT. This follows directly from the fact that DOT between two function types, in particular to derive
can encode F<: , and that these properties are undecidable T2 <: T1 and U1 <: U2
there.
from
Type Inference DOT has no principal types and no global
m(x : T1 ) : U1 <: m(x : T2 ) : U2
Hindley-Milner style type inference procedure. But as in
Scala, local type inference based on subtype constraint solv- when relating method types from a call site and the definition
ing [34, 31] is possible, and in fact easier than in Scala due site.
to the existence of universal greatest lower bounds and least Transitivity is required to collapse multiple subsumption
upper bounds through intersection and union types. For ex- steps that may have been used in type assignment. Narrow-
ample, in Scala, the least upper bound of the two types C and ing can be seen as an instance of the Liskov substitution prin-
D is approximated by an infinite sequence: ciple, preserving subtyping if a binding in the environment
trait A { type T <: A } is replaced with a subtype. Narrowing is required for appli-
trait B { type T <: B } cation, when the argument type is a subtype of the declared
trait C extends A with B { type T <: C } parameter type.
trait D extends A with B { type T <: D } Unfortunately, as we will show next, these properties do
lub(C, D) ~ A with B { type T <: A with B { type T <: ... } } not hold simultaneously in DOT, at least not in their full
DOT’s intersection and union types remedy this brittleness. generality.
While the term syntax and type assignment given in Fig-
ure 1 is presented in Curry-style, without explicit type an- 4.2 Inversion, Transitivity and Narrowing
notations except for type member initializations, a Church- First of all, let us take note that these properties are mutually
style version with types on method arguments (as required dependent. In Figure 1, we have included (T RANS ) as an
for local type inference) is possible just as well. Our mech- axiom. If we drop this axiom, then we obtain key rules like
anized proof handles both Curry and Church style via op- (I NV F UN ) by direct inversion of the corresponding typing
tional parameter and return types. The Curry-style presenta- derivation, as only the structural rule (F UN ) can match the
tion glosses over explicit upcasts – a feature that can easily pattern of comparing two function types. But then, we would
be added, for example through a typed let construct. Upcasts need to prove (T RANS ) as a lemma.
– whether explicit or implicit in the surface syntax – matter Transitivity and narrowing are also mutually dependent.
for nominality by ascription, as discussed in Section 2. Transitivity requires narrowing in the following case, where
4.1 Properties of Subtyping we are given
The relevant static properties we are interested in with regard {z ⇒ T1 } <: {z ⇒ T2 } <: {z ⇒ T3 }
to type safety are transitivity, narrowing, and inversion of and want to derive:
subtyping and type assignment. They are defined as follows.
{z ⇒ T1 } <: {z ⇒ T3 }
Inversion of subtyping (example for functions):
By inversion we obtain
Γ ⊢ m(x : S1 ) : U1x <: m(x : S2 ) : U2x
(I NV F UN ) z : T1 ⊢ T1 <: T2 z : T2 ⊢ T2 <: T3
Γ ⊢ S2 <: S1 Γ, x : S2 ⊢ U1x <: U2x
and we narrow the right-hand derivation to z : T1 ⊢ T2 <:
Transitivity of subtyping: T3 before we apply transitivity inductively to obtain z : T1 ⊢
Γ ⊢ T1 <: T2 , T2 <: T3 T1 <: T3 and thus {z ⇒ T1 } <: {z ⇒ T3 }.
(T RANS ) Narrowing depends on transitivity in the case for type
Γ ⊢ T1 <: T3
selections
Narrowing: x.L <: T or its counterpart T <: x.L
Γ1 ⊢ T1 <: T2 Γ2 ⊢ T3 <: T4 Assume that we want to narrow x’s binding from T2 in
Γ1 = Γ2 (x → T1 ) Γ2 (x) = T2 Γ2 to T1 in Γ1 , with Γ1 ⊢ T1 <: T2 . By inversion we obtain
(NARROW )
Γ1 ⊢ T3 <: T4 x : (L : ⊥..T )
where Γ1 = Γ2 (x → T1 ) denotes that Γ1 is like Γ2 except and, disregarding rules (VAR PACK ) and (VARU NPACK ) we
the binding for x maps to T1 . can deconstruct this assignment as
On a high-level, the basic challenge for type safety is to Γ2 (x) = T2 Γ2 ⊢ T2 <: (L : ⊥..T ).
establish that some value that e.g. has a function type actu-
ally is a function, with arguments and result corresponding We first apply narrowing inductively and then use transi-
to the given type. This is commonly known as the canonical tivity to derive the new binding
forms property. Inversion of subtyping is required to extract Γ1 (x) = T1 Γ1 ⊢ T1 <: T2 <: (L : ⊥..T ).

630
 On first glance, the situation appears to be similar to Now, consider substituting x in t with u, given
simpler calculi like F<: , for which the transitivity rule can Γ ⊢ u : {z ⇒ L : S z ..U z ∧ m(_) : T z }
be shown to be admissible, i.e. implied by other subtyping
rules and hence proved as a lemma and dropped from the First, tx might invoke method x.m(_) and therefore require
definition of the subtyping relation. Unfortunately this is not assigning type (m(_) : T x ) to x. However, the self bind
the case in DOT. layer can only be removed if an object is accessed through a
variable, otherwise we would not be able to substitute away
4.3 Good Bounds, Bad Bounds the self identifier. Second, we cannot derive Γ ⊢ tu : x.L
The transitivity axiom (or subsumption step in type assign- with x removed from the environment, but we also cannot
ment) is essential and cannot be dropped. Let us go through replace x in x.L with a term u that is not an identifier. Hence,
and see why we cannot prove transitivity directly. u cannot be an arbitrary term, because path-dependent types
First of all, observe that transitivity can only hold if all are not syntactically valid for arbitrary terms.
types in the environment have “good bounds”, i.e. only Intuitively, there is still hope for substitution, but only
members where the lower bound is a subtype of the upper with forms that preserve syntactic validity of path-dependent
bound. Through “bad” bounds in the context and subtyping types. Another option is to settle for a relaxed notion of path-
transitivity, the subtyping lattice can collapse. For example, dependent types that allows type selections on values [2].
assume a binding with “bad” bounds like Int..String. Then
4.5 There is Still Hope: Key Observations
the following subtype relation holds via transitivity
Based on the discussion so far, we can make the following
x : {A = Int..String} ⊢ Int <: x.A <: String
observations, which reveal a possible avenue for proving
but Int is not a subtype of String. Of course core DOT does type soundness despite the difficulties:
not have Int and String types, but any other incompatible
types can be taken as well. Observation 1. If objects can only be created with type
But even if we take good bounds as a precondition, we aliases (L = T ), not arbitrary bounds T1 ..T2 , then runtime
cannot show objects cannot have bad bounds.
{z ⇒ T1 } <: {z ⇒ T2 } <: {z ⇒ T3 } Observation 2. If we assume a call-by-value evaluation
because we would need to use x : T1 in the extended strategy, then whenever we execute a method call at runtime,
environment for the inductive call, but we do not know that all variables are bound to existing objects.
T1 has indeed good bounds. Observation 3. The only place in a soundness proof where
Of course we could modify the {z ⇒ T1 } <: {z ⇒ T2 } we rely on the (I NV F UN ) property is for the evaluation of
rule (B IND X) to require T1 to have good bounds. But then such method calls.
this evidence would need to be narrowed, which unfortu-
nately is not possible. Again, here is an example, considering Taken together, these observations suggest that making a
a type under a context: clear distinction between runtime values and other terms is a
prerequisite for a successful soundness proof. Observation 3
x : {A : ⊥..⊤} ⊢ x.A ∧ {B = Int} further suggests that subtyping transitivity and narrowing
This type has good bounds, but when narrowing x in the can be treated as axioms in subtyping comparisons and when
context to the smaller type {A = {B = String}} (which assigning types to static terms, as long as we can recover the
also has good bounds), its bounds become contradictory. (I NV F UN ) property in contexts that consist exclusively of
In summary, even if we assume good bounds in the envi- runtime objects.
ronment, and strengthen our typing rules so that only types
with good bounds are added to the environment, we may 5. Operational Semantics
still end up with bad bounds due to narrowing and intersec- Type soundness is only meaningful with respect to a notion
tion types. This refutes one conjecture about possible proof of evaluation: an operational semantics. In order to realize
avenues from earlier work on DOT [5]. the soundness proof strategy outlined in Section 4.5, we need
Intuitively, all the questions related to bad bounds have to pick a semantics that allows us to distinguish runtime val-
a simple answer: We ensure good bounds at object creation ues from normal terms. While such a distinction is partic-
time, so why do we need to worry in such a fine-grained ularly natural in big-step evaluators, the particular style of
way? semantics does not matter so much, and different styles of
4.4 No (Simple) Substitution Lemma semantics can be formally inter-derived using the techniques
of Danvy et al. [12, 13, 1]. In our development, we have de-
As a final negative result, we illustrate how typing is not fined both big-step evaluators and small-step reduction se-
preserved by straightforward substitution in DOT, because mantics, and used them as the basis for mechanized proofs
of path-dependent types. [36]. Here, we focus our presentation on a small-step reduc-
Γ, x : {z ⇒ L : S z ..U z ∧ m(_) : T z } ⊢ tx : x.L tion semantics, shown in Figure 2.

631
Syntax...
x ::= Variable v ::= y Value (Store Location)
y Concrete Variable (i.e. Store Location)
z Abstract Variable ρ ::= ∅ | ρ, y : d Store

Reduction ρ1 t1 → t2 ρ2
ρ {z ⇒ dz } → v ρ, (v : dv ) with v fresh
v2
ρ v1 .m(v2 ) → t ρ if ρ(v1 ) ∋ m(x) = tx
ρ1 e[t1 ] → e[t2 ] ρ2 if ρ1 t1 → t2 ρ2
where e ::= [ ] | [ ].m(t) | v.m([ ])

Subtyping... ρ Γ ⊢ S <: U Type assignment... ρ Γ ⊢ t :(!) T

ρ(y) ∋ (L = U ) ρ ∅ ⊢ T <: U
ρ Γ ⊢ T <: y.L
(SS EL 2) (y, dy ) ∈ ρ
(labels disjoint) ∀i, 1 ≤ i ≤ n
ρ(y) ∋ (L = U ) ρ ∅ ⊢ U <: T ρ ∅, (x : T1x ∧ . . . ∧ Tnx ) ⊢ dxi : Tix
(SS EL 1) (TL OC )
ρ Γ ⊢ y.L <: T ρ Γ ⊢ y : T1y ∧ . . . ∧ Tny

Figure 2. Small-Step Operational Semantics and Store Typing

We allocate all objects in a store-like structure, which type instead), and it does not consider the abstract context
grows monotonically. In this setting, store locations are the while checking the definitions (because all free variables in
only values, i.e. passed around between functions and stored the store must be concrete).
in environments. Figure 2 also shows necessary extensions
to subtyping and type assignment, which we explain next. 6. Type Soundness
A store-less alternative is also possible as detailed in We discuss in detail our proofs for type soundness (Theo-
Amin’s thesis [2]. The key ideas are to remove the store rem 1), highlighting challenges and insights. Our statement
indirection by treating values as concrete, and variables as of type safety is the following, folding together the usual no-
abstract, and to relax the syntax of path-dependent types to tions of progress and preservation [41]:
also allow values as paths, in addition to variables.
Definition 1 (Type Safety). If a term t typechecks to some
5.1 Concrete Variables in Typing and Subtyping type T in a store and empty context ρ ∅ (i.e. ρ ∅ ⊢ t : T ),
then either the term t is a variable or the store-term con-
To assign types to terms that occur during evaluation, we figuration ρ, t steps to a configuration ρ′ , t′ where the new
need to be able to handle path-dependent types that refer store ρ′ extends the old store ρ and the resulting configura-
to variables bound in the store ρ, and type store locations. tion typechecks to the same type T (i.e. ρ′ ∅ ⊢ t′ : T ).
Accordingly, we extend the type system judgements with
an additional store parameter ρ. The rules from Figure 1 Note that Definition 1 assumes deterministic execution.
are still valid, and merely thread the extra store parameter Otherwise the statement would need to be modified to con-
ρ unchanged. The additional cases are shown in Figure 2. sider all possible following configurations.
For concrete variables (i.e. store locations) in type selec- We outline the main strategic choices next, with pointers
tions, we use the precise type member given at object cre- to further subsections that describe the technical details. We
ation time by looking it up in the store, as defined by the reflect again on the higher-level strategy in Section 6.5.
new rules (SS EL 1) and (SS EL 2).
Lenient Well-Formedness Any syntactically valid form
In this extended subtyping relation, we continue to use
(type or term) is considered well-formed, if all its free vari-
the same rules for type selections on variables bound in
ables are bound in environments. Our strategy is to impose
Γ, (S EL 1) and (S EL 2) from Figure 1. Hence, the auxiliary
no semantics (e.g. good bounds for type members) on well-
judgement ρ Γ ⊢ z :! T , which excludes (VAR PACK ), is
formedness, and ensure desired properties by construction
only used for typing abstract variables.
only when they’re needed (e.g. for runtime objects).
Finally, we also need a new case for concrete variables in
typing, (TL OC ). It resembles (TN EW ), except that it looks Lemma 1 (Regularity). If a judgement holds, all its forms
up the definitions in the store, it does not create a recursive are well-formed.
type (because we can reuse the store location in the result

632
Lemma 2 (Subtyping Reflexivity). Any well-formed type is Such a strategy is reminiscent of cut elimination in natu-
a subtype of itself. ral deduction, and in fact, the possibility of cut elimination
strategies is already mentioned in Cardelli’s original work
This leniency pays off. As we saw in Section 4.3, trying to
on F<: [9].
enforce semantic properties can break narrowing and other
The narrowing lemma does not have any dependencies:
monotonicity properties. For example, the subtyping lattice
is full just by definition, since the greatest lower bound and Lemma 3 (Narrowing).
least upper bound of two types always exist, just by syntactic ρ Γ1 ⊢ T1 <: T2 ρ Γ2 ⊢ T3 <: T4
constructs (intersection and union). Γ1 = Γ2 (z → T1 ) Γ2 (z) = T2
“Pushback” For type soundness, we need to establish ρ Γ1 ⊢ T3 <: T4
Canonical Forms (Section 6.3) properties: that if a concrete
variable has a structural member type, then its definition in Proof. By structural induction, and using the (T RANS ) ax-
the store include a matching member definition. iom.
This is challenging, as the evidence from the typing Lemma 4 (Transitivity Pushback).
derivation might be indirect, because of subsumption and
subtyping transitivity. Hence, we need to “pushback” such ρ ∅ ⊢ T1 <: T2
indirections. ρ ∅ ⊢ T1 <! T2
We have two choices: pushback transitivity in subtyping
Proof. We prove an auxiliary lemma by induction on the
(described in Section 6.1), or pushback value typing into
subtyping derivation T1 <: T2 :
directly invertible evidence (an independent alternative de-
scribed in Section 6.6). ρ ∅ ⊢ T1 <: T2 , T2 <! T3
In both options, a key insight is that we only need to do ρ ∅ ⊢ T1 <! T3
the pushback in an empty abstract context, which circum-
vents the impossibility results of Section 4. This is where using narrowing (Lemma 3) in cases (F UN ), (B IND X),
it pays off to distinguish between runtime values and only (B IND 1). Transitivity pushback follows from the special
static types. Plus, for runtime values, we can rely on any case T2 = T3 .
properties enforced during their construction, in particular Lemma 5 (Inversion of Subtyping). For example for func-
“good bounds”. tion types:
Substitution By design, substitution is only needed to re- ρ ∅ ⊢ m(x : S1 ) → U1x <: m(x : S2 ) → U2x
place an abstract variable with a concrete one. Because the
ρ ∅ ⊢ S2 <: S1 ρ x : S2 ⊢ U1x <: U2x
abstract variable might have a less precise type, there’s also
a narrowing step involved. Furthermore, type selections on Proof. By transitivity pushback (Lemma 4) and inversion of
concrete variables are defined more precisely than for ab- the resulting derivation.
stract ones, which requires converting the evidence from
subtyping with abstract type selections to concrete. We de- Inversion of subtyping is only required in a concrete run-
scribe further in Section 6.2 time context, without abstract component (Γ = ∅). There-
fore, transitivity pushback is only required then. Transitivity
6.1 Narrowing and Transitivity Pushback pushback requires narrowing, but only for abstract bindings
In simpler type systems like F<: , transitivity can be proved (those in Γ, never in ρ). Narrowing requires these bindings
as a lemma, together with narrowing, in a mutual induction to be potentially imprecise, so that the transitivity axiom can
on the size of the middle type in a chain T1 <: T2 <: T3 be used to inject a step to a smaller type without recursing
(see e.g. the POPLmark challenge documentation [7]). into the derivation. In summary, we need both (actual, non-
Unfortunately, for subtyping in DOT, the same proof axiom) transitivity and narrowing, but not at the same time.
strategy fails, because subtyping may involve a type selec- The insight that transitivity pushback is only required in a
tion as the middle type: T1 <: z.L <: T3 . Since proving concrete-only runtime context is crucial for supporting lan-
transitivity becomes much harder, we adopt a strategy from guage features such as intersection types that may collapse
previous DOT developments [5]: admit transitivity as an ax- the subtyping lattice in unrealizable contexts.
iom (T RANS ), but prove a ‘pushback’ lemma that allows to 6.2 Bootstrapping Substitution and Canonical Forms
push uses of the axiom further up into a subtyping deriva-
To mirror the effect of reduction ρ x.m(y) → ty ρ given
tion, so that the top level becomes invertible. We denote this
ρ(x) ∋ m(z) = tz , we need a substitution lemma for terms,
as precise subtyping T1 <! T2 .
but we also need to mirror the reduction on the type level,
Definition 2 (Precise Subtyping). If ρ Γ ⊢ T1 <: T2 and since types can refer to variables via type selections. More
the derivation does not end in rule (T RANS ) then we say that precisely, we need a substitution lemma that enables us to
ρ Γ ⊢ T1 <! T2 . replace all type selections on an abstract variable z.A with

633
concrete ones y.A. For this, we need to ensure that for a con- Proof. The key challenge is translating from the rules (S EL 1)
crete variable with a structural type-member type, its def- / (S EL 2) to the rules (SS EL 1) / (SS EL 2). For (S EL 2), if we
initions in the store include a corresponding type member are selecting z.A, we have ρ z : S z ⊢ z :! (L : T z ..⊤), and
– a Canonical Forms property for type members (see Sec- with Lemma 10 we obtain ρ ∅ ⊢≤m y : (L : T y ..⊤). We in-
tion 6.3). voke canonical forms (Lemma 7), which yields ρ(y) ∋ (L =
We cannot prove either of these properties directly and U ) and ρ ∅ ⊢ T y <: U . Note that we can apply Lemma 7
therefore need to bootstrap a mutual induction. The key because of our outer induction on m. If we are selecting z ′ .A
induction measure will be an upper bound on the uses of with z ′ 6= z, we apply Lemma 9. Case (S EL 1) is analogous.
(VAR PACK ) in a typing derivation. Note that the (S EL 1)/(S EL 2) rules are carefully set up so
that Γ[z] = z : S.
Definition 3 (VAR PACK Metric). Let ρ Γ ⊢≤m y : S
denote a derivation ρ Γ ⊢ y : S with no more than m uses Lemma 9 (Substitution for :! ).
of (VAR PACK ).
ρ ∅ ⊢≤m y : S y z ′ 6= z ρ z : S z , Γz ⊢ z ′ : ! T z
Definition 4 (Substitution). Let Subst(m) denote:
ρ Γy ⊢ z ′ :! T y
ρ ∅ ⊢≤m1 y : S y m1 < m
ρ z : S z , Γz ⊢ T1 z <: T2 z Proof. Straightforward. Case (S UB ) uses Lemma 8.
ρ Γy ⊢ T1 y <: T2 y
Lemma 10 (Substitution for :).
We go on to prove preliminary canonical forms lemmas,
ρ ∅ ⊢≤m y : S y ρ z : S z , Γz ⊢ z :! T z
assuming the ability to perform substitution for a given m.
ρ ∅ ⊢≤m y : T y
Lemma 6 (Pre-canonical Forms for Recursive Types).
Proof. Case (VAR ) is immediate. In case (VARU NPACK ),
ρ ∅ ⊢≤m y : {z ⇒ T z } Subst(m)
we have ρ z : S z , Γz z :! {z2 ⇒ T z2 }z and by induction
y
ρ ∅ ⊢≤m−1 y : T we obtain ρ ∅ ⊢≤m y : {z2 ⇒ T z2 }y , as required. In case
(S UB ), we have ρ z : S z , Γz z :! T ′z and ρ z : S z , Γz z :!
Proof. Any trailing uses of (S UB ) can be accumulated into T ′z <: T z . Applying the induction hypothesis and Lemma 8
a single subtyping statement ρ ∅ ⊢ {z ⇒ T ′z } <: {z ⇒ and using (S UB ) we get ρ ∅ ⊢≤m y : T ′y .
T z }, and the remaining derivation must end in (VAR PACK ).
By inversion we obtain ρ ∅ ⊢≤m−1 y : T ′y . After tran- Finally, we can prove a substitution on terms.
sitivity pushback (Lemma 4), the subtyping derivation must
Lemma 11 (Substitution in Term Typing).
end in (B IND X), from which we obtain ρ z : T ′z ⊢ T ′z <:
T z . We can now apply our Subst(m) capability to obtain ρ (z : S), Γz ⊢ tz : T z ρ ⊢ y :! S
ρ ∅ ⊢ T ′y <: T y . Applying subsumption (S UB ) yields y
ρΓ ⊢ t :Ty y
ρ ∅ ⊢≤m−1 y : T y .
Proof. Straightforward induction. Case (S UB ) uses substitu-
Lemma 7 (Pre-canonical Forms for Type Members). tion of subtyping (Lemma 8).
ρ ∅ ⊢≤m y : {L : S..U } Subst(m) 6.3 Inversion of Value Typing (Canonical Forms)
ρ(y) ∋ (L = T ) ρ ∅ ⊢ S <: T <: U As a corollary of substitution (Lemma 8), we can extend the
preliminary canonical forms lemmas to all m.
Proof. Again, we accumulate trailing uses of (S UB ) into
an invertible subtyping. If we hit (VAR PACK ), the resulting Lemma 12 (Canonical Forms for Type Members).
subtyping derivation must collapse into (B IND 1). We fin-
ρ ∅ ⊢ y : {L : S..U }
ish the case by applying Lemma 6, Subst(m), and (S UB ).
Case (TL OC ) is immediate from inversion of member case ρ(y) ∋ (L = T ) ρ ∅ ⊢ S <: T <: U
(DT YP ). Proof. Follows directly from Lemma 7 and Lemma 8.
We are now ready to prove our substitution lemma, together We also prove an additional canonical forms lemma for
with two helpers. The proof is by simultaneous induction, function members, which will be required by the main proof.
first over m, and then an inner induction over the size of the
Lemma 13 (Canonical Forms for Method Members).
<: or :! derivation.
ρ ∅ ⊢ y : m(x : S2 ) → U2x
Lemma 8 (Substitution for <:). ∀m.Subst(m), i.e.:
ρ(y) ∋ m(x) = t
ρ ∅ ⊢≤m y : S y ρ z : S z , Γz ⊢ T1 z <: T2 z ρ ∅, x : S1 ⊢ t : U1x
ρ Γy ⊢ T1 y <: T2 y ρ ∅ ⊢ m(x : S1 ) → U1x <: m(x : S2 ) → U2x

634
Proof. Analogous to Lemma 7. Case (TL OC ) eliminates the imprecise derivation
self variable in the abstract context by applying substitution T1 <: U <: T2
of term typing (Lemma 11).
which may be bigger than the original derivation due to
6.4 The Main Soundness Proof transitivity pushback. So, we cannot process the result of the
inversion further during an induction. This increase in size
Our main type safety theorem combines the usual progress is a well-known property of cut elimination: removing uses
and preservation lemmas into a single unified statement. of a cut rule (like our transitivity axiom) from a proof term
Theorem 1 (Type Safety). If ρ ∅ ⊢ t : T , then either t = y may increase the proof size exponentially.
and ρ(y) = {d} or ρ t → t′ ρ′ and ρ′ ∅ ⊢ t′ : T This is why type selections use the abstract variable type
assignment, which disallow packing, relying on unpacking
Proof. By structural induction. The most interesting case is and subtyping instead.
the dependent application (TA PP VAR ), if the receiver of Furthermore, for sub-derivations on a self type, the ab-
the call is already evaluated to a store location y. We have stract context must be restricted to not include any binding
ρ ∅ ⊢ y.m(y1 ) : U2y1 and, by inversion, ρ ∅ ⊢ y : (m(x : added after the binding for the self type, so that the push-
S2 ) : T2x ) and ρ ∅ ⊢ y1 : S1 . By canonical forms for back lemma can be applied during substitution. In fact, this
method members (Lemma 13) we obtain ρ(y) ∋ m(x) = tx , last restriction in the model is not just a technical device, it
ρ x : S1 ⊢ tx : U1x , and ρ ⊢ m(x : S1 ) : U1x <: seems reasonable for soundness. Indeed, a self type might
m(x : S2 ) : U2x . We know that ρ y.m(y1 ) → ty1 ρ, so use a type that has bad bounds within a definition (for exam-
we need to show that the result is well-typed with the same ple, in a function parameter type, or a type member alias).
type: ρ ∅ ⊢ ty1 : U2y1 . We apply inversion of subtyping When subtyping two recursive types, such nonsensical types
(Lemma 5) and obtain ρ ∅ ⊢ S2 <: S1 and ρ x : S2 ⊢ might be added to the abstract context, but we do not want
U1x <: U2x . With (S UB ), we have ρ ∅ ⊢ y1 : S1 , and we to unpack a self type by using such temporary bad evidence.
can apply substitution of term typing (Lemma 11), to obtain 6.6 Alternative: Invertible Concrete Variable Typing
ρ ∅ ⊢ ty1 : U2y1 . With (S UB ) and applying substitution of
In the preceding sections, the presence of the subsumption
subtyping (Lemma 8) to derive ρ ∅ ⊢ U1y1 <: U2y1 , we
rule in type assignment required us to prove various canon-
arrive at the required ρ ∅ ⊢ ty1 : U2y1 .
ical forms lemmas. It is also possible to turn this around:
design a type assignment relation for concrete variables that
6.5 Some Reflection
is directly invertible, and prove the subsumption property
The soundness proof was set up carefully to avoid cycles (upwards-closure with respect to subtyping) as a lemma.
between required lemmas. Where cycles did occur, as with Here we sketch this alternative, focusing on the set up
transitivity and narrowing, we broke them using a pushback of the auxiliary relation and lemmas rather than the proof
technique. Where this was cumbersome to do, as with sub- details.
stitution and canonical forms, we used mutual induction. A
Invertible Concrete Variable Type Assignment We define
key property of the system is that, in general, we are very le-
the concrete variable type assignment, ρ ⊢ y :! T , to be
nient about things outside of the concrete runtime store. The
directly invertible by excluding subsumption, and instead
only place where we invert a dependent function type and go
relating a value in the store to each of its possible type. There
from abstract to concrete is in showing safety of the corre-
is one case per syntactic form, except no case for ⊥ and two
sponding type assignment rules. This enables subtyping in-
cases for union types.
version and pushback to disregard abstract bindings for the
most part. Definition 5 (Concrete Variable Type Assignment). ρ ⊢
When seeking to unpack recursive self types within y :! T is defined inductively by the following rules.
lookups of type selections in subtype comparisons, the y∈ρ
option of disregarding abstract bindings is no longer so (V-T OP )
ρ ⊢ y :! ⊤
easy. Every lookup of a variable, while considering a path-
dependent type, may potentially need to unfold and invert ρ(y) ∋ (L = T ) ρ ∅ ⊢ S <: T , T <: U
(V-T YP )
self types. In particular, the substitution lemma itself that ρ ⊢ y :! (L : S..U )
converts imprecise into precise bounds may unfold a self
(y, dy ) ∈ ρ
type. Then it will be faced with an abstract variable that first
(labels disjoint) ∀i, 1 ≤ i ≤ n
needs to be converted to a concrete variable. More generally,
ρ . . . ∧ Tnx ) ⊢ dxi : Tix
∅, (x : T1x ∧
whenever we have a chain
∃j, dxj = (m(z : S) = tz ) Tjx = m(z : S x ) : U x,z
{z ⇒ T1 } <: T <: {z ⇒ T2 }, ρ ∅ ⊢ S ′ <: S y ρ ∅, (z : S ′ ) ⊢ U y,z <: U ′
z

we first need to apply transitivity pushback to perform in- ρ ⊢ y :! (m(x : S ′ ) : U ′x )

version. But then, the result of inversion will yield another (V-F UN )

635
 ρ(x) ∋ (L = T ) ρ ⊢ y :! T Lemma 17 (Concrete Variable Widening). ∀m.Widen(m),
(V-S EL ) i.e.:
ρ ⊢ y :! (x.L)
ρ ⊢m y : ! T ρ ∅ ⊢ T <: U
ρ ⊢ y :! T y
(V-B IND ) ρ ⊢≤m y :! ⊢ U
ρ ⊢ y :! {z ⇒ T z }
Finally, we can relate the normal typing relation and our
ρ ⊢ y : ! T1 , y : ! T2 concrete variable typing.
(V-A ND )
ρ ⊢ y : ! T 1 ∧ T2 Lemma 18 (Concrete Variable Typing Inversion). Term typ-
ρ ⊢ y : ! T1 ing of a concrete variable in an empty abstract context im-
(V-O R 1) plies the same concrete variable type assignment.
ρ ⊢ y : ! T 1 ∨ T2
ρ∅ ⊢ y:T
ρ ⊢ y : ! T2
(V-O R 2) ρ ⊢ y :! T
ρ ⊢ y : ! T 1 ∨ T2
Bootstrapping Substitution and Widening We proceed in 7. Perspectives
a way similar to Section 6.2 to bootstrap a mutual induction, 7.1 DOT is Sound, but is Scala Sound?
but this time with swapped assumptions: canonical forms
It is not always clear how well results from a small formal
properties are now immediate, but we need to assume a
model translate to a realistic language. In the case of DOT,
widening (i.e. subsumption) capability.
the interleaved process of designing and proving sound a
Definition 6 (V-B IND Metric). Let ρ ⊢≤m y :! S denote prescriptive core model of Scala’s type system has provided
a derivation ρ ⊢ y :! S with no more than m uses of (V- valuable insights into the design space. Through debugging
B IND ). DOT models, we have uncovered several soundness issues
Definition 7 (Widening). Let Widen(m) denote: in Scala. We have already discussed problems related to null
values in Section 2. While it can be argued that null is a fun-
ρ ⊢m y : ! T ρ ∅ ⊢ T <: U damentally unsound feature anyways, and therefore sound-
ρ ⊢≤m y :! U ness issues involving null may be acceptable, we give two
We prove three substitution lemmas, analogous to Lem- further examples here, which use only safe language features
mas 8,9, and 10, but predicated on Widen(m), and with re- and thus constitute uncontroversial soundness violations.
spect to concrete variable typing (ρ ⊢ y :! T ) instead of In DOT, type members in new instances are restricted
term typing (ρ ∅ ⊢ y : T ). to aliases, so that “good bounds” are enforced syntactically
rather than semantically. This restriction was added after it
Lemma 14 (Substitution for Subtyping). became clear that subtle situations could arise during object
ρ ⊢≤m y :! S y Widen(m) initialization with recursive types, where runtime contexts
ρ z : S z , Γz ⊢ T1 z <: T2 z would be polluted by “bad” evidence that is temporary or
ρ Γy ⊢ T1 y <: T2 y justified only through circular reasoning. For a similar rea-
son, there is no subsumption in member initialization, so
Lemma 15 (Substitution for Abstract Variable Typing). type-checking at object creation (TN EW ) can tie the recur-
ρ ⊢≤m y :! S y Widen(m) sive knot, without needing to check bounds.
′
z 6= z ρ z : S z , Γz ⊢ z ′ : ! T z Scala was designed and implemented before all these cor-
ρ Γy ⊢ z ′ :! T y ner cases became apparent and allows more flexible bounds.
Bounds are checked to be “good”, but these checks are not
Lemma 16 (Substitution for Concrete Variable Typing).
sufficient. Here is an example where a concrete object with
Widen(m) ρ ⊢≤m y :! S y ρ z : S z , Γz ⊢ z :! T z “bad bounds” slips through in Scala 2.11.8, causing a cast
ρ ⊢≤m y :! T y exception at runtime.
trait O { type A >: Any <: B; type B >: A <: Nothing }
Note that the abstract context in the premise of Lemma 16 val o = new O {}
disappears entirely from the conclusion, which is about con- def id(a: Any): Nothing = (a: o.B)
crete type assignment. This gives another intuition why the val n: Int = id("Boom!") // runtime cast exception
model restricts the abstract context when typing recursive As another example, Scala allows lazy vals in paths of
types for type selections. Indeed, the extra abstract bindings type selections, while trying to enforce realizability to pre-
that come from subtyping recursive types within recursive vent unsoundness due to “bad bounds” on non-terminating
types might cause more derivations to hold, via lattice col- lazy paths that are never forced but appear in types. But from
lapsing, in the abstract than in the concrete. DOT, we know that realizability is not preserved by narrow-
We can now prove that a general widening or subsump- ing, and with a bit of work, we can exploit this insight and
tion rule is admissible. demonstrate the pitfalls of this approach.

636
trait A { type L <: Nothing } and reduction in type selections, field initialization, circular
trait B { type L >: Any} reasoning with self occurrences. (2) Singleton Types: x.type
trait U { in addition to x.A, denoting the type that is only inhabited by
type X <: B
the value of x. An interesting question is whether singleton
val p: X
types are already encodable in DOT.
def id(x: Any): p.L = x // used in plausible context
} Restricted Extensions (1) Laziness: DOT relies on the
trait V extends U { assumption of call-by-value evaluation. To model Scala’s
type X = B with A // unrealizable
lazy vals, some restrictions are necessary. As a first ap-
lazy val p: X = p // non-terminating
proximation one can forbid type selections on lazy vals, but
}
val v = new V {}
relaxations in combination with traits and class types may be
val n: Int = v.id("Boom!") // runtime cast exception possible, though challenging in terms of balancing flexibility
To conclude this section, we believe that formal work and safety. Another avenue is deliberately forcing evaluation
on core language models is important and, even though we of lazy vals that occur in types. (2) By-Name Arguments:
do not and cannot consider a full language, this work still must not occur in type selections.
helps making full languages safer. In addition, formal work Debatable Extensions Type Projections, Type Lambdas
can also chart new territory and lead to more general and and Higher-Kinded Types: These features are most likely not
more regular full languages, by (cautiously) suggesting that faithfully encodable in DOT. Type projections T#A are similar
a feature may be safer than previously thought and relaxing to type selections x.A, but crucially lose the guarantee of
some constraints. For example, structural recursive types are variable x pointing to an existing object. Thus, it is presently
more expressive in our DOT model than in Scala. unclear how to approach soundness of type projections. For
7.2 Scaling up: The Road Ahead type lambdas, what is missing is a way to calculate the type
resulting from a type application. This could be encoded
While we have seen in Section 2 that DOT can encode a through type projections or through dependent types beyond
large class of realistic Scala programming patterns, a num- just paths. Simplified models are readily doable (as outlined
ber of non-quintessential but practically relevant features in the introduction of Section 2), so it is not clear whether
have been (sometimes deliberately) left out of DOT’s for- the unrestricted encoding is worth the extra complexity.
mal model. Below is an attempt to classify these features ac-
cording to their ease of integration with DOT and potential Incompatible Extensions As discussed in Section 2 and
implications for type soundness. elsewhere [6], Scala’s oblivious treatment of null pointers,
which mainly exists for backwards compatibility with Java,
Largely Orthogonal Features (1) Traits, Classes, Inheri- seems to be fundamentally unsound. Future version of Scala
tance and Mixins: DOT does not model any “implementation can achieve soundness by (1) reflecting nullability in the
reuse” mechanisms such as inheritance and mixins (which type system, e.g. via union types, (2) preventing nullable
Scala has) and prototype dispatch (which does not currently expressions in type selections, similar to mutable variables
exist in Scala, but would be interesting to consider). Most or by-name arguments, and (3) tightening the rules for object
likely, such extensions will be through encodings, showing member initialization so that null values cannot be observed
type preservation of a translation, and not through extending during object creation.
the DOT meta-theory itself. Some challenges: type member
inheritance vs “good bounds” at creation time, open con- 8. Related Work
struction of nominal hierarchies. (2) Mutable State: this will
Scala Foundations Much work has been done on ground-
require standard extensions to the operational semantics, and
ing Scala’s type system in theory. Early efforts included
it is important that type selections remain stable, i.e. exclude
νObj [30], Featherweight Scala [11] and Scalina [26], all of
mutable variables. As is standard, the interaction of mutation
them more complex than what is studied here. None of them
and polymorphism requires care [39], but previous work [36]
lead to a mechanized soundness result, and due to their in-
has shown that mutation can be added to DOT-like type sys-
herent complexity, not much insight was gained why sound-
tems without interfering with soundness. (3) Implicits: Scala
ness was so hard to prove. DOT [4] was proposed as a sim-
has both implicit parameters and implicit conversions, which
pler and more foundational core calculus, focusing on path-
are automatically inserted by the compiler based on types
dependent types but disregarding classes, mixin linearization
and scopes. Implicit parameters are useful for modeling type
and similar questions. The original DOT formulation [4] had
classes. Implicits do not introduce new types as typing rules
actual preservation issues because lookup was required to be
and are unlikely to interfere with soundness.
precise. This prevented narrowing, as explained in Section 4.
Fitting Extensions (1) Full Paths: extend type selections The originally proposed small step rewriting semantics with
to include chains of immutable field selections x.a.b.C in a store exposed the difficulty of relating paths at different
addition to variables x.A. Some challenges: path equality stages of reductions.

637
 The µDOT calculus [5] is the first calculus in the line on transparent bindings by Harper and Lillibridge [21] and
with a mechanized soundness result, (in Twelf, based on Leroy [24]. MixML [14] drops the stratification requirement
total big-step semantics), but the calculus is much simpler and enables modules as first-class values.
than what is studied in this paper. Most importantly, µDOT
Other Related Languages Other languages and calculi
lacks bottom, intersections and type refinement. Amin et
that include features related to DOT’s path dependent types
al. [5] describe in great detail why adding these features
include the family polymorphism of Ernst [15], Virtual
causes trouble. Because of its simplicity, µDOT supports
Classes [17, 16, 27, 19], and ownership type systems like
both narrowing and transitivity with precise lookup. The
Tribe [10, 8]. Nominality by ascription is also achieved in
soundness proof for µDOT was also with respect to big-
Grace [23].
step semantics. However, the semantics had no concept of
distinct runtime type assignment and would thus not be able 9. Conclusions
to encode F<: and much less full DOT.
After the first version of this paper was circulated as a The key aim behind DOT is to build a solid foundation for
tech report [36], a soundness proof sketch for another DOT Scala and similar languages from first principles. DOT has
variant was proposed by Odersky [3]. While on the surface also been described as the essence of Scala: what remains
similar to the DOT version in this paper and in [36], there after you “boil Scala on a slow flame and wait until all
are some important differences that render the calculus in incidental features evaporate” [29].
[3] much less expressive. First, the calculus is restricted to We have presented the first soundness result for a variant
Administrative Normal Form (ANF) [18], requiring all inter- of DOT that includes recursive type refinement and a sub-
mediate subexpressions to be let-bound with explicit names. typing lattice with full intersection types, demonstrating how
While seemingly a minor issue, reported difficulties in prov- the difficulties that prevented such a result previously can be
ing encodings of simpler calculi such as F<: that are not in overcome with a semantic model that exposes a distinction
ANF may suggest that this restriction is not entirely trivial. between static terms and runtime values.
Second, and more importantly, the calculus does not sup- We also think that it is important to convey not just that a
port subtyping between recursive types (rules (B IND X) and calculus is sound in isolation, but also what assumptions the
(B IND 1)), only their introduction and elimination as part of soundness proof relies on in order to evaluate the broader
type assignment. This skirts most of the thorny issues in the applicability of the work. In particular, our proof relies cru-
proofs (see Section 6.2) and also limits the expressiveness of cially on runtime values having only type members with
the calculus. For example, an identifier x bound to a refined good bounds, which the syntax enforces. Because of recur-
type {z ⇒ T ∧ U z } can be treated as having type T , but if sive types, such a property would be difficult to enforce se-
it instead has type S → {z ⇒ T ∧ U z }, it can not be as- mantically. It also relies on call-by-value semantics, in that
signed type S → T . Instead, one has to eta-expand the term it expects all variables that can partake in types to point to
into a function (i.e. an object with a single method), let-bind runtime values when a method body is evaluated.
the result of the call, and insert the required coercion to T . Finally, in our own experience with DOT, the process
Similar considerations apply to types in other non-toplevel of designing the calculus and proving it sound have been
positions such as bounds of type members, but there it is intertwined. As we understood the landscape better, we have
not even clear if an analogue of eta-expansion is available. been able to make the model more uniform yet powerful.
With this requirement for explicit conversions, the calculus Acknowledgements
in [3] does not, at least in our view, capture the essence of
a type system based on subtyping. The results reported in The initial design of DOT is due to Martin Odersky. Ge-
the present paper predate those from [3], and they have no offrey Washburn, Adriaan Moors, Donna Malayeri, Samuel
such restrictions: we provide a soundness proof, mechanized Grütter and Sandro Stucki have contributed to its develop-
in Coq, for a calculus that is not restricted to ANF, and that ment. For insightful discussions we thank Amal Ahmed,
supports subtyping between recursive types. Jonathan Aldrich, Derek Dreyer, Sebastian Erdweg, Erik
Ernst, Matthias Felleisen, Ronald Garcia, Paolo Giarrusso,
ML Module Systems 1ML [37] unifies the ML module Scott Kilpatrick, Grzegorz Kossakowski, Alexander Kuklev,
and core languages through an elaboration to System Fω Viktor Kuncak, Ondřej Lhoták, Alex Potanin, Jon Pretty, Di-
based on earlier such work [38]. Compared to DOT, the dier Rémy, Lukas Rytz, Miles Sabin, Ilya Sergey, Jeremy
formalism treats recursive modules in a less general way Siek, Josh Suereth, Ross Tate, Eelco Visser, Philip Wadler
and it only models fully abstract vs fully concrete types, and Jason Zaugg. Finally, we thank the anonymous review-
not bounded abstract types. Although an implementation is ers for their thoughtful comments.
provided, there is no mechanized proof. In good ML tradi- This research received funding from the European Re-
tion, 1ML supports Hindler-Milner style type inference, with search Council (ERC) under grant 587327 DOPPLER, from
only small restrictions. Path-dependent types in ML mod- NSF under CAREER award 1553471, and from Purdue Uni-
ules go back at least to SML [25], with foundational work versity through a faculty startup package.

638
References minimal core calculus for java and gj. ACM Trans. Program.
Lang. Syst., 23(3), 2001.
[1] M. S. Ager, D. Biernacki, O. Danvy, and J. Midtgaard. A [23] T. Jones, M. Homer, and J. Noble. Brand objects for nominal
functional correspondence between evaluators and abstract typing. In ECOOP, 2015.
machines. In PPDP, 2003.
[24] X. Leroy. Manifest types, modules and separate compilation.
[2] N. Amin. Dependent Object Types. PhD thesis, EPFL, 2016. In POPL, 1994.
[3] N. Amin, S. Grütter, M. Odersky, T. Rompf, and S. Stucki. [25] D. Macqueen. Using dependent types to express modular
The essence of dependent object types. In WadlerFest, A List structure. In POPL, 1986.
of Successes That Can Change the World: Essays Dedicated
to Philip Wadler on the Occasion of His 60th Birthday, 2016. [26] A. Moors, F. Piessens, and M. Odersky. Safe type-level
abstraction in Scala. In FOOL, 2008.
[4] N. Amin, A. Moors, and M. Odersky. Dependent object types.
In FOOL, 2012. [27] N. Nystrom, S. Chong, and A. C. Myers. Scalable extensibil-
ity via nested inheritance. In OOPSLA, 2004.
[5] N. Amin, T. Rompf, and M. Odersky. Foundations of path-
dependent types. In OOPSLA, 2014. [28] M. Odersky. The trouble with types. Presentation at Strange
Loop, 2013.
[6] N. Amin and R. Tate. Java and Scala’s type systems are
unsound: the existential crisis of null pointers. In OOPSLA, [29] M. Odersky. The essence of Scala. http://www.scala-lang.
org/blog/2016/02/03/essence-of-scala.html, February
2016.
2016.
[7] B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C.
Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and [30] M. Odersky, V. Cremet, C. Röckl, and M. Zenger. A nominal
S. Zdancewic. Mechanized metatheory for the masses: The theory of objects with dependent types. In ECOOP, 2003.
PoplMark Challenge. In TPHOLs, 2005. [31] M. Odersky and K. Läufer. Putting type annotations to work.
[8] N. R. Cameron, J. Noble, and T. Wrigstad. Tribal ownership. In POPL, 1996.
In OOPSLA, 2010. [32] M. Odersky and T. Rompf. Unifying functional and object-
[9] L. Cardelli, S. Martini, J. C. Mitchell, and A. Scedrov. An ex- oriented programming with Scala. Commun. ACM, 57(4):76–
tension of system F with subtyping. Inf. Comput., 109(1/2):4– 86, 2014.
56, 1994. [33] B. C. Pierce. Types and programming languages. MIT Press,
[10] D. Clarke, S. Drossopoulou, J. Noble, and T. Wrigstad. Tribe: 2002.
a simple virtual class calculus. In AOSD, 2007. [34] B. C. Pierce and D. N. Turner. Local type inference. ACM
[11] V. Cremet, F. Garillot, S. Lenglet, and M. Odersky. A core Trans. Program. Lang. Syst., 22(1):1–44, 2000.
calculus for Scala type checking. In MFCS, 2006. [35] J. C. Reynolds. Towards a theory of type structure. In
[12] O. Danvy and J. Johannsen. Inter-deriving semantic arti- Symposium on Programming, volume 19 of Lecture Notes in
facts for object-oriented programming. J. Comput. Syst. Sci., Computer Science, pages 408–423. Springer, 1974.
76(5):302–323, 2010. [36] T. Rompf and N. Amin. From F to DOT: Type soundness
[13] O. Danvy, K. Millikin, J. Munk, and I. Zerny. On inter- proofs with definitional interpreters. Technical report, Purdue
deriving small-step and big-step semantics: A case study University, July 2015.
http://arxiv.org/abs/1510.05216.
for storeless call-by-need evaluation. Theor. Comput. Sci.,
435:21–42, 2012. [37] A. Rossberg. 1ML - core and modules united (f-ing first-class
[14] D. Dreyer and A. Rossberg. Mixin’ up the ML module modules). In ICFP, 2015.
system. In ICFP, 2008. [38] A. Rossberg, C. V. Russo, and D. Dreyer. F-ing modules. J.
[15] E. Ernst. Family polymorphism. In ECOOP, 2001. Funct. Program., 24(5):529–607, 2014.

[16] E. Ernst. Higher-order hierarchies. In ECOOP, 2003. [39] A. J. Summers. Modelling java requires state. In Proceedings
of the 11th International Workshop on Formal Techniques for
[17] E. Ernst, K. Ostermann, and W. R. Cook. A virtual class Java-like Programs, page 10. ACM, 2009.
calculus. In POPL, 2006.
[40] G. A. Washburn. SI-1557: Another type soundness hole.
[18] C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The https://issues.scala-lang.org/browse/SI-1557, 2008.
essence of compiling with continuations. In PLDI, 1993.
[41] A. K. Wright and M. Felleisen. A syntactic approach to type
[19] V. Gasiunas, M. Mezini, and K. Ostermann. Dependent soundness. Inf. Comput., 115(1):38–94, 1994.
classes. In OOPSLA, 2007.
[20] J.-Y. Girard. Interprétation fonctionelle et élimination des
coupures de l’arithmétique d’ordre supérieur. 1972.
[21] R. Harper and M. Lillibridge. A type-theoretic approach to
higher-order modules with sharing. In POPL, 1994.
[22] A. Igarashi, B. C. Pierce, and P. Wadler. Featherweight java: a

639
A. Mechanization in Coq
We outline the correspondence between the formalism on paper and its implementation in Coq (oopsla16.namin.net).

A.1 Model (dot.v)

A.1.1 Syntax (Figure 1)
ty S, T, U ::= Type
TTop ⊤ top type
TBot ⊥ bottom type
TTyp L S U L : S..U type member
TFun m S U m(x : S) : U x method member
TSel X L x.L type selection
TBind T {z ⇒ T z } recursive self type
TAnd T T T ∧T intersection type
TOr T T T ∨T union type
tm t, u ::= Term
tvar bx x variable reference
tobj d {z ⇒ d} new instance
tapp t m t t.m(t) method invocation
dm d ::= Initialization
dty T L=T type initialization
dfun [S] [T] t m(x) = t method initialization
dms d
To demonstrate that both Church and Curry syle are possible, the parameter and return types S and T of a method initialization
dfun [S] [T] t are optional.
For representing variable names in relation to an environment (context or store), we use a reverse de Bruijn convention, so
that the name is invariant under environment extension. An environment is a list of right-hand sides. The older the binding, the
more to the right, the smaller its number name. The name is uniquely determined by the position in the list as the length of
the tail. For terms, a concrete variable y corresponds to tvar true y, and an abstract variable z corresponds to tvar false z.
Similarly, in types, a concrete variable y corresponds to TVar true y, and an abstract variable z corresponds to TVar false z.
Like in the paper, the y identifiers map to the store ρ and the z identifiers to the context Γ.
In addition, for types, we use a locally-nameless de Bruijn convention for variables under dependent types so that it’s easy
to substitute binders without variable capture. A variable x bound in T x by a recursive type {x ⇒ T x } or a method member
m(x : S) : T x is represented by TVarB i where i is the de Bruijn level, i.e. the number of other binders in scope in between a
bound variable occurrence and its binder.
The labels L and m are not part of the Coq syntax for member initialization (dty and dfun), so that label disjointness is by
design. Labels are auto-assigns from 0 at the right to n − 1 at the left, for a sequence of length n. (Viewed as a list of right-hand
sides, this is the same naming convention as for environments above.)

A.1.2 Small-Step Operational Semantics (Figure 2)

step ρ t ρ ′ t′ ρ t → t ′ ρ′ Reduction

The step relation makes explicit the two congruence cases (ST_App1, ST_App2) of the reduction semantics.

A.1.3 Type System (Figures 1 & 2)

stp Γ ρ S U n ρΓ ⊢ S <: U Subtyping
has_type Γ ρ t T n ρΓ ⊢ t:T Typing
dms_has_type Γ ρ d Tn ρΓ ⊢ d:T Member Initialization
htp ΓρxTn ρΓ ⊢ x :! T Abstract Variable Typing (for Subtyping)

The argument n at the end of each judgement denotes the size of derivation.

640
 The relation dms_has_type is used in the premise of both (TN EW ) mapping to T_Obj and (TL OC ) mapping to T_Vary.
It folds in member initialization, as it recursively maps over the sequence of member definitions. The resulting sequence of
intersected types is associated to the right. For uniformity, an empty sequence adds an inner most ⊤ type.
The context restriction in subtyping type selection in rules (S EL 1)/(S EL 2) mapping to stp_sel1/stp_sel2 is folded into
the relation htp.
As we mention in Section 3, we omit routine well-formedness checks from the rules on paper for readability. In Coq, these
correspond to closed conditions, which ensure that all the variables in a type are well-bound for the given environment and
binding structure. The relation closed |Γ| |ρ| k T ensures that T is well-bound in a context Γ, a store ρ and under at most ≤ k
binders.
A.1.4 Type-Checked Examples (dot_exs.v)
As a sanity check, we ensure that our model can indeed type-check some intended examples, including a module for covariant
lists as presented in Section 2.
A.2 Soundness Proofs (dot.v, dot_soundness.v, dot_soundness_alt.v)
The file dot_soundness.v presents the main development of the soundness proof, as presented in Section 6. The file
dot_soundness_alt.v presents the alternative development of the soundness proof, briefly sketched in Section 6.6. In addition
to the model, the file dot.v contains common infrastructure and lemmas.
A.2.1 Definitions
1. (Type Safety) – see also Theorem 1 – corresponds to Theorem type_safety.

2. (Precise Subtyping) corresponds to Inductive stpp.

3. (VAR PACK Metric) corresponds to Inductive htpy as ρ Γ ⊢≤m y : S maps to htpy m ρ y S with Γ = ∅.
4. (Substitution) corresponds to Definition Subst.

5. (Concrete Variable Type Assignment) corresponds to Inductive vtp.

6. (V-B IND Metric) is built-into Inductive vtp as ρ ⊢≤m y :! S maps to vtp m ρ y S n.

7. (Widening) corresponds to Lemma vtp_widen.

A.2.2 Lemmas
1. (Regularity) corresponds to Lemma stpd_reg1 and Lemma stpd_reg2.

2. (Subtyping Reflexivity) corresponds to Lemma stpd_refl.

3. (Narrowing) corresponds to Lemma stp_narrow.

4. (Transitivity Pushback) corresponds to Lemma stp_trans_pushback.

5. (Inversion of Subtyping) corresponds to Coq’s Inversion after pushing back from stp to stpp.
6. (Pre-canonical Forms for Recursive Types) corresponds to pre_canon_bind.
7. (Pre-canonical Forms for Type Members) corresponds to pre_canon_typ.
8. (Substitution for <:) corresponds to the first projection in Lemma subst_aux. See also Lemma stp_subst and Lemma all_Subst.

9. (Substitution for :! ) corresponds to the second projection in Lemma subst_aux.

10. (Substitution for :) corresponds to the third projection of Lemma subst_aux.

11. (Substitution in Term Typing) corresponds to Lemma hastp_subst.

12. (Canonical Forms for Type Members) corresponds to Lemma canon_typ.

13. (Canonical Forms for Method Members) corresponds to Lemma canon_fun.

14. (Substitution for Subtyping) corresponds to Lemma stp_subst_narrow0.

15. (Substitution for Abstract Variable Typing) corresponds to the helper lemma htp_subst_narrow02 within htp_subst_narrow0.
16. (Substitution for Concrete Variable Typing) corresponds to Lemma stp_subst_narrowX.

17. (Concrete Variable Widening) corresponds to Lemma vtp_widen.

18. (Concrete Variable Typing Inversion) corresponds to Lemma hastp_inv.

641