1

# A case for DOT: Theoretical Foundations for Objects With Pattern Matching
and GADT-style Reasoning

Aleksander Boruch-Gruszecki<EMAIL_ADDRESS>0000-0001-5769-6684 EPFLSwitzerland ,  Radosław Waśko<EMAIL_ADDRESS>0000-0001-5539-8245 University of WarsawPoland ,  Yichen Xu<EMAIL_ADDRESS>0000-0003-2089-6767 EPFLSwitzerland and  Lionel Parreaux<EMAIL_ADDRESS>0000-0002-8805-0728 HKUSTHong Kong, China

###### Abstract.

Many programming languages in the OO tradition now support pattern matching in
some form. Historical examples include Scala and Ceylon, with the more recent
additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on
generic class hierarchies currently results in puzzling type errors in most of
these languages. Yet this combination of features occurs naturally in many
scenarios, such as when manipulating typed ASTs. To support it properly,
compilers needs to implement a form of _subtyping reconstruction_ : the
ability to reconstruct subtyping information uncovered at runtime during
pattern matching. We introduce cDOT, a new calculus in the family of Dependent
Object Types (DOT) intended to serve as a formal foundation for subtyping
reconstruction. Being descended from pDOT, itself a formal foundation for
Scala, cDOT can be used to encode advanced object-oriented features such as
generic inheritance, type constructor variance, F-bounded polymorphism, and
first-class recursive modules. We demonstrate that subtyping reconstruction
subsumes GADTs by encoding $\lambda_{2,G\mu}$, a classical constraint-based
GADT calculus, into cDOT.

pattern matching, GADT, classes, type systems

††conference: Technical Report; 2022; arXiv††journalyear: 2022††copyright:
none††ccs: Theory of computation Type structures††ccs: Software and its
engineering Object oriented languages††ccs: Software and its engineering
Classes and objects††ccs: Software and its engineering Patterns

##  1\. Introduction

In recent years, many programming languages in the object-oriented (OO)
tradition started incorporating support for functional programming idioms,
such as lambda expressions and pattern matching. Notably, Java gained a simple
form of pattern matching (limited to single ‘instanceof’ type patterns) in JDK
16, and work on extending this feature to more full-fledged pattern matching
support is ongoing, with an implementation available as a feature preview in
JDK 17. Version 7.0 of C♯ introduced support for type patterns in switch
statements, and version 8.0 introduced switch expressions. Kotlin similarly
supports a restricted form of pattern matching through its ‘when block’
feature. Other widely-used statically-typed languages such as Typescript and
Flow support a variant of pattern matching called _flow-sensitive_ or
_occurrence_ typing. Finally, languages like Scala and Ceylon, which merge the
object-oriented and functional paradigms in a single language, have supported
pattern matching from the start.

⬇

sealed class Expr<A>()

class IntLit (val value: Int) : Expr<Int>()

class ... // other subclasses

⬇

fun <T>eval(expr: Expr<T>): T =

when (expr) {

is IntLit -> expr.value

is ... -> // other cases

}

Figure 1. Example: evaluating simple conditional expressions in Kotlin

These new pattern matching approaches all rely on the idea to statically
_refine_ the type of a “scrutinee” (the object which is being pattern-matched)
based on its runtime shape. Typically, they allow one to test whether a given
value is an instance of some class C, and in the branch where it is known to
be, use the value as such, without requiring an unsafe cast to C.

But combining generic classes with this form of refining type tests leads to
puzzling cases where code that should seemingly compile is rejected. Consider
the example in Figure 1, where we use Kotlin to define Expr, a class that
represents simple arithmetic expressions, and eval, a function which evaluates
said expressions. eval takes an argument of type Expr<T> and returns a T.
Intuitively, the single case shown in Figure 1 is correct. Yet, the latest
version of the Kotlin compiler to date (as of April 2022) rejects it, saying
that the type of expr.value is Int and not T. But our intuition is not wrong:
we have checked that expr is an instance of IntLit, which means that it is
simultaneously an Expr<Int> and an Expr<T>, which in turn means that T is
Int.111 This reasoning is based on the fact that in languages like Kotlin,
Java, Scala, C♯, etc. a derived class may inherit from a given base class at
most once, with specific type arguments. It would not work in C++, where a
class could inherit from two instantiations of the same class, such as
Expr<int> and Expr<bool>, which C++ considers to be two unrelated classes.  In
other words, pattern matching on a value of type Expr<T> lets us discover that
T is the same type as Int in the IntLit branch, which should let us conclude
that eval is well-typed.

Generic class hierarchies (Bracha et al., 1998) have become pervasive in real-
world code bases in Java (Parnin et al., 2013) and many other OO languages.
Therefore, it seems inevitable that the adoption of new pattern-matching
capabilities in these languages will lead to problems like the one outlined
above. Yet, until now, this important topic saw surprisingly little formal or
informal investigation. To the best of our knowledge, Scala is the only
object-oriented language whose implementation currently attempts to allow such
pattern matches, but formal investigations into how it does this have remained
preliminary (Parreaux et al., 2019; Xu et al., 2021), and previous work on the
topic (Emir et al., 2006, 2007; Kennedy and Russo, 2005) was restricted to
simple type systems. Furthermore, none of the previous approaches were
mechanically verified. This is a problematic state of affairs because such
reasoning turns out to be very subtle and hard to implement correctly
(Giarrusso, 2013; Parreaux et al., 2019).

The specific example of Figure 1 will appear familiar to readers already aware
of _generalized algebraic data types_ (GADTs), available in languages such as
Haskell and OCaml, which also allow discovering hidden types and type
relationships by matching on values. However, traditional GADTs operate in
very different type systems than the ones of object-oriented languages.
Traditional GADT constructors do not introduce a type of their own, and are
only attached to a single parent type, forming a flat and closed hierarchy,
contrasting with OOP’s nested and possibly open class hierarchies. Moreover,
traditional GADT implementations only reason about type _equations_ ,222
Interestingly, only reasoning about type _equations_ leads to some paradoxes
in languages like OCaml which do support (an explicit form of) subtyping,
which was previously investigated by Scherer and Rémy (2013).  whereas
inheritance hierarchies, particularly when they involve type constructor
variance, require us to reason about type _inequations_ (i.e., _subtyping_
relationships).

In this paper, we lay out formal foundations for GADT-style reasoning in
object-oriented programming languages. We introduce _subtyping reconstruction_
, a technique that allows pattern-matching functions like eval to be
recognized as well-typed. We base our approach on a new and improved version
of DOT (the Dependant Object Types calculus) extended with a case construct
for pattern matching, and thus named _cDOT_. The expressiveness of this
foundational calculus allows us to establish our reasoning principles in the
presence of advanced object-oriented type system features, such as generic
inheritance, type constructor variance, F-bounded polymorphism, and first-
class recursive module types. This is important because such features are
often present in practical programming languages like Java, C♯, and Scala, and
they significantly complicate the task at hand. We also rigorously explore the
connection between our GADT-style reasoning and traditional GADTs, formally
demonstrating that our approach encompasses traditional GADT reasoning, since
the latter can be encoded in the former.

We make the following specific contributions:

  * –

We introduce cDOT, a formal calculus to serve as a foundation for subtyping
reconstruction (Section 3 and Section 4). cDOT is based on pDOT (Rapoport and
Lhoták, 2019), which is itself an evolution of the original DOT (Amin et al.,
2016), which has been proposed as a foundation for statically-typed object-
oriented programming (Martres, 2022a). We provide a mechanized proof of
soundness for cDOT.

  * –

We propose a variant of the $\lambda_{2,G\mu}$ calculus formalizing
traditional GADTs (Xi et al., 2003) (Section 5.2). Our variant removes some
idiosyncrasies present in the original formulation of $\lambda_{2,G\mu}$,
notably by making its operational semantics deterministic and by making
progress hold. We also provide a mechanized soundness proof for this modified
calculus.

  * –

We develop an encoding of our variant of $\lambda_{2,G\mu}$ into cDOT (Section
5.4) and show that this encoding preserves typing (Section 5.5), which
demonstrates that cDOT can express traditional GADT reasoning. This goes to
show that subtyping reconstruction _subsumes_ (i.e., is at least as powerful
as) traditional GADT reasoning.

##  2\. Static Typing of Class-Based Pattern Matching

In this section, we present the problem of objects with pattern-matching and
GADT-style reasoning, as well as our proposed solution to it, from a high-
level and intuition-focused point of view.

###  2.1. A Core View on Pattern Matching

We define pattern-matching loosely as any conditional expression form which
allows learning about the runtime shape of a value and consequently extracting
information from this shape _in a statically type-safe way_. For instance,
Java’s original instanceof construct does not constitute proper pattern
matching because making use of the information it returns (a boolean value)
requires the use of an _unsafe_ cast, as in ‘if (x instanceof IntLint) return
((IntLint)x).value’. The problem is that the consistency between the runtime
class instance test and the cast to IntLit is not statically checked, and
programmers could (and often do) get it wrong, for example if they had written
‘if (some_condition || x instanceof IntLint) return ((IntLint)x).value’
instead, possibly resulting in runtime ClassCastException crashes. On the
other hand, Java’s newer construct ‘if (x instanceof IntLint y) return
y.value’ is a proper pattern matching implementation, statically known to be
safe.

Many pattern matching implementations allow complex nested patterns, but these
can usually be treated as “syntactic sugar” over a core representation of
pattern matching that proceeds one level at a time. In an object-oriented
language, this core construct would be matching on the class of a given
instance,333 Indeed, the Scala compiler essentially desugars its complex
pattern matching syntax into a succession of instance tests.  similar to
Java’s new ‘instanceof’ construct and to Kotlin’s ‘when’.

###  2.2. Uncovering Types and Subtype Relationships

Consider the Expr/eval example from the introduction again, with more cases
filled in:444 In Kotlin, the star symbol * is used as a placeholder when a
type argument is unknown.

⬇

sealed class Expr<A>()

class IntLit (val value: Int) : Expr<Int>()

class MkPair<B,C>(val lhs: Expr<B>, val rhs: Expr<C>) : Expr<Pair<B,C>>()

class First <B,C>(val pair: Expr<Pair<B,C>>) : Expr<B>()

class Second<B,C>(val pair: Expr<Pair<B,C>>) : Expr<C>()

fun <T>eval(expr: Expr<T>): T =

when (expr) {

is IntLit -> expr.value

is MkPair<*,*> -> Pair(eval(expr.lhs), eval(expr.rhs))

is First <T,*> -> eval(expr.pair).first

is Second<*,T> -> eval(expr.pair).second

}

As we saw, the IntLit branch of this example should compile even though
expr.value returns an Int where a value of type T is expected: when we enter
the IntLit branch, we discover that expr is simultaneously an Expr<T> and an
Expr<Int>, and since Expr is invariant, this can only hold if T and Int are
the same type. While this particular case appears simple, in general this form
of reasoning is non-trivial.

Consider the other cases of eval, and notice the use of * to fill in those
type parameters we locally do not know. For instance, having an Expr<T> that
is also a First<B,C> tells us that B is T, because First<B,C> extends Expr<B>;
however, it tells us _nothing_ about C, which could be Int, Boolean, or any
other type. Accordingly, C needs to be treated as an unknown. Just like for
traditional GADTs, matching on generic classes may uncover unknown types,
which are thus said to be _existentially quantified_. To handle these types
adequately, the compiler must treat them as unspecified abstract types,
locally considered to be distinct from all other types in the program
(sometimes referred to as a “skolem”). Here again the Kotlin compiler fails
us: it disregards these types, widening the corresponding pattern class types
to Any and Nothing. Typing eval also necessitates relating types that are only
_partially_ known, containing references to locally-uncovered type arguments.
This is the case in the MkPair branch: the result of the branch should have
type Pair<?B, ?C>, where ?B and ?C are the locally-uncovered unknown types
associated with MkPair<?B, ?C>, and a compiler implementing GADT-style
reasoning should recognize that in this branch, T is the same as Pair<?B, ?C>,
allowing the expression to type check.

The addition of bounded polymorphism (Cardelli and Wegner, 1985), and
F-bounded polymorphism (Canning et al., 1989) in particular, which are
supported by many object-oriented programming languages (including Java) and
whereby every type parameter may be associated with possibly-cyclic bounds,555
A standard example is a polymorphic function working over any type T where T
is assumed to be a subtype of Comparable<T>, which means that T has a cyclic
bound – i.e., T’s bound refers to T itself.  complicates the picture further.
Essentially, it mean that we should not treat locally-uncovered types as
complete unknowns, but rather as _bounded_ , possibly-recursive abstract
types. This is already a strong justification to reach for the expressive
power of the Dependent Object Types calculus, which features abstract types
with recursive bounds.

###  2.3. Type Constructor Variance

Languages like Kotlin, Scala, and C♯ support a concept known as _(declaration-
site) type constructor variance_ , which allows more flexibility in the way
generic types can be related with each other. Declaring a class such as Expr
to be _covariant_ , which is done in Kotlin with the syntax class Expr<out T>,
means that if Apple is a subtype of Fruit (written Apple $<:$ Fruit), then
Expr<Apple> is itself considered a subtype of Expr<Fruit> (i.e., Expr<Apple>
$<:$ Expr<Fruit>). How does defining Expr as covariant impact eval?

It turns out eval should still type check even when Expr is made covariant,
but the reasoning becomes more subtle. For example, in the IntLit branch, T is
no longer the same as Int. Indeed, the Expr<Int> we got in parameter may have
been _widened_ to any supertype, such as Expr<Any> (since Int is a subtype of
Any) at the time it was passed to eval, so T = Any is anther possibility we
now have to account for. So all we can assume here is that Int is a _subtype_
of T. Fortunately, this is enough for this branch to type check. Moreover,
similar _subtype_ -based reasoning can be applied to the other branches,
allowing eval to type check as a whole.

As another example, if we discover through pattern matching that some value v
is simultaneously a Comparable<T> and a Comparable<Int>, we cannot actually
conclude anything about T and Int. Since Comparable is _contra_ variant
(meaning Comparable<S> $<:$ Comparable<T> if T $<:$ S), v could for example
very well be a Comparable<Any>, since we have both T $<:$ Any and Int $<:$
Any, without T and Int being related in any way. This case differs from the
IntLit case of the eval function described above because in the latter we
_know_ what is the precise type A that IntLit inherits Expr<A> with. Assuming
a covariant Expr, we would be similarly stuck if all we had was the
information that the scrutinee is both of type Expr<T> and of type Expr<Int> —
we would then be unable to related T and Int.

In general, type constructor variance makes GADT-style reasoning for pattern
matching in object-oriented languages a lot more difficult. Indeed, when a
pattern class is covariant or contravariant, we can learn _strictly less_
about the way its type parameters relate with the type of the scrutinee than
in the invariant case. To make matters worse, some languages like Scala (but
unlike Kotlin) support a feature called _variant inheritance_ , whereby a
class may inherit from a variant base several times and at _different_ type
arguments. For example, the following Kotlin code is illegal, but its
equivalent in Scala is legal and is treated as Derived2 inheriting from both
Base<Any> _and_ Base<String>:

⬇

interface Base<out T>

open class Derived1: Base<Any>()

class Derived2: Derived1(), Base<String>

This has led to paradoxes related to pattern matching (Giarrusso, 2013;
Parreaux et al., 2019).

These considerations show that the study of subtyping reconstruction diverges
significantly from that of traditional GADT reasoning.

###  2.4. A Guiding Reasoning Principle

The previous subsection seems to point us in an important direction: our
reasoning should somehow be based on the existence of a “most precise” type
argument used when inheriting from the scrutinee’s class. When we create a new
instance of a class, we need to pick specific type arguments for every type
parameter of every inherited class. But the type arguments we later ascribe to
this instance may become less precise due to variance, and it is crucial to
take that into account.

Let us inspect another example. We define a SUB<S, T> class that is
contravariant in S and covariant in T and that works as runtime evidence that
S is a subtype of T (Yallop and Dolan, 2019):

⬇

sealed class SUB<in S, out T>()

class Refl<U>() : SUB<U, U>()

To illustrate its use, we define a function to convert between two seemingly
unrelated types:

⬇

fun <T>convert(t: T, ev: SUB<T, Int>): Int =

when (ev) { is Refl<*> -> t }

When we check that ev is an instance the Refl class, we discover is that there
was some type U which was used as a type argument to Refl when creating ev.
This type is both a supertype of T and a subtype of Int, so it can only exist
if T $<:$ Int (otherwise the bounds of U would be inconsistent), which is what
we need to type check convert.

