The Duality of Subtyping
Bruno C. d. S. Oliveira
The University of Hong Kong, Hong Kong, China
bruno@cs.hku.hk

Cui Shaobo
University of California San Diego, United Statescuishaobo@gmail.com

Baber Rehman
The University of Hong Kong, Hong Kong, China
brehman@cs.hku.hk

Abstract
Subtyping is a concept frequently encountered in many programming languages and calculi. Various
forms of subtyping exist for different type system features, including intersection types, union types
or bounded quantification. Normally these features are designed independently of each other, without
exploiting obvious similarities (or dualities) between features.
This paper proposes a novel methodology for designing subtyping relations that exploits duality
between features. At the core of our methodology is a generalization of subtyping relations, which
we call Duotyping. Duotyping is parameterized by the mode of the relation. One of these modes is theusual subtyping, while another mode is supertyping (the dual of subtyping). Using the mode it ispossible to generalize the usual rules of subtyping to account not only for the intended behaviour of
one particular language construct, but also of its dual. Duotyping brings multiple benefits, including:shorter specifications and implementations, dual features that come essentially for free, as well as
new proof techniques for various properties of subtyping. To evaluate a design based on Duotyping
against traditional designs, we formalized various calculi with common OOP features (including
union types, intersection types and bounded quantification) in Coq in both styles. Our results showthat the metatheory when using Duotyping does not come at a significant cost: the metatheory
with Duotyping has similar complexity and size compared to the metatheory for traditional designs.
However, we discover new features as duals to well-known features. Furthermore, we also show that
Duotyping can significantly simplify transitivity proofs for many of the calculi studied by us.
2012 ACM Subject Classification Software and its engineering → Object oriented languages
Keywords and phrases DuoTyping, OOP, Duality, Subtyping, Supertyping
Digital Object Identifier 10.4230/LIPIcs.ECOOP.2020.29
Supplement Material https://github.com/baberrehman/coq-duotyping
Funding Funded by Hong Kong Research Grant Council projects number 17210617 and 17209519.
Acknowledgements We thank the anonymous reviewers for their helpful comments.

1

Introduction

Subtyping is a concept frequently encountered in many programming languages and calculi.
It is also a pervasive and fundamental feature in Object-Oriented Programming (OOP).
Various forms of subtyping exist for different type system features, including intersection
types [6], union types [6] or bounded quantification [15]. Modern OOP languages such as
Scala [34], Ceylon [29], Flow [19] or TypeScript [12] all support the aforementioned typesystem features.
As programming languages evolve, new features are added. This requires that subtyping
for these new features is developed and also integrated with existing features. However, the© Bruno C. d. S. Oliveira, Shaobo Cui and Baber Rehman;
licensed under Creative Commons License CC-BY
34th European Conference on Object-Oriented Programming (ECOOP 2020).
Editors: Robert Hirschfeld and Tobias Pape; Article No. 29; pp. 29:1–29:28
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

29:2

The Duality of Subtyping

design and implementation of subtyping for new features is quite often non-trivial. There
are several, well-documented issues in the literature. These include finding algorithmic forms
for subtyping (for instance doing transitivity elimination) [43] or proving metatheoreticalproperties such as transitivity or narrowing [1]. Such issues occur, for instance, in someof the latest developments for OOP languages, such as the DOT calculi (which model theessence of Scala) [3]. One possible way to reduce the non-trivial amount of work needed
to develop new features, would be if two related features could be develop at once with acoherent design. This paper explores a new methodology that enables such benefits.
Normally programming language features are designed independently of each other.
However there are features that are closely related to each other, and can be viewed as dualfeatures. Various programming language features are known to be dual in programming
language theory. For instance sum and product types are well-known to be duals [14].
Similarly universal and existential quantification are dual concepts as well [9]. Moreover
duality is a key concept in category theory [30] and many abstractions widely used infunctional programming (such as Monads and CoMonads [44]) are also known to be duals.
In OOP type systems dual features are also common. For instance all OOP languages
contain a top type (called Object in Java or Any in Scala), which is the supertype of all
types. Many OOP languages also contain a bottom type, which is a subtype of all types. Top
and bottom types can be viewed as dual features, mirroring the functionality of each other.
Intersection and union types are another example of dual features. The intersection of two
types A and B can be used to type a value that implements both A and B. The union of two
types A and B can be used to type a value that implements either A or B.
Duality in OOP and subtyping is often only informally observed by humans. For instance,by simply understanding the behaviour of the features and observing their complementaryroles, as we just did in the previous paragraph. At best duality is more precisely observed
by looking at the rules for the language constructs and their duals and observing a certain
symmetry between those rules. However existing formalisms and language designs for typesystems and subtyping relations do not directly incorporate duality. Unfortunately thismeans that an opportunity to exploit obvious similarities between features is lost.
This paper proposes a novel methodology for designing subtyping relations that exploits
duality between features directly in the formalism. At the core of our methodology is a
generalization of subtyping relations, which we call Duotyping. Duotyping is parameterized
by the mode of the relation. One of these modes is the usual subtyping, while anothermode is supertyping (the dual of subtyping). Using the mode it is possible to generalize theusual rules of subtyping to account not only for the intended behaviour of one particularlanguage construct, but also of its dual. This means that the behaviour of the language
construct and its dual is modelled by a single, common set of rules. In turn this ensuresthat the behaviour of the two features is modelled consistently. Moreover it also enables
various theorems/properties of subtyping to be generalized to account for the dual features.
Therefore, Duotyping offers similar benefits to the how duality is exploited in category theory.
More concretely, Duotyping brings multiple benefits for the design of subtyping relations,which are discussed next.
Shorter specifications: When duality is exploited in specifications of subtyping it leads toshorter specifications because rules for dual features are shared. This also ensures a consistentdesign of the rules between the dual features directly in the formalism. Such consistency is notenforceable in traditional formulations of subtyping where the rules are designed separately,
and thus their design is completely unconstrained with respect to the dual feature. A concrete
example that illustrates shorter specifications is a traditional subtyping relation with top,

Oliveira et al.

29:3

bottom, union and intersection types, which would normally have 8 subtyping rules for those
constructs. In a design with Duotyping we only need 5 subtyping rules. Basically we need
only half of the rules (4 in this case) to model the feature-specific rules, plus an additional
duality rule which is generic (and plays a similar role to reflexivity and transitivity).
“Buy” one feature get one feature for free! Duality can lead to the discovery of newfeatures. While top and bottom types, or intersection and union types are well-known in theliterature (and understood to be duals), other features in languages with subtyping do nothave a known dual feature in the literature. This is partly because, when a language designer
employs traditional formulations of subtyping, he/she is often only interested in the design ofa feature (but not necessarily of its dual). Even for the case of union and intersection types,
intersection types were developed first and the development of union types occurred years
later. Because the dual feature is often also useful, the traditional way to design subtyping
rules represents a loss of opportunity to get another language feature essentially for free.
One well-known example of a language feature that has been widely exploited in theliterature, but its dual feature has received much less attention is bounded quantification [17].
Bounded quantification allows type variables to be defined with upper bounds. However
lower bounds are also useful. One can think of universal quantification with lower bounds
as a dual to universal quantification with upper bounds. The essence of (upper) bounded
quantification is captured by the well-known F<: calculus [17]. However, as far as we know,
there is no design that extends F<: with lower bounded quantification in the literature.
Applying a Duotyping design to F<: gives us, naturally, the two features at once (lower
and upper bounded quantification), as illustrated in our Section 4. Such generalization ofbounded quantification is related to the recent form of universal quantification with typebounds employed in Scala and the DOT family of calculi [3]. However, while Scala’s typebounds are more expressive than what we propose, they are also much more complex andare in fact one of the key complications in the type systems of languages like Scala. Most
DOT calculi require a built-in transitivity rule in subtyping because it is not known how toeliminate transitivity. In contrast, the generalization of F<: proposed by us has a formulationof subtyping where transitivity can be proved as a separate lemma.
New proof techniques: Designs of subtyping with duality also enable new proof techniquesthat exploit such duality. For instance there are various theorems that can be stated for botha feature and its dual, instead of having separate theorems for both. Some of the propertiesof union and intersection types are examples of this. Moreover, Duotyping also enables new
proof techniques to prove traditionally hard theorems such as transitivity. Surprisingly to us,
for the vast majority of the calculi that we have applied Duotyping to, transitivity proofs
have been considerably simpler than their corresponding traditional formulations due to theuse of Duotyping!
Shorter implementations: Finally Duotyping also enables for shorter implementations.
The benefits of shorter implementations are similar and follow from the benefits of shorter
specifications. However there is a complicating factor when moving from a relational
specification into an implementation: the duality rule is non-algorithmic. This is akin to what
happens with transitivity, which is often also used in declarative formulations of subtyping.
Eliminating transitivity to obtain an algorithmic system can often be a non-trivial challenge(as illustrated, for instance, by the DOT family of calculi [3]). However, we show that there
is a simple and generally applicable technique that can be used to move from a declarative
formulation of Duotyping into an algorithmic version. This contrasts with transitivity, forwhich there is not a generally applicable transitivity elimination technique.
To evaluate a design based on Duotyping against traditional designs of subtyping, we

ECOOP 2020

29:4

The Duality of Subtyping