Let us inspect one final example:

⬇

fun <T>convert2(t: T, ev: SUB<Expr<T>, Expr<Int>>): Int =

when (ev) { is Refl<*> -> t }

By analogous reasoning, we discover that Expr<T> $<:$ Expr<Int>. However, by
itself this is not enough to type check convert2. Since Expr is covariant, we
need to infer that T must necessarily be a subtype of Int for this
relationship to hold, which exemplifies that subtyping reconstruction needs to
“invert” subtyping relationships, inferring things about the arguments of
related types.

Given a value x of some covariant class type Expr<T> (declared as class
Expr<out A>), let us denote by x.A the precise argument type used to construct
this instance, regardless of any widening that may have happened afterwards.
So we must have that x.A $<:$ T. The fact that this notation looks like a
reference to a _member_ A in x is not accidental: our main idea is to
represent these “most precise types” as _type members_. Type members live
inside class instances, which thus in a sense behave like first-class modules.
This notation allows us to conveniently make explicit how a function like
convert above could type check, by rephrasing it as follows:

⬇

fun <T>convert(t: T, ev: SUB<T, Int>): Int =

when (ev) { is Refl<*> -> t : ev.U@ }

In the above, we added a type annotation to t which shows that it has type
ev.U, since T $<:$ ev.U by contravariance, which allows the term to type check
since ev.U $<:$ Int by covariance.

Reasoning about most-precise type arguments in terms of type members allows us
to clarify and resolve subtleties and paradoxes related to pattern matching
and inheritance. Going back to the Derived2 example from Section 2.3, we can
now explain how Kotlin and Scala have two different notion of inheritance:
when seeing an inheritance clause like ‘: Base<Int>’, Kotlin implicitly
assumes this.T = Int, whereas Scala only assumes this.T $<:$ Int because T is
covariant in Base.666 In fact, in Scala makes an exception for final and case
classes, which use _invariant_ inheritance. This is because case classes are
usually intended for pattern matching, so it is better to recover more
information from them in such use cases.  In fact, in Scala, it is even
possible to inherit (indirectly) from both Base<Int> and Base<String>, which
will result in this.T $<:$ Int & String (where & denotes an _intersection
type_). Both choices are sound and have pros and cons. They also lead to
different subtyping reconstruction capabilities.

###  2.5. Type Parameters As Type Members, Classes as Runtime Tags

As we shall see in the next section, we go even further and completely do away
with type parameters. Indeed, it turns out that type parameters themselves,
along with type constructor variance, can be encoded using type members,
intersections, and structural types, which are all part of our DOT-based
calculus. Doing so allows us to work on a unified representation of all these
concepts, greatly simplifying the specification and soundness proof of our
subtyping reconstruction principles.

Similarly, classes themselves are not a “core” concept of the various DOT
calculi, and are normally encoded using DOT’s expressive recursive object type
system. Indeed, it is possible to encode nominal classes by using bounded type
members and by defining libraries as abstract modules that hide their
implementations. This encoding of the _static typing_ aspect of classes is not
new (Martres, 2022a). What is new in this paper is that we associate runtime
“tags” to such encoded classes, which can be matched against through a case
construct to recover some static type information about the corresponding
instance, as we shall explained in detail in the next section.

Many of the ideas presented in this paper are already well-known. In fact,
they are essentially how the problem of type checking pattern matching was
reasoned about while implementing the Scala 3 compiler, after a long history
of unsound and limited GADT support in Scala 2.777 The Scala versions of all
examples we have shown so far type check correctly in Scala 3.  But this paper
is the first to rigorously formalize the system and derive (mechanized) proofs
of its soundness.

###  2.6. Real-World Justification

Our experience with Scala is that GADT-style reasoning is pervasive in code
bases that make advanced use of the type system to enforce compile-time
guarantee about their programs. Classes like Expr naturally occur in programs
that manipulate typed abstract syntax trees, for instance in database
libraries, which need to manipulate query representations. Indeed, one of our
motivating examples has been the design of a query compiler called
dbStage888Early prototypes of dbStage can be found at
https://github.com/epfldata/dbstage. using the Squid type-safe metaprogramming
framework (Parreaux, 2020) that relies very heavily on GADT-style reasoning.
As another example, Eisenberg (2020) recently described Stitch, an interpreter
and type checker similarly making heavy use of GADTs. Being able to discover
type relationships by pattern matching also allows design patterns that were
not possible or convenient before, for example using subtyping evidence
(Yallop and Dolan, 2019) as described in Section 2.4; the Scala standard
library itself makes heavy use of similar subtyping evidence types.999For
example, the unzip method on List<T> requires an implicit parameter evidence
that T $<:$ (A, B) for some A, B.

##  3\. Informal Introduction to cDOT

In this section, we informally present cDOT and discuss how it allows pattern
matching to uncover hidden types and subtyping relationships.

cDOT belongs to the DOT family of systems, which were originally intended as
formal foundations for Scala. The base DOT calculus was designed to explain
surface type features of Scala using as few core features as possible (Amin et
al., 2016). Importantly for our purposes, there are no classes nor type
parameters in DOT, as both can be encoded through type members (Amin et al.,
2016; Rapoport and Lhoták, 2019; Martres, 2022b). This incidentally
demonstrates that a language does not need to feature nominality in order to
support subtyping reconstruction.

We now gradually introduce the concepts of cDOT by using Scala as the surface
syntax. Our first goal is to encode IntLit from Figure 1. In cDOT, objects are
created via object literals, which are typed with structural types, as in val
e = new { val x = 0 } : { val x: Int }.

Types are compared based on their _structure_ , so to encode IntLit, we need
to first recover nominality. To do this, we rely on the fact that in cDOT, as
well as in Scala, an object instance can contain associated types — called
_type members_. For instance:

⬇

type Animal = { type Food; def eat(food: this.Food): Unit }

def feed(ani: Animal, food: ani.Food) = ani.eat(food)

In the above example, Food is a type member of the object type Animal. Given a
value of type Animal, for instance ani, we can reference the type member that
lives in that instance using a _path-dependent type_ , in this case ani.Food.
This is analogous to defining Animal as a generic class and adding a type
parameter to feed. The distinction between the above type and one like
Animal<Food> is that a type member is existential by default. For instance, we
can refer to a List<Animal>, a list in which every animal may have its own
distinct type of food.

Like type parameters, type members can have (upper and lower) bounds, and in
particular they can also be equal to some type (which simply means that their
lower and upper bounds are the same). Much like instantiating a generic class
requires specific type arguments for all type parameters of the class (they
are often inferred, but are there nonetheless), when we create an object in
cDOT, all of its type members must be defined to be equal to some existing
types. This idea allows cDOT to capture our intuition from before about the
“most precise” type arguments of object instances. To illustrate, we can
create a value of type Animal as follows:

⬇

val goat: Animal = new { type Food = Any; def eat(food: Any) = () }

Given the above val, goat.Food refers to the precise food type that this
specific animal eats, even though it is an abstract type and we know nothing
about it due to the Animal type ascription.

Using bounded type members and structural types, we can recover nominal
classes. To encode IntLit, we create a “package” object g with a type member
IntLit that defines the members of the class. We also define a method
newIntLit which allows us to create instances of said type member (i.e., a
class constructor). We annotate the package object with a type that only
leaves an upper bound on g.IntLit. Taking everything together, our g looks as
follows:

⬇

val g: {

type IntLit <: { val value: Int }

def newIntLit(i: Int): IntLit

} = new {

type IntLit = { val value: Int }

def newIntLit(i: Int): IntLit = new { val value = i }

}

Outside of g, we only have an upper bound on g.IntLit. As a result, with the
above definition the only way to create an object of type g.IntLit is by
calling g.newIntLit. In particular, a value that has the same _shape_ as
IntLit but does not statically have g.IntLit as part of its type will _not_ be
usable as a g.IntLit. In this way, by hiding the exact type g.IntLit stands
for, we have encoded nominality.

We now take a separate look at encoding generic classes based on the example
of Expr<A>. The class itself is encoded as a type member: type Expr $<:$ {
type A }; notice that its type parameter turns into a type member. An applied
type like Expr<Int> is translated to an intersection type Expr & { type A =
Int }. This translation is variance-sensitive; if Expr were covariant, its
type argument would be translated using an _upper bound_ instead, as Expr & {
type A $<:$ Int }; likewise, contravariant type arguments correspond to _lower
bounds_ in applied types.

Let us now come back to our package object g, which we extend with Expr<A>,
with which IntExpr is now related through an intersection type:

⬇

val g: {

type Expr <: { type A }

type IntLit <: Expr & { type A = Int; val value: Int }

def newIntLit(i: Int): IntLit

} = new {

type Expr = { type A }

type IntLit = Expr & { type A = Int; val value: Int }

def newIntLit(i: Int): IntLit = new { type A = Int; val value = i }

}

Again, g’s annotation leaves only upper bounds for g.Expr and g.IntLit, to
encode nominality. In cDOT, structural types with multiple members are
represented via single-member structural type intersections. For instance, {
type A = Int; val value: Int } is represented as { type A = Int } & { val
value: Int }. We use the former as a _shorthand_ for the latter.

Function type parameters are also encoded using type members. A generic
function in cDOT takes an additional argument with one type member per
original type parameter. To illustrate, we can now take a look at an encoded
version of eval from Figure 1:

⬇

def eval(tp: { type T }, e: g.Expr & { type A = tp.T }): tp.T =

e match { case e1: g.IntLit => e1.value }

As expected, this example is well-typed in cDOT; let us inspect it in detail.
The type of e1 is e.type & g.IntLit, with e.type being the singleton type of
e. Singleton types are, conceptually, only inhabited by a single object
instance (here e). Subtyping interacts with intersection types as expected: we
can type e1 both as e.type and as g.IntLit. Since we have e1 : e.type, we know
that e1 is the same object as e, i.e. it is an alias. However, because of the
other part of the intersection type, the type of e1 is more precise than
g.Expr & { type A = tp.T }, the type of e. In this sense, e1 makes the type of
e more precise, which is what we need to type the example.

Since we have both e1 : g.IntLit and e1 : e.type, we respectively know that
Int $<:$ e1.A and e1.A $<:$ tp.T. We conclude that Int <: tp.T by transitivity
of subtyping. So we can return e1.value (whose type is Int) from eval (whose
result type is tp.T).

One problem with eval so far is that the match expression cannot succeed at
runtime, since our encoding of IntLit so far lacks a _runtime tag_.
Implementations of OO languages typically tag every object value with its
_runtime class_ , which enables dynamic type checks and casts. To account for
this, we actually encode each class C as _both_ a type member (as seen before)
_and_ a tag value:

⬇

type C <: { val tag: g.C_tag.type; $\ldots$ }; val C_tag = g.freshTag()

where each call to g.freshTag() creates a unique tag value.101010 This concept
of unique tag is akin to TypeScript’s unique symbol feature
(https://www.typescriptlang.org/docs/handbook/release-
notes/typescript-2-7.html), although the latter only works with static paths,
while we allow path-dependent tags. The representation of tag values at
runtime does not matter as long as we can compare them. E.g., we could use new
empty objects, compared by object identity. Accordingly, to match on an object
we now inspect its tag:

⬇

x match { case e1: g.C => $\ldots$ }

// is encoded as:

x.tag match { case g.C_tag => $\ldots$ }

By construction of the encoding, we know that only objects created through the
constructor of g.C will be associated with g.C_tag at runtime, which lets us
type x in the branch body as x.type & g.C. (Note that this reasoning is not
supported by Scala itself.) Finally, to encode class hierarchies more than one
level deep, we would need to add multiple tags to each object.

This concludes our informal explanation of cDOT’s main ideas. As we shall see,
in the actual formal calculus we strive for simplicity: objects may only have
_one_ tag and _all_ type members are associated with a runtime tag, even those
not meant to represent classes. Extending the system so that objects can have
multiple tags is straightforward and so is left out of cDOT. Associating all
type members with a tag is not a problem because when translating a program to
cDOT all tags used in objects correspond to actual classes, so non-class type
member tags could be erased.

##  4\. Formal Presentation of cDOT

Variable $\displaystyle x,\,y,\,z$ Term member $\displaystyle a,\,b,\,c$ Type
member $\displaystyle A,\,B,\,C$ Path $\displaystyle p,\,q,\,r\coloneqq\ $
variable $\displaystyle x$ field selection $\displaystyle p.a$ Term
$\displaystyle t,\,u\coloneqq\ $ stable term $\displaystyle s$ application
$\displaystyle p\,q$ let binding $\displaystyle{\small\textsf{{let} }}x=t\
{\small\textsf{{in} }}u$ case matching $\displaystyle{\small\textsf{{case}
}}p\ {\small\textsf{{of} }}y\colon q.A\ \Rightarrow t_{1}\
{\small\textsf{{else} }}\Rightarrow t_{2}$ Value $\displaystyle v\coloneqq\ $
tagged object $\displaystyle\nu(x\colon T)[p.A]d$ lambda
$\displaystyle\lambda(x\colon T)\,t$ Stable Term $\displaystyle s\coloneqq\ $
path or value $\displaystyle p\;|\;v$ Definition $\displaystyle d\coloneqq\ $
field definition $\displaystyle\left\\{a=s\right\\}$ type definition
$\displaystyle\left\\{A=T\right\\}$ aggregate definition $\displaystyle
d\wedge d$ Type $\displaystyle S,\,T,\,U,\,V\coloneqq$ top type
$\displaystyle\top$ bottom type $\displaystyle\bot$ field declaration
$\displaystyle\left\\{a\colon T\right\\}$ type declaration
$\displaystyle\left\\{A\colon S..T\right\\}$ intersection $\displaystyle
S\wedge T$ recursive type $\displaystyle\mu\left(x\colon T\right)$ dependent
function $\displaystyle\forall(x\colon S)\,T$ type projection $\displaystyle
p.A$ singleton type $\displaystyle p\mathsf{.type}$

Figure 2. Abstract syntax of cDOT

We now present the cDOT calculus. cDOT extends pDOT (Rapoport and Lhoták,
2019), which itself is a generalization of DOT (Amin et al., 2016) that allows
arbitrary path lengths in path-dependent types: both $x\mathsf{.type}$ and
$x.y\mathsf{.type}$ are permitted. Importantly for us, it also formalizes
singleton types.

All cDOT terms are in a variant of A-normal form, or ANF (Sabry and Felleisen,
1993). For instance, to apply one term to another, we must first bind the
expressions to variables:

$\operatorname{\mathbf{let}}x=t\operatorname{\mathbf{in}}\operatorname{\mathbf{let}}y=s\operatorname{\mathbf{in}}x\,y$

This does not lead to any loss of expressivity, since a simple syntactic
translation can change regular terms to ANF. Essentially, ANF gives us a name
for every value, which is important when we allow function results to depend
on their arguments with path-dependent types. Other DOT systems did not
require ANF (Rompf and Amin, 2016), but at the cost of having two rules for
typing application: one for value arguments and another for variable
arguments.

Since function results can depend on their arguments, in cDOT they are typed
with path-dependent function types. The identity function is typed as follows:

$\vdash\lambda(x:\top)\,x:\forall(x:\top)\,x\mathsf{.type}$

If the result of a function type $\forall(x:S)\,T$ does not depend on its
argument (i.e. if we have $x\notin\mathrm{fv}\,T$), we spell it as
$S\rightarrow T$ as a shorthand.

So far, we have been simplifying one aspect of the syntax. Whereas one would
typically use variables to reference let-bound values, in cDOT we can use
paths. A path $x.a_{1}.\cdots.a_{n}$ is a chain of field selections $.a_{i}$
starting from a variable $x$. Like in pDOT, a cDOT path also represents the
_identity_ of an object, an important notion for a path-dependent type system.
In other DOT systems, objects were bound in a store and referenced by simple
variables, whereas in pDOT and cDOT objects may also be nested inside other
objects, justifying the use of paths for object identity. The typing judgment
$\Gamma\vdash p\colon q\mathsf{.type}$ means that $p$ and $q$ have the same
identity. Like in pDOT, a path is never directly substituted for a value in
cDOT, since doing so would strip an object of its identity.

In cDOT, objects are _tagged_ in order to allow pattern matching. An object
literal in cDOT looks as follows, where $\nu$ is a binder that stands for the
usual new in Scala:

${\nu(x\colon T)[p.A]d}$

Let us inspect it from the right. $d$ is the body of the object; it can
contain fields and type members, whose names are case-sensitive: we use
$A,B,C$ for type members and $a,b,c$ for term members. Object definitions in
cDOT can be circular: their fields can freely reference other fields,
regardless of the definition order. In order to ensure this does not lead to
initialization problems, all fields must be initialized with _stable_ terms
$s$ which are either values or paths. Methods are represented with fields
bound to lambda abstractions. The “tag” $p.A$ is the part of the object value
that enables pattern matching. In cDOT, every object is tagged with a _type
member_ — recall that type members are how we formally represent classes. The
_self reference_ $x$ (usually known as this) is explicitly bound in the syntax
and annotated with a type $T$, which can be used to specify the type that this
object instance should have.

As an illustration, the body of the newIntLit function from before would look
as follows:

$\lambda(i:\mathrm{Int})\,\nu(x:\left\\{A=\mathrm{Int}\right\\}\wedge\left\\{\mathrm{value}:\mathrm{Int}\right\\})[g.\mathrm{IntLit}]\left\\{A=\mathrm{Int}\right\\}\wedge\left\\{\mathrm{value}=i\right\\}$

Finally, the case form ${\small\textsf{{case}}}\ p\ {\small\textsf{{of}}}\
y\colon q.A\Rightarrow t_{1}\ {\small\textsf{{else}}}\Rightarrow t_{2}$ allows
pattern-matching on arbitrary values. There are two branches in this form: if
$p$ resolves to an object whose tag conforms to $q.A$, we bind $y$ to $p$ and
enter $t_{1}$, otherwise we enter $t_{2}$.

We will now inspect the typing and subtyping rules of cDOT. Most of the rules
are the same as in pDOT; we have highlighted all the changes in grey.

###  4.1. Typing

Type environment $\displaystyle\Gamma$ $\displaystyle\Coloneqq\varnothing\ |\
\Gamma,\,x\colon T$

Term typing $\Gamma\vdash t\colon T$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma(x)=T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
x\colon T\end{array}}$ (Var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma,\,x\colon T\vdash t\colon
U\quad\quad
x\notin\mathsf{fv}(T)\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\lambda(x\colon
T)\,t\colon\forall(x\colon T)\,U\end{array}}$ (All-I)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
p\colon\forall(z\colon S)\,T\quad\quad\Gamma\vdash q\colon
S\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash{p\,q}\colon{T}\left[\nicefrac{{q}}{{z}}\right]\end{array}}$
(All-E)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x;\,\Gamma,\,x\colon T\vdash
d\colon T\\\ \hbox{\pagecolor{newrule}$\displaystyle\Gamma,\,x\colon T\vdash
x\colon q.A$}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\nu(x\colon
T)[q.A]d\colon\mu\left(x\colon T\right)\end{array}}$ ({}-I)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
p\colon\left\\{a\colon
T\right\\}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash p.a\colon
T\end{array}}$ (Fld-E)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash p.a\colon
T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash p\colon\left\\{a\colon
T\right\\}\end{array}}$ (Fld-I)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash t\colon T\\\
\Gamma,\,x\colon T\vdash u\colon U\quad\quad
x\notin\mathsf{fv}(U)\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash{\small\textsf{{let}}}\
x=t\ {\small\textsf{{in}}}\ u\colon U\end{array}}$ (Let)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash p\quad\quad\Gamma\vdash q\\\
\Gamma,\,y\colon p\mathsf{.type}\wedge q.A\vdash t_{1}\colon U\\\ \Gamma\vdash
t_{2}\colon U\quad\quad
y\notin\mathsf{fv}(U)\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash{\small\textsf{{case}}}\
p\ {\small\textsf{{of}}}\ y\colon q.A\Rightarrow t_{1}\
{\small\textsf{{else}}}\Rightarrow t_{2}\colon U\end{array}}$ (Case)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash p\colon
q\mathsf{.type}\quad\quad\Gamma\vdash q\colon
T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash p\colon T\end{array}}$
(Sngl-Trans)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
p\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash p\colon
p\mathsf{.type}\end{array}}$ (Sngl-Self)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash p\colon
q\mathsf{.type}\quad\quad\Gamma\vdash
q.a\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash p.a\colon
q.a\mathsf{.type}\end{array}}$ (Sngl-E)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
p\colon{T}\left[\nicefrac{{p}}{{x}}\right]\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
p\colon\mu\left(x\colon T\right)\end{array}}$ (Rec-I)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
p\colon\mu\left(x\colon
T\right)\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
p\colon{T}\left[\nicefrac{{p}}{{x}}\right]\end{array}}$ (Rec-E)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash p\colon
T\quad\quad\Gamma\vdash p\colon
U\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash p\colon T\wedge
U\end{array}}$ (&-I)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash t\colon
T\quad\quad\Gamma\vdash T<:U\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
t\colon U\end{array}}$ (Sub)

Definition typing $p;\,\Gamma\vdash d\colon T$

$\displaystyle\begin{array}[]{@{}c@{}}p;\,\Gamma\vdash\left\\{A=T\right\\}\colon\left\\{A\colon
T..T\right\\}\end{array}$ (Def-Typ)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash\lambda(x\colon
T)\,t\colon\forall(x\colon
U)\,V\end{array}}{\begin{array}[]{@{}c@{}}p;\,\Gamma\vdash\left\\{a=\lambda(x\colon
T)\,t\right\\}\colon\left\\{a\colon\forall(x\colon U)\,V\right\\}\end{array}}$
(Def-All)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}p.a;\,\Gamma\vdash d\theta\colon
T\theta\quad\quad\hbox{\pagecolor{newrule}$\displaystyle\Gamma\vdash p.a\colon
q.A\theta$}\\\
\theta=\\!{{}\left[\nicefrac{{p.a}}{{y}}\right]}\quad\quad{\small\textsf{tight}}\,T\end{array}}{\begin{array}[]{@{}c@{}}p;\,\Gamma\vdash\left\\{a=\nu(y\colon
T)\hbox{\pagecolor{newrule}$\displaystyle[q.A]$}d\right\\}\colon\left\\{a\colon\mu\left(y\colon
T\right)\right\\}\end{array}}$ (Def-New)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
q\end{array}}{\begin{array}[]{@{}c@{}}p;\,\Gamma\vdash\left\\{a=q\right\\}\colon\left\\{a\colon
q\mathsf{.type}\right\\}\end{array}}$ (Def-Path)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}p;\,\Gamma\vdash d_{1}\colon
T_{1}\quad\quad p;\,\Gamma\vdash d_{1}\colon T_{2}\\\
\mathsf{dom}(d_{1})\cap\mathsf{dom}(d_{2})=\varnothing\end{array}}{\begin{array}[]{@{}c@{}}p;\,\Gamma\vdash
d_{1}\wedge d_{2}\colon T_{1}\wedge T_{2}\end{array}}$ (AndDef-I)

Typeable paths $\Gamma\vdash p$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash p\colon
T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash p\end{array}}$ (Wf)

Tight bounds ${\small\textsf{tight}}\,T$

${{\small\textsf{tight}}\,T}=\begin{cases}U=V&\text{if }T=\left\\{A\colon
U..V\right\\}\\\ {\small\textsf{tight}}\,U&\text{if }T=\mu\left(x\colon
U\right)\text{ or }\left\\{a\colon U\right\\}\\\
{\small\textsf{tight}}\,U\text{ and }{\small\textsf{tight}}\,V&\text{if
}T=U\wedge V\\\ \text{true}&\text{otherwise}\end{cases}$

Figure 3. cDOT typing rules

We first go through the typing and subtyping rules of cDOT one by one. Figure
3 presents the typing rules of cDOT. We start with term typing rules, followed
by definition typing, and finally explain the subtyping rules.

##### Term typing rules

The Var, Let and Sub rules for typing variables, let forms and subsumption are
as expected. Term abstractions are typed with dependent function types by
All-I. Rule All-E assigns term applications the function result type, with the
term argument replacing the function parameter. For example, if $\Gamma\vdash
p\colon\forall(x\colon\top)\,x.type$ and $q$ is a typeable path, then $p\,q$
is typed as $q\mathsf{.type}$. The {}-I rule types the tagged objects. The
body is typed with definition typing, explained later. The object type also
must conform to its self-reference type and its tag.

Rules Sngl-Trans, Sngl-Self and Sngl-E deal with singleton types. If $p$ is
typeable, it can be typed as $p\mathsf{.type}$ with Sngl-Self. This rule not
only lets cDOT model Scala’s type system more closely than pDOT (which
surprisingly lacks it), but also turns out to seriously impact both soundness
(Section 4.4) and subtyping (Section 4.2). If $\Gamma\vdash p\colon
q\mathsf{.type}$, we say that $p$ _aliases_ $q$. In such a case, we can always
assign $p$ the same type as $q$ using Sngl-Trans. Aliasing is propagated
through field selection with Sngl-E: $p.a$ aliases $q.a$ if $q$ has a field
$a$ and $p$ aliases $q$.

Field selections are typed with Fld-E. The Fld-I rule introduces field types
when the field selection is typeable. This rule increases the expressiveness
of the type system (Rapoport and Lhoták, 2019). Given $\Gamma\vdash
p\colon\mu\left(x\colon\left\\{a\colon q\mathsf{.type}\right\\}\right)$ and
$\Gamma\vdash q\colon U$, we cannot derive that $\Gamma\vdash
q\mathsf{.type}<:U$. However, with Fld-I we still can type $p$ as
$\left\\{a\colon U\right\\}$.

The Rec-I and Rec-E rules respectively introduce and eliminate recursive
types. Recursive types do not participate in cDOT subtyping; instead, we
unwrap recursive types with Rec-E and re-introduce them with Rec-I. For
example, the following derivation tree shows how we can derive $\Gamma\vdash
p\colon\mu\left(x\colon\left\\{a\colon T\right\\}\right)$ when $\Gamma\vdash
p\colon\mu\left(x\colon\left\\{a\colon S\right\\}\right)$ and $\Gamma\vdash
S<:T$ (where $x$ is absent from $S$ and $T$): *[right=Rec-I] *[right=Sub]
*[right=Rec-E] Γ⊢p:μ(x:{a:S}) Γ⊢p:{a:S}
*[right=Fld-<:-Fld] Γ⊢S<:T Γ⊢{a:S}<:{a:T} Γ⊢p:{a:T} Γ⊢p:μ(x:{a:T}) Although leaving out subtyping relationships between recursive types results in a small loss of expressiveness, it significantly simplifies the metatheory (Amin et al., 2016).

The &-I rule is the introduction rule for intersection types. One may think
that this rule is redundant because we have the Sub and <:-And rules. However,
this rule does add expressiveness when interacting with recursive types (Amin
et al., 2016).

The Case rule types case forms ${{\small\textsf{{case}}}\ p\
{\small\textsf{{of}}}\ y\colon q.A\Rightarrow t_{1}\
{\small\textsf{{else}}}\Rightarrow t_{2}}$. Typing the else branch $t_{2}$ is
straightforward. When typing $t_{1}$, we extend the environment with
$y:{p\mathsf{.type}\wedge q.A}$, which essentially introduces a witness that
the path $p$ can be typed as $q.A$. We see in Section 4.2 that together with
_subtyping inversion_ , such a witness allows reconstruction of subtype
relationships.

##### Definition typing

The definition typing rules in Figure 3 are used to type object bodies. In
pDOT and cDOT, only function values, object values and paths can be used to
initialize a field. The Def-All, Def-New and Def-Path rules type object fields
as their precise type. The ${\small\textsf{tight}}\,T$ condition in Def-New
ensures all type members in $T$ have equal bounds. In addition to type
checking the definition, the Def-New rule also checks the conformance between
the object type and the type tag. The Def-Typ rule types the type member
definition. The AndDef-I rule type multiple member definitions as an
intersection type. The prefix $p$ in definition typing keeps track of the
identity of the currently typing object, since the definition typing rules can
be used to type nested object definitions.

##### Tagged objects

An object form $\nu(y\colon T)[x.A]d$ must itself be typeable as its tag
$x.A$; this condition is checked by the {}-I and Def-New rules. It may appear
problematic to require _all_ object to refer to another object’s type member
in its tag: after all we need a tag to type check the very first object in a
cDOT program, but tags themselves come from objects! This is not actually a
problem because in cDOT objects can be typed recursively: we can type check a
self-tagged object
$\operatorname{\mathbf{let}}x=\nu(x\colon\left\\{A=\top\right\\})[x.A]\left\\{A=\top\right\\}$,
whose type member $x.A$ may later be used as a “top tag” that can tag any
object. In later examples we will sometimes skip the tag of an object; we
understand such objects to be tagged with this “top tag”. Notice that our tag
system does not support inheritance: in order to encode class hierarchies more
than one level deep, we would need to tag objects with _several_ class tags.
For simplicity, we leave this straightforward extension out of cDOT.

###  4.2. Subtyping

Subtyping $\Gamma\vdash S<:T$

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash T<:\top\end{array}$ (Top)

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash\bot<:T\end{array}$ (Bot)

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash T<:T\end{array}$ (Refl)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
S<:T\quad\quad\Gamma\vdash
T<:U\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash S<:U\end{array}}$
(Trans)

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash T\wedge U<:T\end{array}$
(And1-$<:$)

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash T\wedge U<:U\end{array}$
(And2-$<:$)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
S<:T\quad\quad\Gamma\vdash
S<:U\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash S<:T\wedge
U\end{array}}$ ($<:$-And)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
T<:U\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\left\\{a\colon
T\right\\}<:\left\\{a\colon U\right\\}\end{array}}$ (Fld-$<:$-Fld)

$\frac{\begin{array}[]{@{}c@{}}U\searrow\left\\{a\colon T_{1}\right\\}\\\
\Gamma\vdash U<:\left\\{a\colon
T_{2}\right\\}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
T_{1}<:T_{2}\end{array}}$ (Fld-$<:$-Fld-Inv)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
S_{2}<:S_{1}\quad\quad\Gamma\vdash
T_{1}<:T_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\left\\{A\colon
S_{1}..T_{1}\right\\}<:\left\\{A\colon S_{2}..T_{2}\right\\}\end{array}}$
(Typ-$<:$-Typ)

$\frac{\begin{array}[]{@{}c@{}}U\searrow\left\\{A\colon
S_{1}..T_{1}\right\\}\\\ \Gamma\vdash U<:\left\\{A\colon
S_{2}..T_{2}\right\\}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
S_{2}<:S_{1}\end{array}}$ (Typ-$<:$-Typ-Inv1)

$\frac{\begin{array}[]{@{}c@{}}U\searrow\left\\{A\colon
S_{1}..T_{1}\right\\}\\\ \Gamma\vdash U<:\left\\{A\colon
S_{2}..T_{2}\right\\}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
T_{1}<:T_{2}\end{array}}$ (Typ-$<:$-Typ-Inv2)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
p\colon\left\\{A\colon
S..T\right\\}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
S<:{p}.A\end{array}}$ ($<:$-Sel)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash p\colon
q\mathsf{.type}\quad\quad\Gamma\vdash
q\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
T<:{T}\left[\nicefrac{{q}}{{{p}}}\right]\end{array}}$ (Snglpq-$<:$)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash p\colon
q\mathsf{.type}\quad\quad\Gamma\vdash
q\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
T<:{T}\left[\nicefrac{{p}}{{{q}}}\right]\end{array}}$ (Snglqp-$<:$)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
p\colon\left\\{A\colon
S..T\right\\}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
p.A<:T\end{array}}$ (Sel-$<:$)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash S_{2}<:S_{1}\\\
\Gamma,\,x\colon S_{2}\vdash
T_{1}<:T_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\forall(x\colon
S_{1})\,T_{1}<:\forall(x\colon S_{2})\,T_{2}\end{array}}$ (All-$<:$-All)

Unique membership $T\searrow U$

$\frac{\begin{array}[]{@{}c@{}}T\searrow
U;\mathcal{L}\end{array}}{\begin{array}[]{@{}c@{}}T\searrow U\end{array}}$
(Unique-Label)

Unique membership with label $T\searrow U;\mathcal{L}$

$\begin{array}[]{@{}c@{}}\left\\{A\colon S..T\right\\}\searrow\left\\{A\colon
S..T\right\\};\left\\{A\right\\}\end{array}$ (One-Typ)

$\begin{array}[]{@{}c@{}}\left\\{a\colon T\right\\}\searrow\left\\{a\colon
T\right\\};\left\\{a\right\\}\end{array}$ (One-Fld)