formalized various calculi with common OOP features (including union types, intersection
types and bounded quantification) in Coq in both styles. Our results show that the metatheory
when using Duotyping has similar complexity and size compared to traditional designs.
However, the Duotyping formalizations come with more features (for instance lower-bounded
quantification) that dualize other well-known features (upper-bounded quantification). Finally,
we also show that Duotyping can significantly simplify transitivity proofs for many of thecalculi studied by us.
In summary, the contributions of this paper are:Duotyping: A new methodology for the design of subtyping relations exploiting duality.
A case study on Duotyping: A comprehensive study of various existing type systems
and features, which were redesigned to employ the Duotyping methodology. Our results
show that in most systems the size of the metatheory without duality and with duality iscomparable, while often transitivity proofs become simpler when employing duality.
F<: with lower bounded quantification: We propose a new generalization of System
F<: , called Fk , which allows not only type variables to be quantified with upper bounds
and lower bounds as well. While this system is weaker than Scala/DOT’s type bounds, it
nonetheless allows for simple transitivity proofs (which have been a significant challenge
in calculi with type bounds [40]).
Mechanization in Coq: All the systems in our case study have been formalized in the
Coq theorem prover [8].

2

Overview

This section gives an overview of Duotyping. We show how to design subtyping relations
employing Duotyping, and discuss the advantages of a design with Duotyping instead of a
traditional subtyping formulation in more detail.

2.1

Subtyping with union and intersection types

To motivate the design of Duotyping relations we first consider a traditional subtyping relation
with union and intersection types, as well as top and bottom types. We choose a systemwith union and intersection types because these features are nowadays common in various
OOP languages, including Scala [34], TypeScript [12], Ceylon [29] or Flow [19]. Therefore
union and intersection types are of practical interest. Furthermore union and intersection
types are simple, intuitive and good for showing duality between concepts.
The types used for the subtyping relation include the top type >, the bottom type ⊥,
integer types Int, function types A → B, intersection types A ∧ B and union types A ∨ B:

Types

A, B

::=

> | ⊥ | Int | A → B | A ∧ B | A ∨ B

Traditional Subtyping A simple subtyping relation accounting for union and intersection
types is given in Figure 1. Rule ts-top defines that every type is a subtype of >, andRule ts-btm states that every type is a supertype of ⊥. Rule ts-int is for integers, andstates that Int is a subtype of itself. Rule ts-arrow is the traditional subtyping rule forfunction types. Rules ts-anda, ts-andb, and ts-andc are subtyping rules for intersection
types. Rules ts-ora, ts-orb, and ts-orc are subtyping rules for union types. The rulesthat we employ here are quite common for systems with union and intersection types. For

Oliveira et al.

29:5

A <: B(Traditional Subtyping)B1 <: A1

A <: >

ts-topA <: A1⊥ <: A
A <: A2

A <: A1 ∧ A2
A1 <: A

ts-btmts-intA1 ∧ A2 <: A

A <: A1 ∨ A2

ts-arrow

A2 <: A
ts-andb

A1 ∧ A2 <: A

A <: A1
ts-oraA2 <: B2

A1 → A2 <: B1 → B2

A1 <: A
ts-andaA2 <: AA1 ∨ A2 <: A

Int <: Int

ts-andc

A <: A2
ts-orb

A <: A1 ∨ A2

ts-orcFigure 1 Subtyping for union and intersection types.

instance they are the same rules used in various DOT-calculi [3] (which model the essence of
Scala). For simplicity we do not account for distributivity rules, which also appear in some
type systems and calculi [7, 11, 47].

2.2

Subtyping Specifications using Duotyping

In the subtyping relation presented in Figure 1, it is quite obvious that many rules lookalike. Some rules are essentially a “mirror image” of other rules. The rules for top andbottom types are an example of this. Another example are the rules ts-andb and ts-orb.
Although informally humans can easily observe the similarity between many of the rules, thissimilarity/duality is not expressed directly in the formalism. For example, there is nothing
preventing us from designing rules that are not duals. Duotyping aims at capturing duality inthe rules themselves, and expressing duality as part of the formalism, rather than just leaving
duality informally observable by humans. This can prevent, for instance, designing rules fordual concepts that do not really dualize. Therefore Duotyping can enforce consistency of dual
rule designs.
To illustrate how Duotyping rules are designed and relate to the traditional subtyping
rules, lets refactor the traditional rules in a few basic steps. Firstly, lets assume that we have asecond relation A :> B that captures the supertyping between a type A and B. Supertyping
is nothing but the subtyping relation with its arguments flipped. So, the rules of supertyping
could be simply obtained by taking all the rules in Figure 1 and deriving corresponding rules
where all the arguments are flipped around. We skip that boring definition here. With bothsupertyping and subtyping, the top and bottom rules can be presented as follows:
A <: >

ts-top

A :> ⊥

tsp-btm

Similarly the rules rule ts-andb and rule ts-orb, can be presented as:
A1 <: AA1 ∧ A2 <: A

A1 :> A
ts-andb

A1 ∨ A2 :> A

tsp-orb

This simple refactoring shows that the only difference between dual rules is the relation itself,
and the (dual) language constructs. Apart from that everything else is the same.
Duotyping With Duotyping we can provide a single unified rule, which captures the two
distinct subtyping rules, instead. The Duotyping relation is parameterized by a mode ♦:ECOOP 2020

29:6

The Duality of Subtyping

Mode

♦

::=

<: | :>

which can be subtyping (<:) or supertyping (:>). Thus the Duotyping relation is of the form:
A♦B
The mode ♦ is a (third) parameter of the relation (besides A and B). With this mode inplace, we can readily capture the two refactored rules for supertyping of bottom types andsubtyping of top types as two Duotyping rules. However this still requires us to write two
distinct rules. To unify those rules into a single one, we introduce a function e♦d that chooses
the right bound depending on the mode being used:e <: d = >e :> d = ⊥If the mode is subtyping the upper bound of the relation is the top type, otherwise it is thebottom type. With e♦d we can then write a single unified rule that captures the upper boundsof subtyping and supertyping, and which generalizes both rule ts-top and rule tsp-btm:
A ♦ e♦dgds-topbtm

The Duality rule The Duotyping rule above captures the 2 rules that were refactored above.
However there are 4 rules in total for top and bottom types (two for subtyping and two forsupertyping). The two missing rules are:
⊥ <: A

ts-btm> :> A

tsp-top

To capture these missing rules, the Duotyping relation includes a special duality rule:
B ♦A
A♦B

gds-dual

which simply inverts the mode and flips the arguments of the relation. The definition of ♦ is,unsurprisingly:<: = :>:> = <:

With the duality rule it is clear that the two missing rules are now derivable from the
Duotyping rule for bounds and the duality rule. In essence this is the overall idea of thedesign of Duotyping rules.
Complete set of rules Figure 2 shows the complete version of declarative Duotyping rules
for a system with union and intersection types. Rule gds-topbtm defines the rule bounds(which generalizes the rules for top and bottom types). Rule gds-int is a simple rule for
integers. Int is subtype and supertype of Int. Rule gds-arrow is an interesting case. In thefirst premise A ♦ B we invert the mode instead of flipping the arguments of the relation, as
done in rule ts-arrow. One side-effect of this change is that it keeps the rule fully covariant,which contrasts with subtyping relations where for arrow types we need contravariance forsubtyping of the inputs. This apparently innocent change has important consequences andplays a fundamental role to simplify transitivity proofs as we shall see in Section 2.5.
Rules gds-Left, gds-Right, and gds-both each generalize two rules in the traditional
formulation of subtyping. Rule gds-Left generalizes rules ts-andb and ts-orb. Rule gdsRight generalizes rules ts-andc and ts-orc. Rule gds-both generalizes rules ts-anda
and ts-ora. In the three rules an operation A ♦? B is used:Oliveira et al.

29:7(Declarative Duotyping)A♦B
A1 ♦ A2A ♦ e♦dgds-topbtm

Int ♦ Int

gds-Left

B1 ♦ B2

A1 → B1 ♦ A2 → B2

B ♦C

A♦C
(A ♦? B) ♦ C

gds-int

A♦B(A ♦? B) ♦ C

gds-Right

gds-arrowA♦C

A ♦ (B ♦? C )gds-bothB ♦AA♦B

gds-dual

Figure 2 The Duotyping relation for a calculus with union and intersection types.

A <:? B = A ∧ B
A :>? B = A ∨ BThis operation is used to choose between intersection or union types depending on the mode.
If the Duotyping mode is subtyping then we get a rule for intersection types, otherwise we
get a dual rule for union types.
Uniform and dual rules In the context of Duotyping it is useful to distinguish between
two different kinds of rules: uniform rules and dual rules.
Uniform rules are those that are essentially the same for supertyping and subtyping.
Rules gds-int and gds-arrow are uniform rules. In those rules the arguments of therelation are exactly the same no matter which mode is being used (subtyping or supertyping).
Dual rules are those that employ dual constructs, like the rules for top and bottom or
the rules for union and intersections. Rules gds-topbtm, gds-left, gds-right, andgds-both are dual rules. The interesting point in these rules is that they use different(dual) constructs depending on the mode. For example, when instantiated with subtyping
and supertyping, respectively, the rule gds-topbtm results in:

A <: >

2.3

A :> ⊥

Implementations using Duotyping

Figure 2 showed the declarative Duotyping rules for a calculus with union and intersection
types. All the rules are syntax directed, except for the duality rule (rule gds-dual). This
rule flips the mode and arguments to generate a formulation using the dual mode: i.e. it flips
subtyping to provide the equivalent supertyping formulation and vice versa. A benefit ofusing a formulation with the duality rule is that it enables a short specification of Duotyping.
Unfortunately the duality rule is not algorithmic, because the duality rule can always beapplied indefinitely. In other words naively translating the rules into an program would
easily result in a non-terminating procedure. Therefore to obtain an algorithmic formulationsome additional work is needed.
Fortunately, for declarative formulations of Duotyping, there is a simple technique thatcan be used to obtain an algorithmic formulation. A key observation is that Duotyping only
needs to be flipped (with the duality rule) at most one time. Flipping the relation two or
more times simply gets us back to the starting point. To capture this idea we can use a

ECOOP 2020

29:8

The Duality of Subtyping

data Op = And | Ordata Typ = TInt | TArrow Typ Typ | TOp Op Typ Typ | TBot | TTopdata Mode = Sub | Sup
duo :: Bool -> Mode -> Typ -> Typ -> Bool
duo f m TInt TInt
= Trueduo f m _ b | b == mode_to_sub m= Trueduo f m (TArrow a b) (TArrow c d)=duo True (flip m) a c && duo True m b d
duo f m (TOp op a b) c | choose m == op = duo True m a c || duo True m b c
duo f m a (TOp op b c) | choose m == op = duo True m a b && duo True m a c
duo True m a b= duo False (flip m) b a
duo _ _ _ _= FalseFigure 3 Haskell code for implementing an algorithmic formulation of Duotyping rules.

(boolean) flag that keeps track of whether the procedure has already employed the duality
rule or not.
To make such an idea concrete, Figure 3 shows Haskell code that implements a procedure
duo for determining Duotyping for two types. The code is based on the rules in Figure 2, but
it uses a boolean flag to prevent the dual rule (the second to last case in duo) from being
applied indefinitely. The boolean is true in the initial call or recursive calls to structurally
smaller arguments. If the algorithm fails for the first five cases (which are basically a directtranslation of the rules gds-topbtm, gds-int, gds-arrow, gds-Left, and gds-Right),
then the algorithm simply flips the boolean flag, mode and arguments to run over a dual
formulation. This is the second to last line of the algorithm.
For example, if the algorithm is called with the mode set to subtyping and it is not able tofind any matching case with the first 5 rules, then it flips the boolean flag to False, subtyping
to supertyping and the arguments to check the equivalent supertyping formulation. If again
it fails to find a matching rule, False will be returned and the algorithm will terminate.
This illustrates that it is enough to flip the boolean flag once to exploit Duotyping. In all our
Coq formulations of Duotyping we have developed an alternative algorithmic formulation of
Duotyping which uses an extra boolean flag and is shown to be sound and complete to thedeclarative formulations with the duality rule. In short there is an easy, general and provably
sound and complete way to implement algorithms based on the idea of Duotyping, while atthe same time retaining the benefits of reuse of the logic for rules for dual constructs.

2.4

Discovering new features

Duotyping can provide interesting extra features essentially for free. For example, the hallmark
feature of the well-known F<: calculus (a polymorphic calculus with subtyping) [15] is bounded
quantification, which is a feature used in most modern OOP languages (such as Scala orJava). In F<: , bounded quantification allows type variables to be defined with upper bounds.
For example, the following Scala program illustrates the use of such upper bounds:
class Person {def name: String = "person"}

Oliveira et al.

29:9class Student extends Person {override def name: String = "student"
def id: String = "id"}class StudentsCollection[S <: Student](obj: S) {def student: S = obj}

The Scala program shown above uses the upper bounds for the class StudentsCollection
written as S <: Student. This upper bound restricts StudentsCollection to be instantiatedwith Student and its subtypes. Since the upper bound is Student, any class that is supertypeof Student like Person cannot be instantiated in StudentsCollection.
However lower bounds are also useful, and indeed the Scala language allows them (thoughJava does not). One example of a program with lower bounds in Scala is:class GraduateStudent extends Student {def degree: String = "graduate degree"}class ResearchStudent extends GraduateStudent {override def degree: String = "research degree"}class CollectionExcludingResearchStudents[S >: GraduateStudent](obj: S) {def student: S = obj}

In contrast to the upper bounds, the Scala program shown above uses the lower bounds forthe class CollectionExcludingResearchStudents written as S >: GraduateStudent. This lower
bound restricts CollectionExcludingResearchStudents to be instantiated with GraduateStudent
and its supertypes. Since the lower bound is GraduateStudent. Any class that is a subtype ofGraduateStudent (such as ResearchStudent) cannot be instantiated in CollectionExcludingResearchStudents. But any supertype of GraduateStudent like Student and Person (including
GraduateStudent) can be instantiated in CollectionExcludingResearchStudents.
One can think of universal quantification with lower bounds as a dual to universal
quantification with upper bounds. While there is no extension of F<: that we know of that
presents universal quantification with lower bounds in the literature, applying a Duotyping
design to F<: gives us, naturally, the two features at once (lower and upper bounded
quantification).
Bounded quantification in F<: The traditional subtyping rule of System kernel F<: withupper bounded quantification is:
Γ, X <: A ` B <: CΓ ` (∀X <: A.B) <: (∀X <: A.C )ts-forallkfs

In the premise of this rule, we add the type variable X to the context with an upper bound
A. If under the extended context the bodies of the universal quantifier (B and C ) are in a
subtyping relation then the universal quantifiers are also in a subtyping relation.
To add lower bounded quantification the obvious idea is to add a second rule:
Γ, X :> A ` B <: CΓ ` (∀X :> A.B) <: (∀X :> A.C )ts-forallkfsb

ECOOP 2020

29:10The Duality of Subtyping

However this alone is not quite right because the environment is also extended with a lower
bound (X >: A), which does not exist in F<: contexts. Therefore some additional care isalso needed for the variable cases of F<: extended with lower bounded quantification. Whenan upper bounded constraint is found in the environment, the variable case needs to deal
with the upper bound appropriately. Since there are two rules dealing with the variable casein F<: , one possible approach is to add two more rules for dealing with upper bounds:
X :>A ∈ ΓΓ ` B <: AΓ ` B <: X

X :>A ∈ Γ
ts-TVarbΓ ` X <: X

ts-ReflTvar

However such a design feels a little unsatisfactory. We need a total of 6 rules to fully deal
with lower and upper bounded quantification (instead of 3 rules in F<: ). At the same time
the rules are nearly identical, differing only on the kind of bounds that is used. Furthermore
the metatheory of F<: also needs to be significantly changed. In particular narrowing has
to be adapted to account for the lower bounds and transitivity has to be extended withseveral new cases. Since both narrowing and transitivity proofs for F<: are non-trivial, thisextension is also non-trivial and adds further complexity to already complex proofs.
A variant of Kernel F<: with Duotyping We now reconsider the design of Kernel F<:
from scratch employing the Duotyping methodology. In the subtyping rule for universal
quantification, it is important to note that the subtyping relation between two universal
quantifiers in the conclusion is the same as the relation between types B and C in premise.
Similarly, the (subtyping/supertyping) bounds of type variable X in the conclusion are thesame as the bounds of type variable X in premise. In a design with Duotyping, we would liketo generalize the two uses of subtyping. Therefore, we can design a single unified rule withthe help of two modes:
Γ, X ♦1 A ` B ♦2 C
Γ ` (∀X ♦1 A.B) ♦2 (∀X ♦1 A.C )gs-forallkfs

Section 4.1 explains the Duotyping rules of our Duotyping kernel F<: variant with union and∧∨intersection types (Fk♦
) in detail. Rule gs-forallkfs is the interesting case, capturing
both upper and lower bounded quantification in an elegant way. This rule states that if in awell-formed context, type variable X has a ♦1 relation with type A and if type B has ♦2
relation with type C , then the universal quantification with body B has a ♦2 relation withthe universal quantification with body C . Correspondingly there are also two Duotyping
rules for variables:
X ♦A ∈ ΓΓ ` A♦BΓ ` X ♦B

X ♦1 A ∈ Γ
gs-TVaraΓ ` X ♦2 X

gs-ReflTvar

In short, the design of a variant of F<: with Duotyping leads to a system that naturally
accounts for both upper and lower bounded quantification. Moreover, the metatheory,and in particular the proofs of narrowing and transitivity are not more complex than thecorresponding original F<: proofs. In fact the proof of transitivity is significantly simpler,
because Duotyping enables novel proof techniques as we discuss next.

2.5

New proof techniques

Transitivity proofs are usually a challenge for systems with subtyping. This is partly because
subtyping relations often need to deal with some contravariance. For instance, the rule tsarrow (in Figure 1) is contravariant on the input types. Such contravariance causes problems

Oliveira et al.

29:11(Algorithmic Duotyping)A♦B
A ♦ e♦dgs-topbtmae♦d ♦ AA1 ♦ A2

gs-topbtmb

Int ♦ Int

gs-intB1 ♦ B2

A1 → B1 ♦ A2 → B2

gs-arrow

Figure 4 The Duotyping relation for simply typed lambda calculus calculus.

in certain proofs, including transitivity. To illustrate the issue more concretely, let’s distill
the essence of the problem by considering a simple lambda calculus with subtyping called
λ<: , where the types are:
Types

A, B

::=

> | Int | A → B

and the subtyping rules for those types are just the relevant subset of the rules in Figure 1.
The transitivity proof for this simple calculus is:
I Lemma 1 (λ<: Transitivity). If A <: B and B <: C then A <: C .
Proof. By induction on type B.
Case > and case Int are trivial to prove by destructing the hypothesis in context.
Case B1 → B2 requires inversion of the two hypotheses to discover that A can only be afunction type, while C is either a function type or >.
J
In the arrow case, we need to invert both hypotheses to discover more information about
A and C . For this very simply language this double inversion is not too problematic, but
as the language of types grows and the subtyping relation becomes more complicated, suchinversions become significantly harder to deal with.
At this point one may wonder if the transitivity proof could be done using a different
inductive argument to start with, and thus avoid the double inversions. After all there arevarious other possible choices. Perhaps the most obvious choice is to try induction on thesubtyping relation itself (A <: B), rather than on type B. However this does not work
because of the contravariance for arrow types, which renders one of induction hypothesisin the arrow case useless (and thus do not allow the case to be proved). Other alternative
choices for an inductive argument (such as type A or C) do not work for similar reasons.
Developing metatheory with Duotyping In order to develop metatheory with Duotyping
it is convenient to use an equivalent formulation of Duotyping that eliminates the duality
rule (which is non-algorithmic and makes inversions more difficult). For λ♦ , which is a
Duotyping version of λ<: , this would lead to the set of rules in Figure 4. This alternativealgorithmic version eliminates the duality rule. Rules gs-topbtma, gs-int, and gs-arrow
are similar to the rules we discussed in Section 2.2. Rule gs-topbtmb is the dual rule ofrule gs-topbtma. With Rule gs-topbtmb, the duality rule is unnecessary.
Transitivity with Duotyping Now we turn our attention to the proof of transitivity:
I Lemma 2 (λ♦ Transitivity). If A♦B and B♦C then A♦C .
Proof. By induction on A♦B.