$\begin{array}[]{@{}c@{}}\mu\left(x\colon T\right)\searrow\mu\left(x\colon
T\right);\emptysetAlt\end{array}$ (One-Rec)

$\frac{\begin{array}[]{@{}c@{}}U_{1}\searrow T_{1};\mathcal{L}_{1}\quad\quad
U_{2}\searrow T_{2};\mathcal{L}_{2}\\\
\mathcal{L}_{1}\cap\mathcal{L}_{2}=\emptysetAlt\end{array}}{\begin{array}[]{@{}c@{}}U_{1}\wedge
U_{2}\searrow T_{1};\mathcal{L}_{1}\cup\mathcal{L}_{2}\end{array}}$ (And-Left)

$\frac{\begin{array}[]{@{}c@{}}U_{1}\searrow T_{1};\mathcal{L}_{1}\quad\quad
U_{2}\searrow T_{2};\mathcal{L}_{2}\\\
\mathcal{L}_{1}\cap\mathcal{L}_{2}=\emptysetAlt\end{array}}{\begin{array}[]{@{}c@{}}U_{1}\wedge
U_{2}\searrow T_{2};\mathcal{L}_{1}\cup\mathcal{L}_{2}\end{array}}$ (And-
Right)

Figure 4. cDOT subtyping rules

We now inspect the subtyping rules defined in Figure 4. Subtyping is made
reflexive and transitive with Refl and Trans. Rules for top, bottom and
intersection types are typical (respectively Top, Bot and And1-<:, And2-<:,
<:-And). Rules Fld-<:-Fld, Typ-<:-Typ and All-<:-All derive the standard
subtyping relationships between object fields, type members and functions.
Rules <:-Sel and Sel-<: relate a path-dependent type and its bounds.
Importantly, these rules also allow path-dependent types to introduce new
subtyping relationships. For example, if we have $\Gamma\vdash
p\colon\left\\{A\colon\mathrm{Int}..q.T\right\\}$, then by Trans and relating
$q.T$ with its bounds we also can derive $\Gamma\vdash\mathrm{Int}<:q.T$.

##### Aliasing paths

Rules Snglpq-<: and Snglqp-<: establish equivalence of aliasing paths: if we
can derive $\Gamma|-p:q\mathsf{.type}$, then with subtyping we can freely
substitute $p$ for $q$ in types and vice versa. The expressivity of these
rules is augmented by Sngl-Self. Consider the following example:

${\small\textsf{{case}}}\ p\ {\small\textsf{{of}}}\ y\colon
g.\mathrm{IntLit}\Rightarrow p\ {\small\textsf{{else}}}\Rightarrow\cdots$

In the matched branch we should be able to type $p$ as $g.\mathrm{LitInt}$.
However, this is not possible without the Sngl-Self rule. When typing the type
case, the environment is extended with $y:p\mathsf{.type}\wedge
g.\mathrm{LitInt}$. In pDOT, we can only type $\Gamma\vdash y\colon
p\mathsf{.type}$, but not the other direction due to the asymmetric nature of
pDOT path aliasing: the Sngl-Trans rule only allows the propagation of typing
from $p$ to $y$, but not the reverse. This means that, although $y$ should
witness that $p$ can be typed as $g.\mathrm{LitInt}$, there is no way to
assign the witnessed type to $p$. The Sngl-Self rule mitigates the limitation
by making path aliasing symmetric (i.e. we can derive $\Gamma\vdash p\colon
q\mathsf{.type}$ from $\Gamma\vdash q\colon p\mathsf{.type}$). The Sngl-Trans
can type $p$ as $g.\mathrm{LitInt}$. The following derivation tree illustrates
how Sngl-Self enables us to type path aliasing symmetrically Here
$\Gamma^{\prime}$ denotes $\Gamma,\,y\colon p\mathsf{.type}\wedge
g.\mathrm{IntLit}$. *[right=Sub] *[right=Sngl-Self] Γ^′⊢p Γ^′⊢p:p.type
*[right=Snglqp-<:] Γ^′⊢y:p.type
Γ^′⊢p Γ^′⊢p.type<:y.type Γ^′⊢p:y.type

#### Subtyping inversion

Finally, we can reconstruct premises of other subtyping rules with
Fld-$<:$-Fld-Inv, Typ-$<:$-Typ-Inv1 and Typ-$<:$-Typ-Inv2, the _inversion
rules_. For instance, using Fld-$<:$-Fld-Inv, we can derive
$\Gamma\vdash\mathrm{Int}<:x.T$ from
$\Gamma\vdash\left\\{a:\mathrm{Int}\right\\}<:\left\\{a:x.T\right\\}$,
respectively the premise and conclusion of Fld-$<:$-Fld. The inversion rules
are only useful if the bindings in the context introduce some subtyping
relationships as assumptions. Consider the following example:

$\displaystyle\lambda(x\colon\left\\{T\colon\bot..\top\right\\})\,\,\lambda(f\colon
x.T\rightarrow\mathrm{Int})\,\,\lambda(y\colon\left\\{A:{\left\\{a\colon\mathrm{Int}\right\\}}..{\left\\{a\colon
x.T\right\\}}\right\\})\,\;\;f\,0$

To type it, we need to derive that $\mathrm{Int}<:x.T$. Based on the bounds of
$y.A$, we can derive that
$\left\\{a\colon\mathrm{Int}\right\\}<:\left\\{a\colon x.T\right\\}$; in other
words, this relationship is an assumption introduced by $y$. Intuitively, in
any context in which we can construct a value for $y$, we can also derive that
$\mathrm{Int}<:x.T$; using bounds of $y$ and subtyping inversion, we can also
derive that if we only have $y$:

… <:-Sel $\Gamma\vdash\left\\{a\colon\mathrm{Int}\right\\}<:y.A$ … Sel-<:
$\Gamma\vdash y.A<:\left\\{a\colon x.T\right\\}$ Trans
$\Gamma\vdash\left\\{a\colon\mathrm{Int}\right\\}<:\left\\{a\colon
x.T\right\\}$
$\left\\{a\colon\mathrm{Int}\right\\}\searrow\left\\{a\colon\mathrm{Int}\right\\}$
Fld-<:<-Fld-Inv $\Gamma\vdash\mathrm{Int}<:x.T$

The combination of bindings that introduce subtyping assumptions and inversion
rules that allow deriving premises of assumptions is _subtyping
reconstruction_ : the ability to use a binding to derive subtyping
relationships necessary to construct a value which could stand for the
binding.

The inversion rules use the unique membership relation $T\searrow U$, defined
in Figure 4. It allows extracting a component $U$ out of an intersection type
$T$, which allows inverting relationships involving intersection types, for
instance:

$\Gamma\vdash\left\\{a:S\right\\}\wedge\left\\{b:U_{2}\right\\}<:\left\\{a:T\right\\}$
$\left\\{a:S\right\\}\wedge\left\\{b:U\right\\}\searrow\left\\{a:S\right\\}$
Fld-<:-Fld-Inv $\Gamma\vdash S<:T$

In order to invert relationships that involve an intersection type on the RHS,
we can use Trans. For instance, in the above derivation, the inverted
subtyping relation could be derived like this:

$\Gamma\vdash\left\\{a:S\right\\}\wedge\left\\{b:U_{1}\right\\}<:\left\\{a:T\right\\}\wedge\left\\{c:U_{2}\right\\}$
$\Gamma\vdash\left\\{a:T\right\\}\wedge\left\\{c:U_{2}\right\\}<:\left\\{a:T\right\\}$
Trans
$\Gamma\vdash\left\\{a:S\right\\}\wedge\left\\{b:U_{2}\right\\}<:\left\\{a:T\right\\}$

In order for subtyping inversion to be sound, all the labels of $T$ in
$T\searrow U$ must be unique. To see why, consider this relationship:

$\Gamma\vdash\left\\{a\colon T_{1}\right\\}\wedge\left\\{a\colon
T_{2}\right\\}<:\left\\{a\colon U\right\\},$

The original premise used to derive this relationship may have been either
$\Gamma\vdash T_{1}<:U$ or $\Gamma\vdash T_{2}<:U$. Since we cannot know which
one it was, we can derive neither with the inversion rules.

###  4.3. Evaluation

Store $\displaystyle\gamma\Coloneqq$ $\displaystyle\ \varnothing\ |\
\gamma,\,x\mapsto v$ Resolved Path $\displaystyle\rho^{\gamma}\Coloneqq$
$\displaystyle\ p\quad\text{(if $\exists v.\,\gamma\vdash p\leadsto v$)}$

Evaluation Context $\displaystyle e^{\gamma}\Coloneqq$ $\displaystyle[\ ]\ |\
[\ ]\,q\ |\ \rho^{\gamma}\,[\ ]$ $\displaystyle|$ $\displaystyle\
{\small\textsf{{let}}}\ x=e^{\gamma}\ {\small\textsf{{in}}}\ u$
$\displaystyle|$ $\displaystyle\ {\small\textsf{{case}}}\ [\ ]\
{\small\textsf{{of}}}\ y\colon q.A\Rightarrow t_{1}\
{\small\textsf{{else}}}\Rightarrow t_{2}$ $\displaystyle|$ $\displaystyle\
{\small\textsf{{case}}}\ \rho^{\gamma}\ {\small\textsf{{of}}}\ y\colon[\
].A\Rightarrow t_{1}\ {\small\textsf{{else}}}\Rightarrow t_{2}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\gamma\mid
t\,\longmapsto\,\gamma^{\prime}\mid
t^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\gamma\mid
e^{\gamma}[t]\,\longmapsto\,\gamma^{\prime}\mid
e^{\gamma}[t^{\prime}]\end{array}}$ (Ctx)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\gamma\vdash p\leadsto
q}\end{array}}{\begin{array}[]{@{}c@{}}\gamma\mid p\,\longmapsto\,\gamma\mid
q\end{array}}$ (Resolve)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\gamma\vdash
q\leadsto\lambda(z\colon
T)\,t}\end{array}}{\begin{array}[]{@{}c@{}}\gamma\mid{q\,\rho^{\gamma}}\,\longmapsto\,\gamma\mid{t}\left[\nicefrac{{\rho^{\gamma}}}{{z}}\right]\end{array}}$
(Apply)

$\displaystyle\begin{array}[]{@{}c@{}}\gamma\mid{\small\textsf{{let}}}\
x=\rho^{\gamma}\ {\small\textsf{{in}}}\
t\,\longmapsto\,\gamma\mid{t}\left[\nicefrac{{\rho^{\gamma}}}{{x}}\right]\end{array}$
(Let-Path)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x\notin\mathsf{dom}(\gamma)\end{array}}{\begin{array}[]{@{}c@{}}\gamma\mid{\small\textsf{{let}}}\
x=v\ {\small\textsf{{in}}}\ t\,\longmapsto\,\gamma,\,x\mapsto v\mid
t\end{array}}$ (Let-Value)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\gamma\vdash q\leadsto\nu(x\colon
T)[r.A]d\quad\quad\gamma\vdash
r\leadsto^{*}\rho^{\gamma}\end{array}}{\begin{array}[]{@{}c@{}}\gamma\mid{\small\textsf{{case}}}\
q\ {\small\textsf{{of}}}\ y\colon\rho^{\gamma}\\!.\,A\Rightarrow t_{1}\
{\small\textsf{{else}}}\Rightarrow
t_{2}\,\longmapsto\,\gamma\mid{t_{1}}\left[\nicefrac{{p}}{{y}}\right]\end{array}}$
(Case-Then)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\gamma\vdash q\leadsto\nu(x\colon
T)[r.A]d\quad\gamma\vdash
r\leadsto^{*}\rho^{\gamma}_{1}\quad{\rho^{\gamma}_{1}}\\!.\,A\neq{\rho^{\gamma}_{2}}.B\end{array}}{\begin{array}[]{@{}c@{}}\gamma\mid{\small\textsf{{case}}}\
q\ {\small\textsf{{of}}}\ y\colon{\rho^{\gamma}_{2}}.B\Rightarrow t_{1}\
{\small\textsf{{else}}}\Rightarrow t_{2}\,\longmapsto\,\gamma\mid
t_{2}\end{array}}$ (Case-Else)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\gamma\vdash
p\leadsto\lambda(x\colon
T)\,U\end{array}}{\begin{array}[]{@{}c@{}}\gamma\mid{\small\textsf{{case}}}\
p\ {\small\textsf{{of}}}\ y\colon\rho^{\gamma}\\!.\,A\Rightarrow t_{1}\
{\small\textsf{{else}}}\Rightarrow t_{2}\,\longmapsto\,\gamma\mid
t_{2}\end{array}}$ (Case-$\forall$)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\gamma(x)=v\end{array}}{\begin{array}[]{@{}c@{}}\gamma\vdash
x\leadsto v\end{array}}$ (Lookup-Step-Var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\gamma\vdash p\leadsto\nu(x\colon
T)[r.A]\dots\left\\{a=s\right\\}\dots\end{array}}{\begin{array}[]{@{}c@{}}\gamma\vdash
p.a\leadsto{s}\left[\nicefrac{{p}}{{x}}\right]\end{array}}$ (Lookup-Step-Val)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\gamma\vdash p\leadsto
q\end{array}}{\begin{array}[]{@{}c@{}}\gamma\vdash p.a\leadsto
q.a\end{array}}$ (Lookup-Step-Path)

Figure 5. Operational semantics of cDOT

The operational semantics of cDOT is presented in Figure 5. We define
$\leadsto^{*}$ as the transitive, reflexive closure of $\leadsto$. Since our
reduction rules are significantly different from pDOT, we do not highlight the
differences.

#### Store.

Similarly to pDOT, cDOT reduction is store-based. During evaluation, we still
need to keep track of object identities; to do so, the store $\gamma$ binds
_variables_ to values. Note that objects still contains nested objects during
evaluation: in general, the identity of an object may be a path.

#### Path resolution.

Compared to pDOT, the most significant change in cDOT is that the Resolve rule
allows reducing aliasing paths: given $\gamma\vdash p\leadsto q$, we can
reduce $\gamma\mid p\,\longmapsto\,\gamma\mid q$. We call a path $p$ that
directly resolves to a value in $\gamma$ a _resolved path_ $\rho^{\gamma}$
(see Figure 5). Resolved paths cannot be reduced any further; much like
singleton types capture object identities on the type level, on the term level
a resolved path directly corresponds to the runtime identity of an object.
Importantly, as a consequence of modelling recursive objects and modules, it
is possible to create objects with circular fields. References to such fields
results in infinite loops. A circular object may be defined like this:

$\nu(x:\left\\{a:x.b\mathsf{.type}\right\\}\wedge\left\\{b:x.a\mathsf{.type}\right\\})\left\\{a=x.b\right\\}\wedge\left\\{b=x.a\right\\}$

In pDOT, it is impossible to reduce paths, and even resolving path aliases
breaks preservation. For example, if $p$ can be typed as $q.type$ in $\Gamma$
and it looks up to $q$ in $\gamma$, there is still no guarantee that $q$ can
be typed as $q.type$ in $\Gamma$ and so allowing $\gamma\mid
p\,\longmapsto\,\gamma\mid q$ would violate type preservation. In cDOT, we can
always type $q$ as $q.type$ thanks to the Sngl-Self rule and so reducing paths
preserves their types.

$\displaystyle\begin{array}[]{@{}c@{}}\gamma\mid{\small\textsf{{let}}}\ x=p\
{\small\textsf{{in}}}\
t\,\longmapsto\,\gamma\mid{t}\left[\nicefrac{{p}}{{x}}\right]\end{array}$

$\displaystyle\begin{array}[]{@{}c@{}}\gamma\mid{\small\textsf{{let}}}\
x=\hbox{\pagecolor{newrule}$\displaystyle\rho^{\gamma}$}\
{\small\textsf{{in}}}\
t\,\longmapsto\,\gamma\mid{t}\left[\nicefrac{{\rho^{\gamma}}}{{x}}\right]\end{array}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\gamma\vdash
q\leadsto^{*}\lambda(z\colon
T)\,t}\end{array}}{\begin{array}[]{@{}c@{}}\gamma\mid{q\,p}\,\longmapsto\,\gamma\mid{t}\left[\nicefrac{{p}}{{z}}\right]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\gamma\vdash
q\leadsto\lambda(z\colon
T)\,t}\end{array}}{\begin{array}[]{@{}c@{}}\gamma\mid{q\,\hbox{\pagecolor{newrule}$\displaystyle\rho^{\gamma}$}}\,\longmapsto\,\gamma\mid{t}\left[\nicefrac{{\hbox{\pagecolor{newrule}$\displaystyle\rho^{\gamma}$}}}{{z}}\right]\end{array}}$