ECOOP 2020

29:12

The Duality of Subtyping

All cases are trivial to prove by destructing ♦ and inversion of the second hypothesis(B♦C ).
J
Transitivity of systems with Duotyping can often be proved by induction on the subtyping
relation itself. This has the nice advantage that all the cases essentially become trivial toprove (for λ♦ ) and only a single inversion is needed for arrow types. A key reason why
such approach works in the formulation with Duotyping is that we can keep case for arrow
types covariant. Instead we only flip the mode. Another important observation is thatwhen we prove a transitivity lemma with Duotyping we are, in fact, proving two lemmas
simultaneously: one lemma for transitivity of subtyping, and another one for transitivityof supertyping. When we use the induction hypothesis we have access to both lemmas (bychoosing the appropriate mode).
The proof of the transitivity lemma by induction on the Duotyping relation can scale
up to more complex subtyping/Duotyping relations. This includes subtyping relations withadvanced features such as intersection types, union types, parametric polymorphism andbounded quantification. All of these can follow the same strategy (induction on the Duotyping
relation) to simplify the transitivity proof, as we shall see in Section 5.

3

The λ∧∨♦ calculus

In Section 2 we gave an overview and discussed advantages of using the Duotyping relation.
In this section we introduce a lambda calculus with union and intersection types that isbased on Duotyping. We aim at showing that developing calculi and metatheory using
Duotyping is simple, requiring only a few small adaptations compared with more traditional
formulations based on subtyping. Our main aim is to show type soundness (subject-reduction
and preservation) for λ∧∨
♦ .

3.1

Syntax and Duotyping

Syntax Figure 5 shows the syntax of the calculus. The types for λ∧∨♦ were already introducedin Section 2. Terms include all the constructs for the lambda calculus (variables x, functions
λx : A. e and applications e1 e2 ) and integers (n). Values are a subset of terms, consisting of
abstractions and integers only. The mode ♦ is used to choose the mode of the relation: it
can be either subtyping (<:) or supertyping (:>). Typing contexts Γ are standard and used
to track the types of the variables in a program. Finally, a well-formedness relation Γ ` ok
ensures that typing contexts are well-formed.
∧∨
Duotyping for λ∧∨♦ The Duotyping rules for λ♦ were already partly presented in Figure 2.
In addition to the rules in the λ♦ , we also need extra rules for union and intersection types.
These extra rules are presented in Figure 5. Rules gs-lefta, gs-righta, and gs-botha
are also similar to the rules gds-Left, gds-Right, and gds-both presented in Figure 2.
Since we eliminate the duality rule in the algorithmic version, we add dual subtyping rules.
Rules gs-leftb, gs-rightb, and gs-bothb are the dual versions of rules gs-lefta, gsrighta, and gs-botha respectively. This formulation is shown to be sound and completewith respect to the formulation with the duality rule in Figure 2. As explained in Section 2
this variant of the rules makes some proofs easier, thus we employ it here. The Duotyping
relation is reflexive and transitive:

I Theorem 1 (Reflexivity). A♦A.

Oliveira et al.

29:13

Types
Terms
ValuesContext
Mode

A, B
e
v
Γ
♦

::=
::=
::=
::=
::=

> | ⊥ | Int | A → B | A ∧ B | A ∨ B
x | n | λx : A. e | e1 e2
n | λx : A. e
• | Γ, x : A<: | :>(Algorithmic Duotyping)

A♦B
A♦B

A♦C
(A ♦? B) ♦ C

gs-lefta

A♦C
A ♦ (B ♦? C )A ♦ (B ♦? C )A♦Bgs-rightb

B ♦C
gs-leftb

A♦CA♦C

A ♦ (B ♦? C )(A ♦? B) ♦ C

gs-botha

gs-righta

B ♦C(A ♦? B) ♦ C

gs-bothb

Figure 5 Syntax and Duotyping relation for union and intersection types.

Proof. By induction on type A. Reflexivity is trivial to prove by applying subtyping rules. J
I Theorem 2 (Transitivity). If A♦B and B♦C then A♦C .
Proof. By induction on subtyping relation.
Cases rule gs-topbtma, rule gs-int, rule gs-lefta, rule gs-righta and rule gs-botha
are trivial to prove.
Case rule gs-topbtmb requires an additional Lemma 1.
Case rule gs-arrow requires induction on hypothesis and subtyping rules.
Cases rule gs-leftb and rule gs-rightb requires an additional Lemma 2 to be appliedon hypothesis in context.
Case rule gs-bothb requires induction on the hypothesis. This case also requires rule gsleftb, rule gs-rightb, and rule gs-botha subtyping rules.
J
We used the following auxiliary lemmas to prove transitivity.
B Lemma 1 (Bound Selection). If e♦d♦B then A♦B.
This lemma captures the upper and lower bounds with respect to relation between two
types. If the mode is subtyping, then it states that any type that is supertype of > issupertype of all the other types. If the mode is supertyping, then it states that any typethat is subtype of ⊥ is subtype of all the other types. In essence the lemma generalizes thefollowing two lemmas (defined directly over subtyping and supertyping):
If > <: B then A <: B
If ⊥ :> B then A :> B
B Lemma 2 (Inversion for rule GDS-Both). If C ♦ (A ♦? B) then (C ♦ A) and (C ♦ B).
This lemma captures the relation between types with respect to the duality of union andintersection types. It is the general form of two lemmas:
B Lemma 3 (Inversion for Union types). If (A ∨ B) <: C then (A <: C ) and (B <: C ).

ECOOP 2020

29:14

The Duality of Subtyping

Γ`e:A(Typing)Γ ` ok

x:A∈Γ

Γ`x:A

Γ ` okg-var

Γ, x : A1 ` e2 : A2

Γ ` n : IntΓ ` e1 : A1 → A2g-int

Γ ` e2 : A1

Γ ` e1 e2 : A2

Γ ` λx : A1 . e2 : A1 → A2
Γ`e:B

g-app

B <: A
g-sub

Γ`e:A

e1 −→ e2

(Reduction)e1 −→ e10

(λx : A1 . e1 ) v2 −→ [x 7→ v2 ]e1

g-abs

gred-AppAbs

gred-Fune1 e −→ e10 e

e1 −→ e10v e1 −→ v e10

gred-Arg

Figure 6 Typing and reduction for λ∧∨♦ .

B Lemma 4 (Inversion for Intersection types). If C <: (A ∧ B) then (C <: A) and (C <: B).
Finally there is also a duality lemma, which complements reflexivity and transitivity:
I Lemma 3 (Duality). A♦B = B♦A.
This lemma captures the essence of duality, and enables us to switch the mode of therelation by flipping the arguments as well. Furthermore, the duality lemma plays a crucialrole when proving soundness and completeness with respect to the declarative version of
Duotyping, which has duality as an axiom instead. All of these lemmas are used in later
proofs for type soundness.

3.2

Semantics and type soundness

Typing The first part of Figure 6 presents the typing rules of λ∧∨♦ . The rules are standard.
Note that rule g-sub is the subsumption rule: if an expression e has type B and B is asubtype of A then e has type A. Noteworthy, B <: A is the Duotyping relation being usedwith the subtyping mode.
Reduction At the bottom of Figure 6 we show the reduction rules of λ∧∨♦ . Again, thereduction rules are standard. Rule gred-AppAbs is the usual beta-reduction rule, which
substitutes a value v2 for x in the lambda body e1 . Rule gred-Fun and rule gred-Arg are
the standard call-by-value rules for applications.
Type soundness The proof for type soundness relies on the usual preservation and progress
lemmas:B Lemma 5 (Type Preservation). If Γ ` e : A and e −→ e 0 then: Γ ` e 0 : A.
Proof. By induction on the typing relation and with the help of Lemma 3.

J

B Lemma 6 (Progress). If Γ ` e : A then:
1. either e is a value.
2. or e can take a step to e 0 .
Proof. By induction on the typing relation.
JOliveira et al.

Types
Terms
ValuesContext
Mode

29:15

A, B
e
v
Γ
♦

> | ⊥ | Int | A → B | A ∧ B | A ∨ B | X | ∀(X ♦A).B
x | n | λx : A. e | e1 e2 | Λ(X ♦ A).e | e An | λx : A. e | Λ(X ♦ A).e
• | Γ, x : A | Γ, X ♦ A<: | :>

::=
::=
::=
::=
::=

∧∨
(Fk♦
Duotyping)Γ ` A♦BΓ ` okX ♦1 A ∈ ΓΓ ` X ♦2 X
X ♦A ∈ Γ

X ♦A ∈ Γ
gs-ReflTvaraΓ ` B ♦AΓ ` B ♦XΓ ` A♦BΓ ` X ♦B

gs-TVara

Γ, X ♦1 A ` B ♦2 C
gs-TVarbΓ ` (∀X ♦1 A.B) ♦2 (∀X ♦1 A.C )gs-forallkfs∧∨
Figure 7 Syntax and additional rules for Duotyping in Fk♦.

3.3

Summary and Comparison

Besides λ∧∨♦ , which employs the Duotyping relation, we have also formalized a lambda calculus
with union and intersection types using the traditional subtyping relation (λ∧∨<: ). Most of
the metatheory is similar with a great deal of theorems being almost the same. The maindifferences are in the metatheory for subtyping which has to be generalized. For example
both reflexivity and transitivity have to be generalized to operate in the Duotyping relation
instead. The formalization with Duotyping only has two additional lemmas (the duality
lemma and the bound selection lemma), which have no counterparts with subtyping. The∧∨
number of lines of code for the formalization of λ∧∨<: is 596 whereas for λ♦ is 630. The total∧∨∧∨
number of lemmas required for λ<: are 23 and 25 for λ♦ . Following two lemmas in λ∧∨<: arecaptured as one lemma in λ∧∨(Lemma2):♦
Inversion for Union Types This lemma is already stated as Lemma 3: it is the inversionof the subtyping rule for the union types in the traditional subtyping relation. The lemma
states that if the union of two types A and B is the subtype of a type C , then both types A
and B are subtypes of type C .
Inversion for Intersection Types This lemma, which corresponds to Lemma 4, is theinversion of the subtyping rule for the intersection types with the traditional subtyping
relation. It states that if a type C is the subtype of the intersection of two types A and B,
then the type C is a subtype of both types A and B.

4∧∨
The Fk♦calculus

In Section 3 we introduced a simple calculus with union and intersection types using
Duotyping. This section extends that calculus with bounded quantification based on kernel∧∨
F<: . This new variant also employs Duotyping and is called Fk♦. The main aim of thissection is to show that sometimes we can get interesting and novel dual features come for free.
∧∨
In addition to upper bounded quantification of F<: , System Fk♦
provides lower bounded∧∨
quantification as well. Additionally, we also show the type soundness of Fk♦.

ECOOP 2020

29:16

The Duality of Subtyping

4.1

Syntax and Duotyping∧∨
Syntax Figure 7 shows the syntax of the calculus Fk♦. Types >, ⊥, Int, A → B, A ∧ B,
A ∨ B are already introduced in Section 2. Type variable X and a universal quantifier on∧∨type variables ∀(X ♦A).B are the two additional types in Fk♦. Terms x, n, λx : A. e, e1 e2
are already discussed in Section 3.1. Type abstraction Λ(X ♦ A).e and type application e A∧∨
are two additional terms in Fk♦. Values are a subset of terms, consisting of term abstraction,
type abstraction and integers.
∧∨
Duotyping rules for a calculus with union and intersection types are
Duotyping for Fk♦∧∨
presented in Figure 4. Fk♦
has two significant differences in its Duotyping rules in comparison
to Figure 4, which are presented in Figure 7. The first one is the addition of a typing context
in the Duotyping rules. This is important to ensure that type variables are bound. Thus,∧∨
Duotyping for Fk♦
is now of the form Γ ` A ♦ B. The second difference is that there are
four more rules, three of them (rules gs-ReflTvara, gs-TVara, and gs-forallkfs)
were already explained in Section 2.4. Rule gs-TVarb is the dual of rule gs-TVara. We
introduce this rule to eliminate the duality rule.
∧∨
The Duotyping relation for Fk♦
is reflexive and transitive as well:

I Theorem 3 (Reflexivity). Γ ` A♦A.
Proof. By induction on type A.

J

I Theorem 4 (Transitivity). If Γ ` A♦B and Γ ` B♦C then Γ ` A♦C .
Proof. By induction on Γ ` A♦B.
Cases rule gs-topbtma, rule gs-topbtmb, rule gs-int, rule gs-ReflTvar, rule gsTVara, rule gs-lefta, rule gs-righta, rule gs-botha are trivial to prove.
Case rule gs-arrow is proved using the induction hypotheses.
Case rule gs-TVarb can be proved using Lemma 4.
Case rule gs-forallkfs is proved using the induction hypotheses.
Case rule gs-leftb can be proved using an additional Lemma 8.
Case rule gs-rightb also uses Lemma 8.
Case rule gs-bothb is proved using the induction hypotheses.
J
The auxiliary lemmas for transitivity are described next and are essentially the same as
in Section 3.1.
B Lemma 7 (Bound Selection). If Γ `e♦d♦B then Γ ` A♦B.
B Lemma 8 (Inversion for rule GDS-Both). If Γ ` C ♦ (A ♦? B) then Γ ` (C ♦ A) and (C ♦B).
There is also a duality lemma:
I Lemma 4 (Duality). Γ ` A♦B = Γ ` B♦A.
Finally, We also proved weakening and the narrowing lemmas for Duotyping calculus.
∧∨∧∨
Here we briefly compare the narrowing lemma for Fk<:and Fk♦:∧∨B Lemma 9 (Fk<:Narrowing Lemma).
Γ, X <: A, Γ1 ` C <: D

If Γ ` A <: B and Γ, X <: B, Γ1 ` C <: D thenOliveira et al.

29:17

Γ`e:A

(Typing)Γ ` ok

x:A∈Γ

Γ`x:A

Γ ` okg-var

Γ ` e1 : A1 → A2

Γ, x : A1 ` e2 : A2

Γ ` n : Intg-intΓ ` e2 : A 1

Γ ` λx : A1 . e2 : A1 → A2
Γ`e:B

g-app

Γ ` e1 e 2 : A 2

Γ ` B <: A
g-subsΓ`e:AΓ, X ♦ A ` e : BΓ ` e : ∀(X ♦A).BΓ ` ΛX ♦ A. e : ∀(X ♦A).B

g-tabsΓ ` C ♦A
g-tappΓ ` e C : [X 7→ C ]B

e1 −→ e2

(Reduction)e1 −→ e10

(λx : A1 . e1 ) v2 −→ [x 7→ v2 ]e1

g-abs

gred-AppAbs

e1 e −→ e10 e

e1 −→ e10gred-Funv e1 −→ v e10

gred-Arg

e1 −→ e10(ΛX ♦ A. e1 ) B −→ [X 7→ B]e1

gred-TAppTAbs

e1 A −→ e10 A

gred-TFun

Figure 8 Typing and reduction of the duotyped kernel F<: .

∧∨B Lemma 10 (Fk♦Narrowing Lemma).
Γ, X ♦1 A, Γ1 ` C♦2 D

If Γ ` A ♦1 B and Γ, X ♦1 B, Γ1 ` C♦2 D thenLemma 9 exploits only the subtyping relation while Lemma 10 exploits our Duotyping relation.
Lemma 10 illustrates how lower and upper bounds are captured under a unified mode relationin narrowing. Like the transitivity statement using a Duotyping formulation, one can thinkof the Duotyping narrowing lemma as actually two distinct lemmas: one for narrowing ofupper bounds and another for narrowing of lower bounds. Also, it is important to note that
Lemma 10 is using two modes ♦1 and ♦2 . ♦1 is the relation between types A, B and the typevariable X . Whereas, ♦2 is the relation between type C and type D. Those two relations do
not need to be the same.

4.2

Semantics and type soundness∧∨
Typing The first part of Figure 8 presents the typing rules of Fk♦. The first five rules are
standard and are already explained in Section 2.1. Rules g-tabs and g-tapp are the two∧∨
additional rules in Fk♦. Rule g-tabs is similar to the standard rule for type abstractions
in F<: except that it generalizes the subtyping bound to a ♦ bound, which could either besubtyping or supertyping. Rule g-app again differs from the rule for type applications in F<:
by using a ♦ bound instead of just a subtyping bound. These two rules rules are noteworthy
because they also illustrate an advantage of using Duotyping in the typing relation. Without
Duotyping we would need multiple typing rules to capture different variations of the bounds.

Reduction The last part of Figure 8 presents the reduction rules of our calculus. Again,
reduction rules are standard except for the rule gred-TAppTAbs. In rule gred-TAppTAbs
the duality relation captures both upper and the lower bounds. Rule gred-TFun is thestandard reduction rule for the type applications.
Type Soundness We proved the type soundness for our calculus. All the proofs are

ECOOP 2020

29:18

The Duality of Subtyping

formalized in Coq theorem prover.
B Lemma 11 (Type Preservation). If Γ ` e : A and e −→ e 0 then: Γ ` e 0 : A.
Proof. By induction on the typing relation.
Case rules g-var, g-int, g-abs, g-tabs, and g-subs are trivial to solve.
Case rule g-app uses Theorem 3 and Lemma 4.
Case rule g-tapp uses Theorem 3.
J
B Lemma 12 (Progress). If Γ ` e : A then:
1. either e is value.
2. or e can take step to e 0 .
Proof. By induction on the typing relation.
Case rules g-var, g-int, g-abs, g-tabs, and g-subs are trivial to solve.
Case rule g-app requires canonical forms.
Case rule g-tapp requires canonical forms.
J

4.3

Summary and Comparison∧∨
Besides Fk♦, which employs the Duotyping relation, we have also formalized a calculus∧∨
Fk<: : an extension of kernel F<: (only with upper bounded quantification) with union andintersection types using the traditional subtyping relation. The essential differences are
similar to what we already discussed in Section 3.3. The formalization with Duotyping only
has two additional lemmas (the duality lemma and the bound selection lemma), besides a∧∨
few minor auxiliary lemmas. The number of lines for proof for the formalization of Fk<:
is
∧∨
∧∨
∧∨
1648 whereas for Fk♦ is 1770. The total lemmas required for Fk<: are 74 and 81 for Fk♦ .
∧∨∧∨We emphasize that one significant difference between Fk<:and Fk♦is the additional lower∧∨
bounded quantification provided by Fk♦ . This is an extra feature which comes essentiallyfor free with Duotyping.

5

A Case Study on Duotyping

In this section we present an empirical case study, which we conducted to validate some of
the benefits of Duotyping. Overall, the results of our case study indicate that: Duotyping does
allow for compact specifications; the complexity of developing formalization with Duotyping iscomparable to similar developments using traditional subtyping relations; transitivity proofs
are often significantly simpler; and Duotyping is a generally applicable technique.