Figure 6. The Let-Path (top) and Apply (bottom) rules of pDOT (left) and cDOT
(right).

The reduction of paths also brings significant changes to the reduction of let
bindings and lambda applications, as we can see on Figure 6. In pDOT, a let-
bound path is reduced by substituting the path into the let body; in cDOT, we
first reduce the path until it is fully resolved.

#### Case term reduction.

Both pDOT and cDOT ensure that paths typeable with function and object types
always resolve to a value, which is necessary for soundness (Rapoport and
Lhoták, 2019). Figure 6 shows that pDOT transitively looks up paths when
reducing apply forms $q\,p$: being unable to look up $q$ would result in a
stuck term. However, cDOT case forms allow scrutinees of arbitrary types and
such scrutinees may refer to a circularly-defined field. To avoid transitive
lookups of such fields, cDOT allows reducing paths, letting case forms with
such scrutinees loop endlessly. This mirrors how looking up lazily defined,
circular fields in Scala also results in endless loops.

###  4.4. Metatheory

We provide a mechanized soundness proof for cDOT, basing on soundness proof
for pDOT (Rapoport and Lhoták, 2019), at its core formulated in the standard
progress-and-preservation style (Wright and Felleisen, 1994). Our Coq proof
scripts have $\approx$ 13100 lines of code, compared to $\approx$ 9800 lines
in the pDOT soundness proof. We attach the proof as an artifact.

Evaluating any well-typed cDOT program either diverges or results in a normal
form.

###### Theorem 4.1 (Type Safety).

If $\vdash t\colon T$, then the evaluation of $t$ either diverges, or
$\emptysetAlt\mid t\,\longmapsto\,\gamma\mid u$ such that (a) $u$ is a normal
form under $\gamma$; (b) $\Gamma\vdash u\colon T$ for some $\Gamma$ and (c)
${\gamma\colon\Gamma}$.

${\gamma\colon\Gamma}$ means that $\gamma$ conforms to $\Gamma$, i.e. for any
variable $x_{i}\in\mathrm{dom}\,\Gamma$, if $\Gamma(x_{i})=T_{i}$ and
$\gamma(x_{i})=v_{i}$, then $\Gamma\vdash v_{i}\colon T_{i}$. Normal forms are
values and resolved paths.

####  4.4.1. Soundness Proof: From pDOT to cDOT

Our soundness proof extensively reuses the infrastructure and toolkits
provided by pDOT. The strategy central to the proof of pDOT is to stratify
typing rules into seven levels (Rapoport and Lhoták, 2019), as illustrated in
the following diagram:

$\displaystyle{\tiny\text{General }(\vdash)\rightarrow\text{Tight
}(\vdash_{\\#})\rightarrow{\text{{Introduction-$qp$
}}(\vdash_{qp})}\rightarrow\text{Introduction-$pq$
}(\vdash_{pq})\rightarrow{\text{Elim-III
}(\vdash_{e3})}\rightarrow{\text{Elim-II
}(\vdash_{e2})}\rightarrow\text{Elim-I }(\vdash_{e1})}$

The stratified typing level hierarchy tackles the bad bounds problem (Amin et
al., 2016) and eliminates cycles in type derivation (Rapoport and Lhoták,
2019; Rapoport et al., 2017). Innermost typing levels assign precise typing
information to paths directly followed from the environment and path aliasing.
It is easy to do induction and reason about typing judgments on these levels.
With a series of transformation lemmas converting judgments between levels,
the general recipe of pDOT soundness proof is to transform the surface typing
level (general typing $\vdash$) to inner typing levels and then reason about
the typing judgments. (See Appendix B for a detailed description.)

The soundness proof of cDOT follows the stratified typing levels of the pDOT
soundness proof. We describe our extensions in detail in Section 4.4.2. We
state Preservation and Progress as follows:

###### Theorem 4.2 (Preservation).

Let $\Gamma$ be an inert, well-formed typing environment and let
${\gamma\colon\Gamma}$. If $\gamma\mid t\,\longmapsto\,\gamma^{\prime}\mid
t^{\prime}$ and $\Gamma\vdash t\colon T$, then there exists an inert and well-
formed typing environment $\Gamma^{\prime}$ such that
${\Gamma^{\prime}\colon\gamma^{\prime}}$ and $\Gamma^{\prime}\vdash
t^{\prime}\colon T$.

###### Theorem 4.3 (Progress).

Let $\Gamma$ be an inert, well-formed typing environment and let
${\gamma\colon\Gamma}$. If $\Gamma\vdash t\colon T$, then either $t$ is a
normal form, or there exists $\gamma^{\prime}$ and $t^{\prime}$, such that
$\gamma\mid t\,\longmapsto\,\gamma^{\prime}\mid t^{\prime}$.

An environment is inert if it only contains inert types, i.e. types that
cannot introduce subtyping assumptions. A type is inert if it is a lambda type
or an object types with tight type members (see Appendix B). An environment
$\Gamma$ is well-formed if every path mentioned in $\Gamma$ is typeable in
$\Gamma$. Notably, Sngl-Self is necessary to show Preservation. For example,
consider the following term:

${\small\textsf{{case}}}\ p\ {\small\textsf{{of}}}\ y\colon q.A\Rightarrow y\
{\small\textsf{{else}}}\Rightarrow t_{2}$

We assume that both $p$ and $q$ are resolved, the pattern is matched and
$t_{2}$ is a term that can be typed as $p\mathsf{.type}$. We can type the case
term $t$ as $p\mathsf{.type}$ with the Case rule. Then, when reducing the case
term, we apply the Case-Then rule and reduce the term to
${y}\left[\nicefrac{{p}}{{y}}\right]=p$. Here, to prove preservation,
$\Gamma\vdash p\colon p\mathsf{.type}$ must be derivable, which is only made
possible by the Sngl-Self rule.

The Progress proof in the case for terms of the form ${\small\textsf{{case}}}\
p\ {\small\textsf{{of}}}\ y\colon{\rho^{\gamma}}.A\Rightarrow t_{1}\
{\small\textsf{{else}}}\Rightarrow t_{2}$ relies on 4.1, which shows if $p$
resolves to an object $\nu(x\colon T)[r.A]d$ then $r$ also can be resolved.
Otherwise, neither Case-Then nor Case-Else would apply, making the term stuck.

###### Lemma 4.1 (Tag Resolution).

Let $\Gamma$ be inert and well formed. If $p$ is typeable in $\Gamma$,
${\gamma\colon\Gamma}$ and $\gamma\vdash p\leadsto\nu(x\colon T)[r.A]d$, then
there exists $\rho^{\gamma}$ such that $\gamma\vdash
r\leadsto^{*}\rho^{\gamma}$.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\hbox{\pagecolor{newrule}$\displaystyle\Gamma\vdash_{\\#}S_{2}<:S_{1}$}\quad\quad\hbox{\pagecolor{newrule}$\displaystyle\Gamma\vdash_{\\#}T_{1}<:T_{2}$}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#\\#}\left\\{A\colon
S_{1}..T_{1}\right\\}<:\left\\{A\colon S_{2}..T_{2}\right\\}\end{array}}$
(Typ-$<:$-Typ##)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{e3}p\colon\left\\{A\colon
T..T\right\\}\\\
\hbox{\pagecolor{newrule}$\displaystyle\Gamma\vdash_{\\#\\#}S<:T$}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#\\#}\hbox{\pagecolor{newrule}$\displaystyle
S$}<:{p}.A\end{array}}$ ($<:$-Sel##)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{e3}p\colon\left\\{A\colon
T..T\right\\}\\\
\hbox{\pagecolor{newrule}$\displaystyle\Gamma\vdash_{\\#\\#}T<:U$}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#\\#}p.A<:\hbox{\pagecolor{newrule}$\displaystyle
U$}\end{array}}$ (Sel-$<:$##)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{e3}p\colon
q\mathsf{.type}\quad\quad\Gamma\vdash_{e2}q\\\
\Gamma\vdash_{\\#\\#}\hbox{\pagecolor{newrule}$\displaystyle
S$}<:T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#\\#}\hbox{\pagecolor{newrule}$\displaystyle
S$}<:{T}\left[\nicefrac{{q}}{{{p}}}\right]\end{array}}$ (Snglpq2-$<:$##)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{e3}p\colon
q\mathsf{.type}\quad\quad\Gamma\vdash_{e2}q\\\
\Gamma\vdash_{\\#\\#}S<:T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#\\#}{S}\left[\nicefrac{{q}}{{{p}}}\right]<:T\end{array}}$
(Snglpq1-$<:$##)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{e3}p\colon
q\mathsf{.type}\quad\quad\Gamma\vdash_{e2}q\\\
\Gamma\vdash_{\\#\\#}\hbox{\pagecolor{newrule}$\displaystyle
S$}<:T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#\\#}\hbox{\pagecolor{newrule}$\displaystyle
S$}<:{T}\left[\nicefrac{{p}}{{{q}}}\right]\end{array}}$ (Snglqp2-$<:$##)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{e3}p\colon
q\mathsf{.type}\quad\quad\Gamma\vdash_{e2}q\\\
\Gamma\vdash_{\\#\\#}S<:T\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#\\#}{S}\left[\nicefrac{{p}}{{{q}}}\right]<:T\end{array}}$
(Snglqp1-$<:$##)

Figure 7. Invertible subtyping rules (interesting cases, with changes
highlighted).

####  4.4.2. Proving Inversion Rules with Invertible Subtyping

When implementing the soundness proof, we add inversion rules only to the
surface typing level, and keep the inner levels unchanged. Then, we only need
to re-prove the transformation lemma from general typing to the tight level.
This is to prove that the inversion rules are _admissible_ in tight typing
when the environment is inert, which is stated in the following two lemmas.

###### Lemma 4.2 (Field Inversion).

In an inert environment $\Gamma$, if $\Gamma\vdash_{\\#}U<:\left\\{a\colon
T_{2}\right\\}$ and $U\searrow\left\\{a\colon T_{1}\right\\}$, then
$\Gamma\vdash_{\\#}T_{1}<:T_{2}$.

###### Lemma 4.3 (Type Member Inversion).

In an inert environment $\Gamma$, if $\Gamma\vdash_{\\#}U<:\left\\{A\colon
S_{2}..T_{2}\right\\}$ and $U\searrow\left\\{A\colon S_{1}..T_{1}\right\\}$,
then $\Gamma\vdash_{\\#}S_{2}<:S_{1}$ and $\Gamma\vdash_{\\#}T_{1}<:T_{2}$.

$\Gamma\vdash_{\\#}S<:T$ denotes tight subtyping, a notion inherited from pDOT
(see Appendix B). Tight typing and inertness forbid the derivation of
subtyping relations from type member bounds. They can rule out absurd
subtyping relations, such as
$\left\\{a\colon\forall(x:S)T\right\\}<:\left\\{a\colon\bot\right\\}$, which
cannot be inverted.

The major obstacle when proving subtyping inversion is Trans. For instance, if
we try to invert the tight subtyping relation
$\Gamma\vdash_{\\#}\left\\{a\colon S\right\\}<:\left\\{a\colon T\right\\}$ to
get $\Gamma\vdash_{\\#}S<:T$ by induction on its derivation, we become stuck
at the Trans case. There, we have $\Gamma\vdash_{\\#}\left\\{a\colon
S\right\\}<:U$ and $\Gamma\vdash_{\\#}U<:\left\\{a\colon T\right\\}$ as
premises and the inductive hypothesis is not applicable since the shape of $U$
is unknown.

To tackle this problem, we add invertible subtyping as an additional layer
(see Figure 7). In this layer, we remove Trans and instead inline it in the
path replacement and type member subtyping rules. We have four rules for path
replacement in invertible subtyping, compared to two in general and tight
subtyping. This is because general subtyping relies on transitivity to replace
aliasing paths on the left hand side. If $\Gamma\vdash_{\\#}S<:T$ and $p$
aliases $q$, to derive
$\Gamma\vdash_{\\#}{S}\left[\nicefrac{{q}}{{{p}}}\right]<:T$ we first need to
derive $\Gamma\vdash_{\\#}{S}\left[\nicefrac{{q}}{{{p}}}\right]<:S$ by
Snglqp-<:# and then derive
$\Gamma\vdash_{\\#}{S}\left[\nicefrac{{q}}{{{p}}}\right]<:T$ by Trans.

Invertible subtyping can easily be inverted and inductively reasoned about.
Similarly to typing, we prove that tight subtyping can be transformed to
invertible subtyping.

###### Lemma 4.4 ($<:_{\\#}$ to $<:_{\\#\\#}$).

If $\Gamma$ is an inert typing environment and $\Gamma\vdash_{\\#}S<:T$, then
$\Gamma\vdash_{\\#\\#}S<:T$.

And it is easy to prove that we can transform invertible subtyping to tight
subtyping.

###### Lemma 4.5 ($<:_{\\#\\#}$ to $<:_{\\#}$).

For any environment $\Gamma$, if $\Gamma\vdash_{\\#\\#}S<:T$ then
$\Gamma\vdash_{\\#}S<:T$

###### Lemma 4.6 (Field Inversion in $<:_{\\#\\#}$).

If $\Gamma\vdash_{\\#\\#}\left\\{a\colon S\right\\}<:\left\\{a\colon
T\right\\}$, then $\Gamma\vdash_{\\#\\#}S<:T$.

_Proof sketch._ We can prove the theorem by induction on the derivation of the
judgment. The Refl## and Fld-<:-Fld## cases are trivial. In the first case we
get $S=T$. The goal can be proven by applying the reflexivity rule. In the
second case the goal is already proven. The other four cases from path
replacement can be proven with the inductive hypothesis and the typing rules.

##  5\. Translating Constraint-Based GADTs into cDOT

In this section, we demonstrate the expressiveness of subtyping reconstruction
by proving that it subsumes generalised algebraic data types (GADTs).

###  5.1. Introducing GADTs

Algebraic Data Types (ADTs) are a feature of ML-like languages which allow
representing data types that can be created with a set of _constructors_ known
in advance. They are similar to class hierarchies one level deep, like Expr
from Figure 1; ADT constructors correspond to subclasses of Expr. However,
every constructor of a polymorphic ADT must have the exact same type
parameters as the ADT itself. To correspond to an ADT, each subclass of
Expr<A> would need to be generic in A and would need to extend Expr<A>, a
restriction which is violated by IntLit. GADTs lift this restriction: GADT
constructors may have arbitrary type parameters, and may apply the GADT type
constructor to arbitrary types. In particular, Expr<A> can be faithfully
represented as a GADT.

Xi et al. studied GADTs in the ML setting and presents the GADT calculus
$\lambda_{2,G\mu}$. Given an appropriate definition of Expr, we can express
the eval example in $\lambda_{2,G\mu}$ as follows:

$\displaystyle\mathrm{eval}$
$\displaystyle:\mathrm{Expr}\,\alpha\rightarrow\mathrm{Int}$
$\displaystyle\mathrm{eval}$ $\displaystyle=\Lambda\,\alpha.\,\lambda
x:\mathrm{Expr}\,\alpha.\,\operatorname{\mathbf{case}}x\operatorname{\mathbf{of}}\mathrm{IntLit}(i)=>i\;|\;\dots$

To support GADTs, the typing judgment in $\lambda_{2,G\mu}$ keeps track of a
constraint $\Delta$; the judgment itself has the form $\Delta;\Pi|-t:\tau$,
where $\Pi$ stands for a typing context in $\lambda_{2,G\mu}$.111111 Xi et al.
used $\Gamma$ for their environments as expected. We use $\Pi$ instead, to
avoid reusing the $\Gamma$ metavariable. Pattern matching on GADTs extends
$\Delta$ with additional information. As long as the constraint entails
equivalence between some types (denoted as
$\Delta\vDash\tau_{1}\equiv\tau_{2}$), they are interchangeable to the typing
judgment. For instance, in the above $\mathrm{eval}$ example, the constraint
$\Delta$ used to type the $\mathrm{IntLit}$ branch would contain
$\alpha\equiv\mathrm{Int}$, which we could use to type $i$ as $\alpha$ instead
of $\mathrm{Int}$. The entailment relationship in $\lambda_{2,G\mu}$ is based
on substitution: we have $\Delta\vDash\tau_{1}\equiv\tau_{2}$ if for any
$\theta$ that solves $\Delta$, we also have
$\theta\tau_{1}\equiv\theta\tau_{2}$. To illustrate, given
$\mathrm{List}\,\alpha\equiv\mathrm{List}\,\mathrm{Int}\in\Delta$, we would
also have $\Delta\vDash\alpha\equiv Int$.

Our notion of subtyping reconstruction subsumes GADTs from $\lambda_{2,G\mu}$:
it supports subtyping and class hierarchies of arbitrary depth. cDOT does not
need an additional context $\Delta$, since its bindings can introduce
subtyping assumptions which later can be inverted (Section 4.2). In order to
make this claim precise and validate it, we show an encoding of a variant of
$\lambda_{2,G\mu}$ into cDOT.

###  5.2. A Variant of $\lambda_{2,G\mu}$

We have adjusted $\lambda_{2,G\mu}$ by removing those features which are not
relevant for the purpose of demonstrating that cDOT can encode GADTs. In order
of significance, the changes are:

#### Adjusted constraint reasoning.

Besides the constraint-based entailment, $\lambda_{2,G\mu}$ also features an
equivalent relation $\Delta|-\tau_{1}\equiv\tau_{2}$ defined syntactically (Xi
et al., 2003, Fig. 7). Our variant of $\lambda_{2,G\mu}$ uses a restricted
version of this relation, which we denote as $|-^{\prime}$. Our changes are
limited to removing rules that allow ex-falso reasoning, as well as reasoning
about function and universal types. We give the exact rules in the appendix.

Ex-falso rules allow deriving arbitrary type equivalences from a contradictory
constraint. Branches which introduce contradictory constraints would never be
entered at runtime, since they correspond to patterns that cannot match. Such
cases could in principle be handled while preserving their semantics by
replacing the branch bodies with a loop, for instance. We excluded these
rules, as programming languages that support GADTs (for instance OCaml,
Haskell, Agda) typically do not allow typing arbitrary code if a branch cannot
be entered.

Similarly, we have excluded the rules that allow reasoning based on equality
of function and universal types. Again, such reasoning is not core to GADTs
and not all implementations of GADTs allow it (for instance, Agda and Idris
don’t invert function types and Haskell does not invert polymorphic types). We
still allow inverting equalities of GADTs and tuples, for example given
$\alpha*\beta\equiv\gamma*\delta\in\Delta$ we can infer
$\Delta|-^{\prime}\alpha\equiv\gamma$.

To show what the rules defining $\vdash^{\prime}$ look like, we present two of
them below. One allows replacing a type with a variable equal to it, another
allows inverting GADT equality.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\alpha\text{ has no free
occurrences in }\tau\\\
\vec{\alpha},\Delta[\alpha\mapsto\tau]\vdash^{\prime}\tau_{1}[\alpha\mapsto\tau]\equiv\tau_{2}[\alpha\mapsto\tau]\end{array}}{\begin{array}[]{@{}c@{}}\vec{\alpha},\tau\equiv\alpha,\Delta\vdash^{\prime}\tau_{1}\equiv\tau_{2}\end{array}}$

$\vec{\alpha},\vec{\tau_{A}}\equiv\vec{\tau_{B}}\vdash^{\prime}\tau_{1}\equiv\tau_{2}$
$\vec{\alpha},(\vec{\tau_{A}})T\equiv(\vec{\tau_{B}})T\vdash^{\prime}\tau_{1}\equiv\tau_{2}$

#### Deterministic reduction.

$\lambda_{2,G\mu}$ reduces $\operatorname{\mathbf{case}}$ forms non-
deterministically if multiple patterns match, which is a strange choice of
evaluation semantics. Handling non-determinism in cDOT would be quite
involved, as we would either need to modify the evaluation rules of pDOT to be
non-deterministic or encode non-determinism. While either choice is an
interesting problem, non-determinism is orthogonal to GADTs and reduction is
deterministic in our variant of $\lambda_{2,G\mu}$.

#### Exhaustive and not-nested patterns.

In contrast to Xi et al., our variant of $\lambda_{2,G\mu}$ disallows nested
patterns and requires $\operatorname{\mathbf{case}}$ forms to match on all
GADT constructors. Nested patterns can be desugared to remove the nesting.
Many languages, like Coq for example (Inria, CNRS and contributors, 2021),
desugar such matches to make compilation into primitive operations easier. See
(Maranget, 2008) for an efficient algorithm converting nested pattern matches
into decision trees.

Original $\lambda_{2,G\mu}$ allowed inexhaustive pattern matches, which were
allowed to get stuck. We instead require patterns to be exhaustive; verifying
this is simple without nested patterns.

###  5.3. Metatheory

In order to validate our variant of $\lambda_{2,G\mu}$, we provide a
mechanised proof of soundness, expressed as standard progress and preservation
theorems. Thanks to the additional exhaustivity requirement we added to
pattern matching, well-typed terms never get stuck: we can prove progress,
which did not hold in the original formulation. The mechanized proof was
originally described by Waśko (2021) and is attached as one of the artifacts
of this paper.

###### Theorem 5.1 (Preservation).

For any well typed term $\Delta;\Pi\vdash e:\tau$, if $e\longrightarrow
e^{\prime}$, then the other term is also well-typed and has the same type:
$\Delta;\Pi\vdash e^{\prime}:\tau$.

###### Theorem 5.2 (Progress).

For any well typed term $\Delta;\Pi\vdash e:\tau$, the term is either a value
or it can be reduced further: there exists a term $e^{\prime}$ such that
$e\longrightarrow e^{\prime}$.

###  5.4. Encoding

To encode $\lambda_{2,G\mu}$ in cDOT, we emulate GADTs using object types
equipped with type members which will serve the purpose of encoding type
parameters and evidence for type equalities together with a visitor function
(analogous to Scott-encoding (Stump, 2009, Sec. 5.2)) which will allow to
emulate exhaustive pattern matching together with refinement of type
equalities. As our encoding does not depend on $\operatorname{\mathbf{case}}$
forms, it remains applicable to other systems in the DOT family which may
potentially support subtyping reconstruction, such as gDOT (Giarrusso et al.,
2020).

We denote an encoding of a term $e$ as $\mathcal{E}(e,\Theta)$ and an encoding
of a type $\tau$ as $\mathcal{T}(\tau,\Theta)$. Both definitions depend on a
substitution $\Theta$ mapping $\lambda_{2,G\mu}$ type names $\alpha$ to type
projections $p.A$ and $\lambda_{2,G\mu}$ variable names $x$ to cDOT
expressions. For example, we may have: $\Theta=[\alpha\mapsto
x_{\alpha}.T,x\mapsto y]$.

In order to encode a complete $\lambda_{2,G\mu}$ program, we define a function
to encode the signature $\Sigma$ and a term lib representing basic primitives
like the unit and tuple types. The signature $\Sigma$ defines what GADTs
definitions a program may use: it maps GADT constructors to their signatures,
for example:
$\Sigma(c_{j})=\forall\vec{\beta_{j}}.\tau_{j}\to(\vec{\sigma_{j}})T$. We show
a full definition in the appendix. Overall, encoding of a $\lambda_{2,G\mu}$
program $e$ under a signature $\Sigma$ is defined as follows:

⬇

EncodeProgram(e, $\Sigma$) =

let lib = ... in let env = EncodeSigma($\Sigma$) in $\mathcal{E}$(e,
$\varnothing$)

Figure 8 shows how we would translate a $\lambda_{2,G\mu}$ version of Expr
from Figure 1 into cDOT.

let $\displaystyle\mathrm{lib}\ =\nu(\mathrm{lib})[\mathrm{lib}.A]\\{$
$\displaystyle A=\top;$
$\displaystyle\mathrm{Expr}=\mu(x:\left\\{X\colon\bot..\top\right\\}\wedge\left\\{\mathrm{pmatch}\colon\forall(r:\left\\{R\colon\bot..\top\right\\})\forall(\mathrm{litIntCase}:\mathrm{lib}.\mathrm{IntLit}\rightarrow{r.R})\,{r.R}\right\\});$
$\displaystyle\mathrm{IntLit}=\mu($ $\displaystyle\quad
x:\left\\{X\colon\mathrm{Int}..\mathrm{Int}\right\\}\wedge\left\\{\mathrm{data}\colon\lambda(\\_)\,x.X\right\\}$
$\displaystyle\quad\quad\wedge\left\\{\mathrm{pmatch}\colon\forall(r:\left\\{R\colon\bot..\top\right\\})\forall(\mathrm{litIntCase}:\mathrm{lib}.\mathrm{IntLit}\rightarrow{r.R})\,{r.R}\right\\}$
$\displaystyle);$
$\displaystyle\mathrm{mkIntLit}\colon\forall(x:\mathrm{Int})\,\mathrm{lib}.\mathrm{IntLit};$
$\displaystyle\mathrm{mkIntLit}=\lambda(x:\mathrm{Int})\nu(y)[\mathrm{lib}.\mathrm{IntLit}]\\{$
$\displaystyle\quad
X=\mathrm{Int};\mathrm{data}:\forall(\\_)\,y.X;\mathrm{data}=\lambda(\\_)\,x;$
$\displaystyle\quad\mathrm{pmatch}\colon{\forall(r:\left\\{R\colon\bot..\top\right\\})\forall(\mathrm{litIntCase}:\mathrm{lib}.\mathrm{IntLit}\rightarrow{r.R})\,{r.R}}$
$\displaystyle\quad\mathrm{pmatch}={\lambda(r:\left\\{R\colon\bot..\top\right\\})\lambda(\mathrm{litIntCase}:\mathrm{lib}.\mathrm{IntLit}\rightarrow{r.R})\
\mathrm{litIntCase}\ {y}}$ $\displaystyle\\};$
$\displaystyle\mathrm{eval}\colon\forall(x:\mathrm{lib}.\mathrm{Expr})\,x.X;$
$\displaystyle\mathrm{eval}=\lambda(x:\mathrm{lib}.\mathrm{Expr})\,{\small\textsf{{let}}}\
y=\lambda(y:\mathrm{lib}.\mathrm{IntLit})\ {y.\mathrm{data}}\
{\small\textsf{{in}}}\ {x.\mathrm{pmatch}\ y}$
$\displaystyle\\!\\!\\!\\!\\!\\!\\!\\!\\!\\}\ {\small\textsf{{in}}}\ \cdots$
Figure 8. Translating Expr from $\lambda_{2,G\mu}$ into cDOT

###  5.5. Typing Preservation

To prove typing preservation, we first define a notion of correspondence
between environments in $\lambda_{2,G\mu}$ and cDOT. We define cDOT type
equality as follows:

###### Definition 5.3 (Type equality in cDOT).

We introduce a shorthand notation $\Gamma\vdash A=:=B$ which just stands for
$\Gamma\vdash A<:B\wedge\Gamma\vdash B<:A$.

Then we formalize that our environment contains definitions of lib and env as
expected by the described encoding.

###### Definition 5.4 (Signature encoding).

For any $\lambda_{2,G\mu}$ signature $\Sigma$ we denote by
$\mathcal{S}(\Sigma)$ the types defined by its cDOT encoded counterpart.
$\mathcal{S}(\Sigma)$ contains two variables:

  * –

$\mathrm{lib}$ which is defined as in the encoding, giving us the builtin
types,

  * –

$\mathrm{env}$ which encodes the signature $\Sigma$: for every
$\Sigma(c_{i})=\forall\vec{\alpha}.\tau_{A}\to\tau_{B}$ we have:

$\displaystyle\mathrm{env}.c_{i}:\forall(ts:\\{B_{i,1}:\bot..\top;\ldots\\})\;\forall(v:\mathcal{T}(\tau_{A},\theta_{\vec{\alpha}}))\;\mathcal{T}(\tau_{B},\theta_{\vec{\alpha}})$
$\displaystyle\qquad\text{where}\;\theta_{\vec{\alpha}}=[\alpha_{1}\mapsto
ts.B_{i,1},\ldots,\alpha_{m}\mapsto ts.B_{i,m}]$

Now we can define a property specifying that all equations from the original
environment $\Delta$ are also analogously emulated in the encoded environment
$\Gamma$.

###### Definition 5.5 (Equational correspondence
$\Psi(\Delta;\Theta;\Gamma)$).

A cDOT environment $\Gamma$ together with a substitution $\Theta$ satisfies
equations of $\Delta$ if the following conditions are met:

  1. (1)

For each $\alpha\in\Delta$, for $\Theta(\alpha)=p.A$, $\Gamma\vdash
p:\\{A:\bot..\top\\}$.

  2. (2)

For each $\tau_{1}\equiv\tau_{2}\in\Delta$,
$\Gamma\vdash\mathcal{T}(\tau_{1},\Theta)=:=\mathcal{T}(\tau_{2},\Theta)$.

  3. (3)

$\Gamma$ contains the bindings lib and env as defined in
$\mathcal{S}(\Sigma)$.

We also introduce a similar notion for data environments: every variable in
the original environment $\Pi$ also has its encoded counterpart, typeable to
the encoded variant of its original type. We gather both notions in a single
property:

###### Definition 5.6 (Environment correspondence
$\Phi(\Delta;\Pi;\Theta;\Gamma)$).

A cDOT environment $\Gamma$ corresponds to $\lambda_{2,G\mu}$ contexts
$\Delta$ and $\Pi$ under a substitution $\Theta$ if
$\Psi(\Delta;\Theta;\Gamma)$ and for each $\mathit{xf}$ such that
$\Pi(\mathit{xf})=\tau$, we have
$\Gamma\vdash\Theta(\mathit{xf}):\mathcal{T}(\tau,\Theta)$.

With all that, we can state the main theorem.

###### Theorem 5.7 (Type Preservation).

For every $\Pi$, $\Delta$, $e$, $\tau$, any $\Theta$ such that
$\mathit{fv}(e)\cup\mathit{fv}(\tau)\subseteq\mathit{dom}(\Theta)$, any
$\Gamma$ such that $\Phi(\Delta;\Pi;\Theta;\Gamma)$, we have
$\Gamma\vdash\mathcal{E}(e,\Theta):\mathcal{T}(\tau,\Theta)$.

Based on this theorem and correctness of the env and lib encodings (shown in
the appendix), we can prove that for any well-typed $\lambda_{2,G\mu}$
program, the result of EncodeProgram is also a well-typed program in cDOT.

Apart from other more technical lemmas, an important lemma that we are using
in the proof is one that specifies that under our modified notion of
constraint reasoning, if an equation is derivable using this reasoning, then
an analogous equation is also derivable in cDOT starting from analogous
assumptions:

###### Lemma 5.8 (Equation emulation).

For any $\Delta\vdash^{\prime}\tau_{1}\equiv\tau_{2}$ and any $\Theta$ and
$\Gamma$, if $\Psi(\Delta;\Theta;\Gamma)$, then
$\Gamma\vdash\mathcal{T}(\tau_{1},\Theta)=:=\mathcal{T}(\tau_{2},\Theta)$.

###  5.6. Preservation of Operational Semantics

We conjecture that our encoding preserves the operational semantics of
$\lambda_{2,G\mu}$ in the sense that if $e$, a $\lambda_{2,G\mu}$ term,
reduces to some $e^{\prime}$, then $\mathrm{Enc}(e)-->^{*}t^{\prime}$ such
that $\mathrm{Enc}(e^{\prime})$ corresponds to $t^{\prime}$. This is
illustrated by the following diagram, where $\eqsim$ is an equivalence
relation described below:

${e}$${e^{\prime}}$${\mathrm{Enc}(e)}$${t^{\prime}\eqsim\mathrm{Enc}(e^{\prime})}$$\scriptstyle{Enc}$$\vphantom{\to}{}^{*}$$\scriptstyle{Enc}$$\vphantom{\to}{}^{*}$

The main technicality which would be involved in the proof of the above
property is that reduction in $\lambda_{2,G\mu}$ relies on substitution as
opposed a store like cDOT. We envision the gap between the two can be bridged
by defining an equivalence relation $t\eqsim s$ on cDOT terms. Two terms
should be considered equivalent if they are the same modulo
$\alpha$-equivalence as well as order of let- and store-bindings and presence
of unused bindings. In particular, this equivalence makes it possible to deal
with the fact that reduction in $\lambda_{2,G\mu}$ inherently may duplicate a
value, while reduction in cDOT only duplicates references to a store-binding.

Aside from this problem, the proof should be rather straightforward: most
forms from $\lambda_{2,G\mu}$ are translated to their direct cDOT equivalents,
and our encodings of type abstraction and tuples are standard (Amin et al.,
2016). The most involved case of the proof will be correctness of the pattern
matching translation, which relies on encoding $\operatorname{\mathbf{case}}$
forms into calls to $\mathrm{pmatch}$ like in Scott encoding (Stump, 2009,
Sec. 5.2). In particular, the proof will have to demonstrate that replacing
contradictory branches by infinite loops in the encoded term preserves the
operational semantics; intuitively, this is because a contradictory branch
cannot be entered, which is precisely why $\lambda_{2,G\mu}$ allows typing any
term as any type in such branches in the first place.

##  6\. Implementing Subtyping Reconstruction

How can we implement subtyping reconstruction? We begin by inspecting the
basic problem with writing an algorithm that can use subtyping relationships
reconstructed by pattern matching.

###  6.1. Towards Formal Decidable Subtyping

Recall that cDOT term variables can introduce subtyping assumptions to the
context (see _subtyping inversion_ in Section 4.2). As a concrete example,
consider
$\Gamma=x:\left\\{A\colon\bot..\top\right\\},y:\left\\{B\colon\bot..\top\right\\},z:\left\\{C\colon
x.A..y.B\right\\}$. We can derive $\Gamma|-x.A<:y.B$ thanks to the bounds of
$z.C$.

The question is how to design an algorithmic subtyping judgment which is a
subset of the declarative subtyping rules from Figure 4. More specifically,
how do we decide what subtyping assumptions are introduced by bindings and
when to use the inversion rules? Kennedy and Russo (2005) show C♯ minor, a
formalisation of C♯ which allows pattern matching much like cDOT. The
declarative subtyping judgment in C♯ minor has the form $\Delta|-S<:T$, where
$\Delta$ is a list of subtyping assumptions. This judgment features inversion
rules which allow recovering the premises of assumptions, again much like
cDOT. In their system, a branch of a pattern match may introduce subtyping
assumptions; specifically, if $Q$ is the type of the value being matched and
$P$ is the type of values matched by the pattern, then the subtyping
assumptions introduced by the branch can be found by finding a class $K$ such
that $Q<:K[\overline{T}]$ and $P<:K[\overline{S}]$, and then relating $S_{i}$
to $T_{i}$ based on type parameter variance. Conceptually, the problem is much
simpler in cDOT: the assumptions introduced by a binding can be found by
simply listing all of its type members and then relating each member’s upper
and lower bounds. cDOT also clearly points to the reason we can relate $S_{i}$
to $T_{i}$; if the branch is entered, we have a value $v$ which can be typed
as both $Q$ and $P$, and this value’s type member (representing the _most
precise_ type argument to $K$) is related to both $S_{i}$ and $T_{i}$.

This leaves the question of deciding when to use the inversion rules. Emir et
al. (2006) solve the problem for C♯ minor: they show an algorithmic subtyping
judgment $\Psi|-S<:T$, with $\Psi$ being a list of _upper and lower bounds_ on
type variables of the form $X<:T$ and $T<:X$. This judgment no longer needs
inversion rules: the assumptions in $\Psi$ are as simple as possible and
cannot be inverted. $\Delta$ and $\Psi$ are related: any subtyping assumption
$S<:T$ can be _decomposed_ into bounds by repeatedly applying appropriate
inversion rules; we denote the result of doing so as $\mathrm{Dec}(S<:T)$. Any
$\Delta$ can be converted to an equivalent $\Psi$ by first decomposing
assumptions in $\Delta$ and then repeatedly simplifying the assumptions
transitively introduced by the bounds, i.e. by reaching a fixpoint of the
following sequence:

$\displaystyle\Psi_{1}$
$\displaystyle=\bigcup\left\\{\mathrm{Dec}(S<:T):S<:T\in\Delta\right\\}$
$\displaystyle\Psi_{i+1}$
$\displaystyle=\bigcup\left\\{\mathrm{Dec}(S<:T):\\{S<:X,X<:T\\}\subset\Psi_{i}\right\\}\cup\Psi_{i}$

The algorithmic and declarative subtyping judgments are equivalent; subtyping
in C♯ minor is decidable only if we restrict contravariant classes (Kennedy
and Pierce, 2007).

Intuitively, we should be able to define an algorithmic subtyping judgment for
cDOT with a similar approach, though we leave the details of this process to
future work. This hypothetical subtyping would have the form
$\Gamma;\hat{\Psi}|-S<:T$, with $\hat{\Psi}$ being a list of upper and lower
bounds on _abstract types_ $\hat{A}$: type projections $p.A$ and singleton
types $p\mathsf{.type}$. However, cDOT features intersection types and
dependent function types (both absent from C♯ minor), which make the problem
more complex. For instance, it is not possible in general to decompose
$\hat{A}\land\hat{B}<:T$ into bounds. These difficulties would be encountered
when implementing subtyping reconstruction for any sufficiently advanced type
system, such as the one in Scala or TypeScript. Still, it is possible to have
an algorithm which gives an incomplete approximation of the declarative
subtyping. For the particular case of cDOT as presented, we are unlikely do
better. We can encode System $F_{<:}$ in cDOT (Amin et al., 2014), making it
likely that cDOT subtyping is undecidable (Hu and Lhoták, 2019).

###  6.2. Outline of the Scala Implementation

The first author of this paper was at the center of the effort to implement
subtyping reconstruction for Scala 3. Based on this experience, we outline key
aspects of the implementation and relate them to the formalism developed in
the present paper.

The sketch from the previous section gives us the two basic problems the
implementation needs to solve: finding subtyping assumptions introduced by
patterns, and decomposing them into bounds so that they can be used for type
checking. In the implementation, the abstract types $\hat{A}$ for which bounds
can be reconstructed include type projections $p.A$ and singleton types
$p\mathsf{.type}$, as well as type parameters and pattern-bound types,121212
In Scala, types starting with a lower-case letter mentioned in a pattern are
_bound_ by the pattern, c.f. Section 2.2.  both denoted as $X$. As the
assumptions following from a pattern are decomposed into bounds, we store the
latter in a map from abstract types to pairs of types: upper and lower bounds
of the abstract types.131313 The particular data structures of the Scala
implementation were described by Xu et al. (2021).  This map will later be
used for type checking the branch associated with the pattern, making it part
of the context used to type check Scala code. Before we describe how we find
assumptions and decompose them, we should note that the implementation can be
incomplete: it is always sound to reconstruct less precise bounds than the
ones permitted by the formalism. Being able to do so is helpful when dealing
with a language with a complex type system. The Scala implementation at first
only supported reconstructing bounds on function type parameters and finding
assumptions following from class141414 When discussing Scala, we follow
Martres (2022b) and say “class” to mean either a _proper_ class or a trait.
types; it was then progressively expanded to support bounds on class type
parameters, type projections and singleton types, as well as assumptions
following from structural, intersection and union types.151515The support for
type projections, singleton types, and structural types is currently under
review and not yet merged.

We now inspect the two problems in a simplified setting. The bounds are
reconstructed based on the _scrutinee_ type $Q$, i.e. the type of the value
being matched, and the _pattern_ type $P$, i.e. the type of values matched by
the pattern. We initially disregard Scala’s variant refinement, as well as
intersection, union, and higher-kinded types. We only consider two forms of
pattern types: either $P=K$, where $K$ is a class, or $P=K[\overline{X}]$,
where $\overline{X}$ are all pattern-bound types, i.e. fresh abstract types.
To illustrate, only the first two patterns in the following example would be
allowed:

⬇

def eval[T](expr: Expr[T]): T = expr match

case e : IntLit => e.value

case e : First[b,c] => eval[b](e.pair)._1

case e : Second[Int,c] => // pattern type disallowed

Observe how _naming_ type arguments in the above example mirrors how in cDOT
we need to use type projections $x.A$ to reference type arguments of a pattern
type representing a generic class. To illustrate, we show a cDOT term that
formally models the two first cases (assuming a simple generalisation of
$\operatorname{\mathbf{case}}$ forms). In particular, note how we reference
the type argument of the encoded version of First:

$\displaystyle\mathrm{eval}=\lambda(\mathrm{tl}\colon\left\\{T\colon\bot..\top\right\\})\,\,\lambda(\mathrm{expr}\colon
g.\mathrm{Expr}\land\\{A:\mathrm{tl}.T..\mathrm{tl}.T\\})\,$
$\displaystyle\quad\quad\quad\operatorname{\mathbf{case}}\mathrm{expr}\begin{aligned}
&\operatorname{\mathbf{of}}e:g.\mathrm{IntLit}=>e.\mathrm{value}\\\
&\;\,|\;\,e:g.\mathrm{First}=>\mathrm{eval}(\nu(s){\left\\{T={e.B}\right\\}})(e.\mathrm{pair}).\mathrm{\\_1}\end{aligned}$

Essentially, there are three procedures involved in reconstructing bounds.
First, ASSUM(Q,P) lists subtyping assumptions following a value of type $Q$
being also of type $P$. Second, DEC(S <: T) decomposes an assumption into a
list of bounds. Third, BOUNDS(Q,P) = ASSUM(Q,P).map(DEC) reconstructs _bounds_
following from $Q$ and $P$. These definitions should be understood as
pseudocode rather than the precise implementation.

To find subtyping assumptions based on scrutinee and pattern types $Q$ and
$P$, we look for classes $K$ such that $Q<:K[\overline{T}]$ and
$P<:K[\overline{S}]$; such classes can be found by walking the inheritance
hierarchy and in general there might be more than one such class. The
relationships between the type arguments of each such $K$ are what we are
looking for: if the $i$-th parameter of C is covariant or invariant, we must
have $S_{i}<:T_{i}$, and likewise for contravariance. For instance, if
$Q=\mathrm{Expr}[X]$ and $P=\mathrm{IntLit}$, we have $Q<:\mathrm{Expr}[X]$
and $P<:\mathrm{Expr}[\mathrm{Int}]$ and we return
$\mathrm{Int}<:X,X<:\mathrm{Int}$.

Then, each assumption we find is decomposed into bounds and stored in the
aforementioned map. Decomposing an assumption $S<:T$ is implemented similarly
to checking if $S$ is a subtype of $T$. The main difference is that if we
encounter a (sub)goal of the form $\hat{A}<:T$ or $T<:\hat{A}$ which cannot be
concluded based on current bounds, we add the relationship to the map of
reconstructed bounds. For instance, when decomposing
$\mathrm{List}[X]<:\mathrm{List}[\mathrm{Int}]$, we encounter the subgoal
$X<:\mathrm{Int}$ and store the relationship. Much like in the formal sketch,
adding a new bound may result in new transitive subtyping assumptions: as a
simple example, if we extend $\mathrm{List}[X]<:Y$ with
$Y<:\mathrm{List}[\mathrm{Int}]$, it now follows that
$\mathrm{List}[X]<:\mathrm{List}[\mathrm{Int}]$. To handle such cases, we
first decompose these transitive assumptions and then return to decomposing
the original assumption $S<:T$.

What we described so far is very close to the algorithm sketched by Kennedy
and Russo (2005) and presented there more formally. We will now briefly sketch
how we support more complex type system features. The implementation supports
pattern types containing subelements of the form $K[\overline{T}]$ (generic
classes applied to arbitrary types, not only pattern-bound fresh abstract
types) by behaving as though all type arguments were fresh abstract types,
then checking if the concrete arguments conform to the bounds of the
corresponding abstract type. Due to higher-kinded types (HKTs), we need to
consider the _injectivity_ of type operators when decomposing assumptions.
Specifically, if we encounter a (sub)goal of the form $F[\overline{S}]<:T$ or
$S<:F[\overline{T}]$, we proceed only if $F$ is an alias of a class type, and
therefore is known to be injective. This correctly handles situations where
one can conclude that $F[\overline{S}]<:F[\overline{T}]$ with $\overline{S}$
and $\overline{T}$ being unrelated, for instance when we define type F[X] =
Int. While we could support annotating abstract types with their injectivity
(Stolarek et al., 2015), so far we did not find the complexity that this would
introduce worth the corresponding gains. Scala’s variant inheritance161616
Recall that in Scala, only final and case classes invariantly inherit from
their parents (see Section 2.3).  forces adjustments to listing subtyping
assumptions ASSUM(Q,P). If $P$ is an (applied) class type using variant
inheritance and $Q<:K[\overline{T}]$ as well as $P<:K[\overline{S}]$, we only
take the relationships between invariant type arguments as assumptions. The
support for intersection and union types is the most complex extension and
relies on seeing reconstructed bounds $\hat{\Psi}$ as _constraints_ on
abstract types; we unfortunately lack the space for an appropriately detailed
description.171717 The most important aspect is that we need to consider
constraint _disjunctions_ (see, for instance, Petrucciani (2019)) in
ASSUM(Q,P) when either type is a union type and in DEC(S <: T) when $S$ is an
intersection type or $T$ is a union type. Since calculating exact disjunctions
is too costly, we approximate them such that the exact constraint entails the
approximation.

While developing the implementation, we always used a translation from class
types into structural types as a guide for what bounds to reconstruct.
Contrary to expectations, correctly handling various features of Scala’s type
system required quite sophisticated notions. Based on our findings, we believe
that the complexity of the implementation may be reduced if we instead based
it directly on cDOT concepts. While we leave developing this alternative
implementation as future work, we envision it as follows. To find subtyping
assumptions based on pattern and scrutinee types $P,Q$, we would first
translate them to structural types $\widetilde{P},\widetilde{Q}$ and then
return the relationships between upper and lower bounds of the type members of
$\widetilde{P}\land\widetilde{Q}$. For example, Expr[X] and IntLit would be
translated to { type A = X } and { type A = Int } and we would return Int $<:$
X, X $<:$ Int, like the current implementation. Likewise, to decompose an
assumption $S<:T$ into bounds, we would first translate $S$ and $T$ into
structural types $\widetilde{S},\widetilde{T}$ and then decompose
$\widetilde{S}<:\widetilde{T}$ into bounds according to cDOT inversion rules.
For example, to decompose List[X] $<:$ List[Int], we would translate it to {
type A <: X } $<:$ { type A <: Int }, which can be inverted into X $<:$ Int.
We believe that this algorithm would at least match the precision of the
current implementation, would require less special cases and would potentially
naturally extend to intersections and unions without resolving to constraint-
like reasoning. To illustrate, consider that the current implementation needs
special reasoning to handle a covariant Expr and IntLit using invariant
refinement, while the alternative implementation would simply translate Expr
to { type A $<:$ X } and IntLit to { type A = Int }.

##  7\. Related Work

The earliest implementation of pattern matching based on runtime subtype
checks we are aware of is that of Modula-3 (Böszörményi and Weich, 2012) with
its TYPECASE statements,181818
https://www.cs.purdue.edu/homes/hosking/m3/reference/typecase.html allowing
type-safe conditional refinement based on the runtime type of a scrutinee.

Subtyping in DOT systems is believed to be undecidable, as we can encode
$F_{<:}$ bounded polymorphism in DOT. Hu and Lhoták (2019) show that this
reasoning does not constitute a proof and demonstrate $D_{<:}$, an undecidable
fragment of DOT without self-references and intersection types. $D_{<:}$
subtyping itself has two fragments which have subtyping algorithms. However,
undecidability of cDOT subtyping is unlikely to be a problem in practice.
Specific class hierarchies (allowed in Scala) on their own make subtyping
undecidable (Kennedy and Pierce, 2007). Similarly, Java generics are also
Turing-complete, as one can reduce a Turing machine to a fragment of Java
(Grigore, 2017).

Parreaux et al. (2019) describe that DOT type members can be used to encode
GADTs. They observe that doing so solves the soundness problem of variant
inheritance (Giarrusso, 2013).

GADTs are well-known and widely implemented (Peyton Jones et al., 2006). Xi et
al. (2003) may have been the first to study them in an ML-like setting with
$\lambda_{2,G\mu}$. The original OCaml GADT implementation was based on a
type-and-constraint system like $\lambda_{2,G\mu}$ (Garrigue and Normand,
2011). Sulzmann et al. (2007) present System FC, an intermediate
representation in the Haskell compiler which supports GADTs (and other
features) with type equality witnesses and coercions (Mitchell, 1984). They
report that the Haskell implementation was previously based on a type-and-
constraint system as well and they show how to encode that system into System
FC. In System FC the $\mathrm{IntLit}$ constructor of $\mathrm{Expr}\,\alpha$
contains a witness $\mathsf{co}:\mathrm{\alpha\sim\mathrm{Int}}$. Pattern
matching on $\mathrm{Expr}\,\alpha$ binds this witness, which then can be used
to type $0$ as $\mathrm{Int}$ with an explicit coercion:
$0\blacktriangleright\mathrm{sym}\,\mathsf{co}$. Sulzmann et al. claim that
explicit casts make System FC code more robust to transformations by ensuring
that they do not violate witness scoping. cDOT objects also act like witnesses
of subtyping assumptions, but they only participate implicitly in subtyping.
It would be interesting to see a variant of cDOT where objects participate in
subtyping through explicit coercions, like System FC witnesses.

Scherer and Rémy (2013) study the combination of GADTs and variance in the
OCaml setting. They demonstrate that associating the constructors of a GADT
such as Expr with type equality constraints prevents the GADT from being
covariant. The problem does not arise in our setting, where constructors are,
essentially, associated with subtyping constraints.

GADTs present a unique challenge for checking pattern exhaustivity: based on a
value’s type, we can rule out that it was created using particular
constructors. For instance, a value of type Expr<Int> cannot be an instance of
MkPair. Without special support for GADTs, checking pattern exhaustivity emits
spurious inexhaustivity warnings, for instance that a pattern for MkPair is
missing when matching on an Expr<Int>. Karachalias et al. (2015) show a GADT-
aware algorithm implemented in GHC, the Haskell compiler. Boruch-Gruszecki
(2017) builds on their work to propose an analogous algorithm for Scala.

Recently, Martres (2022a)191919 As of August 2022, the cited thesis is not yet
public. A technical report containing parts of the thesis is available
(Martres, 2022b). A draft may be accessible at
http://guillaume.martres.me/thesis.pdf.  has shown a complete version of the
class encoding we sketched in Section 3. In order to preserve subtyping
relationships in the general case, this encoding relies on subtyping between
recursive types using rules from an understudied branch of the DOT family
(Rompf and Amin, 2016). Such rules are unnecessary to encode specific class
hierarchies (like in our sketch); Martres conjectures that not relying on them
in general is possible if encoding a class type accounts for generic classes
it extends. For instance, an applied type like MkPair[T1,T2] would be encoded
as
$g.\mathrm{MkPair}\land\left\\{B<:\widetilde{T_{1}};\;C<:\widetilde{T_{2}};\;A<:\widetilde{(T_{1},T_{2})}\right\\}$,
where $\widetilde{T}$ is the encoded version of $T$.

Intensional type analysis allows performing runtime type analysis on values.
Harper and Morrisett (1995) develop $\lambda^{\mathrm{ML}}_{i}$ to allow
efficient universal representations of values in polymorphic contexts. Their
calculus was later generalised by Trifonov et al. (2000), arriving at a _fully
reflexive_ version: one that can analyse the runtime type of any value. cDOT
supports a limited version of runtime type analysis with its tagged objects
and $\operatorname{\mathbf{case}}$ forms. Unlike true intensional type
analysis, we cannot analyze arbitrary runtime type representations, but on the
other hand our system admits efficient implementation strategies (like the
runtime-class-based design it formalizes).

Bindings in DOT calculi, including cDOT, can introduce subtyping assumptions.
This was noticed early in the study of DOT systems, as it leads to the crucial
_bad bounds_ problem (Rompf and Amin, 2016; Amin et al., 2014). Hu and Lhoták
(2019) frame this idea as _subtyping reflection_ : the notion that the context
may contain evidence of subtyping, which can be _reflected_ into the subtyping
judgment. This name hints at the analogy to _equality reflection_ from
extensional type theories,202020See, for instance, Nordström et al. (1990).
where the context can contain evidence of equality which can be reflected into
the typing judgment.

## References

  * (1)
  * Amin et al. (2016) Nada Amin, Samuel Grü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_. Springer, 249–272.
  * Amin et al. (2014) Nada Amin, Tiark Rompf, and Martin Odersky. 2014.  Foundations of Path-Dependent Types.  _ACM SIGPLAN Notices_ 49, 10 (Oct. 2014), 233–249.  https://doi.org/10.1145/2714064.2660216
  * Boruch-Gruszecki (2017) Aleksander Boruch-Gruszecki. 2017\.  _Verifying the totality of pattern matching in Scala_.  Master’s thesis. Wrocław University of Science and Technology.
  * Böszörményi and Weich (2012) László Böszörményi and Carsten Weich. 2012.  _Programming in Modula-3: an introduction in programming with style_.  Springer Science & Business Media.
  * Bracha et al. (1998) Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. 1998.  Making the Future Safe for the Past: Adding Genericity to the Java Programming Language. In _Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications_ (Vancouver, British Columbia, Canada) _(OOPSLA ’98)_. Association for Computing Machinery, New York, NY, USA, 183–200.  https://doi.org/10.1145/286936.286957
  * Canning et al. (1989) Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John C Mitchell. 1989.  F-bounded polymorphism for object-oriented programming. In _Proceedings of the fourth international conference on functional programming languages and computer architecture_. 273–280.
  * Cardelli and Wegner (1985) Luca Cardelli and Peter Wegner. 1985.  On Understanding Types, Data Abstraction, and Polymorphism.  _ACM Comput. Surv._ 17, 4 (dec 1985), 471–523.  https://doi.org/10.1145/6041.6042
  * Eisenberg (2020) Richard A. Eisenberg. 2020\.  Stitch: The Sound Type-Indexed Type Checker (Functional Pearl). In _Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell_ _(Haskell 2020)_. Association for Computing Machinery, New York, NY, USA, 39–53.  https://doi.org/10.1145/3406088.3409015
  * Emir et al. (2006) Burak Emir, Andrew Kennedy, Claudio Russo, and Dachuan Yu. 2006.  Variance and Generalized Constraints for C♯ Generics. In _ECOOP 2006 – Object-Oriented Programming_ , Dave Thomas (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 279–303.
  * Emir et al. (2007) Burak Emir, Martin Odersky, and John Williams. 2007\.  Matching Objects with Patterns. In _ECOOP 2007 – Object-Oriented Programming_ , Erik Ernst (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 273–298.
  * Garrigue and Normand (2011) Jacques Garrigue and J. L. Normand. 2011.  Adding GADTs to OCaml: The Direct Approach. In _Workshop on ML_.
  * Giarrusso (2013) Paolo G. Giarrusso. 2013\.  Open GADTs and Declaration-site Variance: A Problem Statement. In _Proceedings of the 4th Workshop on Scala_ _(SCALA ’13)_. ACM, New York, NY, USA, 5:1–5:4.  https://doi.org/10.1145/2489837.2489842
  * Giarrusso et al. (2020) Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers. 2020\.  Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris.  _Proceedings of the ACM on Programming Languages_ 4, ICFP (Aug. 2020), 114:1–114:29.  https://doi.org/10.1145/3408996
  * Grigore (2017) Radu Grigore. 2017\.  Java Generics Are Turing Complete.  _ACM SIGPLAN Notices_ 52, 1 (Jan. 2017), 73–85.  https://doi.org/10.1145/3093333.3009871
  * Harper and Morrisett (1995) Robert Harper and Greg Morrisett. 1995.  Compiling Polymorphism Using Intensional Type Analysis. In _Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’95)_. Association for Computing Machinery, New York, NY, USA, 130–141.  https://doi.org/10.1145/199448.199475
  * Hu and Lhoták (2019) Jason Z. S. Hu and Ondřej Lhoták. 2019.  Undecidability of D<: And Its Decidable Fragments.  _Proc. ACM Program. Lang._ 4, POPL, Article 9 (Dec. 2019), 30 pages.  https://doi.org/10.1145/3371077
  * Inria, CNRS and contributors (2021) Inria, CNRS and contributors. 2021\.  _Extended pattern matching — Coq 8.13.2 documentation_.  https://coq.inria.fr/distrib/V8.13.2/refman/language/extensions/match.html#nested-patterns
  * Karachalias et al. (2015) Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, and Simon Peyton Jones. 2015.  GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness. In _Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming_ _(ICFP 2015)_. Association for Computing Machinery, New York, NY, USA, 424–436.  https://doi.org/10.1145/2784731.2784748
  * Kennedy and Pierce (2007) Andrew Kennedy and Benjamin C. Pierce. 2007.  On Decidability of Nominal Subtyping with Variance. In _International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL/WOOD)_.
  * Kennedy and Russo (2005) Andrew Kennedy and Claudio V. Russo. 2005.  Generalized Algebraic Data Types and Object-Oriented Programming. In _Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications_ (San Diego, CA, USA) _(OOPSLA ’05)_. Association for Computing Machinery, New York, NY, USA, 21–40.  https://doi.org/10.1145/1094811.1094814
  * Maranget (2008) Luc Maranget. 2008\.  Compiling Pattern Matching to Good Decision Trees. In _Proceedings of the 2008 ACM SIGPLAN Workshop on ML_ (Victoria, BC, Canada) _(ML ’08)_. ACM, New York, NY, USA, 35–46.  https://doi.org/10.1145/1411304.1411311
  * Martres (2022a) Guillaume Martres. 2022a.  _Type-Preserving Compilation of Class-Based Languages_.  Ph. D. Dissertation. EPFL, Lausanne.
  * Martres (2022b) Guillaume Martres. 2022b.  _Type-Preserving Compilation of FGJ into DOT_.  Technical Report.  https://infoscience.epfl.ch/record/293463?&ln=en
  * Mitchell (1984) John C. Mitchell. 1984\.  Coercion and Type Inference. In _Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages_ _(POPL ’84)_. Association for Computing Machinery, New York, NY, USA, 175–185.  https://doi.org/10.1145/800017.800529
  * Nordström et al. (1990) Bengt Nordström, Kent Petersson, and Jan M. Smith. 1990\.  _Programming in Martin-Löf’s Type Theory_. Vol. 200.  Oxford University Press Oxford.
  * Parnin et al. (2013) Chris Parnin, Christian Bird, and Emerson Murphy-Hill. 2013\.  Adoption and use of Java generics.  _Empirical Software Engineering_ 18, 6 (2013), 1047–1089.
  * Parreaux et al. (2019) Lionel Parreaux, Aleksander Boruch-Gruszecki, and Paolo G. Giarrusso. 2019.  Towards Improved GADT Reasoning in Scala. In _Proceedings of the Tenth ACM SIGPLAN Symposium on Scala_ _(Scala ’19)_. Association for Computing Machinery, New York, NY, USA, 12–16.  https://doi.org/10.1145/3337932.3338813
  * Parreaux (2020) Lionel Emile Vincent Parreaux. 2020\.  _Type-Safe Metaprogramming and Compilation Techniques For Designing Efficient Systems in High-Level Languages_.  Ph. D. Dissertation. EPFL, Lausanne.  https://doi.org/10.5075/epfl-thesis-10285
  * Petrucciani (2019) Tommaso Petrucciani. 2019\.  _Polymorphic Set-Theoretic Types for Functional Languages_.  Ph. D. Dissertation. Università di Genova ; Université Sorbonne Paris Cité – Université Paris Diderot.
  * Peyton Jones et al. (2006) Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. 2006.  Simple Unification-based Type Inference for GADTs. In _Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming_ _(ICFP ’06)_. ACM, New York, NY, USA, 50–61.  https://doi.org/10.1145/1159803.1159811
  * Rapoport et al. (2017) Marianna Rapoport, Ifaz Kabir, Paul He, and Ondrej Lhoták. 2017\.  A Simple Soundness Proof for Dependent Object Types. In _Proc. ACM Program. Lang._ 46:1–46:27.
  * Rapoport and Lhoták (2019) Marianna Rapoport and Ondřej Lhoták. 2019.  A Path To DOT: Formalizing Fully-Path-Dependent Types.  _arXiv:1904.07298 [cs]_ (April 2019).  arXiv:1904.07298 [cs]
  * Rompf and Amin (2016) 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)_. Association for Computing Machinery, New York, NY, USA, 624–641.  https://doi.org/10.1145/2983990.2984008
  * Sabry and Felleisen (1993) AMR Sabry and Matthias Felleisen. 1993.  Reasoning about Programs in Continuation-Passing Style.  _LISP and Symbolic Computation_ 6, 3 (Nov. 1993), 289–360.  https://doi.org/10.1007/BF01019462
  * Scherer and Rémy (2013) Gabriel Scherer and Didier Rémy. 2013.  GADTs Meet Subtyping. In _Programming Languages and Systems_ _(Lecture Notes in Computer Science)_ , Matthias Felleisen and Philippa Gardner (Eds.). Springer, Berlin, Heidelberg, 554–573.  https://doi.org/10.1007/978-3-642-37036-6_30
  * Stolarek et al. (2015) Jan Stolarek, Simon Peyton Jones, and Richard A. Eisenberg. 2015\.  Injective Type Families for Haskell.  _ACM SIGPLAN Notices_ 50, 12 (Aug. 2015), 118–128.  https://doi.org/10.1145/2887747.2804314
  * Stump (2009) Aaron Stump. 2009\.  Directly Reflective Meta-Programming.  _Higher-Order and Symbolic Computation_ 22, 2 (June 2009), 115–144.  https://doi.org/10.1007/s10990-007-9022-0
  * Sulzmann et al. (2007) Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. 2007.  System F with Type Equality Coercions. In _Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation_ _(TLDI ’07)_. Association for Computing Machinery, New York, NY, USA, 53–66.  https://doi.org/10.1145/1190315.1190324
  * Trifonov et al. (2000) Valery Trifonov, Bratin Saha, and Zhong Shao. 2000.  Fully Reflexive Intensional Type Analysis. In _Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming_ _(ICFP ’00)_. Association for Computing Machinery, New York, NY, USA, 82–93.  https://doi.org/10.1145/351240.351248
  * Waśko (2021) Radosław Waśko. 2021\.  _Formal foundations for Generalized Algebraic Data Types in Scala_.  Master’s thesis. University of Warsaw.  https://apd.uw.edu.pl/diplomas/197329/.
  * Wright and Felleisen (1994) A. K. Wright and M. Felleisen. 1994.  A Syntactic Approach to Type Soundness.  _Information and Computation_ 115, 1 (Nov. 1994), 38–94.  https://doi.org/10.1006/inco.1994.1093
  * Xi et al. (2003) Hongwei Xi, Chiyan Chen, and Gang Chen. 2003.  Guarded Recursive Datatype Constructors. In _ACM SIGPLAN Notices_ , Vol. 38. ACM, 224–235.
  * Xu et al. (2021) Yichen Xu, Aleksander Boruch-Gruszecki, and Lionel Parreaux. 2021\.  Implementing Path-Dependent GADT Reasoning for Scala 3. In _Proceedings of the 12th ACM SIGPLAN International Symposium on Scala_ _(SCALA 2021)_. Association for Computing Machinery, New York, NY, USA, 22–32.  https://doi.org/10.1145/3486610.3486892
  * Yallop and Dolan (2019) Jeremy Yallop and Stephen Dolan. 2019.  First-Class Subtypes.  _Electronic Proceedings in Theoretical Computer Science_ 294 (May 2019), 74–85.  https://doi.org/10.4204/EPTCS.294.4 arXiv:1905.06546

##  Appendix A Subsuming GADTs

###  A.1. Modifications to $\lambda_{2,G\mu}$

In this section, we cover those details of our modified version of
$\lambda_{2,G\mu}$ which are only relevant to the encoding. The variant is
exhaustively described in (Waśko, 2021).

#### Type annotations

We will want to encode $\lambda_{2,G\mu}$ into cDOT. In some places this
encoding will need to state the types of some objects in the syntax of the
target calculus. To ensure that the encoding can be defined just by looking at
the syntax of the input terms, we add the necessary annotations to the syntax
of the calculus. These annotations do not change semantics or expressivity. In
fact, a well-typed program without these annotations can be easily converted
into a program with the annotations, just by appending the necessary types
coming from the typing derivation. We actually have mechanized two variants of
the calculus: one with these annotations and another without them.

The only modifications are in the tuple syntax, where $\langle
e_{1},e_{2}\rangle$ becomes $\langle e_{1}:\tau_{1},e_{2}:\tau_{2}\rangle$ and
in the pattern matching syntax, explained in the next paragraph. This
modification does not affect the reduction rules (they can simply ignore the
annotations). In the typing rules, we simply verify that the type in the
annotation matches the actual type stemming from the typing judgment. For
example, below we show the old and new versions of the ty-tup rule. The change
is purely technical in that the type now not only appears in the judgment, but
also at the syntax level.

$\Delta;\Pi\vdash e_{1}:\tau_{1}$ $\Delta;\Pi\vdash e_{2}:\tau_{2}$ (old ty-
tup) $\Delta;\Pi\vdash\langle e_{1},e_{2}\rangle:\tau_{1}*\tau_{2}$