5.1

Case Study

We formalized a number of different calculi using Duotyping. All the proofs and metatheory
are mechanically checked by the Coq theorem prover. We also formalized a few traditional
subtyping systems for comparison. Table 1 shows a brief overview of various systems that we∧∨formalized. λ<: , λ∧∨<: , Fk<: , Fk<: and FF <: are the traditional subtyping systems. The Coq
formalizations for the traditional subtyping systems are based on existing Coq formalizations
from the locally nameless representation with cofinite quantification tutorial and repository

Oliveira et al.

29:19(https://www.chargueraud.org/softs/ln/) by Charguéraud [18]. The formalizations of∧∨
λ♦ , λ∧∨♦ , Fk♦ , Fk♦ and FF ♦ are their respective Duotyping formulations, and modify theoriginal ones with traditional subtyping. Subscript <: represents a calculus with traditional
subtyping whereas ♦ represents a calculus with Duotyping. Superscript ∧∨ is the notation
for a system with intersection and union types. Subscript k corresponds to the kernel version
of a variant of F<: , while subscript F corresponds to the corresponding full version. We also
formalized a simple polymorphic system without bounded quantification using Duotyping. We
have two Duotyping variants for this polymorphic type system without bounded quantification.
One without union and intersection types (F♦ ) and another with union and intersection
types (F♦∧∨ ).
In Table 1, the last column (Transitivity) summarizes the proof technique used in eachsystem to prove transitivity. Recall the transitivity lemma (using the Duotyping formulation):
I Theorem 5 (Transitivity). If A♦B and B♦C then A♦C .
Induction on the middle type means induction on type B (or well-formed type B for
polymorphic systems), whereas induction on the Duotyping relation means induction on
A♦B.
Research Questions Section 1 discussed benefits of using Duotyping. This section attempts
to quantify some of these benefits. More concretely, we answer the following questions inthis section:
Does Duotyping provide shorter specifications?
Does Duotyping increase the complexity of the formalization and metatheory of thelanguage?
Does Duotyping make transitivity proofs simpler?
Is Duotyping a generally applicable technique?
We follow an empirical approach to answer these questions and address each question in
a separate (sub)section. Obviously a precise measure for complexity/simplicity is hardto obtain. We use SLOC for the formalization and proofs as an approximation. All theformalizations are written in the same Coq style to ensure that the comparisons are fair.

5.2

Does Duotyping provide shorter specifications?

This section answers our first question. In short our case study seems to support thisconclusion. The declarative Duotyping rules of all the systems that we formalized are shownin Table 2. Please note that the formulation also contains the duality rule. λ♦ has thebasic set of Duotyping rules. These rules are common in all of the systems. λ∧∨♦ has thesubtyping rules for intersection types and union types in addition to the rules from λ♦ .
F♦ contains two more rules (rules gds-ReflTvarp and gds-forallfsp) in addition to
the rules from λ♦ . F♦∧∨ has all the rules from λ♦ , λ∧∨♦ and F♦ . Fk♦ has three additional
subtyping rules gds-ReflTvar, gds-TVar, and gds-forallkfs in addition to the rules∧∨
from λ♦ . Fk♦
has all the rules from λ♦ , λ∧∨♦ , and Fk♦ . FF ♦ has an additional subtyping
rule gds-forallffs.
Comparison with systems using traditional subtyping. Table 3 shows the numberof rules and features for different calculi formulated with subtyping and Duotyping. In ourformulation, λ<: has 3 types >, Int, and A → B. This requires 3 subtyping rules to capture
the subtyping relation of these 3 types. If we wanted to support the ⊥ type in λ<: we would
need to add 1 more subtyping rule. In the table we express the extra rules required for extra

ECOOP 2020

29:20The Duality of Subtyping

Name
λ<:
λ♦

Description
STLC with subtyping
STLC with Duotyping

SLOC
537
583

λ∧∨
<:

595

Fk<:

STLC with subtyping, union types
and intersection types
STLC with Duotyping, union types
and intersection types
Simple polymorphic system with
Duotyping and without bounded
quantification
Simple polymorphic system with
Duotyping, union types and intersection types and without bounded
quantification
System F<: kernel

Fk♦

System F<: kernel with Duotyping

1579

∧∨
Fk<:

1648

FF <:

System F<: kernel with subtyping,union types and intersection types
System F<: kernel with Duotyping,union types and intersection types
System full F<:

FF ♦System full F<: with Duotyping

1786

λ∧∨
♦
F♦

F♦∧∨

∧∨
Fk♦

623
1466

Transitivity
By induction on the middle type.
By induction on the Duotyping relation.
By induction on the middle type.
By induction on the Duotyping relation.
By induction on the Duotyping relation.

1546

By induction on the Duotyping relation.

1542

By induction on the (well-formed)
middle type.
By induction on the Duotyping relation.
By induction on the (well-formed)
middle type.
By induction on the Duotyping relation.
By induction on the (well-formed)
middle type.
By induction on the (well-formed)
middle type.

1770
1518

Table 1 Description of all systems.

features as (+n), where n is the number of extra rules. Duotyping supports ⊥ for free by
exploiting the dual nature of > with the help of duality rule. Systems with more rules follow
the same approach for traditional systems i.e more types require more subtyping rules. If
we wanted to support the ⊥ type in λ∧∨<: we also need 1 additional rule. To further extend
our discussion to the polymorphic systems with bounded quantification, we would need 4
additional rules in Fk<: (1 for ⊥ type and 3 for lower bounded quantification). Similarly wewould need 4 additional rules to support lower bounds and lower bounded quantification in
∧∨
Fk<:
.
In summary, in the systems that we compared Duotyping has a similar number of rules tosystems with subtyping, but it comes with extra features. If we wanted to add those features
to systems with traditional subtyping, then that would generally result in more rules for the
traditional versions compared to Duotyping. This would also have an impact in the SLOC ofthe metatheory, increasing the metatheory for those systems considerably.

5.3

Does Duotyping increase the complexity of the formalization andmetatheory of the language?

At first, one may think that Duotyping increases the complexity of formalization and metatheory of the language, since it provides interesting extra features and generalizations normally

Oliveira et al.

Name
λ♦

29:21

Duotyping Rules(λ♦ Duotyping)A♦B
A1 ♦ A2A ♦ e♦dgds-topbtm

Int ♦ Int

gds-int

B1 ♦ B2

A1 → B1 ♦ A2 → B2

gds-arrow

B ♦A
A♦B

gds-dual

λ∧∨
♦
(λ∧∨
Duotyping plus all rules from λ♦ )
♦

A♦B
A♦C

B ♦C

(A ♦? B) ♦ C

gds-Left(A ♦? B) ♦ C

A♦B
gds-RightA♦CA ♦ (B ♦? C )gds-bothF♦(F♦ Duotyping plus all rules from λ♦ )

A♦B

A♦B
X ♦X

gds-ReflTvarp(∀X .A) ♦ (∀X .B)

gds-forallfsp

F♦∧∨(F♦∧∨ Duotyping plus all rules from λ♦ , λ∧∨and F♦ )
♦

A♦B

Fk♦
Γ ` A♦B(Fk♦ Duotyping plus all rules from λ♦ )Γ ` okX ♦1 A ∈ ΓΓ ` X ♦2 X

X ♦A ∈ Γ
gds-ReflTvar

Γ ` A♦BΓ ` X ♦B

gds-TVarΓ, X ♦1 A ` B ♦2 C
Γ ` (∀X ♦1 A.B) ♦2 (∀X ♦1 A.C )gds-forallkfs

∧∨
Fk♦
∧∨
(Fk♦
Duotyping plus all rules from λ♦ , λ∧∨and Fk♦ )♦Γ ` A♦BFF ♦Γ ` A♦B(FF ♦ Duotyping plus all rules from Fk♦ excluding rule gs-forallkfs andunion/intersection rules)Γ ` A | ♦1 |♦2 B

e B) ` A1 ♦2 B1
Γ, X ♦1 (A ♦

Γ ` (∀X ♦1 A.A1 ) ♦2 (∀X ♦1 B.B1 )gds-forallffs

Table 2 Declarative Duotyping rules of all systems.

ECOOP 2020

29:22

The Duality of Subtyping

System Subtyping
rules countλ<:3 (+1)
λ∧∨9 (+1)<:
Fk<:
5 (+4)

System Duotyping
rules count
λ♦
4
λ∧∨
7
♦
Fk♦
7

Duotyping extra features

lower bounds in λ♦lower bounds in λ∧∨♦lower bounds and lower bounded
quantification in Fk♦
∧∨
∧∨
Fk<:
11 (+4)Fk♦
10
lower bounds and lower bounded∧∨
quantification in Fk♦
Table 3 Comparing the features and number of rules with subtyping and Duotyping.

Subtyping
SLOC
Duotyping
SLOC
SystemSystem
λ<:
537
λ♦
583
∧∨
λ∧∨
595
λ
623
<:
♦
Fk<:
1542
Fk♦
1579
∧∨
∧∨
Fk<:
1648
Fk♦
1770
Table 4 SLOC of traditional subtyping and Duotyping systems.

come at a cost. Interestingly, Duotyping does not add significant extra complexity in theformalization and metatheory of the language. Table 4 shows the SLOC for formalizations
using traditional subtyping and Duotyping systems. The lines of code for λ∧∨<: are 595 and∧∨∧∨the lines of code for λ♦ are 623. Similarly, the lines of code for Fk<: are 1648 and 1770 for∧∨
Fk♦. Although SLOC for Duotyping systems are slightly more than traditional subtyping
systems, the Duotyping systems come with extra features. Nevertheless the mechanization
effort is roughly the same for version with and without Duotyping. Also, as illustrated in
Sections 3 and 4, the vast majority of the lemmas/metatheory for calculi with Duotyping are
similar to traditional systems with subtyping.

5.4

Does Duotyping make transitivity proofs simpler?

Transitivity is often the most difficult property to prove in the metatheory of a language with
subtyping. Table 1 highlights a brief comparison between the techniques for the transitivity
proof of various systems. Transitivity of systems with Duotyping is generally proved byinduction on the Duotyping relation. One exception is FF ♦ where induction on the Duotyping
does not work. As discussed in Section 2.5 Duotyping allows us to simplify the transitivity
proof by using a different inductive argument.
Table 5 shows the SLOC for transitivity proofs of various systems. The SLOC for λ<:transitivity proof are 7 and the SLOC for λ♦ transitivity proof are 4. Similarly, the SLOC∧∨∧∨
for Fk<:transitivity proof are 38 and 18 for the transitivity proof of Fk♦. This evaluationshows that Duotyping always allows us to reduce the size of the transitivity proof. Again,
it is important to note that Duotyping also provides extra features of lower bound andlower bounded quantification. Despite these additional features in Duotyping systems, theirtransitivity proofs are shorter than the traditional systems with subtyping.
However we could not employ this proof technique in our Duotyping version of full F<:(FF ♦ ). The problem is related to narrowing, which in FF ♦ is closely coupled with transitivity.
Despite that we could still apply the technique to most systems with Duotyping, and even forOliveira et al.

29:23

SubtypingTransitivity
System
SLOC
λ<:
7
λ∧∨
13
<:
Fk<:
26
∧∨
Fk<:
38
Table 5 SLOC for transitivity proofs.

Duotyping
System
λ♦
λ∧∨
♦
Fk♦
∧∨
Fk♦

Transitivity
SLOC
4
11
13
18

FF ♦ we can still prove transitivity using the same technique as in the traditional F<: (i.e.
using the middle type as the inductive argument).

5.5

Is Duotyping a generally applicable technique?

Our case studies indicate that Duotyping is generally an applicable technique. In all thesystems that we have tried to use Duotyping, we have managed to successfully apply it.
Furthermore we believe that Duotyping can be essentially applied to any system with a
traditional subtyping relation. The most complex system where we have employed Duotyping
is FF ♦ . In FF ♦ universal quantification allows Duotyping between the bounds, generalizing
the universal quantification presented in Section 4. Rule gds-forallffs in FF ♦ employse B:
two operations |♦1 |♦2 and A ♦|♦1 |♦2| <: |♦2 = ♦2
| :> |♦2 = ♦2eBA♦e B= BA <:e B= AA :>|♦1 |♦2 takes two modes ♦1 and ♦2 as input, and flips ♦2 if ♦1 is subtyping, otherwise it
returns ♦2 . This operation chooses the mode to check the relationship between the boundseBof the two universal quantifiers being compared for Duotyping. The second operation A ♦selects the bounds to use in the environment when checking the Duotyping of the bodies of
the universal quantifiers. It takes a mode ♦ and two types A B as inputs, and returns thesecond type if the mode is subtyping, otherwise it returns the first type.

6

Related Work

Apart from informally observing duality of type system features, as far as we known, formally
exploiting duality in subtyping relations has not been investigated in the past. However thereis plenty of work on uses of duality in programming language theory. Furthermore there isrelated work on type systems that exploit various generalizations for added expressive poweror economy in metatheory and implementation. We discuss these next.

6.1

Duality in Logic and Programming Language Theory

In type theory [5] and/or category theory [30, 14] duality occurs in various forms. For
instance, the duality between sum and product types is well-known in both type and category
theory. Properties about such types often explicitly acknowledge duality. Many properties

ECOOP 2020

29:24

The Duality of Subtyping

about sum types are presented as dual properties of corresponding properties on producttypes and vice-versa. Our Lemma 2 is an example of a property that applies to both union
and/or intersection types. In this property duality is not only acknowledged, but directly
exploited in the lemma itself to provide a generalized property that can be specialized to one
construct and its dual. Various other dualities between constructs are known and exploited
in various ways in type and/or category theory. For example, existential and universal
quantification can be captured by an encoding by one through the other. The type ∃α. A
can be encoded as ∀β.(∀α. A → β) → β, which requires a kind of CPS translation [20] of thecorresponding terms. Similar encodings exist for sums and products.
In the field of proof-theoretic semantics [25] and in natural deduction the concept ofharmony is used to describe introduction and elimination rules that are in some sense dual.
For instance, the usual rules for introduction and elimination of conjunction are in perfectharmony. The inversion principles by Prawitz [38] are a general procedure to associate to
any arbitrary collection of introduction rules a specific collection of elimination rules. The
elimination rules are in harmony with the given collection of introduction rules. Prawitz
inversion principles attempt to capture harmony in a more precise way, directly expressing it
formally. Therefore inversion principles have similar considerations to Duotyping in termsof expressing some form of duality directly in a formalism. However inversion principles
focus on introduction and/or elimination rules, while Duotyping is focused on subtyping.
Nevertheless in future work we are interested in exploiting the use of duality in the typing
relation more. We believe that the notion of harmony and inversion principles could be quite
helpful in such work.
Double-line rules [21] are deduction rules that can be read both from top to bottom(as usual) and also from bottom to top. In other words they express two standard (dual)
deduction rules in a single double-line rule. Like Duotyping, double-line rules aim at expressing
a form of duality in a single rule. Unlike Duotyping, double-line rules are concerned with(dual) rules where the premises and conclusions of one rule become the conclusions andpremises of the other rule, respectively.
Bernardi et al. [10] explain duality relations in the context in session types. Binary
session types have two endpoints connected through one communication channel. In session
types, connected endpoints should have a dual relation in their session types. The duality
relation in session types is related to types and may have various interpretations. In contrast
Duotyping is about subtyping (or supertyping).
The duality between data and codata is well-known in programming language theory [14].
Data types and codata types are duals in the sense that data types are defined in termsof constructors while codata types are defined in terms of destructors. More recently, suchduality has been exploited in language design [35, 13] to provide an automatic way to switch
between programs defined on datatypes and equivalent programs defined on codata types.
The use of duality in this line of work is quite different from ours.

6.2

Generalizations in Type Systems and Type Theory

Pure type systems (PTSs) [45, 31, 2, 28, 41, 48] capture a generalization of various typesystems (F, F ω , λP). Typing rules of multiple type systems are expressed in pure type systems
via parameterization. PTSs are parameterized by three sets: a set of sorts; a set of axioms;
and a set of rules. Concrete type systems (such as System F ), are recovered with concrete
instantiations of those sets. Pure type systems with subtyping [48] are a variant of pure typesystems that captures a family of type systems with subtyping. This variant captures only
the upper bounds. It does not provide subtyping generalization with both upper and theOliveira et al.

29:25

lower bounded quantification like our Duotyping generalizations of F<: . Pure subtype systems[26] is a family of calculi based on subtyping only (and without a typing relation). Thissystem eliminates the need of typing and presents an alternative to typing using subtyping
only. Pure subtype systems support upper bounded quantification, but no lower bounded
quantification.
Modal Type Theory Modal type theory [33] is an extension of type theory which provides
type rules using modalities. Modal type theory can represent a proposition as types which
may be proved based upon the deduction rules in a given context. Modal type theory also
employs modes, for instance possibility and necessity [42, 33]. There are many type systems
that use modes to generalize typing relations. One can view Duotyping as a simple instanceof a relation with a mode. In Duotyping the mode is either subtyping or supertyping.
Bi-directional type checking Bi-directional type checking [37, 23] also employs a mode,
but in the typing relation instead. Bi-directional type checking is a common technique,used in implementations of programming languages, that can eliminate redundant type
annotations. Bi-directional type-checking is also employed is several type systems, especiallythose where full type inference is undecidable [37, 24]. In such cases only partial inference
methods are feasible in practice, which means that some type annotations are necessary.
Bi-directional type checking is useful in such cases, allowing the type information to be easily
propagated without requiring further (redundant) annotations. The modes in bi-directional
type-checking are checking or synthesis. Checking checks a given term against a given type,whereas the synthesis infers the type based upon the available information in the context.
Unified Subtyping Unified subtyping [46] is a technique that can be used in dependently
typed systems supporting unified syntax to model typing and subtyping in a single relation.
The single unified subtyping relation generalizes both typing and subtyping. Like Duotyping,
unified subtyping can also help reducing language metatheory and duplication. However
unified subtyping is orthogonal to Duotyping and does not exploit duality of features. We
believe that both techniques can complement each other.
Bounded quantification and generalizations System F<: [16] is extensively studied due
to its feature of bounded quantification. F-bounded quantification [15] is a generalization ofbounded quantification to handle recursive types. Although we are not aware of an extensionof F<: with lower bounded quantification, such notion has appeared before in some calculi.
For instance, Igarashi and Viroli [27] have pointed out correspondence between use-site
variance and existential types and, in order to capture contravariance, they introduced
lower-bounded existential types.
One generalization of F<: is studied by Amin and Rompf [4], which formalizes type bounds
in Scala. Type bounds is an interesting feature in Scala as elaborated by the following code
(code extended from Section 2.4):class TypeBoundsCollection[S >: GraduateStudent <: Student](obj: S) {def student: S = obj}

While in our variants of F<: we support either lower bounded quantification or upper bounded
quantification (but not both at once), Scala’s type bounds allow both upper and lower bounds
at once. This is clearly more expressive than what we have, but it comes with its own
problems. Formalisms with Scala-like type bounds often need to include a transitivity axiom(and thus are non-algorithmic) and they have to deal with the bad bounds problem. In
contrast our simpler extension of type bounds is comparable in complexity to F<: ’s upper

ECOOP 2020

29:26

The Duality of Subtyping

bounded quantification, and there is a set of algorithmic subtyping rules without a built-in
transitivity axiom.
Intersection and Union Types Intersection and union types [6, 22, 32, 36] are getting
significant attention in recent years, and are used in several modern programming languages(including Scala, Flow or TypeScript). Reynolds [39] was the first to promote the use ofintersection types in programming languages. Later on, Pierce [36] studied intersection
types, union types and polymorphism combined in a typed λ-calculus. Recently, Muehlboeck
and Tate [32] presented a generalized formulation of calculi with union and intersection
types. They demonstrated it with the help of Ceylon programming language [29]. Dunfield[22] presented an expressive calculus with a merge operator and unrestricted intersection
types with union types. We exploit the duality of union and intersection types to illustrate
Duotyping. Our Duotyping calculi manages to capture the six common rules for unions andintersections using three rules only (plus the duality rule), which provides a simple illustrative
example of the use of duality.

7

Conclusion

In this paper, we have presented a generalization of subtyping using a relation parameterized
by a mode. We call this relation Duotyping. Duotyping allows formalizations of subtyping to
exploit duality between features directly in the formalism, and provides multiple benefits overtraditional subtyping relation. It shortens subtyping specifications, provides dual features
essentially for free and simplifies the transitivity proof in many calculi. An example ofan extra dual feature that is obtained for free, with a Duotyping design, is lower bounded
quantification. Lower bounded quantification arises naturally when we apply the Duotyping
to conventional F<: type systems. To validate the benefits of Duotyping, we have conducted
an empirical evaluation, implemented multiple calculi using both a traditional subtyping
relation and a Duotyping formulation, and compared the resulting formalizations.
Duality has been studied extensively in several contexts in the past. However, as far as
we know, our work is the first to study duality in the context of subtyping. Future work on
Duotyping includes applying the Duotyping methodology to several other forms of subtypingthat are of practical interest. We are particularly interested to apply Duotyping to systems
that include a feature, but have no obvious dual feature. We hope to discover potentiallynew features that are useful for programming. Furthermore, we hope to scale the approachso that it can be used in real programming language implementations, leading to morecompact and consistent implementations of subtyping. Another domain for future workon Duotyping is the typing relation. Although we already have some simple cases where
Duotyping also provides benefits for typing (see Section 4), we acknowledge that introductionand elimination rules for some (dual) constructs introduce new challenges. For instance,
more complex introduction and elimination forms for union types and intersection types canbe quite different [22]. Further exploration is needed to see how much Duotyping can help in
typing relations for calculi with such features. More generally, Duotyping promotes the use ofduality in language design. We envision that in the future new language designs can exploit
duality to ensure consistency between various language constructs, by exploiting techniques
similar to Duotyping.
References
1

Andreas Abel and Dulma Rodriguez. Syntactic metatheory of higher-order subtyping. In
International Workshop on Computer Science Logic, pages 446–460. Springer, 2008.

Oliveira et al.

2
3
4

5
6
7
8

9
10

11
12
13

14
15
16
17
18
19
20
21
22
23
24
25

29:27

Robin Adams. Pure type systems with judgemental equality. Journal of Functional Programming, 16(2):219–246, 2006.
Nada Amin, Adriaan Moors, and Martin Odersky. Dependent object types. In 19th International Workshop on Foundations of Object-Oriented Languages, number CONF, 2012.
Nada Amin and Tiark Rompf. Type soundness proofs with definitional interpreters. In
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages,
POPL 2017, 2017.
Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth through
Proof. Academic Press, Inc., 1986.
Franco Barbanera, Mariangiola Dezaniciancaglini, and Ugo Deliguoro. Intersection and union
types: syntax and semantics. Information and Computation, 119(2):202–230, 1995.
Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda modeland the completeness of type assignment 1. The journal of symbolic logic, 48(4):931–940, 1983.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicael Courant, Jean-Christophe Filliatre,
Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The
coq proof assistant reference manual: Version 6.1. 1997.
Jon Barwise and Robin Cooper. Generalized quantifiers and natural language. In Philosophy,
language, and artificial intelligence, pages 241–301. Springer, 1981.
Giovanni Bernardi, Ornela Dardha, Simon J Gay, and Dimitrios Kouzapas. On duality relations
for session types. In International Symposium on Trustworthy Global Computing, pages 51–66.
Springer, 2014.
Jan Bessai, Boris Düdder, Andrej Dudenhefner, Tzu-Chun Chen, and Ugo de’Liguoro. Typingclasses and mixins with intersection types. arXiv preprint arXiv:1503.04911, 2015.
Gavin Bierman, Martín Abadi, and Mads Torgersen. Understanding typescript. In European
Conference on Object-Oriented Programming, pages 257–281. Springer, 2014.
David Binder, Julian Jabs, Ingo Skupin, and Klaus Ostermann. Decomposition diversity withsymmetric data and codata. Proceedings of the ACM on Programming Languages, 4(POPL):30,
2019.
Richard Bird and Oege de Moor. The Algebra of Programming. Prentice-Hall, 1996. URL:
http://www.cs.ox.ac.uk/publications/books/algebra/.
Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John C Mitchell. F-boundedpolymorphism for object-oriented programming. In FPCA, volume 89, pages 273–280, 1989.
Luca Cardelli, Simone Martini, John C Mitchell, and Andre Scedrov. An extension of systemf with subtyping. Information and Computation, 109(1-2):4–56, 1994.
Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism.
ACM Computing Surveys (CSUR), 17(4):471–523, 1985.
Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning,
2011.
Avik Chaudhuri. Flow: a static type checker for javascript. SPLASH-I In Systems, Programming, Languages and Applications: Software for Humanity, 2015.
Oliver Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation.
Mathematical Structures in Computer Science, 2(4):361–391, December 1992.
Kosta Došen. Logical constants as punctuation marks. Notre Dame J. Formal Logic, 30(3):362–
381, 06 1989. doi:10.1305/ndjfl/1093635154.
Joshua Dunfield. Elaborating intersection and union types. Journal of Functional Programming,24(2-3):133–165, 2014.
Joshua Dunfield and Neel Krishnaswami. Bidirectional typing. arXiv preprint arXiv:1908.05839,
2019.
Joshua Dunfield and Neelakantan R. Krishnaswami. Complete and easy bidirectional typechecking for higher-rank polymorphism. In ICFP, 2013.
Gerhard Gentzen. Untersuchungen über das logische Schliessen. Mathematische Zeitschrift,
39:176–210, 405–431, 1934.

ECOOP 2020

29:28

The Duality of Subtyping

26
27

28
29
30
31
32
33
34

35
36
37
38

39
40

41
42
43
44
45

46
47

48

DeLesley S. Hutchins. Pure subtype systems. 2010.
Atsushi Igarashi and Mirko Viroli. On variance-based subtyping for parametric types. In
ecoop, pages 441–469, Malaga, Spain, June 2002. sv. To appear in ACM Transactions on
Programming Languages and Systems.
LSV Jutting. Typing in pure type systems. Information and Computation, 105(1):30–41, 1993.
Gavin King. The ceylon language specification, version 1.0, 2013.
Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts
in Mathematics. Springer, 2 edition, 1998.
James McKinna and Robert Pollack. Pure type systems formalized. In International Conference
on Typed Lambda Calculi and Applications, pages 289–305. Springer, 1993.
Fabian Muehlboeck and Ross Tate. Empowering union and intersection types with integrated
subtyping. Proceedings of the ACM on Programming Languages, 2(OOPSLA):112, 2018.
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory.
ACM Transactions on Computational Logic (TOCL), 9(3):23, 2008.
Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Sebastian Maneth, Stéphane
Micheloud, Nikolay Mihaylov, Michel Schinz, Erik Stenman, and Matthias Zenger. An overview
of the scala programming language. Technical report, 2004.
Klaus Ostermann and Julian Jabs. Dualizing generalized algebraic data types by matrix
transposition. In European Symposium on Programming, pages 60–85. Springer, 2018.
Benjamin C Pierce. Programming with intersection types, union types, and polymorphism.
2002.
Benjamin C. Pierce and David N. Turner. Local type inference. ACM Trans. Program. Lang.
Syst., 22(1), 2000.
Dag Prawitz. Proofs and the meaning and completeness of the logical constants. In Essays
on Mathematical and Philosophical Logic. Synthese Library (Studies in Epistemology, Logic,
Methodology, and Philosophy of Science), 1979.
John C Reynolds. Preliminary design of the programming language forsythe. 1988.
Tiark Rompf and Nada Amin. Type soundness for dependent object types (dot). In Proceedingsof the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming,
Systems, Languages, and Applications, OOPSLA 2016, 2016.
Paula Severi and Erik Poll. Pure type systems with definitions. In International Symposiumon Logical Foundations of Computer Science, pages 316–328. Springer, 1994.
Alex K Simpson. The proof theory and semantics of intuitionistic modal logic. 1994.
Martin Steffen and Benjamin Pierce. Higher-order subtyping. 1994.
Tarmo Uustalu and Varmo Vene. Comonadic notions of computation. Electronic Notes in
Theoretical Computer Science, 203(5):263–284, 2008.
LS van Benthem Jutting, James McKinna, and Robert Pollack. Checking algorithms for puretype systems. In International Workshop on Types for Proofs and Programs, pages 19–61.
Springer, 1993.
Yanpeng Yang and Bruno C. d. S. Oliveira. Unifying typing and subtyping. Proceedings of
the ACM on Programming Languages, 1(OOPSLA):47, 2017.
Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn, Benjamin Chung, Jeff Bezanson,
and Jan Vitek. Julia subtyping: a rational reconstruction. Proceedings of the ACM on
Programming Languages, 2(OOPSLA):113, 2018.
Jan Zwanenburg. Pure type systems with subtyping. In International Conference on Typed
Lambda Calculi and Applications, pages 381–396. Springer, 1999.