Consistent Subtyping for All
NINGNING XIE, The University of Hong Kong, China
XUAN BI, The University of Hong Kong, China
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China
TOM SCHRIJVERS, KU Leuven, Belgium
Consistent subtyping is employed in some gradual type systems to validate type conversions. The original
definition by Siek and Taha serves as a guideline for designing gradual type systems with subtyping. Polymorphic types à la System F also induce a subtyping relation that relates polymorphic types to their instantiations.
However Siek and Taha’s definition is not adequate for polymorphic subtyping. The first goal of this paper is to
propose a generalization of consistent subtyping that is adequate for polymorphic subtyping, and subsumes theoriginal definition by Siek and Taha. The new definition of consistent subtyping provides novel insights withrespect to previous polymorphic gradual type systems, which did not employ consistent subtyping. The second
goal of this paper is to present a gradually typed calculus for implicit (higher-rank) polymorphism that uses
our new notion of consistent subtyping. We develop both declarative and (bidirectional) algorithmic versions
for the type system. The algorithmic version employs techniques developed by Dunfield and Krishnaswami
for higher-rank polymorphism to deal with instantiation. We prove that the new calculus satisfies all static
aspects of the refined criteria for gradual typing. We also study an extension of the type system with staticand gradual type parameters, in an attempt to support a variant of the dynamic criterion for gradual typing.
Assuming a coherence conjecture for the extended calculus, we show that the dynamic gradual guarantee ofour source language can be reduced to that of λB, which, at the time of writing, is still an open question. Mostof the metatheory of this paper, except some manual proofs for the algorithmic type system and extensions,has been mechanically formalized using the Coq proof assistant.
ACM Reference Format:
Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2010. Consistent Subtyping for All. ACM
Trans. Web 9, 4, Article 39 (March 2010), 85 pages. https://doi.org/0000001.0000001

1

INTRODUCTION

Gradual typing [Siek and Taha 2006] is an increasingly popular topic in both programming language practice and theory. On the practical side there is a growing number of programming languages adopting gradual typing. Those languages include Clojure [Bonnaire-Sergeant et al. 2016],
Python [Lehtosalo et al. 2006; Vitousek et al. 2014], TypeScript [Bierman et al. 2014], Hack [Verlaguet 2013], and the addition of Dynamic to C# [Bierman et al. 2010], to name a few. On thetheoretical side, recent years have seen a large body of research that defines the foundations ofgradual typing [Cimini and Siek 2016, 2017; Garcia et al. 2016], explores their use for both functionaland object-oriented programming [Siek and Taha 2006, 2007], as well as its applications to many
Authors’ addresses: Ningning Xie, The University of Hong Kong, Hong Kong, China, nnxie@cs.hku.hk; Xuan Bi, The
University of Hong Kong, Hong Kong, China, xbi@cs.hku.hk; Bruno C. d. S. Oliveira, The University of Hong Kong, Hong
Kong, China, bruno@cs.hku.hk; Tom Schrijvers, KU Leuven, Leuven, Belgium, tom.schrijvers@cs.kuleuven.be.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and thefull citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored.
Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires
prior specific permission and/or a fee. Request permissions from permissions@acm.org.
© 2009 Copyright held by the owner/author(s). Publication rights licensed to the Association for Computing Machinery.
1559-1131/2010/3-ART39 $15.00
https://doi.org/0000001.0000001

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39

39:2

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijversother areas [Bañados Schwerter et al. 2014; Castagna and Lanvin 2017; Jafery and Dunfield 2017;
Siek and Wadler 2016].
A key concept in gradual type systems is consistency [Siek and Taha 2006]. Consistency weakens
type equality to allow for the presence of unknown types ⋆. In some gradual type systems with
subtyping, consistency is combined with subtyping to give rise to the notion of consistent subtyping [Siek and Taha 2007]. Consistent subtyping is employed by gradual type systems to validate
type conversions arising from conventional subtyping. One nice feature of consistent subtyping isthat it is derivable from the more primitive notions of consistency and subtyping. As Siek and Taha
[2007] put it, this shows that “gradual typing and subtyping are orthogonal and can be combined ina principled fashion”. Thus consistent subtyping is often used as a guideline for designing gradualtype systems with subtyping.
Unfortunately, as noted by Garcia et al. [2016], notions of consistency and/or consistent subtyping“become more difficult to adapt as type systems get more complex”. In particular, for the case of typesystems with subtyping, certain kinds of subtyping do not fit well with the original definition of
consistent subtyping by Siek and Taha [2007]. One important case where such a mismatch happens isin type systems supporting implicit (higher-rank) polymorphism [Dunfield and Krishnaswami 2013;
Odersky and Läufer 1996; Peyton Jones et al. 2007]. It is well-known that polymorphic types à laSystem F induce a subtyping relation that relates polymorphic types to their instantiations [Mitchell
1990; Odersky and Läufer 1996]. However Siek and Taha’s definition is not adequate for this kindof subtyping. Moreover the current framework for Abstracting Gradual Typing (AGT) [Garcia
et al. 2016] does not account for polymorphism either, but the authors acknowledge that it is aninteresting avenue for future work.
Existing work on gradual type systems with polymorphism does not use consistent subtyping.
The Polymorphic Blame Calculus (λB) [Ahmed et al. 2011, 2017] is an explicitly polymorphic
calculus with explicit casts, which is often used as a target language for gradual type systems withpolymorphism. In λB a notion of compatibility is employed to validate conversions allowed by casts.
Interestingly λB allows conversions from polymorphic types to their instantiations. For example, it ispossible to cast a value with type ∀a. a → a into Int → Int. Thus an important remark here is that,while λB is explicitly polymorphic, casting and conversions are closer to implicit polymorphism.
That is, in a conventional explicitly polymorphic calculus (such as System F), the primary notion istype equality, where instantiation is not taken into account. Thus the types ∀a. a → a and Int → Int
are deemed incompatible. However in implicitly polymorphic calculi [Dunfield and Krishnaswami
2013; Odersky and Läufer 1996; Peyton Jones et al. 2007] ∀a. a → a and Int → Int are deemedcompatible, since the latter type is an instantiation of the former. Therefore λB is in a sense a hybrid
between implicit and explicit polymorphism, utilizing type equality (à la System F) for validating
applications, and compatibility for validating casts.
An alternative approach to polymorphism has recently been proposed by Igarashi et al. [2017].
Like λB their calculus is explicitly polymorphic. However, they employ type consistency to validate
cast conversions, and forbid conversions from ∀a. a → a to Int → Int. This makes their casts
closer to explicit polymorphism, in contrast to λB. Nonetheless, there is still some flavor of implicit
polymorphism in their calculus when it comes to interactions between dynamically typed andpolymorphically typed code. For example, in their calculus type consistency allows types suchas ∀a. a → Int to be related to ⋆ → Int, where some sort of (implicit) polymorphic subtyping is
involved.
The first goal of this paper is to study the gradually typed subtyping and consistent subtyping
relations for predicative implicit polymorphism. To accomplish this, we first show how to reconcile
consistent subtyping with polymorphism by generalizing the original consistent subtyping definition by Siek and Taha. Our new definition of consistent subtyping can deal with polymorphism,
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:3

and preserves the orthogonality between consistency and subtyping. To slightly rephrase Siek andTaha, the motto of our paper is that:
Gradual typing and polymorphism are orthogonal and can be combined in a principledfashion.1
With the insights gained from our work, we argue that, for implicit polymorphism, Ahmed et al.’s
notion of compatibility is too permissive (i.e., too many programs are allowed to type-check), andthat Igarashi et al.’s notion of type consistency is too conservative. As a step towards an algorithmic
version of consistent subtyping, we present a syntax-directed version of consistent subtypingthat is sound and complete with respect to our formal definition of consistent subtyping. The
syntax-directed version of consistent subtyping is remarkably simple and well-behaved, and does
not require the restriction operator of Siek and Taha [2007]. Moreover, to further illustrate thegenerality of our consistent subtyping definition, we show that it can also account for top types,
which cannot be dealt with by Siek and Taha’s definition either.
The second goal of this paper is to present the design of GPC, which stands for Gradually
Polymorphic Calculus: a (source-level) gradually typed calculus for (predicative) implicit higherrank polymorphism that uses our new notion of consistent subtyping. As far as we are aware,
there is no work on bridging the gap between implicit higher-rank polymorphism and gradualtyping, which is interesting for two reasons. On the one hand, modern functional languages (suchas Haskell) employ sophisticated type-inference algorithms that, aided by type annotations, candeal with implicit higher-rank polymorphism. So a natural question is how gradual typing can be
integrated in such languages. On the other hand, there are several existing works on integrating
explicit polymorphism into gradual typing [Ahmed et al. 2011; Igarashi et al. 2017]. Yet no work
investigates how to move its expressive power into a source language with implicit polymorphism.
Therefore as a step towards gradualizing such type systems, this paper develops both declarative
and algorithmic versions for a gradual type system with implicit higher-rank polymorphism. The
new calculus brings the expressive power of full implicit higher-rank polymorphism into a gradually
typed source language. We prove that our calculus satisfies all of the static aspects of the refined
criteria for gradual typing [Siek et al. 2015].
As a step towards the dynamic gradual guarantee property [Siek et al. 2015], we propose an
extension of our calculus. This extension employs static type parameters, which are placeholders formonotypes, and gradual type parameters, which are placeholders for monotypes that are consistent
with the unknown type. The concept of static type parameters and gradual type parameters in thecontext of gradual typing was first introduced by Garcia and Cimini [2015], and later played a central
role in the work of Igarashi et al. [2017]2 . With this extension it becomes possible to talk about
representative translations: those translations that generalize a number of other translations using
specific monotypes. Our work recasts the dynamic gradual guarantee in terms of representativetranslations. Assuming a coherence conjecture regarding representative translations, the dynamic
gradual guarantee of our extended source language now can be reduced to that of λB, which, at thetime of writing, is still an open question. Nonetheless, we believe our discussion of representativetranslations is helpful in shedding some light on this issue.
In summary, the contributions of this paper are:
• We define a framework for consistent subtyping with:– a new definition of consistent subtyping that subsumes and generalizes that of Siek andTaha, and can deal with polymorphism and top types, and
1 Note here that we borrow Siek and Taha’s motto mostly to talk about the static semantics. As Ahmed et al. [2011] show

there are several non-trivial interactions between polymorphism and casts at the level of the dynamic semantics.
2 The static and gradual type variables in their work.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:4

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers• Subtyping• ConsistencyΨ ⊢OL e : A(Fig. 3)(Fig. 4)superimposed
Consistent
Subtyping(Def. 4.1)
generalizes(Prop. 4.2)
Siek and Taha
(Def. 2.2)

gradualizes

Thm. 1Ψ⊢A≲B(Fig. 8)verified on
simple types(Prop. 4.5)

AGT

based onverified on Top(Prop. 8.2)

Ψ⊢e:A
(Fig. 9)Thm. 7.8
Thm. 7.4Γ⊢e ⇒A⊣∆Γ⊢e ⇐A⊣∆(Fig. 15)

type-directedtranslation(Thm. 2)
Ψ ⊢B s : A

Fig. 1. Some key results in the paper.

– a syntax-directed version of consistent subtyping that is sound and complete with respect
to our definition of consistent subtyping, but still guesses instantiations.
• Based on consistent subtyping, we present GPC: a declarative gradual type system withpredicative implicit higher-rank polymorphism. We prove that our calculus satisfies the static
aspects of the refined criteria for gradual typing [Siek et al. 2015], and is type-safe by a
type-directed translation to λB [Ahmed et al. 2011].
• We present a sound and complete bidirectional algorithm for implementing the declarative
system based on the design principle of Garcia and Cimini [2015] and the approach of Dunfield
and Krishnaswami [2013]. A Haskell implementation of the type checker is also available.
• We propose an extension of the type system with type parameters [Garcia and Cimini 2015]as a step towards restoring the dynamic gradual guarantee [Siek et al. 2015]. The extension
significantly changes the algorithmic system. The new algorithm features a novel use ofexistential variables with a different solution space, which is a natural extension of theapproach by Dunfield and Krishnaswami [2013].
• All of the metatheory of this paper, except some manual proofs for the algorithmic typesystem and extensions, has been mechanically formalized in Coq.
Figure 1 summarizes some key results in the paper. The reader is advised to refer back to thisfigure while reading the rest of the paper, as what it depicts will gradually come to make sense.
This article is a significantly expanded version of a conference paper [Xie et al. 2018]. Besides
many improvements and expansions of the conference paper materials, there are several novel
extensions. Firstly, we have added let expressions to our gradually typed calculus. Therefore it
can now be seen as a complete gradual version of the implicitly polymorphic lambda calculus byOdersky and Läufer [1996]. Secondly, we have significantly expanded the discussion of applicationsof the calculus. In particular we now show how we can model algebraic datatypes, and how
the combination of gradual typing and polymorphism enables simple (gradual) formulations ofheterogeneous data structures [Kiselyov et al. 2004; McBride 2002]. Thirdly, we provide an extensive
discussion of a variant of the calculus with a subsumption rule and prove its soundness andcompleteness. Fourthly, we study an extension of the calculus with type parameters and discuss
the dynamic gradual guarantee [Siek et al. 2015] in detail. Furthermore we formalize the notionof coherence up to cast errors in Section 5. We also include detailed proofs on decidability of thealgorithmic system. Finally, we provide an implementation of our type checking algorithm.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:5
A <: BInt <: Int
B 1 <: A1

Bool <: BoolA2 <: B 2

Float <: Float[li : Aii ∈1...n+m ] <: [li : Aii ∈1...n ]A1 → A2 <: B 1 → B 2

Int <: Float⋆ <: ⋆

A∼B
A∼A

A∼⋆

⋆∼A

A1 ∼ B 1

A2 ∼ B 2

A1 → A2 ∼ B 1 → B 2

Ai ∼ B i[li : Ai ] ∼ [li : Bi ]Fig. 2. Subtyping and type consistency in FOb?<:All supplementary materials, including Coq mechanization, manual proofs, and the Haskell implementation of the algorithm, are available at https://github.com/xnning/Consistent-Subtyping-for-All.
2

BACKGROUND

In this section we review a simple gradually typed language with objects [Siek and Taha 2007], tointroduce the concept of consistent subtyping. We also briefly talk about the Odersky and Läufer
type system for higher-rank types [Odersky and Läufer 1996], which serves as the original language
on which our gradually typed calculus with implicit higher-rank polymorphism is based.
2.1

Gradual Subtyping

Siek and Taha [2007] developed a gradual type system for object-oriented languages that they call
FOb?<: . Central to gradual typing is the concept of consistency (written ∼) between gradual types,
which are types that may involve the unknown type ⋆. The intuition is that consistency relaxes
the structure of a type system to tolerate unknown positions in a gradual type. They also defined
the subtyping relation in a way that static type safety is preserved. Their key insight is that theunknown type ⋆ is neutral to subtyping, with only ⋆ <: ⋆. Both relations are defined in Fig. 2.
A primary contribution of their work is to show that consistency and subtyping are orthogonal.
However, the orthogonality of consistency and subtyping does not lead to a deterministic relation.
Thus Siek and Taha defined consistent subtyping (written ≲) based on a restriction operator, written
A|B that “masks off” the parts of type A that are unknown in type B. For example, Int → Int|Bool→⋆ =Int → ⋆, and Bool → ⋆|Int→Int = Bool → ⋆. The definition of the restriction operator is given below:
A|B = case (A, B) of| (_, ⋆) ⇒ ⋆| (A1 → A2 , B 1 → B 2 ) ⇒ A1 |B1 → A2 |B2| ([l 1 : A1 , ..., ln : An ], [l 1 : B 1 , ..., lm : Bm ]) if n ≤ m ⇒ [l 1 : A1 |B1 , ..., ln : An |Bn ]| ([l 1 : A1 , ..., ln : An ], [l 1 : B 1 , ..., lm : Bm ]) if n > m ⇒ [l 1 : A1 |B1 , ..., lm : Am |Bm , ..., ln : An ]| (_, _) ⇒ A

With the restriction operator, consistent subtyping is simply defined as:
Definition 2.1 (Algorithmic Consistent Subtyping of Siek and Taha [2007]). A ≲ B ≡ A|B <: B|A .
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:6

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers
Int | a | A → B | ∀a. A
Int | a | τ → σ
x | n | λx : A. e | λx. e | e1 e2 | let x = e1 in e2• | Ψ, x : A | Ψ, a

F
F
F
F

A, B
τ,σ
e
Ψ

Types
Monotypes
Terms
Contexts
Ψ ⊢OL e : A(Typing)OLΨ, x : A ⊢(x : A) ∈ Ψ
u-var

OL

Ψ⊢

e:B

u-int

OL

Ψ⊢

x:A

u-lamannOLΨ⊢λx : A. e : A → B

Ψ ⊢OL e1 : A1 → A2

Ψ ⊢OL e2 : A1

n : IntΨ, x : τ ⊢OL e : B
u-lam

u-app

Ψ ⊢OL λx. e : τ → B

Ψ ⊢OL e1 e2 : A2
Ψ ⊢ A1 <: A2

Ψ ⊢OL e : A1

Ψ, a ⊢OL e : A
u-sub

Ψ⊢

OL

u-gen

Ψ ⊢OL e : ∀a. A

e : A2Ψ ⊢OL e1 : A

Ψ, x : A ⊢OL e2 : B

Ψ ⊢OL let x = e1 in e2 : B

u-letΨ ⊢ A <: B

(Subtyping)Ψ ⊢ B1 <: A1a∈ΨΨ ⊢ a <: as-tvarΨ⊢τΨ ⊢ Int <: Ints-intΨ ⊢ A1 → A2 <: B1 → B2

s-arrow

Ψ, a ⊢ A <: BΨ ⊢ A[a 7→ τ ] <: B
Ψ ⊢ ∀a. A <: BΨ ⊢ A2 <: B2

s-forallLΨ ⊢ A <: ∀a. B

s-forallR

Fig. 3. Syntax and static semantics of the Odersky-Läufer type system.

Later they show a proposition that consistent subtyping is equivalent to two declarative definitions, which we refer to as the strawman for declarative consistent subtyping because it servers as agood guideline on superimposing consistency and subtyping. Both definitions are non-deterministic
because of the intermediate type C.
Definition 2.2 (Strawman for Declarative Consistent Subtyping). The following two are equivalent:(1) A ≲ B if and only if A ∼ C and C <: B for some C.
(2) A ≲ B if and only if A <: C and C ∼ B for some C.
In our later discussion, it will always be clear which definition we are referring to. For example,
we focus more on Definition 2.2 in Section 4.2, and more on Definition 2.1 in Section 4.5.
2.2

The Odersky-Läufer Type System

The calculus we are combining gradual typing with is the well-established predicative type system
for higher-rank types proposed by Odersky and Läufer [1996].
The syntax of the type system, along with the typing and subtyping judgments is given in Fig. 3.
An implicit assumption throughout the paper is that variables in contexts are distinct. Most typing
rules are standard. The rule u-sub (the subsumption rule) allows us to convert the type A1 of an
expression e to some supertype A2 . The rule u-gen generalizes type variables to polymorphic types.
These two rules can be applied anywhere. Most subtyping rules are standard as well. Rule s-forallL
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:7

guesses a monotype τ to instantiate the type variable a, and the subtyping relation holds if the theinstantiated type A[a 7→ τ ] is a subtype of B. In rule s-forallR, the type variable a is put into thetyping context and subtyping continues with A and B. We save additional explanation about thestatic semantics for Section 5, where we present our gradually typed version of the calculus.
3

MOTIVATION AND APPLICATIONSIn this section we motivate why the combination of gradual typing and implicit polymorphism isuseful. We then illustrate two concrete applications related to algebraic datatypes. The first application shows how gradual typing helps in defining Scott encodings of algebraic datatypes [Curryet al. 1958; Parigot 1992], which are impossible to encode in plain System F. The second applicationshows how gradual typing makes it easy to model and use heterogeneous containers.
3.1

Motivation: Gradually Typed Higher-Rank Polymorphism

Our work combines implicit (higher-rank) polymorphism with gradual typing. As is well known,a gradually typed language supports both fully static and fully dynamic checking of program
properties, as well as the continuum between these two extremes. It also offers programmers finegrained control over the static-to-dynamic spectrum, i.e., a program can be evolved by introducing
more or less precise types as needed [Garcia et al. 2016].
Haskell is a language renowned for its advanced type system, but it does not feature gradualtyping. Of particular interest to us is its support for implicit higher-rank polymorphism, which is
supported via explicit type annotations. In Haskell some programs that are safe at run-time may berejected due to the conservativity of the type system. For example, consider the following Haskell
program adapted from Peyton Jones et al. [2007]:
foo :: ([Int], [Char])foo = let f x = (x [1, 2] , x ['a', 'b']) in f reverse

This program is rejected by Haskell’s type checker because Haskell implements the Damas-Milner[Damas and Milner 1982; Hindley 1969] rule that a lambda-bound argument (such as x) can only
have a monotype, i.e., the type checker can only assign x the type [Int] → [Int], or [Char] →[Char], but not ∀a. [a] → [a]. Finding such manual polymorphic annotations can be non-trivial,
especially when the program scales up and the annotation is long and complicated.
Instead of rejecting the program outright, due to missing type annotations, gradual typing
provides a simple alternative by giving x the unknown type ⋆. With this type the same program
type-checks and produces ([2, 1], ['b', 'a']). By running the program, programmers can gain
more insight about its run-time behaviour. Then, with this insight, they can also give x a more
precise type (∀a. [a] → [a]) a posteriori so that the program continues to type-check via implicit
polymorphism and also grants more static safety. In this paper, we envision such a language thatcombines the benefits of both implicit higher-rank polymorphism and gradual typing.
3.2

Application: Efficient (Partly) Typed Encodings of ADTs

Our calculus does not provide built-in support for algebraic datatypes (ADTs). Nevertheless, thecalculus is expressive enough to support efficient function-based encodings of (optionally polymorphic) ADTs3 . This offers an immediate way to model algebraic datatypes in our calculus without
requiring extensions to our calculus or, more importantly, to its target—the polymorphic blame
calculus. While we believe that such extensions are possible, they would likely require non-trivial
extensions to the polymorphic blame calculus. Thus the alternative of being able to model algebraic
3 In a type system with impure features, such as non-termination or exceptions, the encoded types can have valid inhabitants

with side-effects, which means we only get the lazy version of those datatypes.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:8

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

datatypes without extending λB is appealing. The encoding also paves the way to provide built-in
support for algebraic datatypes in the source language, while elaborating them via the encoding
into λB.
Church and Scott Encodings. It is well-known that polymorphic calculi such as System F canencode datatypes via Church encodings. However these encodings have well-known drawbacks. In
particular, some operations are hard to define, and they can have a time complexity that is greaterthan that of the corresponding functions for built-in algebraic datatypes. A good example is thedefinition of the predecessor function for Church numerals [Church 1941]. Its definition requires
significant ingenuity (while it is trivial with built-in algebraic datatypes), and it has linear timecomplexity (versus the constant time complexity for a definition using built-in algebraic datatypes).
An alternative to Church encodings are the so-called Scott encodings [Curry et al. 1958]. They
address the two drawbacks of Church encodings: they allow simple definitions that directly correspond to programs implemented with built-in algebraic datatypes, and those definitions have thesame time complexity to programs using algebraic datatypes.
Unfortunately, Scott encodings, or more precisely, their typed variant [Parigot 1992], cannot be
expressed in System F: in the general case they require recursive types, which System F does notsupport. However, with gradual typing, we can remove the need for recursive types, thus enabling
Scott encodings in our calculus.
A Scott Encoding of Parametric Lists. Consider for instance the typed Scott encoding of parametriclists in a system with implicit polymorphism:
List a ≜ µL. ∀b. b → (a → L → b) → b
nil ≜ foldList a (λn. λc. n) : ∀a. List acons ≜ λx. λxs. foldList a (λn. λc. c x xs) : ∀a. a → List a → List aThis encoding requires both polymorphic and recursive types4 . Like System F, our calculus only
supports the former, but not the latter. Nevertheless, gradual types still allow us to use the Scottencoding in a partially typed fashion. The trick is to omit the recursive type binder µL and replace
the recursive occurrence of L by the unknown type ⋆:List⋆ a ≜ ∀b. b → (a → ⋆ → b) → b
As a consequence, we need to replace the term-level witnesses of the iso-recursion by explicit type
annotations to respectively forget or recover the type structure of the recursive occurrences:
foldList⋆ a ≜ λx. x : (∀b. b → (a → List⋆ a → b) → b) → List⋆ aunfoldList⋆ a ≜ λx. x : List⋆ a → (∀b. b → (a → List⋆ a → b) → b)
With the reinterpretation of fold and unfold as functions instead of built-in primitives, we haveexactly the same definitions of nil⋆ and cons⋆ .
Note that when we elaborate our calculus into the polymorphic blame calculus, the above type
annotations give rise to explicit casts. For instance, after elaboration foldList⋆ a e results in the cast⟨(∀b. b → (a → List⋆ a → b) → b) ,→ List⋆ a⟩s where s is the elaboration of e.
In order to perform recursive traversals on lists, e.g., to compute their length, we need a fixpoint
combinator like the Y combinator. Unfortunately, this combinator cannot be assigned a type in the
4 Here we use iso-recursive types, but equi-recursive types can be used too.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:9

simply typed lambda calculus or System F. Yet, we can still provide a gradual typing for it in oursystem.
fix ≜ λf . (λx : ⋆. f (x x)) (λx : ⋆. f (x x)) : ∀a. (a → a) → a
This allows us for instance to compute the length of a list.
length ≜ fix (λlen. λl. zero⋆ (λxs. succ⋆ (len xs)))
Here zero⋆ : Nat⋆ and succ⋆ : Nat⋆ → Nat⋆ are the encodings of the constructors for natural
numbers Nat⋆ . In practice, for performance reasons, we could extend our language with a letrec
construct in a standard way to support general recursion, instead of defining a fixpoint combinator.
Observe that the gradual typing of lists still enforces that all elements in the list are of the same
type. For instance, a heterogeneous list like cons⋆ zero⋆ (cons⋆ true⋆ nil⋆ ), is rejected becausezero⋆ : Nat⋆ and true⋆ : Bool⋆ have different types.
Heterogeneous Containers. Heterogeneous containers are datatypes that can store data of different
types, which is very useful in various scenarios. One typical application is that an XML element isheterogeneously typed. Moreover, the result of a SQL query contains heterogeneous rows.
In statically typed languages, there are several ways to obtain heterogeneous lists. For example,
in Haskell, one option is to use dynamic types. Haskell’s library Data.Dynamic provides the special
type Dynamic along with its injection toDyn and projection fromDyn. The drawback is that thecode is littered with toDyn and fromDyn, which obscures the program logic. One can also use the
HList library [Kiselyov et al. 2004], which provides strongly typed data structures for heterogeneouscollections. The library requires several Haskell extensions, such as multi-parameter classes [Joneset al. 1997] and functional dependencies [Jones 2000]. With fake dependent types [McBride 2002],
heterogeneous vectors are also possible with type-level constructors.
In our type system, with explicit type annotations that set the element types to the unknown
type we can disable the homogeneous typing discipline for the elements and get gradually typed
heterogeneous lists5 . Such gradually typed heterogeneous lists are akin to Haskell’s approach with
Dynamic types, but much more convenient to use since no injections and projections are needed,
and the ⋆ type is built-in and natural to use.
An example of such gradually typed heterogeneous collections is:l ≜ cons⋆ (zero⋆ : ⋆) (cons⋆ (true⋆ : ⋆) nil⋆ )Here we annotate each element with type annotation ⋆ and the type system is happy to type-checkthat l : List⋆ ⋆. Note that we are being meticulous about the syntax, but with proper implementationof the source language, we could write more succinct programs akin to Haskell’s syntax, such as[0, True].
4

REVISITING CONSISTENT SUBTYPINGIn this section we explore the design space of consistent subtyping. We start with the definitions ofconsistency and subtyping for polymorphic types, and compare with some relevant work. We thendiscuss the design decisions involved in our new definition of consistent subtyping, and justify the
new definition by demonstrating its equivalence with that of Siek and Taha [2007] and the AGT
approach [Garcia et al. 2016] on simple types.
The syntax of types is given at the top of Fig. 4. We write A, B for types. Types are either the
integer type Int, type variables a, functions types A → B, universal quantification ∀a. A, or the
unknown type ⋆. Though we only have one base type Int, we also use Bool in examples. Note that
5 This argument is based on the extended type system in Section 9.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:10Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers
A, B
τ,σ
Ψ

Types
Monotypes
Contexts

F
F
F

Int | a | A → B | ∀a. A | ⋆Int | a | τ → σ• | Ψ, x : A | Ψ, aA∼B

(Type Consistency)
A1 ∼ B 1
A∼⋆

A∼A

⋆∼A

A∼B

A2 ∼ B2

A1 → A2 ∼ B1 → B2

∀a. A ∼ ∀a. B

Ψ ⊢ A <: B

(Subtyping)Ψ ⊢ B1 <: A1a∈ΨΨ ⊢ a <: aΨ⊢τs-tvarΨ ⊢ Int <: Ints-intΨ ⊢ A[a 7→ τ ] <: BΨ ⊢ A1 → A2 <: B1 → B2

s-arrows-forallRs-unknown

Ψ, a ⊢ A <: B
s-forallLΨ ⊢ ∀a. A <: BΨ ⊢ A2 <: B2

Ψ ⊢ A <: ∀a. BΨ⊢AΨ ⊢ ⋆ <: ⋆(Well-formedness of types)a∈ΨΨ ⊢ Int

Ψ⊢⋆

Ψ⊢a

Ψ⊢A

Ψ⊢B

Ψ⊢A→B

Ψ, a ⊢ AΨ ⊢ ∀a. A

Fig. 4. Syntax of types, consistency, subtyping, well-formedness of types in the declarative system.

monotypes τ contain all types other than the universal quantifier and the unknown type ⋆. We
will discuss this restriction when we present the subtyping rules. Contexts Ψ are ordered lists oftype variable declarations and term variables.
4.1

Consistency and Subtyping

We start by giving the definitions of consistency and subtyping for polymorphic types, and comparing our definitions with the compatibility relation by Ahmed et al. [2011] and type consistency
by Igarashi et al. [2017].
Consistency. The key observation here is that consistency is mostly a structural relation, exceptthat the unknown type ⋆ can be regarded as any type. In other words, consistency is an equivalence
relation lifted from static types to gradual types [Garcia et al. 2016]. Following this observation,
we naturally extend the definition from Fig. 2 with polymorphic types, as shown in the middle ofFig. 4. In particular a polymorphic type ∀a. A is consistent with another polymorphic type ∀a. B if
A is consistent with B.
Subtyping. We express the fact that one type is a polymorphic generalization of another by meansof the subtyping judgment Ψ ⊢ A <: B. Compared with the subtyping rules of Odersky and Läufer
[1996] in Fig. 3, the only addition is the neutral subtyping of ⋆. Notice that, in rule s-forallL, theuniversal quantifier is only allowed to be instantiated with a monotype. The judgment Ψ ⊢ A checks
whether all the type variables in A are bound in the context Ψ. According to the syntax in Fig. 4,
monotypes do not include the unknown type ⋆. This is because if we were to allow the unknown
type to be used for instantiation, we could have ∀a. a → a <: ⋆ → ⋆ by instantiating a with ⋆.
Since ⋆ → ⋆ is consistent with any functions A → B, for instance, Int → Bool, this means that we
could provide an expression of type ∀a. a → a to a function where the input type is supposed to be
Int → Bool. However, as we know, ∀a. a → a is definitely not compatible with Int → Bool. Indeed,this does not hold in any polymorphic type systems without gradual typing. So the gradual type
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:11

system should not accept it either. (This is the conservative extension property that will be madeprecise in Section 5.3.)
Importantly there is a subtle distinction between a type variable and the unknown type, although
they both represent a kind of “arbitrary” type. The unknown type stands for the absence of type
information: it could be any type at any instance. Therefore, the unknown type is consistent withany type, and additional type-checks have to be performed at runtime. On the other hand, a typevariable indicates parametricity. In other words, a type variable can only be instantiated to a single
type. For example, in the type ∀a. a → a, the two occurrences of a represent an arbitrary but single
type (e.g., Int → Int, Bool → Bool), while ⋆ → ⋆ could be an arbitrary function (e.g., Int → Bool)at runtime.
Comparison with Other Relations. In other polymorphic gradual calculi, consistency and subtyping
are often mixed up to some extent. In λB [Ahmed et al. 2011], the compatibility relation forpolymorphic types is defined as follows:A[X 7→ ⋆] ≺ B

A≺B
A ≺ ∀X .B

Comp-AllR∀X .A ≺ B

Comp-AllL

Notice that, in rule Comp-AllL, the universal quantifier is always instantiated to ⋆. However, thisway, λB allows ∀a. a → a ≺ Int → Bool, which as we discussed before might not be what we expect.
Indeed λB relies on sophisticated runtime checks to rule out such instances of the compatibility
relation a posteriori.
Igarashi et al. [2017] introduced the so-called quasi-polymorphic types for types that may be used
where a ∀-type is expected, which is important for their purpose of conservativity over System F.
Their type consistency relation, involving polymorphism, is defined as follows6 :
A∼B

A∼B

∀a. A ∼ ∀a. B

B , ∀a. B ′⋆ ∈ Types(B)∀a. A ∼ B

Compared with our consistency definition in Fig. 4, their first rule is the same as ours. The second
rule says that a non ∀-type can be consistent with a ∀-type only if it contains ⋆. In this way, their
type system is able to reject ∀a. a → a ∼ Int → Bool. However, in order to keep conservativity,
they also reject ∀a. a → a ∼ Int → Int, which is perfectly sensible in their setting of explicit
polymorphism. However with implicit polymorphism, we would expect ∀a. a → a to be relatedwith Int → Int, since a can be instantiated to Int.
Nonetheless, when it comes to interactions between dynamically typed and polymorphically
typed terms, both relations allow ∀a. a → Int to be related with ⋆ → Int for example, which inour view, is a kind of (implicit) polymorphic subtyping combined with type consistency, and thatshould be derivable by the more primitive notions in the type system (instead of inventing new
relations). One of our design principles is that subtyping and consistency are orthogonal, and canbe naturally superimposed, echoing the opinion of Siek and Taha [2007].
4.2

Towards Consistent Subtyping

With the definitions of consistency and subtyping, the question now is how to compose the two
relations so that two types can be compared in a way that takes both relations into account.
Unfortunately, the strawman version of consistent subtyping (Definition 2.2) does not work
well with our definitions of consistency and subtyping for polymorphic types. Consider two types:(∀a. a → Int) → Int, and (⋆ → Int) → Int. The first type can only reach the second type in one
6 This is a simplified version. These two rules are presented in Section 3.1 in their paper as one of the key ideas of the designof type consistency, which are later amended with labels.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:12

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers∅∼(⋆ → Int) → Int<:<:(∀a.a → Int) → Int∼∼

Int → Int<:<:(∀a.⋆ → Int) → Int

∀a.a

∼

(a)
∅

Int → ⋆∅(b)∼(((⋆ → Int) → Int) → Bool) → (Int → ⋆)<:<:(((∀a.a → Int) → Int) → Bool) → (∀a.a)

∼

∅

(c)
Fig. 5. Examples that break the original definition of consistent subtyping.

way (first by applying consistency, then subtyping), but not the other way, as shown in Fig. 5a. We
use ∅ to mean that we cannot find such a type. Similarly, there are situations where the first type
can only reach the second type by the other way (first applying subtyping, and then consistency),
as shown in Fig. 5b.
What is worse, if those two examples are composed in a way that those types all appear covariantly, then the resulting types cannot reach each other in either way. For example, Fig. 5c shows
two such types by putting a Bool type in the middle, and neither definition of consistent subtyping
works.
Observations on Consistent Subtyping Based on Information Propagation. In order to develop a
correct definition of consistent subtyping for polymorphic types, we need to understand how
consistent subtyping works. We first review two important properties of subtyping: (1) subtyping
induces the subsumption rule: if A <: B, then an expression of type A can be used where B is
expected; (2) subtyping is transitive: if A <: B, and B <: C, then A <: C. Though consistentsubtyping takes the unknown type into consideration, the subsumption rule should also apply: if
A ≲ B, then an expression of type A can also be used where B is expected, given that there might
be some information lost by consistency. A crucial difference from subtyping is that consistentsubtyping is not transitive because information can only be lost once (otherwise, any two types
are a consistent subtype of each other). Now consider a situation where we have both A <: B, andB ≲ C, this means that A can be used where B is expected, and B can be used where C is expected,
with possibly some loss of information. In other words, we should expect that A can be used where
C is expected, since there is at most one-time loss of information.
Observation 1. If A <: B, and B ≲ C, then A ≲ C.
This is reflected in Fig. 6a. A symmetrical observation is given in Fig. 6b:
Observation 2. If C ≲ B, and B <: A, then C ≲ A.
From the above observations, we see what the problem is with the original definition. In Fig. 6a,
if B can reach C by T1 , then by subtyping transitivity, A can reach C by T1 . However, if B can only
reach C by T2 , then A cannot reach C through the original definition. A similar problem is shownin Fig. 6b.
It turns out that these two problems can be fixed using the same strategy: instead of taking onestep subtyping and one-step consistency, our definition of consistent subtyping allows types to take
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All
∼

T1

≲

<:
B

39:13

C

A

T2

∼

<:

≲

<:
≲

T1

≲

<:

<:

C

A
(a)

∼

∼

B
<:
T2

(b)

Fig. 6. Observations of consistent subtyping

A2

∼

<:
A1

A3
<:

≲

A4

A1 = (((∀a.a → Int) → Int) → Bool) → (∀a.a)
A2 = ((∀a.a → Int) → Int) → Bool) → (Int → Int)
A3 = ((∀a.⋆ → Int) → Int) → Bool) → (Int → ⋆)A4 = (((⋆ → Int) → Int) → Bool) → (Int → ⋆)Fig. 7. Example that is fixed by the new definition of consistent subtyping.

one-step subtyping, one-step consistency, and one more step subtyping. Specifically, A <: B ∼ T2 <: C(in Fig. 6a) and C <: T1 ∼ B <: A (in Fig. 6b) have the same relation chain: subtyping, consistency,
and subtyping.
Definition of Consistent subtyping. From the above discussion, we are ready to modify Definition 2.2, and adapt it to our notation7 :Definition 4.1 (Consistent Subtyping). Ψ ⊢ A ≲ B if and only if Ψ ⊢ A <: A′, A′ ∼ B ′ andΨ ⊢ B ′ <: B for some A′ and B ′.
With Definition 4.1, Figure 7 illustrates the correct relation chain for the broken example shown in
Fig. 5c.
At first sight, Definition 4.1 seems worse than the original: we need to guess two types! It turns
out that Definition 4.1 is a generalization of Definition 2.2, and they are equivalent in the system
of Siek and Taha [2007]. However, more generally, Definition 4.1 is compatible with polymorphic
types.
Proposition 4.2 (Generalization of Declarative Consistent Subtyping).
• Definition 4.1 subsumes Definition 2.2.
In Definition 4.1, by choosing D = B, we have A <: C and C ∼ B; by choosing C = A, we haveA ∼ D, and D <: B.
• Definition 2.2 is equivalent to Definition 4.1 in the system of Siek and Taha.
If A <: C, C ∼ D, and D <: B, by Definition 2.2, A ∼ C ′, C ′ <: D for some C ′. By subtyping
transitivity, C ′ <: B. So A ≲ B by A ∼ C ′ and C ′ <: B.
7 For readers who are familiar with category theory, this defines consistent subtyping as the least subtyping bimodule

extending consistency.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:14
4.3

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers
Abstracting Gradual Typing

Garcia et al. [2016] presented a new foundation for gradual typing that they call the Abstracting
Gradual Typing (AGT) approach. In the AGT approach, gradual types are interpreted as sets ofstatic types, where static types refer to types containing no unknown types. In this interpretation,
predicates and functions on static types can then be lifted to apply to gradual types. Central totheir approach is the so-called concretization function. For simple types, a concretization γ from
gradual types to a set of static types is defined as follows:
Definition 4.3 (Concretization).
γ (Int) = {Int}γ (A → B) = {A′ → B ′ | A′ ∈ γ (A), B ′ ∈ γ (B)}γ (⋆) = {All static types}

Based on the concretization function, subtyping between static types can be lifted to gradualtypes, resulting in the consistent subtyping relation:
H B if and only if A1 <: B 1 for some static types
Definition 4.4 (Consistent Subtyping in AGT). A <:A1 and B 1 such that A1 ∈ γ (A) and B 1 ∈ γ (B).
Later they proved that this definition of consistent subtyping coincides with that of Definition 2.2.
By Proposition 4.2, we can directly conclude that our definition coincides with AGT:
H B.
Corollary 4.5 (Eqivalence to AGT on Simple Types). A ≲ B if and only if A <:However, AGT does not show how to deal with polymorphism (e.g. the interpretation of typevariables) yet. Still, as noted by Garcia et al. [2016], it is a promising line of future work for AGT,
and the question remains whether our definition would coincide with it.
Another note related to AGT is that the definition is later adopted by Castagna and Lanvin[2017] in a gradual type system with union and intersection types, where the static types A1 , B 1 in
Definition 4.4 can be algorithmically computed by also accounting for top and bottom types.
4.4 Directed Consistency
Directed consistency [Jafery and Dunfield 2017] is defined in terms of precision and subtyping:A′ ⊑ A

A <: BB′ ⊑ BA′ ≲ B ′The judgment A ⊑ B is read “A is less precise than B”.8 In their setting, precision is first defined fortype constructors and then lifted to gradual types, and subtyping is defined for gradual types. If
we interpret this definition from the AGT point of view, finding a more precise static type has thesame effect as concretization. Namely, A′ ⊑ A implies A ∈ γ (A′ ) and B ′ ⊑ B implies B ∈ γ (B ′ ) if A
and B are static types. Therefore we consider this definition as AGT-style. From this perspective,
this definition naturally coincides with Definition 4.4, and by Corollary 4.5, it coincides with
Definition 4.1.
The value of their definition is that consistent subtyping is derived compositionally from gradualsubtyping and precision. Arguably, gradual types play a role in both definitions, which is different
from Definition 4.1 where subtyping is neutral to unknown types. Still, the definition is interesting
as it takes precision into consideration, rather than consistency. Then a question arises as to how
are consistency and precision related.
8 Jafery and Dunfield actually read A ⊑ B as “A is more precise than B”. We, however, use the “less precise” notation (whichis also adopted by Cimini and Siek [2016] ) throughout the paper. The full rules can be found in Fig. 10.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:15

Consistency and Precision. Precision is a partial order (anti-symmetric and transitive), whileconsistency is symmetric but not transitive. Recall that consistency is in fact an equivalence relation
lifted from static types to gradual types [Garcia et al. 2016], which embodies the key role ofgradual types in typing. Therefore defining consistency independently is straightforward, and it istheoretically viable to validate the definition of consistency directly. On the other hand, precision
is usually connected with the gradual criteria [Siek et al. 2015], and finding a correct partial orderthat adheres to the criteria is not always an easy task. For example, Igarashi et al. [2017] argued
that term precision for gradual System F is actually nontrivial, leaving the gradual guarantee ofthe semantics as a conjecture. Thus precision can be difficult to extend to more sophisticated typesystems, e.g. dependent types.
Nonetheless, in our system, precision and consistency can be related by the following lemma 9 :Lemma 1 (Consistency and Precision).
• If A ∼ B, then there exists (static) C, such that A ⊑ C, and B ⊑ C.
• If for some (static) C, we have A ⊑ C, and B ⊑ C, then we have A ∼ B.
4.5

Consistent Subtyping Without Existentials

Definition 4.1 serves as a fine specification of how consistent subtyping should behave in general. But
it is inherently non-deterministic because of the two intermediate types C and D. As Definition 2.1,
we need a combined relation to directly compare two types. A natural attempt is to try to extend
the restriction operator for polymorphic types. Unfortunately, as we show below, this does notwork. However it is possible to devise an equivalent inductive definition instead.
Attempt to Extend the Restriction Operator. Suppose that we try to extend Definition 2.1 to accountfor polymorphic types. The original restriction operator is structural, meaning that it works for typesof similar structures. But for polymorphic types, two input types could have different structuresdue to universal quantifiers, e.g, ∀a. a → Int and (Int → ⋆) → Int. If we try to mask the first typeusing the second, it seems hard to maintain the information that a should be instantiated to afunction while ensuring that the return type is masked. There seems to be no satisfactory way toextend the restriction operator in order to support this kind of non-structural masking.
Interpretation of the Restriction Operator and Consistent Subtyping. If the restriction operator
cannot be extended naturally, it is useful to take a step back and revisit what the restriction
operator actually does. For consistent subtyping, two input types could have unknown types indifferent positions, but we only care about the known parts. What the restriction operator doesis (1) erase the type information in one type if the corresponding position in the other type isthe unknown type; and (2) compare the resulting types using the normal subtyping relation. The
example below shows the masking-off procedure for the types Int → ⋆ → Bool and Int → Int → ⋆.
Since the known parts have the relation that Int → ⋆ → ⋆ <: Int → ⋆ → ⋆, we conclude that
Int → ⋆ → Bool ≲ Int → Int → ⋆.
Int → ⋆→ Bool

Int → Int →⋆| Int → Int → ⋆= Int → ⋆ → ⋆| Int → ⋆ → Bool

= Int → ⋆ → ⋆<:Here differences of the types in boxes are erased because of the restriction operator. Now if wecompare the types in boxes directly instead of through the lens of the restriction operator, we
can observe that the consistent subtyping relation always holds between the unknown type and an
arbitrary type. We can interpret this observation directly from Definition 4.1: the unknown type is
9 Lemmas with L are those proved in Coq. The same applies to T heorems.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:16

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

Ψ⊢A≲B(Consistent Subtyping)a∈ΨΨ ⊢ B1 ≲ A1
cs-tvarΨ ⊢ A2 ≲ B2

cs-intcs-arrowΨ ⊢ Int ≲ Int

Ψ⊢a≲a

Ψ⊢τ

Ψ, a ⊢ A ≲ B

Ψ ⊢ A1 → A2 ≲ B1 → B2

Ψ ⊢ A[a 7→ τ ] ≲ B

cs-forallRcs-forallLΨ ⊢ A ≲ ∀a. BΨ ⊢ ∀a. A ≲ B
Ψ⊢A≲⋆

Ψ⊢⋆≲A

cs-unknownL

cs-unknownR

Fig. 8. Consistent Subtyping for implicit polymorphism.

neutral to subtyping (⋆ <: ⋆), the unknown type is consistent with any type (⋆ ∼ A), and subtyping
is reflexive (A <: A). Therefore, the unknown type is a consistent subtype of any type (⋆ ≲ A),
and vice versa (A ≲ ⋆). Note that this interpretation provides a general recipe for lifting a (static)
subtyping relation to a (gradual) consistent subtyping relation, as discussed below.
Defining Consistent Subtyping Directly. From the above discussion, we can define the consistentsubtyping relation directly, without resorting to subtyping or consistency at all. The key idea isthat we replace <: with ≲ in Fig. 4, get rid of rule s-unknown and add two extra rules concerning⋆, resulting in the rules of consistent subtyping in Fig. 8. Of particular interest are the rules csunknownL and cs-unknownR, both of which correspond to what we just said: the unknown typeis a consistent subtype of any type, and vice versa. From now on, we use the symbol ≲ to refer tothe consistent subtyping relation in Fig. 8. What is more, we can prove that the two definitions areequivalent.
T heorem 1. Ψ ⊢ A ≲ B ⇔ Ψ ⊢ A <: A′, A′ ∼ B ′, Ψ ⊢ B ′ <: B for some A′, B ′.
5

GRADUALLY TYPED IMPLICIT POLYMORPHISM

In Section 4 we introduced our consistent subtyping relation that accommodates polymorphic
types. In this section we continue with the development by giving a declarative type system forpredicative implicit polymorphism that employs the consistent subtyping relation. The declarative
system itself is already quite interesting as it is equipped with both higher-rank polymorphism andthe unknown type. The syntax of expressions in the declarative system is given below:
ExpressionseF

x | n | λx : A. e | λx. e | e1 e2 | let x = e1 in e2

Meta-variable e ranges over expressions. Expressions include variables x, integers n, annotatedlambda abstractions λx : A. e, un-annotated lambda abstractions λx. e, applications e1 e2 , and let
expressions let x = e1 in e2 .
5.1

Typing in Detail

Figure 9 gives the typing rules for our declarative system (the reader is advised to ignore thegray-shaded parts for now). Rule var extracts the type of the variable from the typing context.
Rule int always infers integer types. Rule lamann puts x with type annotation A into the context,
and continues type checking the body e. Rule lam assigns a monotype τ to x, and continues typechecking the body e. Gradual types and polymorphic types are introduced via explicit annotations.
Rule gen puts a fresh type variable a into the type context and generalizes the typing result A to∀a. A. Rule let infers the type A of e1 , then puts x : A in the context to infer the type of e2 . Rule app
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:17

Ψ⊢e:A ⇝s

(Typing)Ψ, a ⊢ e : A ⇝ s(x : A) ∈ Ψ
var

gen

int

Ψ ⊢ n : Int ⇝ nΨ⊢x:A⇝xΨ ⊢ e : ∀a. A ⇝ Λa. s
Ψ, x : τ ⊢ e : B ⇝ s

Ψ, x : A ⊢ e : B ⇝ slamannlamΨ ⊢ λx. e : τ → B ⇝ λx : τ . sΨ ⊢ λx : A. e : A → B ⇝ λx : A. sΨ ⊢ e1 : A ⇝ s 1

Ψ, x : A ⊢ e2 : B ⇝ s 2let

Ψ ⊢ let x = e1 in e2 : B ⇝ (λx : A. s 2 ) s 1
Ψ ⊢ e1 : A ⇝ s 1

Ψ ⊢ A ▷ A1 → A2

Ψ ⊢ e2 : A3 ⇝ s 2

Ψ ⊢ A3 ≲ A1app

Ψ ⊢ e1 e2 : A2 ⇝ (⟨A ,→ A1 → A2 ⟩s 1 ) (⟨A3 ,→ A1 ⟩s 2 )Ψ ⊢ A ▷ A1 → A2Ψ⊢τ

(Matching)Ψ ⊢ A[a 7→ τ ] ▷ A1 → A2Ψ ⊢ ∀a. A ▷ A1 → A2

m-forallΨ ⊢⋆▷⋆→⋆

Ψ ⊢ A1 → A2 ▷ A1 → A2

m-arr

m-unknown

Fig. 9. Declarative typing

first infers the type of e 1 , then the matching judgment Ψ ⊢ A ▷ A1 → A2 extracts the domain typeA1 and the codomain type A2 from type A. The type A3 of the argument e 2 is then compared with
A1 using the consistent subtyping judgment.
Matching. The matching judgment of Siek et al. [2015] is extended to polymorphic types naturally,
resulting in Ψ ⊢ A ▷ A1 → A2 . In rule m-forall, a monotype τ is guessed to instantiate the universal
quantifier a. This rule is inspired by the application judgment Φ ⊢ A • e ⇒ C [Dunfield andKrishnaswami 2013], which says that if we apply a term of type A to an argument e, then we get aterm of type C. If A is a polymorphic type, the judgment works by guessing instantiations until itreaches an arrow type. Matching further simplifies the application judgment, since it is independentof typing. Rules m-arr and m-unknown are the same as Siek et al. [2015]. Rule m-arr returns thedomain type A1 and range type A2 as expected. If the input is ⋆, then rule m-unknown returns ⋆as both the type for the domain and the range.
Note that matching saves us from having a subsumption rule (rule u-sub in Fig. 3). The subsumption rule is incompatible with consistent subtyping, since the latter is not transitive. A discussionof a subsumption rule based on normal subtyping can be found in Section 8.2.
5.2

Type-directed Translation

We give the dynamic semantics of our language by translating it to λB [Ahmed et al. 2011]. Below
we show a subset of the terms in λB that are used in the translation:
λB Terms s

Fx | n | λx : A. s | Λa. s | s 1 s 2 | ⟨A ,→ B⟩s

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:18Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

A cast ⟨A ,→ B⟩s converts the value of term s from type A to type B. A cast from A to B is permitted
only if the types are compatible, written A ≺ B, as briefly mentioned in Section 4.1. The syntax oftypes in λB is the same as ours.
The translation is given in the gray-shaded parts in Fig. 9. The only interesting case here is
to insert explicit casts in the application rule. Note that there is no need to translate matchingor consistent subtyping. Instead we insert the source and target types of a cast directly in thetranslated expressions, thanks to the following two lemmas:
Lemma 2 (▷ to ≺). If Ψ ⊢ A ▷ A1 → A2 , then A ≺ A1 → A2 .
Lemma 3 (≲ to ≺). If Ψ ⊢ A ≲ B, then A ≺ B.
In order to show the correctness of the translation, we prove that our translation always produceswell-typed expressions in λB. By Lemmas 2 and 3, we have the following theorem:
T heorem 2 (Type Safety). If Ψ ⊢ e : A ⇝ s, then Ψ ⊢B s : A.
Parametricity. An important semantic property of polymorphic types is relational parametricity [Reynolds 1983]. The parametricity property says that all instances of a polymorphic function
should behave uniformly. A classic example is a function with the type ∀a. a → a. The parametricity
property guarantees that a value of this type must be either the identity function (i.e., λx. x) or the
undefined function (one which never returns a value). However, with the addition of the unknown
type ⋆, careful measures are to be taken to ensure parametricity. Our translation target λB is takenfrom Ahmed et al. [2011], where relational parametricity is enforced by dynamic sealing [Matthews
and Ahmed 2008; Neis et al. 2009], but there is no rigorous proof. Later, Ahmed et al. [2017] imposeda syntactic restriction on terms of λB, where all type abstractions must have values as their body.
With this invariant, they proved that the restricted λB satisfies relational parametricity. It remains
to see if our translation process can be adjusted to target restricted λB. One possibility is to impose
similar restriction to the rule gen:Ψ, a ⊢ e : A ⇝ v
Gen2

Ψ ⊢ e : ∀a. A ⇝ Λa. v
where we only generate type abstractions if the inner body is a value. However, the type systemwith this rule is a weaker calculus, which is not a conservative extension of the Odersky-Läufer
type system.
Ambiguity from Casts. The translation does not always produce a unique target expression. Thisis because when guessing some monotype τ in rules m-forall and cs-forallL, we could have many
choices, which inevitably leads to different types. This is usually not a problem for (non-gradual)
System F-like systems [Dunfield and Krishnaswami 2013; Peyton Jones et al. 2007] because they
adopt a type-erasure semantics [Pierce 2002]. However, in our case, the choice of monotypes may
affect the runtime behaviour of translated programs, since they could appear inside the explicit
casts. For instance, the following example shows two possible translations for the same source
expression (λx : ⋆. f x) : ⋆ → Int, where the type of f is instantiated to Int → Int and Bool → Int,
respectively:f : ∀a.a → Int ⊢ (λx : ⋆. f x ) : ⋆ → Int⇝ (λx : ⋆. (⟨∀a.a → Int ,→ Int → Int⟩ f ) ( ⟨⋆ ,→ Int⟩ x ))f : ∀a.a → Int ⊢ (λx : ⋆. f x ) : ⋆ → Int⇝ (λx : ⋆. (⟨∀a.a → Int ,→ Bool → Int⟩ f ) ( ⟨⋆ ,→ Bool⟩ x ))ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:19

If we apply λx : ⋆. f x to 3, which is fine since the function can take any input, the first translation
runs smoothly in λB, while the second one will raise a cast error (Int cannot be cast to Bool).
Similarly, if we apply it to true, then the second succeeds while the first fails. The culprit lies in
the highlighted parts where the instantiation of a appears in the explicit cast. More generally, any
choice introduces an explicit cast to that type in the translation, which causes a runtime cast error
if the function is applied to a value whose type does not match the guessed type. Note that thisdoes not compromise the type safety of the translated expressions, since cast errors are part of thetype safety guarantees.
The semantic discrepancy is due to the guessing nature of the declarative system. As far as thestatic semantics is concerned, both Int → Int and Bool → Int are equally acceptable. But this is
not the case at runtime. The astute reader may have found that the only appropriate choice is toinstantiate the type of f to ⋆ → Int in the matching judgment. However, as specified by rule mforall in Fig. 9, we can only instantiate type variables to monotypes, but ⋆ is not a monotype! We
will get back to this issue in Section 9.
Coherence. The ambiguity of translation seems to imply that the declarative system is incoherent.
A semantics is coherent if distinct typing derivations of the same typing judgment possess thesame meaning [Reynolds 1991]. We argue that the declarative system is coherent up to cast errors
in the sense that a well-typed program produces a unique value, or results in a cast error. In theabove example, suppose f is defined as (λx . 1), then whatever the translation might be, applying(λx : ⋆. f x) to 3 either results in a cast error, or produces 1, nothing else.
We defined contextual equivalence [Morris Jr 1969] to formally characterize that two open
expressions have the same behavior. The definition of contextual equivalence requires a notionof well-typed expression contexts C, written C : (Ψ ⊢B A) ⇝ (Ψ ′ ⊢B A′ ). The definitionsof contexts and context typing are standard and thus omitted. As is common, we first define
contextual approximation. In our setting, we need to relax the notion of contextual approximationof λB [Ahmed et al. 2017] to also take into consideration of cast errors. We write Ψ ⊢ s 1 ⪯ct x s 2 : A
to say that s 2 mimics the behaviour of s 1 at type A in the sense that whenever a program containings 1 reduces to an integer, replacing it with s 2 either reduces to the same integer, or emits a cast error.
We restrict the program results to integers to eliminate the role of types in values. If it is not an
integer, it is always possible to embed it into another context that reduces to an integer. Then we
write Ψ ⊢ s 1 ⋍ct x s 2 : A to say s 1 and s 2 are contextually equivalent, that is, they approximate eachother.
Definition 5.1 (Contextual Approximation and Equivalence up to Cast Errors).
Ψ ⊢ s 1 ⪯ct x s 2 : A ≜ Ψ ⊢B s 1 : A ∧ Ψ ⊢B s 2 : A ∧for all C. C : (Ψ ⊢B A) ⇝ (• ⊢B Int) =⇒C{s 1 } ⇓ n =⇒ (C{s 2 } ⇓ n ∨ C{s 2 } ⇓ blame)Ψ ⊢ s 1 ⋍ct x s 2 : A ≜ Ψ ⊢ s 1 ⪯ct x s 2 : A ∧ Ψ ⊢ s 2 ⪯ct x s 1 : A
Before presenting the formal definition of coherence, first we observe that after erasing types andcasts, all translations of the same expression are exactly the same. This is easy to see by examining
each elaboration rule. We use ⌊s⌋ to denote an expression in λB after erasure.
Lemma 5.2. If Ψ ⊢ e : A ⇝ s 1 , and Ψ ⊢ e : A ⇝ s 2 , then ⌊s 1 ⌋ ≡α ⌊s 2 ⌋.
Second, at runtime, the only role of types and casts is to emit cast errors caused by type mismatch.
Therefore, By Lemma 5.2 coherence follows as a corollary:
Lemma 5.3 (Coherence up to cast errors). For any expression e such that Ψ ⊢ e : A ⇝ s 1 andΨ ⊢ e : A ⇝ s 2 , we have Ψ ⊢ s 1 ⋍ct x s 2 : A.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:20Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers
A⊑B

Type precision
A1 ⊑ B 1⋆⊑A

L-Unknown

A2 ⊑ B 2

L-Nat

L-Arrow

Int ⊑ Int

L-TVar

A1 → A2 ⊑ B 1 → B 2

a⊑a

A⊑B
L-Forall∀a.A ⊑ ∀a.B
e1 ⊑ e2A1 ⊑ A2
L-Refle1 ⊑ e2e1 ⊑ e3

λx : A1 . e 1 ⊑ λx : A2 . e 2e ⊑e

Ψ1 p Ψ2 ⊢ e 1 ⊑B e 2
A1 ⊑ A2
L-Varx ⊑B xTerm precision

L-Natn ⊑B ne 1 ⊑B e 3e 1 e 2 ⊑B e 3 e 4

Term less precision in λB
e 1 ⊑B e 2

A1 ⊑ B 1
L-App

L-App

e1 e2 ⊑ e3 e4

λx : A1 . e 1 ⊑B λx : A2 . e 2

e 2 ⊑B e 4

e2 ⊑ e4

L-LamAnne 1 ⊑B e 2
L-LamAnn

L-LamAnnΛa.e 1 ⊑B Λa.e 2
A2 ⊑ B 2e 1 ⊑B e 2⟨A1 ,→ A2 ⟩ e 1 ⊑B ⟨B 1 ,→ B 2 ⟩ e 2

L-CastFig. 10. Less precision

5.3

Correctness Criteria

Siek et al. [2015] present a set of properties, the refined criteria, that a well-designed gradual typing
calculus must have. Among all the criteria, those related to the static aspects of gradual typing are
well summarized by Cimini and Siek [2016]. Here we review those criteria and adapt them to ournotation. We have proved in Coq that our type system satisfies all these criteria.
Lemma 4 (Correctness Criteria).
• Conservative extension: for all static Ψ, e, and A,– if Ψ ⊢OL e : A, then there exists B, such that Ψ ⊢ e : B, and Ψ ⊢ B <: A.
– if Ψ ⊢ e : A, then Ψ ⊢OL e : A• Monotonicity w.r.t. precision: for all Ψ, e, e ′, A, if Ψ ⊢ e : A, and e ′ ⊑ e, then Ψ ⊢ e ′ : B, andB ⊑ A for some B.
• Type Preservation of cast insertion: for all Ψ, e, A, if Ψ ⊢ e : A, then Ψ ⊢ e : A ⇝ s, andΨ ⊢B s : A for some s.
• Monotonicity of cast insertion: for all Ψ, e1 , e2 , s 1 , s 2 , A, if Ψ ⊢ e1 : A ⇝ s 1 , and Ψ ⊢ e2 :A ⇝ s 2 , and e1 ⊑ e2 , then Ψ p Ψ ⊢ s 1 ⊑B s 2 .
The first criterion states that the gradual type system should be a conservative extension of theoriginal system. In other words, a static program is typeable in the Odersky-Läufer type system
if and only if it is typeable in the gradual type system. A static program is one that does notcontain any type ⋆10 . However since our gradual type system does not have the subsumption rule,
it produces more general types.
10 Note that the term static has appeared several times with different meanings.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:21

The second criterion states that if a typeable expression loses some type information, it remains
typeable. This criterion depends on the definition of the precision relation, written A ⊑ B, which is
given in Fig. 10. The relation intuitively captures a notion of types containing more or less unknown
types (⋆). The precision relation over types lifts to programs, i.e., e1 ⊑ e2 means that e 1 and e 2 are
the same program except that e 1 has more unknown types.
The first two criteria are fundamental to gradual typing. They explain for example why thesetwo programs (λx : Int. x + 1) and (λx : ⋆. x + 1) are typeable, as the former is typeable in theOdersky-Läufer type system and the latter is a less-precise version of it.
The last two criteria relate the compilation to the cast calculus. The third criterion is essentiallythe same as T heorem 2, given that a target expression should always exist, which can be easily
seen from Fig. 9. The last criterion ensures that the translation must be monotonic over the
precision relation ⊑. Ahmed et al. [2011] does not include a formal definition of precision, but anapproximation definition and a simulation relation. Here we adapt the simulation relation as theprecision, and a subset of it that is used in our system is given at the bottom of Fig. 10.
The Dynamic Gradual Guarantee. Besides the static criteria, there is also a criterion concerning
the dynamic semantics, known as the dynamic gradual guarantee [Siek et al. 2015].
Definition 5.4 (Dynamic Gradual Guarantee). Suppose e ′ ⊑ e, and • ⊢ e : A ⇝ s and • ⊢ e ′ :A′ ⇝ s ′,• if s ⇓ v, then s ′ ⇓ v ′ and v ′ ⊑ v. If s ⇑ then s ′ ⇑.
• if s ′ ⇓ v ′, then s ⇓ v where v ′ ⊑ v, or s ⇓ blame. If s ′ ⇑ then s ⇑ or s ⇓ blame.
The first part of the dynamic gradual guarantee says that if a gradually typed program evaluates
to a value, then making type annotations less precise always produces a program that evaluates toan less precise value. Unfortunately, coherence up to cast errors in the declarative system breaks
the dynamic gradual guarantee. For instance:(λ f : ∀a.a → Int. λx : Int. f x ) (λx . 1) 3

(λ f : ∀a.a → Int. λx : ⋆. f x ) (λx . 1) 3

The left one evaluates to 1, whereas its less precise version (right) will give a cast error if a isinstantiated to Bool for example. In Section 9, we will present an extension of the declarative systemthat will alleviate the issue.
6

ALGORITHMIC TYPE SYSTEM

In this section we give a bidirectional account of the algorithmic type system that implements
the declarative specification. The algorithm is largely inspired by the algorithmic bidirectional
system of Dunfield and Krishnaswami [2013] (henceforth DK system). However our algorithmic
system differs from theirs in three aspects: (1) the addition of the unknown type ⋆; (2) the use of
the matching judgment; and 3) the approach of gradual inference only producing static types [Garcia
and Cimini 2015]. We then prove that our algorithm is both sound and complete with respect
to the declarative type system. Full proofs can be found in the appendix. We also provide an
implementation, which can be found in the supplementary materials.11
Algorithmic Contexts. Figure 11 shows the syntax of the algorithmic system. A noticeable difference are the algorithmic contexts Γ, which are represented as an ordered list containing declarationsof type variables a and term variables x : A. Unlike declarative contexts, algorithmic contexts also
contain declarations of existential type variables aD, which can be either unsolved (written aD) or
solved to some monotype (written aD = τ ). Finally, algorithmic contexts include a marker ▶aD (read
11 Note that the proofs in the appendix and the implementation are for the extended system in Section 9, which subsumes

the algorithmic system presented in this section.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:22

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers
e
A, B
τ,σ
Γ, ∆, ΘΩ

Expressions
Types
Monotypes
Algorithmic Contexts
Complete Contexts

x | n | λx : A. e | λx. e | e 1 e 2 | e : A | let x = e 1 in e 2
Int | a | aD | A → B | ∀a. A | ⋆Int | a | aD | τ → σ• | Γ, x : A | Γ, a | Γ, aD | Γ, aD = τ | Γ, ▶aD• | Ω, x : A | Ω, a | Ω, aD = τ | Ω, ▶aD

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

Fig. 11. Syntax of the algorithmic system

Γ⊢A(Well-formedness of types)
ad-intΓ ⊢⋆Γ ⊢ Int

ad-unknownΓ⊢B

ad-solved

Γ, a ⊢ A
ad-arrow

ad-forallΓ⊢A→BΓ ⊢ ∀a. A⊢Γ(Well-formedness of algorithmic contexts)⊢Γx < fv(Γ)

wf-empty⊢Γa < fv(Γ)
wf-tvar⊢ Γ, x : A

aD < fv(Γ)⊢Γ
wf-evar⊢ Γ, aDΓ⊢A
wf-var⊢•⊢Γ

ad-evarΓ[Da ] ⊢ aDΓ[a] ⊢ aΓ⊢AΓ[Da = τ ] ⊢ aD

ad-tvaraD < fv(Γ)⊢ Γ, aD = τ⊢ Γ, aΓ ⊢τ⊢Γ
wf-solved▶aD< fv(Γ)

wf-marker⊢ Γ, ▶aD

Fig. 12. Well-formedness of types and contexts in the algorithmic system“marker aD” ), which is used to delineate existential variables created by the algorithm. We will havemore to say about markers when we examine the rules. Complete contexts Ω are the same ascontexts, except that they contain no unsolved variables.
Apart from expressions in the declarative system, we add annotated expressions e : A. The
well-formedness judgments for types and contexts are shown in Fig. 12.
Notational convenience. Following DK system, we use contexts as substitutions on types. We write[Γ]A to mean Γ applied as a substitution to type A. We also use a hole notation, which is useful whenmanipulating contexts by inserting and replacing declarations in the middle. The hole notation isused extensively in proving soundness and completeness. For example, Γ[Θ] means Γ has the form
ΓL , Θ, ΓR ; if we have Γ[Da ] = (ΓL , aD, ΓR ), then Γ[Da = τ ] = (ΓL , aD = τ , ΓR ). Occasionally, we will see acontext with two ordered holes, e.g., Γ = Γ0 [Θ1 ][Θ2 ] means Γ has the form ΓL , Θ1 , ΓM , Θ2 , ΓR .
Input and output contexts. The algorithmic system, compared with the declarative system, includes
similar judgment forms, except that we replace the declarative context Ψ with an algorithmic context
Γ (the input context), and add an output context ∆ after a backward turnstile, e.g., Γ ⊢ A ≲ B ⊣ ∆is the judgment form for the algorithmic consistent subtyping. All algorithmic rules manipulate
input and output contexts in a way that is consistent with the notion of context extension, which
will be described in Section 7.1.
We start with the explanation of the algorithmic consistent subtyping as it involves manipulating
existential type variables explicitly (and solving them if possible).
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:23(Under input context Γ, A is a consistent subtype of B, with output context ∆)Γ⊢A≲B ⊣∆
as-tvaras-intΓ ⊢⋆≲A⊣ΓΓ ⊢ B 1 ≲ A1 ⊣ Θ

as-evarΓ ⊢ Int ≲ Int ⊣ ΓΓ[a] ⊢ a ≲ a ⊣ Γ[a]as-unknownL

Γ[Da ] ⊢ aD ≲ aD ⊣ Γ[Da]Γ ⊢A≲⋆⊣Γ

as-unknownRΓ, a ⊢ A ≲ B ⊣ ∆, a, ΘΘ ⊢ [Θ]A2 ≲ [Θ]B 2 ⊣ ∆as-arrow

as-forallRΓ ⊢ A1 → A2 ≲ B 1 → B 2 ⊣ ∆Γ, ▶aD, aD ⊢ A[a 7→ aD] ≲ B ⊣ ∆, ▶aD, ΘΓ ⊢ A ≲ ∀a. B ⊣ ∆aD < fv(A)Γ[Da ] ⊢ aD ⪅ A ⊣ ∆as-forallLΓ ⊢ ∀a. A ≲ B ⊣ ∆as-instLΓ[Da ] ⊢ aD ≲ A ⊣ ∆aD < fv(A)Γ[Da ] ⊢ A ⪅ aD ⊣ ∆as-instRΓ[Da ] ⊢ A ≲ aD ⊣ ∆Fig. 13. Algorithmic consistent subtyping

6.1

Algorithmic Consistent Subtyping

Figure 13 presents the rules of algorithmic consistent subtyping Γ ⊢ A ≲ B ⊣ ∆, which says that
under input context Γ, A is a consistent subtype of B, with output context ∆. The first five rules do
not manipulate contexts, but illustrate how contexts are propagated.
Rules as-tvar and as-int do not involve existential variables, so the output contexts remainunchanged. Rule as-evar says that any unsolved existential variable is a consistent subtype ofitself. The output is still the same as the input context as the rule gives no clue as to what is thesolution of that existential variable. Rules as-unknownL and as-unknownR are the counterpartsof rules cs-unknownL and cs-unknownR.
Rule as-arrow is a natural extension of its declarative counterpart. The output context of thefirst premise is used by the second premise, and the output context of the second premise is theoutput context of the conclusion. Note that we do not simply check A2 ≲ B2 , but apply Θ (theinput context of the second premise) to both types (e.g., [Θ]A2 ). This is to maintain an importantinvariant: whenever Γ ⊢ A ≲ B ⊣ ∆ holds, the types A and B are fully applied under input context
Γ (they contain no existential variables already solved in Γ). The same invariant applies to every
algorithmic judgment.
Rule as-forallR, similar to the declarative rule cs-forallR, adds a to the input context. Notethat the output context of the premise allows additional existential variables to appear after thetype variable a, in a trailing context Θ. These existential variables could depend on a; since a goesout of scope in the conclusion, we need to drop them from the concluding output, resulting in ∆.
The next rule is essential to eliminating the guessing work. Instead of guessing a monotype τ outof thin air, rule as-forallL generates a fresh existential variable aD, and replaces a with aD in the
body A. The new existential variable aD is then added to the input context, just before the marker▶aD. The output context (∆, ▶aD, Θ) allows additional existential variables to appear after ▶aD in Θ.
For the same reasons as in rule as-forallR, we drop them from the output context. A central idea
behind these two rules is that we defer the decision of picking a monotype for a type variable, andhope that it could be solved later when we have more information at hand. As a side note, whenboth types are universal quantifiers, then either rule as-forallR or as-forallL could be tried. In
practice, one can apply rule as-forallR eagerly as it is invertible.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:24

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

Γ ⊢ aD ⪅ A ⊣ ∆(Under input context Γ, instantiate aD such that aD ≲ A, with output context ∆)Γ ⊢τ′Γ, aD, Γ ⊢ aD ⪅ τ ⊣ Γ, aD = τ , Γ ′D ⊢ aD ⪅ bD ⊣ Γ[DΓ[Da ][b]
a ][bD = aD]

instl-solve

Γ[Da ] ⊢ aD ⪅ ⋆ ⊣ Γ[Da]instl-solveU

Γ[Da ], b ⊢ aD ⪅ B ⊣ ∆, b, Θ

instl-reach

instl-forallRΓ[Da ] ⊢ aD ⪅ ∀b. B ⊣ ∆Γ[Da 2 , aD1 , aD = aD1 → aD2 ] ⊢ A1 ⪅ aD1 ⊣ ΘΘ ⊢ aD2 ⪅ [Θ]A2 ⊣ ∆instl-arr

Γ[Da ] ⊢ aD ⪅ A1 → A2 ⊣ ∆Γ ⊢ A ⪅ aD ⊣ ∆(Under input context Γ, instantiate aD such that A ≲ aD, with output context ∆)Γ ⊢τ′Γ, aD, Γ ⊢ τ ⪅ aD ⊣ Γ, aD = τ , Γ ′D ⊢ bD ⪅ aD ⊣ Γ[DΓ[Da ][b]
a ][bD = aD]

instr-solve

instr-reachΓ[Da ] ⊢ ⋆ ⪅ aD ⊣ Γ[Da]instr-solveUD ⪅ aD ⊣ ∆, ▶ , Θ
Γ[Da ], ▶bD, bD ⊢ B[b 7→ b]bD

instr-forallLΓ[Da ] ⊢ ∀b. B ⪅ aD ⊣ ∆Γ[Da 2 , aD1 , aD = aD1 → aD2 ] ⊢ aD1 ⪅ A1 ⊣ ΘΘ ⊢ [Θ]A2 ⪅ aD2 ⊣ ∆instr-arr

Γ[Da ] ⊢ A1 → A2 ⪅ aD ⊣ ∆Fig. 14. Algorithmic instantiation

The last two rules (as-instL and as-instR) are specific to the algorithm, thus having no counterparts in the declarative version. They both check consistent subtyping with an unsolved existential
variable on one side and an arbitrary type on the other side. Apart from checking that the existential
variable does not occur in the type A, both rules do not directly solve the existential variables, but
leave the real work to the instantiation judgment.
6.2

Instantiation

Two symmetric judgments Γ ⊢ aD ⪅ A ⊣ ∆ and Γ ⊢ A ⪅ aD ⊣ ∆ defined in Fig. 14 instantiate unsolved
existential variables. They read “under input context Γ, instantiate aD to a consistent subtype (orsupertype) of A, with output context ∆”. The judgments are extended naturally from DK system,
whose original inspiration comes from Cardelli [1993]. Since these two judgments are mutually
defined, we discuss them together.
Rule instl-solve is the simplest one – when an existential variable meets a monotype – where
we simply set the solution of aD to the monotype τ in the output context. We also need to check thatthe monotype τ is well-formed under the prefix context Γ.
Rule instl-solveU is similar to rule as-unknownR in that we put no constraint12 on aD when it
meets the unknown type ⋆. This design decision reflects the point that type inference only produces
static types [Garcia and Cimini 2015].
Rule instl-reach deals with the situation where two existential variables meet. Recall thatD denotes a context where some unsolved existential variable aD is declared before b.
D In thisΓ[Da ][b]
situation, the only logical thing we can do is to set the solution of one existential variable to
12 As we will see in Section 9 where we present a more refined system, the “no constraint” statement is not entirely true.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:25

Γ ⊢e ⇒A⊣∆(Under input context Γ, e infers output type A, with output context ∆)Γ⊢A(x : A) ∈ Γ
inf-varinf-annoΓ ⊢ n ⇒ Int ⊣ ΓΓ⊢x ⇒A⊣ΓΓ⊢AΓ ⊢e ⇐A⊣∆

inf-intΓ ⊢e :A⇒A⊣∆
D x : aD ⊢ e ⇐ bD ⊣ ∆, x : aD, ΘΓ, aD, b,

D x : A ⊢ e ⇐ bD ⊣ ∆, x : A, ΘΓ, b,inf-lamann

inf-lamΓ ⊢ λx : A. e ⇒ A → bD ⊣ ∆Γ ⊢ λx. e ⇒ aD → bD ⊣ ∆Θ1 , aD, x : A ⊢ e 2 ⇐ aD ⊣ ∆, x : A, Θ2Γ ⊢ e 1 ⇒ A ⊣ Θ1

inf-letΓ ⊢ let x = e 1 in e 2 ⇒ aD ⊣ ∆Θ1 ⊢ [Θ1 ]A ▷ A1 → A2 ⊣ Θ2

Γ ⊢ e 1 ⇒ A ⊣ Θ1

Θ2 ⊢ e 2 ⇐ [Θ2 ]A1 ⊣ ∆inf-appΓ ⊢ e 1 e 2 ⇒ A2 ⊣ ∆Γ ⊢e ⇐A⊣∆(Under input context Γ, e checks against input type A, with output context ∆)Γ, a ⊢ e ⇐ A ⊣ ∆, a, Θ

Γ, x : A ⊢ e ⇐ B ⊣ ∆, x : A, Θ
chk-lamΓ ⊢ λx. e ⇐ A → B ⊣ ∆chk-genΓ ⊢ e ⇐ ∀a. A ⊣ ∆Γ ⊢e ⇒A⊣ΘΘ ⊢ [Θ]A ≲ [Θ]B ⊣ ∆chk-subΓ ⊢e ⇐B ⊣∆Γ ⊢ A ▷ A1 → A2 ⊣ ∆(Under input context Γ, A matches output type A1 → A2 , with output context ∆)Γ, aD ⊢ A[a 7→ aD] ▷ A1 → A2 ⊣ ∆Γ ⊢ ∀a. A ▷ A1 → A2 ⊣ ∆Γ ⊢⋆▷⋆→⋆⊣ Γ

am-unknown

am-forallΓ ⊢ A1 → A2 ▷ A1 → A2 ⊣ Γam-arrΓ[Da ] ⊢ aD ▷ aD1 → aD2 ⊣ Γ[Da 1 , aD2 , aD = aD1 → aD2 ]am-varFig. 15. Algorithmic typing

the other one, depending on which one is declared before. For example, in the output context ofDrule instl-reach, we have bD = aD because in the input context, aD is declared before b.
Rule instl-forallR is the instantiation version of rule as-forallR. Since our system is predicative, aD cannot be instantiated to ∀b. B, but we can decompose ∀b. B in the same way as inrule as-forallR. Rule instr-forallL is the instantiation version of rule as-forallL.
Rule instl-arr applies when aD meets an arrow type. It follows that the solution must also be anarrow type. This is why, in the first premise, we generate two fresh existential variables aD1 and aD2 ,and insert them just before aD in the input context, so that we can solve aD to aD1 → aD2 . Note that thefirst premise A1 ⪅ aD1 switches to the other instantiation judgment.
6.3

Algorithmic Typing

We now turn to the algorithmic typing rules in Fig. 15. Because general type inference for System F is
undecidable [Wells 1999], our algorithmic system uses bidirectional type checking to accommodate(first-class) polymorphism. Traditionally, two modes are employed in bidirectional systems: thechecking mode Γ ⊢ e ⇐ A ⊣ Θ, which takes a term e and a type A as input, and ensures that theterm e checks against A; the inference mode Γ ⊢ e ⇒ A ⊣ Θ, which takes a term e and produces atype A. We first discuss rules in the inference mode.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:26

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

Rules inf-var and inf-int do not generate any new information and simply propagate the input
context. Rule inf-anno is standard, switching to the checking mode in the premise.
In rule inf-lamann, we generate a fresh existential variable bD for the function codomain, andD Note that it is tempting to write Γ, x : A ⊢ e ⇒ B ⊣ ∆, x : A, Θcheck the function body against b.
as the premise (in the hope of better matching its declarative counterpart rule lamann), which
has a subtle consequence. Consider the expression λx : Int. λy. y. Under the new premise, this isuntypable because of • ⊢ λx : Int. λy. y ⇒ Int → aD → aD ⊣ • where aD is not found in the output
context. This explains why we put bD before x : A so that it remains in the output context ∆. Rule inflam, which corresponds to rule lam, one of the guessing rules, is similar to rule inf-lamann. As
with the other algorithmic rules that eliminate guessing, we create new existential variables aD (forD Rule inf-let
function domain) and bD (for function codomain) and check the function body against b.
is similar to rule inf-lamann.
Algorithmic Matching. Rule inf-app (which differs significantly from that of [Dunfield andKrishnaswami 2013]) deserves attention. It relies on the algorithmic matching judgment Γ ⊢A ▷ A1 → A2 ⊣ ∆. The matching judgment algorithmically synthesizes an arrow type from anarbitrary type. Rule am-forall replaces a with a fresh existential variable aD, thus eliminating
guessing. Rules am-arr and am-unknown correspond directly to the declarative rules. Rule amvar, which has no corresponding declarative version, is similar to rule instl-arr/instr-arr: wecreate aD1 and aD2 and solve aD to aD1 → aD2 in the output context.
Back to the rule inf-app. This rule first infers the type of e1 , producing an output context Θ1 .
Then it applies Θ1 to A and goes into the matching judgment, which delivers an arrow type A1 → A2
and another output context Θ2 . Θ2 is used as the input context when checking e2 against [Θ2 ]A1 ,where we go into the checking mode.
Rules in the checking mode are quite standard. Rule chk-lam checks against A → B. Rule chkgen, like the declarative rule gen, adds a type variable a to the input context. Rule chk-sub uses
the algorithmic consistent subtyping judgment.
6.4

Decidability

Our algorithmic system is decidable. It is not at all obvious to see why this is the case, as many rules
are not strictly structural (e.g., many rules have [Γ]A in the premises). This implies that we need amore sophisticated measure to support the argument. Since the typing rules (Fig. 15) depend on theconsistent subtyping rules (Fig. 13), which in turn depends on the instantiation rules (Fig. 14), toshow the decidability of the typing judgment, we need to show that the instantiation and consistentsubtyping judgments are decidable. The proof strategy mostly follows that of the DK system. Here
only highlights of the proofs are given; the full proofs can be found in Appendix C.
Decidability of Instantiation. The basic idea is that we need to show A in the instantiation
judgments Γ ⊢ aD ⪅ A ⊣ ∆ and Γ ⊢ A ⪅ aD ⊣ ∆ always gets smaller. Most of the rules are structuraland thus easy to verify (e.g., rule instl-forallR); the non-trivial cases are rules instl-arr andinstr-arr where context applications appear in the premises. The key observation there is thatthe instantiation rules preserve the size of (substituted) types. The formal statement of decidabilityof instantiation needs a few pre-conditions: assuming aD is unsolved in the input context Γ, that A
is well-formed under the context Γ, that A is fully applied under the input context Γ ([Γ]A = A),and that aD does not occur in A. Those conditions are actually met when instantiation is invoked:
rule chk-sub applies the input context, and the subtyping rules apply input context when needed.
Theorem 6.1 (Decidability of Instantiation). If Γ = Γ0 [Da ] and Γ ⊢ A such that [Γ]A = A andaD < fv(A) then:
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:27(1) Either there exists ∆ such that Γ ⊢ aD ⪅ A ⊣ ∆, or not.
(2) Either there exists ∆ such that Γ ⊢ A ⪅ aD ⊣ ∆, or not.
Decidability of Algorithmic Consistent Subtyping. Proving decidability of the algorithmic consistent subtyping is a bit more involved, as the induction measure consists of several parts. We
measure the judgment Γ ⊢ A ≲ B ⊣ ∆ lexicographically by(M1) the number of ∀-quantifiers in A and B;(M2) the number of unknown types in A and B;(M3) |unsolved(Γ)|: the number of unsolved existential variables in Γ;(M4) |Γ ⊢ A| + |Γ ⊢ B|.
Notice that because of our gradual setting, we also need to measure the number of unknown types(M2). This is a key difference from the DK system. We refer the reader to Appendix C for moredetails. For (M4), we use contextual size—the size of well-formed types under certain contexts,
which penalizes solved variables (*).
Definition 6.2 (Contextual Size).
|Γ ⊢ Int||Γ ⊢ ⋆||Γ ⊢ a||Γ ⊢ aD||Γ[Da = τ ] ⊢ aD||Γ ⊢ ∀a. A||Γ ⊢ A → B|

=
=
=
=
=
=
=

1
1
1
1
1 + |Γ[Da = τ] ⊢ τ |1 + |Γ, a ⊢ A|
1 + |Γ ⊢ A| + |Γ ⊢ B|(∗)

Theorem 6.3 (Decidability of Algorithmic Consistent Subtyping). Given a context Γ andtypes A, B such that Γ ⊢ A and Γ ⊢ B and [Γ]A = A and [Γ]B = B, it is decidable whether there exists∆ such that Γ ⊢ A ≲ B ⊣ ∆.
Decidability of Algorithmic Typing. Similar to proving decidability of algorithmic consistentsubtyping, the key is to come up with a correct measure. Since the typing rules depend on thematching judgment, we first show decidability of the algorithmic matching.
Lemma 6.4 (Decidability of Algorithmic Matching). Given a context Γ and a type A it isdecidable whether there exist types A1 , A2 and a context ∆ such that Γ ⊢ A ▷ A1 → A2 ⊣ ∆.
Now we are ready to show decidability of typing. The proof is obtained by induction on the lexicographically ordered triple: size of e, typing judgment (where the inference mode ⇒ is consideredsmaller than the checking mode ⇐) and contextual size.
⇒e,|Γ ⊢ A|⇐,The above measure is much simpler than the corresponding one in the DK system, where they alsoneed to consider the application judgment together with the inference and checking judgments.
This shows another benefit (besides the independence from typing) of adopting the matching
judgment.
Theorem 6.5 (Decidability of Algorithmic Typing).
(1) Inference: Given a context Γ and a term e, it is decidable whether there exist a type A and acontext ∆ such that Γ ⊢ e ⇒ A ⊣ ∆.
(2) Checking: Given a context Γ, a term e and a type B such that Γ ⊢ B, it is decidable whether there
exists a context ∆ such that Γ ⊢ e ⇐ B ⊣ ∆.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:28Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

Γ −→ ∆(Context extension)Γ −→ ∆
ext-id• −→ •
Γ −→ ∆

Γ, x : A −→ ∆, x : A′Γ −→ ∆

ext-evarΓ, aD −→ ∆, aD[∆]A = [∆]A′

Γ −→ ∆
ext-varext-tvarΓ, a −→ ∆, a[∆]τ = [∆]τ ′Γ, aD = τ −→ ∆, aD = τ′

Γ −→ ∆
ext-solved

Γ, aD −→ ∆, aD = τ

Γ −→ ∆

Γ −→ ∆
ext-addΓ −→ ∆, aD

Γ −→ ∆, aD = τ

ext-solve

Γ −→ ∆
ext-addSolveext-marker

Γ, ▶aD−→ ∆, ▶aD

Fig. 16. Context extension

7

SOUNDNESS AND COMPLETENESS

To be confident that our algorithmic type system and the declarative type system agree with eachother, we need to prove that the algorithmic rules are sound and complete with respect to thedeclarative specification. Before we give the formal statements of the soundness and completenesstheorems, we need a meta-theoretical device, called context extension [Dunfield and Krishnaswami
2013], to capture a notion of information increase from input contexts to output contexts.
7.1

Context Extension

A context extension judgment Γ −→ ∆ reads “Γ is extended by ∆”. Intuitively, this judgment saysthat ∆ has at least as much information as Γ: some unsolved existential variables in Γ may besolved in ∆. The full inductive definition can be found Fig. 16. We refer the reader to Dunfield andKrishnaswami [2013, Section 4] for further explanation of context extension.
7.2

Soundness

Roughly speaking, soundness of the algorithmic system says that given a derivation of an algorithmic judgment with input context Γ, output context ∆, and a complete context Ω that extends∆, applying Ω throughout the given algorithmic judgment should yield a derivable declarative
judgment. For example, let us consider an algorithmic typing judgment • ⊢ λx. x ⇒ aD → aD ⊣ aD,
and any complete context, say, Ω = (Da = Int), then applying Ω to the above judgment yields• ⊢ λx. x : Int → Int, which is derivable in the declarative system.
However there is one complication: applying Ω to the algorithmic expression does not necessarily
yield a typable declarative expression. For example, by rule chk-lam we have λx. x ⇐ (∀a. a →a) → (∀a. a → a), but λx. x itself cannot have type (∀a. a → a) → (∀a. a → a) in the declarative
system. To circumvent that, we add an annotation to the lambda abstraction, resulting in λx :(∀a. a → a). x, which is typeable in the declarative system with the same type. To relate λx. x andλx : (∀a. a → a). x, we erase all annotations on both expressions.
Definition 7.1 (Type annotation erasure). The erasure function is denoted as ⌊·⌋, and defined asfollows:⌊x⌋ = x⌊n⌋ = n⌊λx : A. e⌋ = λx . ⌊e⌋⌊λx . e⌋ = λx . ⌊e⌋⌊e 1 e 2 ⌋ = ⌊e 1 ⌋ ⌊e 2 ⌋⌊e : A⌋ = ⌊e⌋
Theorem 7.2 (Instantiation Soundness). Given ∆ −→ Ω and [Γ]A = A and aD < fv(A):(1) If Γ ⊢ aD ⪅ A ⊣ ∆ then [Ω]∆ ⊢ [Ω]Da ≲ [Ω]A.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:29(2) If Γ ⊢ A ⪅ aD ⊣ ∆ then [Ω]∆ ⊢ [Ω]A ≲ [Ω]Da.
Notice that the declarative judgment uses [Ω]∆, an operation that applies a complete context Ω tothe algorithmic context ∆, essentially plugging in all known solutions and removing all declarationsof existential variables (both solved and unsolved), resulting in a declarative context.
With instantiation soundness, next we show that the algorithmic consistent subtyping is sound:
Theorem 7.3 (Soundness of Algorithmic Consistent Subtyping). If Γ ⊢ A ≲ B ⊣ ∆ where[Γ]A = A and [Γ]B = B and ∆ −→ Ω then [Ω]∆ ⊢ [Ω]A ≲ [Ω]B.
Finally the soundness theorem of algorithmic typing is:
Theorem 7.4 (Soundness of Algorithmic Typing). Given ∆ −→ Ω:(1) If Γ ⊢ e ⇒ A ⊣ ∆ then ∃e ′ such that [Ω]∆ ⊢ e ′ : [Ω]A and ⌊e⌋ = ⌊e ′⌋.
(2) If Γ ⊢ e ⇐ A ⊣ ∆ then ∃e ′ such that [Ω]∆ ⊢ e ′ : [Ω]A and ⌊e⌋ = ⌊e ′⌋.
7.3

CompletenessCompleteness of the algorithmic system is the reverse of soundness: given a declarative judgmentof the form [Ω]Γ ⊢ [Ω] . . . , we want to get an algorithmic derivation of Γ ⊢ · · · ⊣ ∆. It turns out thatcompleteness is a bit trickier to state in that the algorithmic rules generate existential variables on
the fly, so ∆ could contain unsolved existential variables that are not found in Γ, nor in Ω. Therefore
the completeness proof must produce another complete context Ω ′ that extends both the output
context ∆, and the given complete context Ω. As with soundness, we need erasure to relate both
expressions.
Theorem 7.5 (Instantiation Completeness). Given Γ −→ Ω and A = [Γ]A and aD < unsolved(Γ)
and aD < fv(A):(1) If [Ω]Γ ⊢ [Ω]Da ≲ [Ω]A then there are ∆, Ω ′ such that Ω −→ Ω ′ and ∆ −→ Ω ′ and Γ ⊢ aD ⪅A ⊣ ∆.
(2) If [Ω]Γ ⊢ [Ω]A ≲ [Ω]Da then there are ∆, Ω ′ such that Ω −→ Ω ′ and ∆ −→ Ω ′ and Γ ⊢ A ⪅aD ⊣ ∆.
Next is the completeness of consistent subtyping:
Theorem 7.6 (Generalized Completeness of Consistent Subtyping). If Γ −→ Ω and Γ ⊢ A
and Γ ⊢ B and [Ω]Γ ⊢ [Ω]A ≲ [Ω]B then there exist ∆ and Ω ′ such that ∆ −→ Ω ′ and Ω −→ Ω ′ andΓ ⊢ [Γ]A ≲ [Γ]B ⊣ ∆.
We prove that the algorithmic matching is complete with respect to the declarative matching:
Theorem 7.7 (Matching Completeness). Given Γ −→ Ω and Γ ⊢ A, if [Ω]Γ ⊢ [Ω]A ▷ A1 → A2
then there exist ∆, Ω ′, A′1 and A′2 such that Γ ⊢ [Γ]A ▷ A′1 → A′2 ⊣ ∆ and ∆ −→ Ω ′ and Ω −→ Ω ′ andA1 = [Ω ′]A′1 and A2 = [Ω ′]A′2 .
Finally here is the completeness theorem of the algorithmic typing:
Theorem 7.8 (Completeness of Algorithmic Typing). Given Γ −→ Ω and Γ ⊢ A, if [Ω]Γ ⊢ e : A
then there exist ∆, Ω ′, A′ and e ′ such that ∆ −→ Ω ′ and Ω −→ Ω ′ and Γ ⊢ e ′ ⇒ A′ ⊣ ∆ and
A = [Ω ′]A′ and ⌊e⌋ = ⌊e ′⌋.
8

SIMPLE EXTENSIONS AND VARIANTS

This section considers two simple variations on the presented system. The first variation extends
the system with a top type, while the second variation considers a more declarative formulation
using a subsumption rule.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:30
8.1

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers
Top Types

We argued that our definition of consistent subtyping (Definition 4.1) generalizes the original
definition by Siek and Taha [2007]. We have shown its applicability to polymorphic types, forwhich Siek and Taha [2007] approach cannot be extended naturally. To strengthen our argument,
we show how to extend our approach to Top types, which is also not supported by Siek and Taha
[2007] approach.
Consistent Subtyping with ⊤. In order to preserve the orthogonality between subtyping andconsistency, we require ⊤ to be a common supertype of all static types, as shown in rule S-Top.
This rule might seem strange at first glance, since even if we remove the requirement A static,
the rule still seems reasonable. However, an important point is that, because of the orthogonality
between subtyping and consistency, subtyping itself should not contain a potential information
loss! Therefore, subtyping instances such as ⋆ <: ⊤ are not allowed. For consistency, we add therule that ⊤ is consistent with ⊤, which is actually included in the original reflexive rule A ∼ A. For
consistent subtyping, every type is a consistent subtype of ⊤, for example, Int → ⋆ ≲ ⊤.
A staticΨ ⊢ A <: ⊤

⊤∼⊤

S-Top

CS-TopΨ⊢A≲⊤

It is easy to verify that Definition 4.1 is still equivalent to that in Fig. 8 extended with rule CS-Top.
That is, T heorem 1 holds:
Proposition 8.1 (Extension with ⊤). Ψ ⊢ A ≲ B ⇔ Ψ ⊢ A <: C, C ∼ D, Ψ ⊢ D <: B, for someC, D.
We extend the definition of concretization (Definition 4.3) with ⊤ by adding another equation
γ (⊤) = {⊤}. Note that Castagna and Lanvin [2017] also have this equation in their calculus. It iseasy to verify that Corollary 4.5 still holds:
H B.
Proposition 8.2 (Eqivalent to AGT on ⊤). A ≲ B if only if A <:Siek and Taha’s Definition of Consistent Subtyping Does Not Work for ⊤. As with the analysis in
Section 4.2, Int → ⋆ ≲ ⊤ only holds when we first apply consistency, then subtyping. However
we cannot find a type A such that Int → ⋆ <: A and A ∼ ⊤. The following diagram depicts thesituation:
∼
∅
⊤
<:

<:
Int → ⋆∼

Int → Int

Additionally we have a similar problem in extending the restriction operator: non-structural masking
between Int → ⋆ and ⊤ cannot be easily achieved.
Note that both the top and universally quantified types can be seen as special cases of intersection
types. Indeed, top is the intersection of the empty set, while a universally quantified type is
the intersection of the infinite set of its instantiations [Davies and Pfenning 2000]. Recall from
Section 4.3 that Castagna and Lanvin [2017] shows that consistent subtyping from AGT works wellfor intersection types, and our definition coincides with AGT (Corollary 4.5 and Proposition 8.2).
We thus believe that our definition is compatible with conventional binary intersection types aswell. Yet, a rigorous formalization would be needed to substantiate this belief.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All
8.2

39:31

A More Declarative Type System

In Section 5 we present our declarative system in terms of the matching and consistent subtyping
judgments. The rationale behind this design choice is that the resulting declarative system combines
subtyping and type consistency in the application rule, thus making it easier to design an algorithmic
system accordingly. Still, one may wonder if it is possible to design a more declarative specification.
For example, even though we mentioned that the subsumption rule is incompatible with consistentsubtyping, it might be possible to accommodate a subsumption rule for normal subtyping (insteadof consistent subtyping). In this section, we discuss an alternative for the design of the declarative
system.
Wrong Design. A naive design that does not work is to replace rule App in Fig. 9 with the following
two rules:Ψ⊢e :A
A <: BΨ ⊢ e1 : AΨ ⊢ e 2 : A1
A ∼ A1 → A2
V-Sub

V-App1Ψ⊢e :BΨ ⊢ e 1 e 2 : A2

Rule V-Sub is the standard subsumption rule: if an expression e has type A, then it can be assigned
some type B that is a supertype of A. Rule V-App1 first infers that e 1 has type A, and e 2 has type A1 ,then it finds some A2 so that A is consistent with A1 → A2 .
There would be two obvious benefits of this variant if it did work: firstly this approach closely
resembles the traditional declarative type systems for calculi with subtyping; secondly it saves us
from discussing various forms of A in rule V-App1, leaving the job to the consistency judgment.
The design is wrong because of the information loss caused by the choice of A2 in rule V-App1.
Suppose we have Ψ ⊢ plus : Int → Int → Int, then we can apply it to 1 to getΨ ⊢ plus : Int → Int → IntΨ ⊢ 1 : Int

Int → Int → Int ∼ Int → ⋆ → Int
V-App1Ψ ⊢ plus 1 : ⋆ → Int
Further applying it to true we getΨ ⊢ plus 1 ⇒ ⋆ → Int⋆ → Int ∼ Bool → IntΨ ⊢ true : Bool

V-App1Ψ ⊢ plus 1 true : Int
which is obviously wrong! The type consistency in rule V-App1 causes information loss for boththe argument type A1 and the return type A2 . The problem is that information of A2 can get lostagain if it appears in further applications. The moral of the story is that we should be very carefulwhen using type consistency. We hypothesize that it is inevitable to do case analysis for the type ofthe function in an application (i.e., A in rule V-App1).
Proper Declarative Design. The proper design refines the first variant by using a matching
judgment to carefully distinguish two cases for the typing result of e 1 in rule V-App1: (1) when it isan arrow type, and (2) when it is an unknown type. This variant replaces rule App in Fig. 9 withthe following rules:Γ ⊢e :A

A <: BΨ⊢e:AΨ ⊢ A ▷ A1 → A2

Ψ ⊢ e2 : A3

V-Sub

A1 ∼ A3
V-App2Γ ⊢e :BΨ ⊢ e1 e2 : A2
Ψ ⊢ A1 → A2 ▷ A1 → A2

Ψ ⊢⋆▷⋆→⋆

Rule V-Sub is the same as in the first variant. In rule V-App2, we infer that e 1 has type A, and use
the matching judgment to get an arrow type A1 → A2 . Then we need to ensure that the argument
type A3 is consistent with (rather than a consistent subtype of) A1 , and use A2 as the result type
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:32

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijversof the application. The matching judgment only deals with two cases, as polymorphic types arehandled by rule V-Sub. These rules are closely related to the ones in Siek and Taha [2006] and Siek
and Taha [2007].
The more declarative nature of this system also implies that it is highly non-syntax-directed,
and it does not offer any insight into combining subtyping and consistency. We have proved in
Coq the following lemmas to establish soundness and completeness of this system with respect toour original system (to avoid ambiguity, we use the notation ⊢m to indicate the more declarative
version):Lemma 5 (Completeness of ⊢m ). If Γ ⊢ e : A, then Γ ⊢m e : A.
Lemma 6 (Soundness of ⊢m ). If Γ ⊢m e : A, then there exists some B, such that Γ ⊢ e : B andΓ ⊢ B <: A.
9

RESTORING THE DYNAMIC GRADUAL GUARANTEE WITH TYPE PARAMETERS

In Section 5.2 we have seen an example where a single source expression could produce twodifferent target expressions with different runtime behaviors. As we explained, this is due to theguessing nature of the declarative system, and, from the (source) typing point of view, no guessed
type is particularly better than any other. As a consequence, this breaks the dynamic gradualguarantee as discussed in Section 5.3.
To alleviate this situation, we introduce static type parameters, which are placeholders formonotypes, and gradual type parameters, which are placeholders for monotypes that are consistent
with the unknown type. The concept of static type parameters and gradual type parameters in thecontext of gradual typing was first introduced by Garcia and Cimini [2015], and later played a central
role in the work of Igarashi et al. [2017]. In our type system, type parameters mainly help capture
the notion of representative translations, and should not appear in a source program. With them weare able to recast the dynamic gradual guarantee in terms of representative translations, and toprove that every well-typed source expression possesses at least one representative translation.
With a coherence conjecture regarding representative translations, the dynamic gradual guaranteeof our extended source language now can be reduced to that of λB, which, at the time of writing, isstill an open question.
9.1 Declarative Type System
The new syntax of types is given at the top of Fig. 17, with the differences highlighted. In addition
to the types of Fig. 4, we add static type parameters S, and gradual type parameters G. Both kindsof type parameters are monotypes. The addition of type parameters, however, leads to two newsyntactic categories of types. Castable types C represent types that can be cast from or to ⋆. It
includes all types, except those that contain static type parameters. Castable monotypes t are thosecastable types that are also monotypes.
Consistent Subtyping. The new definition of consistent subtyping is given at the bottom of Fig. 17,
again with the differences highlighted. Now the unknown type is only a consistent subtype of all
castable types, rather than of all types (rule cs-unknownLL), and vice versa (rule cs-unknownRR).
Moreover, the static type parameter S is a consistent subtype of itself (rule cs-spar), and similarly
for the gradual type parameter (rule cs-gpar). From this definition it follows immediately that ⋆ isincomparable with types that contain static type parameters S, such as S → Int.
Typing and Translation. Given these extensions to types and consistent subtyping, the typing
process remains the same as in Fig. 9. To account for the changes in the translation, if we extend λB
with type parameters as in Garcia and Cimini [2015], then the translation remains the same as well.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:33

Types

A, B

::=

Int | a | A → B | ∀a. A | ⋆ | S | G

Monotypes

τ,σ

::=

Int | a | τ → σ | S | G

Castable Types

C::=

Int | a | C1 → C2 | ∀a. C | ⋆ | G

Castable Monotypest::=

Int | a | t 1 → t 2 | GΨ⊢A≲B(Consistent Subtyping)a∈ΨΨ ⊢ B1 ≲ A1
cs-tvarΨ⊢τΨ, a ⊢ A ≲ B

cs-arrowΨ ⊢ A1 → A2 ≲ B1 → B2

Ψ ⊢ A[a 7→ τ ] ≲ B

cs-forallRcs-forallLΨ ⊢ A ≲ ∀a. B
Ψ⊢C≲⋆Ψ ⊢ A2 ≲ B2

cs-intΨ ⊢ Int ≲ IntΨ⊢a≲aΨ ⊢ ∀a. A ≲ B
cs-unknownRRΨ⊢⋆≲C

cs-unknownLL

cs-sparΨ⊢S≲S

cs-gparΨ⊢G≲G

Fig. 17. Syntax of types, and consistent subtyping in the extended declarative system.

9.2

Substitutions and Representative Translations

As we mentioned, type parameters serve as placeholders for monotypes. As a consequence, wherevera type parameter is used, any suitable monotype could appear just as well. To formalize thisobservation, we define substitutions for type parameters as follows:
Definition 9.1 (Substitution). Substitutions for type parameters are defined as:(1) Let S S : S → τ be a total function mapping static type parameters to monotypes.
(2) Let S G : G → t be a total function mapping gradual type parameters to castable monotypes.
(3) Let S P = S G ∪ S S be a union of S S and S G mapping static and gradual type parameters
accordingly.
Note that since G might be compared with ⋆, only castable monotypes are suitable substitutes,
whereas S can be replaced by any monotypes. Therefore, we can substitute G for S, but not theother way around.
Let us go back to our example and its two translations in Section 5.2. The problem with thosetranslations is that neither Int → Int nor Bool → Int is general enough. With type parameters,
however, we can state a more general translation that covers both through substitution:f : ∀a.a → Int ⊢ (λx : ⋆. f x ) : ⋆ → Int⇝ (λx : ⋆. (⟨∀a.a → Int ,→ G → Int⟩ f ) ( ⟨⋆ ,→ G⟩ x ))The advantage of type parameters is that they help reasoning about the dynamic semantics. Now
we are not limited to a particular choice, such as Int → Int or Bool → Int, which might or might
not emit a cast error at runtime. Instead we have a general choice G → Int.
What does the more general choice with type parameters tell us? First, we know that in this case,there is no concrete constraint on a, so we can instantiate it with a type parameter. Second, thefact that the general choice uses G rather than S indicates that any chosen instantiation needs tobe a castable type. It follows that any concrete instantiation will have an impact on the runtime
behavior; therefore it is best to instantiate a with ⋆. However, type inference cannot instantiate
a with ⋆, and substitution cannot replace G with ⋆ either. This means that we need a syntactic
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:34

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

refinement process of the translated programs in order to replace type parameters with allowed
gradual types.
Syntactic Refinement. We define syntactic refinement of the translated expressions as follows. As
S denotes no constraints at all, substituting it with any monotype would work. Here we arbitrarily
use Int. We interpret G as ⋆ since any monotype could possibly lead to a cast error.
Definition 9.2 (Syntactic Refinement). The syntactic refinement of a translated expression s isdenoted by ⌈s⌉, and defined as follows:⌈Int⌉⌈A → B⌉
⌈⋆⌉
⌈G⌉

= Int
= ⌈A⌉ → ⌈B⌉
= ⋆
= ⋆

⌈a⌉
⌈∀a.A⌉⌈S⌉= a= ∀a.⌈A⌉= Int

Applying the syntactic refinement to the translated expression, we get(λx : ⋆. (⟨∀a.a → Int ,→ ⋆ → Int⟩ f ) (⟨⋆ ,→ ⋆ ⟩ x ))where two G are refined by ⋆ as highlighted. It is easy to verify that both applying this expression
to 3 and to true now results in a translation that evaluates to a value.
Representative Translations. To decide whether one translation is more general than the other,
we define a preorder between translations.
Definition 9.3 (Translation Pre-order). Suppose Ψ ⊢ e : A ⇝ s 1 and Ψ ⊢ e : A ⇝ s 2 , we defines 1 ≤ s 2 to mean s 2 ≡α S P (s 1 ) for some S P .
Proposition 9.4. If s 1 ≤ s 2 and s 2 ≤ s 1 , then s 1 and s 2 are α-equivalent (i.e., equivalent up torenaming of type parameters).
The preorder between translations gives rise to a notion of what we call representative translations:Definition 9.5 (Representative Translation). A translation s is said to be a representative translationof a typing derivation Ψ ⊢ e : A ⇝ s if and only if for any other translation Ψ ⊢ e : A ⇝ s ′ suchthat s ′ ≤ s, we have s ≤ s ′. From now on we use r to denote a representative translation.
An important property of representative translations, which we conjecture for the lack of rigorous
proof, is that if there exists any translation of an expression that (after syntactic refinement)
can reduce to a value, so can a representative translation of that expression. Conversely, if a
representative translation runs into a blame, then no translation of that expression can reduce to avalue.
Conjecture 9.6 (Property of Representative Translations). For any expression e such thatΨ ⊢ e : A ⇝ s and Ψ ⊢ e : A ⇝ r and ∀C. C : (Ψ ⊢B A) ⇝ (• ⊢B Int), we have
• If C{⌈s⌉} ⇓ n, then C{⌈r ⌉} ⇓ n.
• If C{⌈r ⌉} ⇓ blame, then C{⌈s⌉} ⇓ blame.
Given this conjecture, we can state a stricter coherence property (without the “up to casts” part)
between any two representative translations. We first strengthen Definition 5.1 following Ahmed
et al. [2017]:
Definition 9.7 (Contextual Approximation à la Ahmed et al. [2017]).
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for AllΨ ⊢ s 1 ⪯ct x s 2 : A

39:35
≜

Ψ ⊢B s 1 : A ∧ Ψ ⊢B s 2 : A ∧for all C. C : (Ψ ⊢B A) ⇝ (• ⊢B Int) =⇒(C{⌈s 1 ⌉} ⇓ n =⇒ C{⌈s 2 ⌉} ⇓ n) ∧(C{⌈s 1 ⌉} ⇓ blame =⇒ C{⌈s 2 ⌉} ⇓ blame)

The only difference is that now when a program containing s 1 reduces to a value, so does one
containing s 2 .
From Conjecture 9.6, it follows that coherence holds between two representative translations of
the same expression.
Corollary 9.8 (Coherence for Representative Translations). For any expression e suchthat Ψ ⊢ e : A ⇝ r 1 and Ψ ⊢ e : A ⇝ r 2 , we have Ψ ⊢ r 1 ⋍ct x r 2 : A.
We have proved that for every typing derivation, at least one representative translation exists.
Lemma 9.9 (Representative Translation for Typing). For any typing derivation Ψ ⊢ e : A
there exists at least one representative translation r such that Ψ ⊢ e : A ⇝ r .
For our example, (λx : ⋆. (⟨∀a.a → Int ,→ G → Int⟩ f ) (⟨⋆ ,→ G⟩ x )) is a representativetranslation, while the other two are not.
9.3

Dynamic Gradual Guarantee, Reloaded

Given the above propositions, we are ready to revisit the dynamic gradual guarantee. The nice thing
about representative translations is that the dynamic gradual guarantee of our source language isessentially that of λB, our target language. However, the dynamic gradual guarantee for λB is still
an open question. According to Igarashi et al. [2017], the difficulty lies in the definition of term
precision that preserves the semantics. We leave it here as a conjecture as well. From a declarative
point of view, we cannot prevent the system from picking undesirable instantiations, but we knowthat some choices are better than the others, so we can restrict the discussion of dynamic gradualguarantee to representative translations.
Conjecture 9.10 (Dynamic Gradual Guarantee in terms of Representative Translations).
Suppose e ′ ⊑ e,(1) If • ⊢ e : A ⇝ r , ⌈r ⌉ ⇓ v, then for some B and r ′, we have • ⊢ e ′ : B ⇝ r ′, and B ⊑ A, and⌈r ′⌉ ⇓ v ′, and v ′ ⊑ v.
(2) If • ⊢ e ′ : B ⇝ r ′, ⌈r ′⌉ ⇓ v ′, then for some A and r , we have • ⊢ e : A ⇝ r , and B ⊑ A. Moreover,⌈r ⌉ ⇓ v and v ′ ⊑ v, or ⌈r ⌉ ⇓ blame.
For the example in Section 5.3, now we know that the representative translation of the right one
will evaluate to 1 as well.
(λ f : ∀a.a → Int. λx : Int. f x ) (λx . 1) 3

(λ f : ∀a.a → Int. λx : ⋆. f x ) (λx . 1) 3

More importantly, in what follows, we show that our extended algorithm is able to find those
representative translations.
9.4

Extended Algorithmic Type System

To understand the design choices involved in the new algorithmic system, we consider the following
algorithmic typing example:
f : ∀a. a → Int, x : ⋆ ⊢ f x ⇒ Int ⊣ f : ∀a. a → Int, x : ⋆, aD
Compared with the declarative typing, where we have many choices (e.g., Int → Int, Bool → Int,and so on) to instantiate ∀a. a → Int, the algorithm computes the instantiation aD → Int with aD
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:36

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers
Types

A, B

::=

Int | a | aD | A → B | ∀a. A | ⋆ | S | G

Monotypes

τ,σ

::=

Int | a | aD | τ → σ | S | G

Existential variables
Castable TypesaD ::=C ::=aDS | aDG
Int | a | aD | C1 → C2 | ∀a. C | ⋆ | G

Castable Monotypest::=

Int | a | aD | t 1 → t 2 | G

Algorithmic Contexts

Γ, ∆, Θ::=• | Γ, x : A | Γ, a | Γ, aD | Γ, aDS = τ | Γ, aDG = t | Γ, ▶aDΩ::=• | Ω, x : A | Ω, a | Ω, aDS = τ | Ω, aDG = t | Ω, ▶aD

Complete Contexts

Fig. 18. Syntax of types, contexts and consistent subtyping in the extended algorithmic system.

unsolved in the output context. What can we know from the algorithmic typing? First we know
that, here aD is not constrained by the typing problem. Second, and more importantly, aD has been
compared with an unknown type (when typing (f x)). Therefore, it is possible to make a morerefined distinction between different kinds of existential variables. The first kind of existential
variables are those that indeed have no constraints at all, as they do not affect the dynamic semantics;
while the second kind (as in this example) are those where the only constraint is that the variable
was once compared with an unknown type [Garcia and Cimini 2015].
The syntax of types is shown in Fig. 18. A notable difference, apart from the addition of static andgradual parameters, is that we further split existential variables aD into static existential variables
aDS and gradual existential variables aDG . Depending on whether an existential variable has been
compared with ⋆ or not, its solution space changes. More specifically, static existential variables canbe solved to a monotype τ , whereas gradual existential variables can only be solved to a castable
monotype t, as can be seen in the changes of algorithmic contexts and complete contexts. As aresult, the typing result for the above example now becomesf : ∀a. a → Int, x : ⋆ ⊢ f x ⇒ Int ⊣ f : ∀a. a → Int, x : ⋆, aDG
since we can solve any unconstrained aDG to G, it is easy to verify that the resulting translation isindeed a representative translation.
Our extended algorithm is novel in the following aspects. We naturally extend the conceptof existential variables [Dunfield and Krishnaswami 2013] to deal with comparisons between
existential variables and unknown types. Unlike Garcia and Cimini [2015], where they use an
extra set to store types that have been compared with unknown types, our two kinds of existential
variables emphasize the type distinction better, and correspond more closely to the two kinds oftype parameters, as we can solve aDS to S and aDG to G.
The implementation of the algorithm can be found in the supplementary materials.
Extended Algorithmic Consistent Subtyping. While the changes in the syntax seem negligible, theaddition of static and gradual type parameters changes the algorithmic judgments in a significant
way. We first discuss the algorithmic consistent subtyping, which is shown in Fig. 19. For notational
convenience, when static and gradual existential variables have the same rule form, we compress
them into one rule. For example, rule as-evar is really two rules Γ[Da S ] ⊢ aDS ≲ aDS ⊣ Γ[Da S ] and
Γ[DaG ] ⊢ aDG ≲ aDG ⊣ Γ[DaG ]; same for rules as-instL and as-instR.
Rules as-spar and as-gpar are direct analogies of rules cs-spar and cs-gpar. Though looking
simple, rules as-unknownLL and as-unknownRR deserve much explanation. To understandwhat the output context contaminate(Γ, C) is for, let us first see why this seemingly intuitive ruleΓ ⊢ ⋆ ≲ C ⊣ Γ (like rule as-unknownL in the original algorithmic system) is wrong. Consider
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:37

Γ⊢A≲B ⊣∆

(Algorithmic Consistent Subtyping)
as-tvaras-intas-evarΓ ⊢ Int ≲ Int ⊣ ΓΓ[a] ⊢ a ≲ a ⊣ Γ[a]

Γ[Da ] ⊢ aD ≲ aD ⊣ Γ[Da]as-sparas-gparΓ⊢S≲S⊣ΓΓ ⊢ ⋆ ≲ C ⊣ contaminate(Γ, C)Γ ⊢ B 1 ≲ A1 ⊣ ΘΓ⊢G≲G⊣Γ
as-unknownLLΓ ⊢ C ≲ ⋆ ⊣ contaminate(Γ, C)

as-unknownRRΓ, a ⊢ A ≲ B ⊣ ∆, a, ΘΘ ⊢ [Θ]A2 ≲ [Θ]B 2 ⊣ ∆as-arrow

as-forallRΓ ⊢ A1 → A2 ≲ B 1 → B 2 ⊣ ∆Γ ⊢ A ≲ ∀a. B ⊣ ∆Γ, ▶aDS , aDS ⊢ A[a 7→ aDS ] ≲ B ⊣ ∆, ▶aDS , Θ

as-forallLLΓ ⊢ ∀a. A ≲ B ⊣ ∆aD < fv(A)aD < fv(A)Γ[Da ] ⊢ aD ⪅ A ⊣ ∆Γ[Da ] ⊢ A ⪅ aD ⊣ ∆as-instLΓ[Da ] ⊢ aD ≲ A ⊣ ∆as-instRΓ[Da ] ⊢ A ≲ aD ⊣ ∆Fig. 19. Extended algorithmic consistent subtyping

the judgment aDS ⊢ ⋆ ≲ aDS → aDS ⊣ aDS , which seems fine. If this holds, then – since aDS is unsolvedin the output context – we can solve it to S for example (recall that aDS can be solved to somemonotype), resulting in ⋆ ≲ S → S. However, this is in direct conflict with rule cs-unknownLL in
the declarative system precisely because S → S is not a castable type! A possible solution would
be to transform all static existential variables to gradual existential variables within C whenever
it is being compared to ⋆: while aDS ⊢ ⋆ ≲ aDS → aDS ⊣ aDS does not hold, aDG ⊢ ⋆ ≲ aDG → aDG ⊣ aDG
does. While substituting static existential variables with gradual existential variables seems to be
intuitively correct, it is rather hard to formulate—not only do we need to perform substitution in C,
we also need to substitute accordingly in both the input and output contexts in order to ensurethat no existential variables become unbound. However, making such changes is at odds with theinterpretation of input contexts: they are “input”, which evolve into output contexts with morevariables solved. Therefore, in line with the use of input contexts, a simple solution is to generate a
new gradual existential variable and solve the static existential variable to it in the output context,
without touching C at all. So we have aDS ⊢ ⋆ ≲ aDS → aDS ⊣ aDG , aDS = aDG .
Based on the above discussion, the following defines contaminate(Γ, A):
Definition 9.11. contaminate(Γ, A) is defined inductively as follows
contaminate(•, A)
contaminate((Γ, x : A), A)
contaminate((Γ, a), A)
contaminate((Γ, aDS ), A)
contaminate((Γ, aDS ), A)
contaminate((Γ, aDG ), A)
contaminate((Γ, aD = τ ), A)
contaminate((Γ, ▶aD), A)

=
=
=
=
=
=
=
=

•
contaminate(Γ, A), x : A
contaminate(Γ, A), a
contaminate(Γ, A), aDG , aDS = aDG
contaminate(Γ, A), aDS
contaminate(Γ, A), aDG
contaminate(Γ, A), aD = τ
contaminate(Γ, A), ▶aD

if aDS occurs in A
if aDS does not occur in A

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:38Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

Γ ⊢ aD ⪅ A ⊣ ∆(Instantiation I)
Γ ⊢τ

Γ ⊢t

Γ, aDS , Γ ′ ⊢ aDS ⪅ τ ⊣ Γ, aDS = τ , Γ ′instl-solveSΓ[Da S ] ⊢ aDS ⪅ ⋆ ⊣ Γ[DaG , aDS = aDG ]Γ, aDG , Γ ′ ⊢ aDG ⪅ t ⊣ Γ, aDG = t, Γ ′instl-solveUS

Γ[DaG ] ⊢ aDG ⪅ ⋆ ⊣ Γ[D
aG ]

Γ[D
a S ][bDG ] ⊢ aDS ⪅ bDG ⊣ Γ[DaG , aDS = aDG ][bDG = aDG ]instl-reachSG1

Γ[bDS ][DaG ] ⊢ aDG ⪅ bDS ⊣ Γ[bDG , bDS = bDG ][DaG = bDG ]instl-reachSG2

D ⊢ aD ⪅ bD ⊣ Γ[DΓ[Da ][b]
a ][bD = aD]

instl-solveG

instl-solveUG

Γ[Da ], b ⊢ aD ⪅ B ⊣ ∆, b, Θ

instl-reachOther

instl-forallRΓ[Da ] ⊢ aD ⪅ ∀b. B ⊣ ∆Γ[Da 2 , aD1 , aD = aD1 → aD2 ] ⊢ A1 ⪅ aD1 ⊣ ΘΘ ⊢ aD2 ⪅ [Θ]A2 ⊣ ∆instl-arr

Γ[Da ] ⊢ aD ⪅ A1 → A2 ⊣ ∆Γ ⊢ A ⪅ aD ⊣ ∆(Instantiation II, excerpt)
Γ[Da ], ▶bD , bDS ⊢ B[b 7→ bDS ] ⪅ aD ⊣ ∆, ▶bD , ΘSS

instr-forallLLΓ[Da ] ⊢ ∀b. B ⪅ aD ⊣ ∆Fig. 20. Instantiation in the extended algorithmic system

contaminate(Γ, A) solves all static existential variables found within A to fresh gradual existential
variables in Γ. Notice the case for contaminate((Γ, aDS ), A) is exactly what we have just described.
Rule as-forallLL is slightly different from rule as-forallL in the original algorithmic systemin that we replace a with a new static existential variable aDS . Note that aDS might be solved to a
gradual existential variable later. The rest of the rules are the same as those in the original system.
Extended Instantiation. The instantiation judgments shown in Fig. 20 also change significantly.
The complication comes from the fact that now we have two different kinds of existential variables,
and the relative order they appear in the context affects their solutions.
Rules instl-solveS and instl-solveG are the refinement to rule instl-solve in the original
system. The next two rules deal with situations where one side is an existential variable and theother side is an unknown type. Rule instl-solveUS is a special case of rule as-unknownRR where
we create a new gradual existential variable aDG and set the solution of aDS to be aDG in the output
context. Rule instl-solveUG is the same as rule instl-solveU in the original system and simply
propagates the input context. The next two rules instl-reachSG1 and instl-reachSG2 are a bit
involved, but they both answer to the same question: how to solve a gradual existential variable
when it is declared after some static existential variable. More concretely, in rule instl-reachSG1,
we feel that we need to solve bDG to another existential variable. However, simply setting bDG = aDS
and leaving aDS untouched in the output context is wrong. The reason is that bDG could be a gradualexistential variable created by rule as-unknownLL/as-unknownRR and solving bDG to a static
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:39

existential variable would result in the same problem as we have discussed. Instead, we create
another new gradual existential variable aDG and set the solutions of both aDS and bDG to it; similarly inrule instl-reachSG2. Rule instl-reachOther deals with the other cases (e.g., aDS ⪅ bDS , aDG ⪅ bDG
and so on). In those cases, we employ the same strategy as in the original system.
As for the other instantiation judgment, most of the rules are symmetric and thus omitted. The
only interesting rule is instr-forallLL, which is similar to what we did for rule as-forallLL.
Algorithmic Typing and Metatheory. Fortunately, the changes in the algorithmic bidirectional
system are minimal: we replace every existential variable with a static existential variable. Furthermore, we proved that the extended algorithmic system is sound and complete with respect to theextended declarative system. The proofs can be found in the appendix.
Do We Really Need Type Parameters in the Algorithmic System? As we mentioned earlier, typeparameters in the declarative system are merely an analysis tool, and in practice, type parameters
are inaccessible to programmers. For the sake of proving soundness and completeness, we have toendow the algorithmic system with type parameters. However, the algorithmic system already has
static and gradual existential variables, which can serve the same purpose. In that regard, we could
directly solve every unsolved static and gradual existential variable in the output context to Int and⋆, respectively.
9.5 Restricted Generalization
In Section 5.2, we discussed the issue that the translation produces multiple target expressions dueto the different choices for instantiations, and those translations have different dynamic semantics.
Besides that, there is another cause for multiple translations: redundant generalization duringtranslation by rule gen. Consider the simple expression (λx : Int. x) 1, the following shows two
possible translations:• ⊢ (λx : Int. x) 1 : Int ⇝ (λx : Int. x) (⟨Int ,→ Int⟩1)• ⊢ (λx : Int. x) 1 : Int ⇝ (λx : Int. x) (⟨∀a. Int ,→ Int⟩(Λa. 1))
The difference comes from the fact that in the second translation, we apply rule gen while typing 1 toget • ⊢ 1 : ∀a. Int. As a consequence, the translation of 1 is accompanied by a cast from ∀a. Int to Int
since the former is a consistent subtype of the latter. This difference is harmless, because obviously
these two expressions will reduce to the same value in λB, thus preserving coherence (up to casterror). While it is not going to break coherence, it does result in multiple representative translations
for one expression (e.g., the above two translations are both the representative translations).
There are several ways to make the translation process more deterministic. For example, we
can restrict generalization to happen only in let expressions and require let expressions to include
annotations, as let x : A = e1 in e2 . Another feasible option would be to give a declarative, bidirectional system as the specification (instead of the type assignment one), in the same spirit ofDunfield and Krishnaswami [2013]. Then we can restrict generalization to be performed throughannotations in checking mode.
With restricted generalization, we hypothesize that now each expression has exactly one representative translation (up to renaming of fresh type parameters). Instead of calling it a representativetranslation, we can say it is a principal translation. Of course the above is only a sketch; we havenot defined the corresponding rules, nor studied metatheory.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:4010

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

RELATED WORK

Along the way we discussed some of the most relevant work to motivate, compare and promote
our gradual typing design. In what follows, we briefly discuss related work on gradual typing andpolymorphism.
Gradual Typing. The seminal paper by Siek and Taha [2006] is the first to propose gradualtyping, which enables programmers to mix static and dynamic typing in a program by providing amechanism to control which parts of a program are statically checked. The original proposal extends
the simply typed lambda calculus by introducing the unknown type ⋆ and replacing type equality
with type consistency. Casts are introduced to mediate between statically and dynamically typed
code. Later Siek and Taha [2007] incorporated gradual typing into a simple object oriented language,
and showed that subtyping and consistency are orthogonal – an insight that partly inspired ourwork. We show that subtyping and consistency are orthogonal in a much richer type systemwith higher-rank polymorphism. Siek et al. [2009] explores the design space of different dynamic
semantics for simply typed lambda calculus with casts and unknown types. In the light of theever-growing popularity of gradual typing, and its somewhat murky theoretical foundations, Siek
et al. [2015] felt the urge to have a complete formal characterization of what it means to be gradually
typed. They proposed a set of criteria that provides important guidelines for designers of gradually
typed languages. Cimini and Siek [2016] introduced the Gradualizer, a general methodology for
generating gradual type systems from static type systems. Later they also develop an algorithm
to generate dynamic semantics [Cimini and Siek 2017]. Garcia et al. [2016] introduced the AGT
approach based on abstract interpretation. As we discussed, none of these approaches instructed
us how to define consistent subtyping for polymorphic types.
There is some work on integrating gradual typing with rich type disciplines. Bañados Schwerter
et al. [2014] establish a framework to combine gradual typing and effects, with which a static
effect system can be transformed to a dynamic effect system or any intermediate blend. Jafery
and Dunfield [2017] present a type system with gradual sums, which combines refinement andimprecision. We have discussed the interesting definition of directed consistency in Section 4.
Castagna and Lanvin [2017] develop a gradual type system with intersection and union types, withconsistent subtyping defined by following the idea of Garcia et al. [2016]. TypeScript [Bierman
et al. 2014] has a distinguished dynamic type, written any, whose fundamental feature is that any
type can be implicitly converted to and from any. Our treatment of the unknown type in Fig. 8 issimilar to their treatment of any. However, their type system does not have polymorphic types.
Also, Unlike our consistent subtyping which inserts runtime casts, in TypeScript, type information
is erased after compilation so there are no runtime casts, which makes runtime type errors possible.
Gradual Type Systems with Explicit Polymorphism. Morris [1973] dynamically enforces parametricpolymorphism and uses sealing functions as the dynamic type mechanism. More recent works
on integrating gradual typing with parametric polymorphism include the dynamic type of Abadiet al. [1995] and the Sage language of Gronski et al. [2006]. None of these has carefully studied
the interaction between statically and dynamically typed code. Ahmed et al. [2011] proposed λBthat extends the blame calculus [Wadler and Findler 2009] to incorporate polymorphism. The key
novelty of their work is to use dynamic sealing to enforce parametricity. As such, they end up witha sophisticated dynamic semantics. Later, Ahmed et al. [2017] prove that with more restrictions,
λB satisfies parametricity. Compared to their work, our type system can catch more errors earlier
since, as we argued, their notion of compatibility is too permissive. For example, the following is
rejected (more precisely, the corresponding source program never gets elaborated) by our type
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:41

system:(λx : ⋆. x + 1) : ∀a.a → a ⇝ ⟨⋆ → Int ,→ ∀a.a → a⟩ (λx : ⋆. x + 1)
while the type system of λB would accept the translation, though at runtime, the program would
result in a cast error as it violates parametricity. We emphasize that it is the combination of ourpowerful type system together with the powerful dynamic semantics of λB that makes it possible
to have implicit higher-rank polymorphism in a gradually typed setting. Devriese et al. [2017]
proved that embedding of System F terms into λB is not fully abstract. Igarashi et al. [2017] alsostudied integrating gradual typing with parametric polymorphism. They proposed System FG , agradually typed extension of System F, and System FC , a new polymorphic blame calculus. As
has been discussed extensively, their definition of type consistency does not apply to our setting(implicit polymorphism). All of these approaches mix consistency with subtyping to some extent,
which we argue should be orthogonal. On a side note, it seems that our calculus can also be safely
translated to System FC . However we do not understand all the tradeoffs involved in the choice
between λB and System FC as a target.
Gradual Type Inference. Siek and Vachharajani [2008] studied unification-based type inference
for gradual typing, where they show why three straightforward approaches fail to meet their design
goals. One of their main observations is that simply ignoring dynamic types during unification
does not work. Therefore, their type system assigns unknown types to type variables and infers
gradual types, which results in a complicated type system and inference algorithm. In our algorithm presented in Section 9, comparisons between existential variables and unknown types areemphasized by the distinction between static existential variables and gradual existential variables.
By syntactically refining unsolved gradual existential variables with unknown types, we gain asimilar effect as assigning unknown types, while keeping the algorithm relatively simple. Garcia
and Cimini [2015] presented a new approach where gradual type inference only produces static
types, which is adopted in our type system. They also deal with let-polymorphism (rank 1 types).
They proposed the distinction between static and gradual type parameters, which inspired our
extension to restore the dynamic gradual guarantee. Although those existing works all involve
gradual types and inference, none of these works deal with higher-rank implicit polymorphism.
Higher-rank Implicit Polymorphism. Odersky and Läufer [1996] introduced a type system forhigher-rank implicit polymorphic types. Based on that, Peyton Jones et al. [2007] developed an
approach for type checking higher-rank predicative polymorphism. Dunfield and Krishnaswami[2013] proposed a bidirectional account of higher-rank polymorphism, and an algorithm for implementing the declarative system, which serves as the main inspiration for our algorithmic system.
The key difference, however, is the integration of gradual typing. As our work, those works are in a
predicative setting, since complete type inference for higher-rank types in an impredicative setting
is undecidable. Still, there are many type systems trying to infer some impredicative types, such
as ML F [Le Botlan and Rémy 2003, 2009; Rémy and Yakobowski 2008], the HML system [Leijen
2009], the FPH system [Vytiniotis et al. 2008] and so on. Those type systems usually end up with
non-standard System F types, and sophisticated forms of type inference.
11

CONCLUSION

In this paper, we have presented a generalized definition of consistent subtyping that works forpolymorphic types. Based on this new definition, we have developed GPC: a gradually typed
calculus with predicative implicit higher-rank polymorphism, and corresponding algorithms thatcan be used to implement the calculus.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:42

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

As far as we know, our work is the first to integrate gradual typing with implicit (higher-rank)polymorphism, which we believe is a major step towards gradualizing modern functional languages,
such as Haskell. Moreover, our extension with type parameters and the extensive discussion ofrelated properties (e.g., representative translations) provides insight into the dynamic semantics forgradual languages with implicit polymorphism. With respect to the dynamic gradual guarantee,
we discuss an extension of the calculus with static and gradual type parameters. We propose avariant of the dynamic gradual guarantee with representative translations. Then we show that our
calculus supports this property if: 1) λB does indeed have the dynamic gradual guarantee (which is
unknown at the time of writing); and 2) our coherence conjecture can be proved.
As future work, we want to investigate whether our notion of consistent subtyping has a more
fundamental conceptual explanation, for example, whether it coincides with AGT on polymorphic
types. It is also interesting to see whether our results can scale to real-world languages (e.g. Haskell)and other programming language features, such as recursive types, union types and intersection
types. Recent work by Castagna and Lanvin [2017] on gradual typing with union and intersection
types in a simply typed setting may shed some light on this direction.
ACKNOWLEDGEMENTS
We thank Ronald Garcia, Dustin Jamner, and the anonymous reviewers for their helpful comments.
This work has been sponsored by the Hong Kong Research Grant Council projects number 17210617
and 17258816, and by the Research Foundation - Flanders.
REFERENCES
Martin Abadi, Luca Cardelli, Benjamin Pierce, and Didier Rémy. 1995. Dynamic Typing in Polymorphic Languages. Journalof Functional Programming 5, 1 (1995), 111–130.
Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011. Blame for All. In Proceedings of the 38th
Symposium on Principles of Programming Languages.
Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for Free for Free: Parametricity, With andWithout Types. In Proceedings of the 22nd International Conference on Functional Programming.
Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2014. A Theory of Gradual Effect Systems. In Proceedings of the
19th International Conference on Functional Programming.
Gavin Bierman, Martín Abadi, and Mads Torgersen. 2014. Understanding TypeScript. In Proceedings of the 28th European
Conference on Object-Oriented Programming.
Gavin Bierman, Erik Meijer, and Mads Torgersen. 2010. Adding Dynamic Types to C#. In Proceedings of the European
Conference on Object-Oriented Programming.
Ambrose Bonnaire-Sergeant, Rowan Davies, and Sam Tobin-Hochstadt. 2016. Practical Optional Types for Clojure. In
Programming Languages and Systems.
Luca Cardelli. 1993. An implementation of FSub. Technical Report. Research Report 97, Digital Equipment Corporation
Systems Research Center.
Giuseppe Castagna and Victor Lanvin. 2017. Gradual Typing with Union and Intersection Types. Proc. ACM Program. Lang.
1, ICFP, Article 41 (Aug. 2017), 28 pages.
Alonzo Church. 1941. The calculi of lambda-conversion. Number 6. Princeton University Press.
Matteo Cimini and Jeremy G. Siek. 2016. The Gradualizer: A Methodology and Algorithm for Generating Gradual Type
Systems. In Proceedings of the 43rd Symposium on Principles of Programming Languages.
Matteo Cimini and Jeremy G. Siek. 2017. Automatically Generating the Dynamic Semantics of Gradually Typed Languages.
In Proceedings of the 44th Symposium on Principles of Programming Languages.
Haskell Brooks Curry, Robert Feys, William Craig, J Roger Hindley, and Jonathan P Seldin. 1958. Combinatory logic. Vol. 1.
North-Holland Amsterdam.
Luis Damas and Robin Milner. 1982. Principal Type-schemes for Functional Programs (POPL ’82). 6.
Rowan Davies and Frank Pfenning. 2000. Intersection Types and Computational Effects. In Proceedings of the Fifth
ACM SIGPLAN International Conference on Functional Programming (ICFP ’00). ACM, New York, NY, USA, 198–208.
https://doi.org/10.1145/351240.351259
Dominique Devriese, Marco Patrignani, and Frank Piessens. 2017. Parametricity versus the universal type. Proceedings of
the ACM on Programming Languages 2, POPL (2017), 38.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:43

Joshua Dunfield and Neelakantan R Krishnaswami. 2013. Complete and Easy Bidirectional Typechecking for Higher-Rank
Polymorphism. In International Conference on Functional Programming. https://arxiv.org/abs/1306.6032.
Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs. In Proceedings of the 42nd Symposiumon Principles of Programming Languages.
Ronald Garcia, Alison M Clark, and Éric Tanter. 2016. Abstracting Gradual Typing. In Proceedings of the 43rd Symposium on
Principles of Programming Languages.
Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N Freund, and Cormac Flanagan. 2006. Sage: Hybrid Checking for
Flexible Specifications. In Scheme and Functional Programming Workshop.
J. Roger Hindley. 1969. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc. 146 (1969),
29–60.
Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On Polymorphic Gradual Typing. In Proceedings of the 22ndInternational Conference on Functional Programming.
Khurram A. Jafery and Joshua Dunfield. 2017. Sums of Uncertainty: Refinements Go Gradual. In Proceedings of the 44th
Symposium on Principles of Programming Languages. 14.
Mark P Jones. 2000. Type classes with functional dependencies. In European Symposium on Programming. Springer, 230–244.
Simon Peyton Jones, Mark Jones, and Erik Meijer. 1997. Type classes: exploring the design space. In Haskell workshop,
Vol. 1997.
Oleg Kiselyov, Ralf Lämmel, and Keean Schupke. 2004. Strongly typed heterogeneous collections. In Proceedings of the 2004
ACM SIGPLAN workshop on Haskell. ACM, 96–107.
Didier Le Botlan and Didier Rémy. 2003. MLF: Raising ML to the Power of System F (ICFP ’03). 12.
Didier Le Botlan and Didier Rémy. 2009. Recasting MLF. Information and Computation 207, 6 (2009), 726–785.
Jukka Lehtosalo et al. 2006. Mypy. (2006). http://www.mypy-lang.org/
Daan Leijen. 2009. Flexible Types: Robust Type Inference for First-class Polymorphism (POPL ’09). 12.
Jacob Matthews and Amal Ahmed. 2008. Parametric polymorphism through run-time sealing or, theorems for low, low
prices!. In European Symposium on Programming. Springer, 16–31.
Conor McBride. 2002. Faking it Simulating dependent types in Haskell. Journal of functional programming 12, 4-5 (2002),
375–392.
John C Mitchell. 1990. Polymorphic Type Inference and Containment. In Logical foundations of functional programming.
James H. Morris, Jr. 1973. Types Are Not Sets. In Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles
of Programming Languages (POPL ’73). ACM, New York, NY, USA, 120–124. https://doi.org/10.1145/512927.512938
James Hiram Morris Jr. 1969. Lambda-calculus models of programming languages. Ph.D. Dissertation. Massachusetts Instituteof Technology.
Georg Neis, Derek Dreyer, and Andreas Rossberg. 2009. Non-parametric Parametricity. In Proceedings of the 14th ACM
SIGPLAN International Conference on Functional Programming (ICFP ’09). ACM, New York, NY, USA, 135–148. https://doi.org/10.1145/1596550.1596572
Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations to Work. In Proceedings of the 23rd Symposium on
Principles of Programming Languages.
Michel Parigot. 1992. Recursive programming with proofs. Theoretical Computer Science 94, 2 (1992), 335–356.
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical Type Inference for ArbitraryRank Types. Journal of Functional Programming 17, 1 (2007), 1–82.
Benjamin C Pierce. 2002. Types and programming languages.
Didier Rémy and Boris Yakobowski. 2008. From ML to MLF: Graphic Type Constraints with Efficient Type Inference (ICFP’08). 12.
John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In Proceedings of the IFIP 9th World Computer
Congress.
John C. Reynolds. 1991. The Coherence of Languages with Intersection Types. In Proceedings of the International Conferenceon Theoretical Aspects of Computer Software.
Jeremy Siek, Ronald Garcia, and Walid Taha. 2009. Exploring the design space of higher-order casts. In European Symposiumon Programming. 17–31.
Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Proceedings of the 2006 Scheme andFunctional Programming Workshop.
Jeremy G. Siek and Walid Taha. 2007. Gradual Typing for Objects. In European Conference on Object-Oriented Programming.
Jeremy G. Siek and Manish Vachharajani. 2008. Gradual Typing with Unification-based Inference. In Proceedings of the 2008
Symposium on Dynamic Languages.
Jeremy G. Siek, Michael M Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In
LIPIcs-Leibniz International Proceedings in Informatics.
Jeremy G. Siek and Philip Wadler. 2016. The Key to Blame: Gradual Typing Meets Cryptography (draft). (2016).

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:44

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

Julien Verlaguet. 2013. Facebook: Analyzing PHP statically. In Proceedings of Commercial Users of Functional Programming.
Michael M. Vitousek, Andrew M. Kent, Jeremy G. Siek, and Jim Baker. 2014. Design and Evaluation of Gradual Typing for
Python. In Proceedings of the 10th Symposium on Dynamic languages.
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. 2008. FPH: First-class Polymorphism for Haskell (ICFP’08). 12.
Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In Proceedings of the 18th European
Symposium on Programming Languages and Systems.
J.B. Wells. 1999. Typability and type checking in System F are equivalent and undecidable. Annals of Pure and Applied Logic
98, 1 (1999), 111 – 156. https://doi.org/10.1016/S0168-0072(98)00047-5
Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. 2018. Consistent Subtyping for All. In European Symposium on
Programming. 3–30.

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All
A

39:45

SOME PROOFS ABOUT THE DECLARATIVE SYSTEM
Lemma 5.2. If Ψ ⊢ e : A ⇝ s 1 , and Ψ ⊢ e : A ⇝ s 2 , then ⌊s 1 ⌋ ≡α ⌊s 2 ⌋.
Proof. By straightforward induction on the typing derivation.

□

Lemma 5.3 (Coherence up to cast errors). For any expression e such that Ψ ⊢ e : A ⇝ s 1 andΨ ⊢ e : A ⇝ s 2 , we have Ψ ⊢ s 1 ⋍ct x s 2 : A.
Proof. According to Lemma 5.2, after erasure of types and casts, C{s 1 } and C{s 2 } are equivalent.
So if C{s 1 } ⇓ n, it is impossible for C{s 2 } to reduce to a different integer according to the dynamic
semantics.
□
Proposition 8.1 (Extension with ⊤). Ψ ⊢ A ≲ B ⇔ Ψ ⊢ A <: C, C ∼ D, Ψ ⊢ D <: B, for someC, D.
Proof.
• From first to second: By induction on the derivation of consistent subtyping. We have extra
case rule CS-Top now, where B = ⊤. We can choose C = A, and D by replacing the unknown
types in C by Int. Namely, D is a static type, so by rule S-Top we are done.
• From second to first: By induction on the derivation of second subtyping. We have extra caserule S-Top now, where B = ⊤, so A ≲ B holds by rule CS-Top.
□
H B.
Proposition 8.2 (Eqivalent to AGT on ⊤). A ≲ B if only if A <:Proof.
• From left to right: By induction on the derivation of consistent subtyping. We have caserule CS-Top now. It follows that for every static type A1 ∈ γ (A), we can derive A1 <: ⊤ byrule S-Top. We have B 1 = B = ⊤ and we are done.
• From right to left: By induction on the derivation of subtyping and inversion on the concretization. We have extra case rule S-Top now, where B is ⊤. So consistent subtyping directly
holds.
□
Proposition 9.4. If s 1 ≤ s 2 and s 2 ≤ s 1 , then s 1 and s 2 are α-equivalent (i.e., equivalent up torenaming of type parameters).
Proof. Follows directly from the definition of Translation Pre-order.

□

Definition A.1 (Measurements of Translation). There are three measurements of a translation s,(1) JsK E , the size of the expression(2) JsK S , the number of distinct static type parameters in s
(3) JsK G , the number of distinct gradual type parameters in s

We use JsK to denote the lexicographical order of the triple (JsK E , −JsK S , −JsK G ).
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:46

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

Definition A.2 (Size of types).
JIntK = 1
JaK = 1

JA → BK = JAK + JBK + 1
J∀a. AK = JAK + 1
J⋆K = 1

JSK = 1JGK = 1
Definition A.3 (Size of expressions).
JxK E = 1
JnK E = 1

Jλx : A. sK E = JAK + JsK E + 1
JΛa. sK E = JsK E + 1

Js 1 s 2 K E = Js 1 K E + Js 2 K E + 1

J⟨A ,→ B⟩sK E = JsK E + JAK + JBK + 1
Lemma A.4. If Ψ ⊢ e : A ⇝ s then JsK E ≥ JeK E .
Proof. Immediate by inspecting each typing rule.

□

Corollary A.5. If Ψ ⊢ e : A ⇝ s then JsK > (JeK E , −JeK E , −JeK E ).

Proof. By Lemma A.4 and note that JsK E > JsK S and JsK E > JsK G□

Lemma A.6. JAK ≤ JS P (A)K.

Proof. By induction on the structure of A. The interesting cases are A = S and A = G. When
A = S, S P (A) = τ for some monotype τ and it is immediate that JSK ≤ Jτ K (note that JSK < JGK
by definition).
□
Lemma A.7 (Substitution Decreases Measurement). If s 1 ≤ s 2 , then Js 1 K ≤ Js 2 K; unless s 2 ≤ s 1
also holds, otherwise we have Js 1 K < Js 2 K.
Proof. Since s 1 ≤ s 2 , we know s 2 = S P (s 1 ) for some S P . By induction on the structure of s 1 .

• Case s 1 = λx : A. s. We have s 2 = λx : S P (A). S P (s). By Lemma A.6 we have JAK ≤ JS P (A)K.
By i.h., we have JsK ≤ JS P (s)K. Therefore Jλx : A. sK ≤ Jλx : S P (A). S P (s)K.
• Case s 1 = ⟨A ,→ B⟩s. We have s 2 = ⟨S P (A) ,→ S P (B)⟩S P (s). By Lemma A.6 we have
JAK ≤ JS P (A)K and JBK ≤ JS P (B)K. By i.h., we have JsK ≤ JS P (s)K. Therefore J⟨A ,→ B⟩sK ≤J⟨S P (A) ,→ S P (B)⟩S P (s)K.
• The rest of cases are immediate.
□
Lemma 9.9 (Representative Translation for Typing). For any typing derivation Ψ ⊢ e : A
there exists at least one representative translation r such that Ψ ⊢ e : A ⇝ r .
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:47

Proof. We already know that at least one translation s = s 1 exists for every typing derivation. If
s 1 is a representative translation then we are done. Otherwise there exists another translation s 2such that s 2 ≤ s 1 and s 1 ≰ s 2 . By Lemma A.7, we have Js 2 K < Js 1 K. We continue with s = s 2 , andget a strictly decreasing sequence Js 1 K, Js 2 K, . . . . By Corollary A.5, we know this sequence cannot
be infinite long. Suppose it ends at Js j K, by the construction of the sequence, we know that s j is a
representative translation of e.
□

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:48B

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

THE EXTENDED ALGORITHMIC SYSTEM

B.1

SyntaxExpressions
Types
Monotypes
Existential variables
Castable Types
Castable Monotypes
Algorithmic Contexts
Complete Contexts

B.2::= x | n | λx : A. e | λx. e | e 1 e 2 | e : A | let x = e 1 in e 2::= Int | a | aD | A → B | ∀a. A | ⋆ | S | G::= Int | a | aD | τ → σ | S | G::= aDS | aDG::= Int | a | aD | C1 → C2 | ∀a. C | ⋆ | G::= Int | a | aD | t 1 → t 2 | G::= • | Γ, x : A | Γ, a | Γ, aD | Γ, aDS = τ | Γ, aDG = t | Γ, ▶aD::= • | Ω, x : A | Ω, a | Ω, aDS = τ | Ω, aDG = t | Ω, ▶aD

e
A, B
τ,σ
aD
C
t
Γ, ∆, ΘΩ

Type System

Γ⊢A≲B ⊣∆

(Algorithmic Consistent Subtyping)
as-tvaras-evarΓ ⊢ B 1 ≲ A1 ⊣ Θas-intΓ ⊢ Int ≲ Int ⊣ Γ

Γ[Da ] ⊢ aD ≲ aD ⊣ Γ[Da]Γ[a] ⊢ a ≲ a ⊣ Γ[a]Γ, a ⊢ A ≲ B ⊣ ∆, a, ΘΘ ⊢ [Θ]A2 ≲ [Θ]B 2 ⊣ ∆as-arrow

as-forallRΓ ⊢ A1 → A2 ≲ B 1 → B 2 ⊣ ∆Γ ⊢ A ≲ ∀a. B ⊣ ∆Γ, ▶aDS , aDS ⊢ A[a 7→ aDS ] ≲ B ⊣ ∆, ▶aDS , Θ
as-forallLL

as-sparΓ ⊢ ∀a. A ≲ B ⊣ ∆Γ⊢S≲S⊣Γ

as-gparΓ ⊢ ⋆ ≲ C ⊣ contaminate(Γ, C)Γ⊢G≲G⊣ΓaD < fv(A)Γ ⊢ C ≲ ⋆ ⊣ contaminate(Γ, C)

as-unknownLLΓ[Da ] ⊢ aD ⪅ A ⊣ ∆as-unknownRR

as-instLΓ[Da ] ⊢ aD ≲ A ⊣ ∆aD < fv(A)Γ[Da ] ⊢ A ⪅ aD ⊣ ∆as-instRΓ[Da ] ⊢ A ≲ aD ⊣ ∆Γ ⊢ aD ⪅ A ⊣ ∆(Instantiation I)
Γ ⊢τ

Γ ⊢t

Γ, aDS , Γ ⊢ aDS ⪅ τ ⊣ Γ, aDS = τ , Γ′′instl-solveSΓ[Da S ] ⊢ aDS ⪅ ⋆ ⊣ Γ[DaG , aDS = aDG ]Γ, aDG , Γ ⊢ aDG ⪅ t ⊣ Γ, aDG = t, Γ ′instl-solveUS′

Γ[DaG ] ⊢ aDG ⪅ ⋆ ⊣ Γ[D
aG ]

Γ[D
a S ][bDG ] ⊢ aDS ⪅ bDG ⊣ Γ[DaG , aDS = aDG ][bDG = aDG ]instl-reachSG1

Γ[bDS ][DaG ] ⊢ aDG ⪅ bDS ⊣ Γ[bDG , bDS = bDG ][DaG = bDG ]instl-reachSG2

D ⊢ aD ⪅ bD ⊣ Γ[DΓ[Da ][b]
a ][bD = aD]

instl-reachOtherACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

instl-solveG

instl-solveUG

Consistent Subtyping for All

39:49

Γ[D
a 2 , aD1 , aD = aD1 → aD2 ] ⊢ A1 ⪅ aD1 ⊣ ΘΘ ⊢ aD2 ⪅ [Θ]A2 ⊣ ∆instl-arr

Γ[Da ] ⊢ aD ⪅ A1 → A2 ⊣ ∆Γ[Da ], b ⊢ aD ⪅ B ⊣ ∆, b, Θ
instl-forallRΓ[Da ] ⊢ aD ⪅ ∀b. B ⊣ ∆Γ ⊢ A ⪅ aD ⊣ ∆(Instantiation II)
Γ ⊢τ

Γ ⊢t

Γ, aDS , Γ ⊢ τ ⪅ aDS ⊣ Γ, aDS = τ , Γ′′

instr-solveSΓ[Da S ] ⊢ ⋆ ⪅ aDS ⊣ Γ[DaG , aDS = aDG ]Γ, aDG , Γ ⊢ t ⪅ aDG ⊣ Γ, aDG = t, Γ ′′instr-solveUS

Γ[DaG ] ⊢ ⋆ ⪅ aDG ⊣ Γ[D
aG ]

Γ[D
a S ][bDG ] ⊢ bDG ⪅ aDS ⊣ Γ[DaG , aDS = aDG ][bDG = aDG ]instr-reachSG1

Γ[bDS ][DaG ] ⊢ bDS ⪅ aDG ⊣ Γ[bDG , bDS = bDG ][DaG = bDG ]instr-reachSG2

instr-solveUG

instr-reachOther

D ⊢ bD ⪅ aD ⊣ Γ[DΓ[Da ][b]
a ][bD = aD]Γ[Da 2 , aD1 , aD = aD1 → aD2 ] ⊢ aD1 ⪅ A1 ⊣ Θ

instr-solveGΘ ⊢ [Θ]A2 ⪅ aD2 ⊣ ∆instr-arr

Γ[Da ] ⊢ A1 → A2 ⪅ aD ⊣ ∆Γ[Da ], ▶bDS , bDS ⊢ B[b 7→ bDS ] ⪅ aD ⊣ ∆, ▶bDS , Θ
instr-forallLLΓ[Da ] ⊢ ∀b. B ⪅ aD ⊣ ∆Γ ⊢e ⇒A⊣∆(Inference)(x : A) ∈ Γ
inf-var

inf-intΓ ⊢ n ⇒ Int ⊣ ΓΓ⊢x ⇒A⊣ΓΓ⊢AΓ, bDS , x : A ⊢ e ⇐ bDS ⊣ ∆, x : A, Θ
inf-lamann2Γ ⊢ λx : A. e ⇒ A → bDS ⊣ ∆Γ, aDS , bDS , x : aDS ⊢ e ⇐ bDS ⊣ ∆, x : aDS , ΘΓ⊢AΓ ⊢e ⇐A⊣∆

inf-lam2Γ ⊢ λx. e ⇒ aDS → bDS ⊣ ∆Γ ⊢ e 1 ⇒ A ⊣ Θ1

inf-annoΓ ⊢e :A⇒A⊣∆

Θ1 ⊢ [Θ1 ]A ▷ A1 → A2 ⊣ Θ2

Θ2 ⊢ e 2 ⇐ [Θ2 ]A1 ⊣ ∆inf-appΓ ⊢ e 1 e 2 ⇒ A2 ⊣ ∆Γ ⊢ e 1 ⇒ A ⊣ Θ1

Θ1 , aDS , x : A ⊢ e 2 ⇐ aDS ⊣ ∆, x : A, Θ2Γ ⊢ let x = e 1 in e 2 ⇒ aDS ⊣ ∆inf-let2

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:50Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

Γ ⊢e ⇐A⊣∆(Checking)Γ, x : A ⊢ e ⇐ B ⊣ ∆, x : A, ΘΓ, a ⊢ e ⇐ A ⊣ ∆, a, Θ
chk-lamΓ ⊢ λx. e ⇐ A → B ⊣ ∆chk-genΓ ⊢ e ⇐ ∀a. A ⊣ ∆Γ ⊢e ⇒A⊣ΘΘ ⊢ [Θ]A ≲ [Θ]B ⊣ ∆chk-subΓ ⊢e ⇐B ⊣∆Γ ⊢ A ▷ A1 → A2 ⊣ ∆(Algorithmic Matching)Γ, aDS ⊢ A[a 7→ aDS ] ▷ A1 → A2 ⊣ ∆Γ ⊢ ∀a. A ▷ A1 → A2 ⊣ ∆Γ ⊢⋆▷⋆→⋆⊣ Γ

am-unknown

am-forallLΓ ⊢ A1 → A2 ▷ A1 → A2 ⊣ Γam-arrΓ[Da ] ⊢ aD ▷ aD1 → aD2 ⊣ Γ[Da 1 , aD2 , aD = aD1 → aD2 ]am-var

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All
C

39:51

DECIDABILITY

The decidability proofs mostly follow that of DK system. Whenever possible, we only show the
new cases; otherwise we provide full detailed proofs.
C.1

Decidability of Instantiation

Lemma C.1 (Left Unsolvedness Preservation). Let Γ = Γ0 , aD, Γ1 . If Γ ⊢ aD ⪅ A ⊣ ∆ or Γ ⊢ A ⪅D ∆1 ) or ∆ = (∆0 , bD′, bD = bD′, ∆1 ) where bD′ is a freshaD ⊣ ∆, and bD ∈ unsolved(Γ0 ), then ∆ = (∆0 , b,
unsolved existential.
Proof. By induction on the given derivation. We show the new cases.
• CaseΓ0 , aDS , Γ1 ⊢ aDS ⪅ ⋆ ⊣ Γ0 , aDG , aDS = aDG , Γ1

instl-solveUS

First notice that bD cannot be aDG . Then to the left of aDS , the contexts ∆ and Γ are the same Γ0 .
• CaseΓ[DaG ] ⊢ aDG ⪅ ⋆ ⊣ Γ[DaG ]instl-solveUG

Immediate, since to the left of aDG , the contexts ∆ and Γ are the same.
• CaseΓ[Da S ][bDG ] ⊢ aDS ⪅ bDG ⊣ Γ[DaG , aDS = aDG ][bDG = aDG ]instl-reachSG1First notice that bD cannot be aDG . Then to the left of aDS , the contexts ∆ and Γ are the same.
• CaseΓ[bDS ][DaG ] ⊢ aDG ⪅ bDS ⊣ Γ[bDG , bDS = bDG ][DaG = bDG ]instl-reachSG2

If bD , bDS , immediate, since to the left of aDG (bD cannot be bDG ), the contexts ∆ and Γ are thesame. Otherwise, bDS ’s solution (i.e., bDG ) is a fresh unsolved existential that lies just before bDS .
• Case instr-solveUS is similar to case instl-solveUS.
• Case instr-solveUG is similar to case instl-solveUG.
• Case instr-reachSG1 is similar to case instl-reachSG1.
• Case instr-reachSG2 is similar to case instl-reachSG2.
□
Lemma C.2 (Left Free Variable Preservation). Let Γ = Γ0 , aD, Γ1 . If Γ ⊢ aD ⪅ A ⊣ ∆ or Γ ⊢ A ⪅aD ⊣ ∆, and Γ ⊢ B and aD < fv([Γ]B) and bD ∈ unsolved(Γ0 ) and bD < fv([Γ]B), then bD < fv([∆]B).
Proof. By induction on the given derivation. We show the new cases.
• CaseΓ[Da S ] ⊢ aDS ⪅ ⋆ ⊣ Γ[DaG , aDS = aDG ]instl-solveUS

Since ∆ differs from Γ only in solving aDS to aDG , and aDG is fresh, applying ∆ to a type will not
D We have bD < fv([Γ]B), so bD < fv([∆]B).
introduce b.
• CaseΓ[DaG ] ⊢ aDG ⪅ ⋆ ⊣ Γ[DaG ]instl-solveUG

Immediate, since ∆ and Γ are the same.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:52

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers• CaseΓ[Da S ][bDG ] ⊢ aDS ⪅ bDG ⊣ Γ[DaG , aDS = aDG ][bDG = aDG ]instl-reachSG1

Since ∆ differs from Γ only in solving aDS and bDG to aDG , and aDG is fresh, applying ∆ to a type
D We have bD < fv([Γ]B), so bD < fv([∆]B).
will not introduce b.
• CaseΓ[bDS ][DaG ] ⊢ aDG ⪅ bDS ⊣ Γ[bDG , bDS = bDG ][DaG = bDG ]instl-reachSG2

Since ∆ differs from Γ only in solving bDS and aDG to bDG , and bDG is fresh, applying ∆ to a type
D We have bD < fv([Γ]B), so bD < fv([∆]B).
will not introduce b.
• Case instr-solveUS is similar to case instl-solveUS.
• Case instr-solveUG is similar to case instl-solveUG.
• Case instr-reachSG1 is similar to case instl-reachSG1.
• Case instr-reachSG2 is similar to case instl-reachSG2.
□
Lemma C.3 (Instantiation Size Preservation). If Γ = Γ0 , aD, Γ1 and Γ ⊢ aD ⪅ A ⊣ ∆ or Γ ⊢ A ⪅aD ⊣ ∆, and Γ ⊢ B and aD < fv([Γ]B), then |[Γ]B| = |[∆]B|, where |C | is the plain size of C.
Proof. By induction on the given derivation. We show the new cases.
• CaseΓ[Da S ] ⊢ aDS ⪅ ⋆ ⊣ Γ[DaG , aDS = aDG ]instl-solveUS

Since ∆ differs Γ only in solving aDS , and we know aDS < fv([Γ]B), we have [∆]B = [Γ]B, so|[Γ]B| = |[∆]B|.
• CaseΓ[DaG ] ⊢ aDG ⪅ ⋆ ⊣ Γ[DaG ]Immediate, since ∆ and Γ are the same.
• Caseinstl-solveUG

Γ[Da S ][bDG ] ⊢ aDS ⪅ bDG ⊣ Γ[DaG , aDS = aDG ][bDG = aDG ]instl-reachSG1

Since ∆ differs Γ only in solving aDS and bDG , and we know aDS < fv([Γ]B), even if bDG occurs in[Γ]B, its solution is again an existential variable, so the size does not change, so |[Γ]B| = |[∆]B|.
• CaseΓ[bDS ][DaG ] ⊢ aDG ⪅ bDS ⊣ Γ[bDG , bDS = bDG ][DaG = bDG ]instl-reachSG2

Since ∆ differs Γ only in solving aDG and bDS , and we know aDG < fv([Γ]B), even if bDS occurs in[Γ]B, its solution is again an existential variable, so the size does not change, so |[Γ]B| = |[∆]B|.
• Case instr-solveUS is similar to case instl-solveUS.
• Case instr-solveUG is similar to case instl-solveUG.
• Case instr-reachSG1 is similar to case instl-reachSG1.
• Case instr-reachSG2 is similar to case instl-reachSG2.
□
Theorem 6.1 (Decidability of Instantiation). If Γ = Γ0 [Da ] and Γ ⊢ A such that [Γ]A = A andaD < fv(A) then:(1) Either there exists ∆ such that Γ ⊢ aD ⪅ A ⊣ ∆, or not.
(2) Either there exists ∆ such that Γ ⊢ A ⪅ aD ⊣ ∆, or not.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:53

Proof. By induction on the derivation of Γ ⊢ A. We show the new cases.
• Casead-unknownΓ ⊢⋆By rule instl-solveUS or rule instl-solveUG.
• Casead-static

Γ⊢S
By rule instl-solveS.
• Casead-gradualΓ⊢G
By rule instl-solveS or rule instl-solveG.
• Casead-evarΓ0 , aDS , Γ1 ⊢ aDG
If aDG ∈ Γ0 , then we have a derivation by rule instl-reachOther. If aDG ∈ Γ1 , then we have aderivation by rule instl-reachSG1.
• Casead-evarΓ0 , aDG , Γ1 ⊢ aDS
If aDS ∈ Γ0 , then we have a derivation by rule instl-reachSG2. If aDS ∈ Γ1 , then we have aderivation by rule instl-reachOther.
□C.2

Decidability of Algorithmic Consistent Subtyping

Lemma C.4 (Monotypes Solve Variables). If Γ ⊢ aD ⪅ τ ⊣ ∆ or Γ ⊢ τ ⪅ aD ⊣ ∆, then if [Γ]τ = τ
and aD < fv([Γ]τ ), then |unsolved(Γ)| = |unsolved(∆)| + 1.
Proof. By induction on the given derivation. Since our syntax of monotypes differ from DK
only in having static and gradual parameters, we show only two affected cases.
• CaseΓ ⊢τinstl-solveSΓ, aDS , Γ ′ ⊢ aDS ⪅ τ ⊣ Γ, aDS = τ , Γ ′It is immediate that |unsolved(Γ, aDS , Γ ′ )| = |unsolved(Γ, aDS = τ , Γ ′ )| + 1.
• CaseΓ ⊢tinstl-solveGΓ, aDG , Γ ′ ⊢ aDG ⪅ t ⊣ Γ, aDG = t, Γ ′It is immediate that |unsolved(Γ, aDG , Γ ′ )| = |unsolved(Γ, aDG = t, Γ ′ )| + 1.
□
Lemma C.5 (Monotype Monotonicity). If Γ ⊢ τ1 ≲ τ2 ⊣ ∆ then |unsolved(∆)| ≤ |unsolved(Γ)|.
Proof. By induction on the derivation. We show the new cases.
• Case as-spar and as-gpar: In these rules, ∆ = Γ, so |unsolved(∆)| = |unsolved(Γ)|.
□
Lemma C.6 (Substitution Decreases Size). If Γ ⊢ A, then |Γ ⊢ [Γ]A| ≤ |Γ ⊢ A|.
Proof. By induction on |Γ ⊢ A|. We show the new cases.
• A = ⋆, or A = S, or A = G then [Γ]A = A. Therefore |Γ ⊢ [Γ]A| = |Γ ⊢ A|.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:54

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers□

Lemma C.7 (Monotype Context Invariance). If Γ ⊢ τ ≲ τ ′ ⊣ ∆ where [Γ]τ = τ and [Γ]τ ′ = τ ′and |unsolved(Γ)| = |unsolved(∆)|, then ∆ = Γ.
Proof. By induction on the derivation. We show the new cases.
• Cases as-spar and as-gpar: In these rules, the output context is the same as the input context,
so the result is immediate.
• CaseaD < fv(A)Γ[Da ] ⊢ aD ⪅ A ⊣ ∆as-instLΓ[Da ] ⊢ aD ≲ A ⊣ ∆By Lemma C.4, |unsolved(∆)| < |unsolved(Γ[Da ])|, which is contrary to what is given, so
this case is impossible.
• Case as-instR is similar to as-instL.
□
Theorem 6.3 (Decidability of Algorithmic Consistent Subtyping). Given a context Γ andtypes A, B such that Γ ⊢ A and Γ ⊢ B and [Γ]A = A and [Γ]B = B, it is decidable whether there exists∆ such that Γ ⊢ A ≲ B ⊣ ∆.
Proof. Let the judgment Γ ⊢ A ≲ B ⊣ ∆ be measured lexicographically by(M1) the number of ∀-quantifiers in A and B;(M2) the number of unknown types in A and B;(M3) |unsolved(Γ)|: the number of unsolved existential variables in Γ;(M4) |Γ ⊢ A| + |Γ ⊢ B|.
We focus on the interesting (and new) cases.
• Cases as-spar, as-gpar, as-unknownLL, and as-unknownRR have no premises.
• CaseΓ ⊢ B 1 ≲ A1 ⊣ ΘΘ ⊢ [Θ]A2 ≲ [Θ]B 2 ⊣ ∆as-arrowΓ ⊢ A1 → A2 ≲ B 1 → B 2 ⊣ ∆We discuss each premise separately:First premise: If A2 or B 2 has a quantifier, then the first premise is smaller by (M1). Otherwise, if
A2 or B 2 has a unknown type, then first premise is smaller by (M2). Otherwise, the first premiseshares the same input context as the conclusion, so it has the same (M3), but the types B 1 and A1
are subterms of the conclusion’s types, so the first premise is smaller by (M4).
Second premise: If B 1 or A1 has a quantifier, then the second premise is smaller by (M1) because
applying contexts will not introduce quantifiers. Otherwise, if B 1 or A1 has a unknown type, thenthe second premise is smaller by (M2) because applying contexts will not introduce unknown
types. Otherwise, at this point, we know B 1 and A1 are monotypes, so by Lemma C.5 on the firstpremise, we have |unsolved(Θ)| ≤ |unsolved(Γ)|.
– If |unsolved(Θ)| < |unsolved(Γ)|, then the second premise is smaller by (M3).
– If |unsolved(Θ)| = |unsolved(Γ)|, then we have the same (M3). By Lemma C.7 on thefirst premise, we know Θ = Γ, so |Θ ⊢ [Θ]A2 | = |Γ ⊢ [Γ]A2 |. By Lemma C.6 we know|Γ ⊢ [Γ]A2 | ≤ |Γ ⊢ A2 |. Therefore we have|Θ ⊢ [Θ]A2 | ≤ |Γ ⊢ A2 |Same for B 2 :|Θ ⊢ [Θ]B 2 | ≤ |Γ ⊢ B 2 |ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:55

Therefore,|Θ ⊢ [Θ]A2 | + |Θ ⊢ [Θ]B 2 | ≤ |Γ ⊢ A2 | + |Γ ⊢ B 2 | < |Γ ⊢ A1 → A2 | + |Γ ⊢ B 1 → B 2 |and the second premise is smaller by (M4).
□
C.3

Decidability of Algorithmic Typing

Lemma 6.4 (Decidability of Algorithmic Matching). Given a context Γ and a type A it isdecidable whether there exist types A1 , A2 and a context ∆ such that Γ ⊢ A ▷ A1 → A2 ⊣ ∆.
Proof. Rules am-arr, am-unknown, and am-var do not have premises. For rule am-forall,
the size of A is decreasing in the premise.
□
Theorem 6.5 (Decidability of Algorithmic Typing).
(1) Inference: Given a context Γ and a term e, it is decidable whether there exist a type A and acontext ∆ such that Γ ⊢ e ⇒ A ⊣ ∆.
(2) Checking: Given a context Γ, a term e and a type B such that Γ ⊢ B, it is decidable whether there
exists a context ∆ such that Γ ⊢ e ⇐ B ⊣ ∆.
Proof. We consider the following measure:

⇒
e,
⇐,


|Γ ⊢ A|and show every inference/checking premise is smaller than the conclusion.
• Rules inf-var and inf-int do not have premises.
• Rules inf-anno, inf-lamann, inf-lam, inf-let, and chk-lam all have strictly smaller e inthe premises.
• Rule inf-app: The first and third premises have strictly smaller e. The second (matching)
judgment is decidable by Lemma 6.4.
• Rule chk-gen: Both the premise and conclusion type the same term, and both are the checking
judgments. However |Γ, a ⊢ A| < |Γ ⊢ ∀a. A|, so the premise is smaller.
• Rule chk-sub: The first premise uses inference mode, so it is smaller. The second premise isdecidable by Theorem 6.3.
□

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:56
D

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

PROPERTIES OF CONSISTENT SUBTYPING
Lemma 7 (Consistent Subtyping is Reflexive). If Ψ ⊢ A then Ψ ⊢ A ≲ A.
Lemma 8 (Monotype Eqality). If Ψ ⊢ τ ≲ σ then τ = σ .
Lemma D.1 (Invertibility). If Ψ ⊢ A ≲ ∀b. B then Ψ, b ⊢ A ≲ B.
Proof. By induction on the given derivation.
• Rules cs-arrow, cs-tvar, cs-int, cs-unknownRR, cs-spar, and cs-gpar are impossible
since the supertype is not a forall type.
• CaseΨ, a ⊢ A ≲ B
cs-forallRΨ ⊢ A ≲ ∀a. B
The premise is exactly what we need.
• CaseΨ⊢τΨ ⊢ A[a 7→ τ ] ≲ B
cs-forallLΨ ⊢ ∀a. A ≲ B
where B = ∀b. B0 . By i.h., we have Ψ, b ⊢ A[a 7→ τ ] ≲ B0 . By rule cs-forallL we haveΨ, b ⊢ ∀a. A ≲ B0 .
• Casecs-unknownLLΨ⊢⋆≲C
where C = ∀b. C0 . By rule cs-unknownLL we have Ψ, b ⊢ ⋆ ≲ C0 .
□ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All
E

39:57

PROPERTIES OF CONTEXT EXTENSION

E.1

Syntactic Properties

Since the definition of the context extension judgment (Γ −→ ∆, Fig. 16) is exactly the same as thatof the DK system, we refer the reader to their technical report [Dunfield and Krishnaswami 2013]
for the proofs of the following syntactic properties of context extension.
Lemma E.1 (Reverse Declaration Order Preservation). If Γ −→ ∆ and a and b are bothdeclared in Γ and a is declared to the left of b in ∆, then a is declared to the left of b in Γ.
Lemma E.2 (Reflexivity). If Γ is well-formed then Γ −→ Γ.
Lemma E.3 (Transitivity). If Γ −→ ∆ and ∆ −→ Θ then Γ −→ Θ.
Definition E.4 (Softness). A context Θ is soft iff it consists only of aD and aD = τ declarations.
Lemma E.5 (Substitution Extension Invariance). If Θ ⊢ A and Θ −→ Γ then [Γ]A = [Γ]([Θ]A)and [Γ]A = [Θ]([Γ]A).
Lemma E.6 (Extension Order). We have the following:(1) If ΓL , a, ΓR −→ ∆ then ∆ = (∆L , a, ∆R ) where ΓL −→ ∆L . Moreover, if ΓR is soft then ∆R is soft.
(2) If ΓL , ▶aD, ΓR −→ ∆ then ∆ = (∆L , ▶aD, ∆R ) where ΓL −→ ∆L . Moreover, if ΓR is soft then ∆R is
soft.
(3) If ΓL , aD, ΓR −→ ∆ then ∆ = (∆L , Θ, ∆R ) where ΓL −→ ∆L and Θ is either aD or aD = τ for some τ .
(4) If ΓL , aD = τ , ΓR −→ ∆ then ∆ = (∆L , aD = τ ′, ∆R ) where ΓL −→ ∆L and and [∆L ]τ = [∆L ]τ ′.
(5) If ΓL , x : A, ΓR −→ ∆ then ∆ = (∆L , x : A′, ∆R ) where ΓL −→ ∆L and [∆L ]A = [∆L ]A′.
Moreover, ΓR is soft if and only if ∆R is soft.
Lemma E.7 (Solution Admissibility for Extension). If ΓL ⊢ τ then ΓL , aD, ΓR −→ ΓL , aD = τ , ΓR .
Lemma E.8 (Unsolved Variable Addition for Extension). We have that ΓL , ΓR −→ ΓL , aD, ΓR
Lemma E.9 (Parallel Admissibility). If ΓL −→ ∆L and ΓL , ΓR −→ ∆L , ∆R then:(1) ΓL , aD, ΓR −→ ∆L , aD, ∆R(2) If ∆L ⊢ τ ′ then ΓL , aD, ΓR −→ ∆L , aD = τ ′, ∆R .
(3) If ΓL ⊢ τ and ∆L ⊢ τ ′ and [∆L ]τ = [∆L ]τ ′, then ΓL , aD = τ , ΓR −→ ∆L , aD = τ ′, ∆R .
Lemma E.10 (Parallel Extension Solution). If ΓL , aD, ΓR −→ ∆L , aD = τ ′, ∆R and ΓL ⊢ τ and[∆L ]τ = [∆L ]τ ′, then ΓL , aD = τ , ΓR −→ ∆L , aD = τ ′, ∆R .
Lemma E.11 (Drop Variable for Extension). If Γ, aD −→ ∆ then Γ −→ ∆.
Lemma E.12 (Finishing Types). If Ω ⊢ A and Ω −→ Ω ′ then [Ω]A = [Ω ′]A.
Lemma E.13 (Finishing completions). If Ω −→ Ω ′ then [Ω]Ω = [Ω ′]Ω ′.
Lemma E.14 (Confluence of Completeness). If ∆1 −→ Ω and ∆2 −→ Ω then [Ω]∆1 = [Ω]∆2 .
Lemma E.15 (Variable Preservation). If (x : A) ∈ ∆ or (x : A) ∈ Ω and ∆ −→ Ω then(x : [Ω]A) ∈ [Ω]∆.
Lemma E.16 (Softness Goes Away). If ∆, Θ −→ Ω, ΩZ where ∆ −→ Ω and Θ is soft, then[Ω, ΩZ ](∆, Θ) = [Ω]∆.
Lemma E.17 (Stability of Complete Contexts). If Γ −→ Ω then [Ω]Γ = [Ω]Ω.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:58E.2

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers
Instantiation Extends

Lemma E.18 (Instantiation Extension). If Γ ⊢ aD ⪅ A ⊣ ∆ or Γ ⊢ A ⪅ aD ⊣ ∆ then Γ −→ ∆.
Proof. By induction on the given instantiation derivation.
• Rules instl-solveS, instl-solveG, instl-reachOther, instr-solveS, instr-solveG, andinstr-reachOther are immediate from Lemma E.7.
• CaseΓ[Da S ] ⊢ aDS ⪅ ⋆ ⊣ Γ[DaG , aDS = aDG ]instl-solveUS

By Lemma E.8 we have Γ[Da S ] −→ Γ[DaG , aDS ]. By Lemma E.7 we have Γ[DaG , aDS ] −→ Γ[DaG , aDS =aDG ]. By Lemma E.3 we have Γ[Da S ] −→ Γ[DaG , aDS = aDG ].
• CaseΓ[DaG ] ⊢ aDG ⪅ ⋆ ⊣ Γ[DaG ]instl-solveUG

Immediate by Lemma E.2.
• CaseΓ[Da S ][bDG ] ⊢ aDS ⪅ bDG ⊣ Γ[DaG , aDS = aDG ][bDG = aDG ]instl-reachSG1

By Lemma E.8 we have Γ[Da S ][bDG ] −→ Γ[DaG , aDS ][bDG ]. By applying Lemma E.7 twice, wehave Γ[DaG , aDS ][bDG ] −→ Γ[DaG , aDS = aDG ][bDG = aDG ]. By Lemma E.3 we have Γ[Da S ][bDG ] −→D
Γ[DaG , aDS = aDG ][bG = aDG ].
• CaseΓ[bDS ][DaG ] ⊢ aDG ⪅ bDS ⊣ Γ[bDG , bDS = bDG ][DaG = bDG ]instl-reachSG2Same as the case for rule instl-reachSG1.
• CaseΓ[Da 2 , aD1 , aD = aD1 → aD2 ] ⊢ A1 ⪅ aD1 ⊣ ΘΘ ⊢ aD2 ⪅ [Θ]A2 ⊣ ∆instl-arr

Γ[Da ] ⊢ aD ⪅ A1 → A2 ⊣ ∆By applying Lemma E.8 twice, we have Γ[Da ] −→ Γ[Da 2 , aD1 , aD]. By Lemma E.7 we haveΓ[Da 2 , aD1 , aD] −→ Γ[Da 2 , aD1 , aD = aD1 → aD2 ]. By i.h., we have Γ[Da 2 , aD1 , aD = aD1 → aD2 ] −→ Θand Θ −→ ∆. By Lemma E.3 we have Γ[Da ] −→ ∆.
• CaseΓ[Da ], b ⊢ aD ⪅ B ⊣ ∆, b, Θ
instl-forallRΓ[Da ] ⊢ aD ⪅ ∀b. B ⊣ ∆By i.h., we have Γ[Da ], b −→ ∆, b, Θ. By Lemma E.6 (1), we have Γ[Da ] −→ ∆.
• CaseΓ[Da S ] ⊢ ⋆ ⪅ aDS ⊣ Γ[DaG , aDS = aDG ]instr-solveUS

Same as the case for rule instl-solveUS.
• CaseΓ[DaG ] ⊢ ⋆ ⪅ aDG ⊣ Γ[DaG ]instr-solveUG

Same as the case for rule instl-solveUG.
• CaseΓ[Da S ][bDG ] ⊢ bDG ⪅ aDS ⊣ Γ[DaG , aDS = aDG ][bDG = aDG ]instr-reachSG1Same as the case for rule instl-reachSG1.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:59• Caseinstr-reachSG2

Γ[bDS ][DaG ] ⊢ bDS ⪅ aDG ⊣ Γ[bDG , bDS = bDG ][DaG = bDG ]Same as the case for rule instl-reachSG1.
• CaseΓ[Da 2 , aD1 , aD = aD1 → aD2 ] ⊢ aD1 ⪅ A1 ⊣ ΘΘ ⊢ [Θ]A2 ⪅ aD2 ⊣ ∆instr-arr

Γ[Da ] ⊢ A1 → A2 ⪅ aD ⊣ ∆Same as the case for rule instl-arr.
• CaseΓ[Da ], ▶bDS , bDS ⊢ B[b 7→ bDS ] ⪅ aD ⊣ ∆, ▶bDS , Θ
instr-forallLLΓ[Da ] ⊢ ∀b. B ⪅ aD ⊣ ∆D
By i.h., we have Γ[Da ], ▶D, bS −→ ∆, ▶D, Θ. By Lemma E.6(2) we have Γ[Da ] −→ ∆.
b

b

□
E.3

Consistent Subtyping Extends

Lemma E.19. If Γ ⊢ A then Γ −→ contaminate(Γ, A).
Proof. By induction on the structure of Γ. The only interesting case is when Γ = Γ ′, aDS .
By Definition 9.11, we have contaminate((Γ ′, aDS ), A) = contaminate(Γ ′, A), aDG , aDS = aDG . By
i.h., we have Γ ′ −→ contaminate(Γ ′, A). By definition of context extension we have Γ ′, aDS −→contaminate(Γ ′, A), aDS . By Lemma E.8 we have contaminate(Γ ′, A), aDS −→ contaminate(Γ ′, A), aDG , aDS .
By Lemma E.7 we have contaminate(Γ ′, A), aDG , aDS −→ contaminate(Γ ′, A), aDG , aDS = aDG . By Lemma E.3
we have Γ ′, aDS −→ contaminate(Γ ′, A), aDG , aDS = aDG .
□Lemma E.20 (Consistent Subtyping Extension). If Γ ⊢ A ≲ B ⊣ ∆ then Γ −→ ∆.
Proof. By induction on the derivation of consistent subtyping.
• Rules as-tvar, as-evar, as-int, as-spar, and as-gpar are immediate from Lemma E.2.
• CaseΓ ⊢ B 1 ≲ A1 ⊣ ΘΘ ⊢ [Θ]A2 ≲ [Θ]B 2 ⊣ ∆as-arrowΓ ⊢ A1 → A2 ≲ B 1 → B 2 ⊣ ∆By i.h., we have Γ −→ Θ and Θ −→ ∆. By Lemma E.3, we have Γ −→ ∆.
• CaseΓ, a ⊢ A ≲ B ⊣ ∆, a, Θ
as-forallRΓ ⊢ A ≲ ∀a. B ⊣ ∆By i.h., we have Γ, a −→ ∆, a, Θ. By Lemma E.6 (1), we have Γ −→ ∆.
• CaseΓ, ▶aDS , aDS ⊢ A[a 7→ aDS ] ≲ B ⊣ ∆, ▶aDS , Θ
as-forallLLΓ ⊢ ∀a. A ≲ B ⊣ ∆By i.h., we have Γ, ▶aD, aDS −→ ∆, ▶aD, Θ. By Lemma E.6 (2), we have Γ −→ ∆.
• CaseΓ ⊢ ⋆ ≲ C ⊣ contaminate(Γ, C)
Immediate by Lemma E.19.
• Caseas-unknownLLΓ ⊢ C ≲ ⋆ ⊣ contaminate(Γ, C)
Immediate by Lemma E.19.

as-unknownRR

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:60Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers• Rules as-instL and as-instR are immediate.
□

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All
F

39:61

SOUNDNESS OF CONSISTENT SUBTYPING
Definition F.1 (Filling). The filling of a context |Γ| solves all unsolved variables:|•|=•|Γ, x : A| = |Γ|, x : A|Γ, a| = |Γ|, a|Γ, aD = τ | = |Γ|, aD = τ|Γ, aD| = |Γ|, aD = Int|Γ, ▶aD | = |Γ|, ▶aD

Lemma F.2 (Substitution Stability). For any well-formed complete context (Ω, ΩZ ), if Ω ⊢ A
then [Ω]A = [Ω, ΩZ ]A.
Proof. By induction on ΩZ . If ΩZ = •, the result is immediate. Otherwise use the i.h. and thefact that Ω ⊢ A implies fv(A) ∩ dom(ΩZ ) = ∅.
□Lemma F.3 (Filling Completes). If Γ −→ Ω and (Γ, Θ) is well-formed, then Γ, Θ −→ Ω, |Θ|.
Proof. By induction on Θ, following Definition F.1 and applying the rules for context extension.
□
Theorem 7.2 (Instantiation Soundness). Given ∆ −→ Ω and [Γ]A = A and aD < fv(A):(1) If Γ ⊢ aD ⪅ A ⊣ ∆ then [Ω]∆ ⊢ [Ω]Da ≲ [Ω]A.
(2) If Γ ⊢ A ⪅ aD ⊣ ∆ then [Ω]∆ ⊢ [Ω]A ≲ [Ω]Da.
Proof. By induction on the given instantiation derivation.
• CaseΓ ⊢τΓ, aDS , Γ ′ ⊢ aDS ⪅ τ ⊣ Γ, aDS = τ , Γ ′instl-solveS

Immediate from Lemma 7.
• CaseΓ ⊢tΓ, aDG , Γ ⊢ aDG ⪅ t ⊣ Γ, aDG = t, Γ ′′instl-solveG

Immediate from Lemma 7.
• CaseΓ[Da S ] ⊢ aDS ⪅ ⋆ ⊣ Γ[DaG , aDS = aDG ]instl-solveUS

We know [Ω]Da S = t for some castable monotype t, and t ∈ C. By rule cs-unknownRR, wehave [Ω](Γ[Da S ]) ⊢ t ≲ ⋆• CaseΓ[DaG ] ⊢ aDG ⪅ ⋆ ⊣ Γ[DaG ]instl-solveUG

Similar to the case for rule instl-solveUS.
• CaseΓ[Da S ][bDG ] ⊢ aDS ⪅ bDG ⊣ Γ[DaG , aDS = aDG ][bDG = aDG ]instl-reachSG1

We know [Ω]Da S = [Ω]DaG = t and [Ω]bDG = [Ω]DaG = t for some castable monotype t. By
DLemma 7 we have [Ω](Γ[Da S ][bG ]) ⊢ t ≲ t.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:62

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers• Caseinstl-reachSG2

Γ[bDS ][DaG ] ⊢ aDG ⪅ bDS ⊣ Γ[bDG , bDS = bDG ][DaG = bDG ]Similar to the case for rule instl-reachSG1.
• Caseinstl-reachOtherD ⊢ aD ⪅ bD ⊣ Γ[DΓ[Da ][b]
a ][bD = aD]

D we have [Ω]DLet ∆ = Γ[Da ][b],
a = τ and [Ω]bD = [Ω]Da = τ for some monotype τ . By Lemma 7
we have [Ω]∆ ⊢ τ ≲ τ .
• CaseΓ[Da 2 , aD1 , aD = aD1 → aD2 ] ⊢ A1 ⪅ aD1 ⊣ ΘΘ ⊢ aD2 ⪅ [Θ]A2 ⊣ ∆instl-arr

Γ[Da ] ⊢ aD ⪅ A1 → A2 ⊣ ∆Let Γ1 = Γ[Da 2 , aD1 , aD = aD1 → aD2 ]:Θ ⊢ aD2 ⪅ [Θ]A2 ⊣ ∆Θ −→ ∆∆ −→ Ω
Θ −→ Ω
Γ1 ⊢ A1 ⪅ aD1 ⊣ Θ[Ω]∆ ⊢ [Ω]A1 ≲ [Ω]Da1
Θ ⊢ aD2 ⪅ [Θ]A2 ⊣ ∆[Ω]∆ ⊢ [Ω]Da 2 ≲ [Ω]([Θ]A2 )Θ −→ ∆[Ω]∆ ⊢ [Ω]Da 2 ≲ [Ω]A2[Ω]∆ ⊢ [Ω]D
a 1 → [Ω]Da 2 ≲ [Ω]A1 → [Ω]A2[Ω]∆ ⊢ [Ω]Da ≲ [Ω](A1 → A2 )PremiseBy Lemma E.18
Given
By Lemma E.3
Given
By i.h. and Lemma E.14
PremiseBy i.h.
Above
By Lemma E.5
By rule cs-arrow
By def. of substitution• CaseΓ[Da ], b ⊢ aD ⪅ B ⊣ ∆, b, Θ
instl-forallRΓ[Da ] ⊢ aD ⪅ ∀b. B ⊣ ∆∆, b, Θ −→ Ω, b, |Θ|Γ[Da ], b ⊢ aD ⪅ B ⊣ ∆, b, Θ[Ω, b, |Θ|](∆, b, Θ) ⊢ [Ω, b, |Θ|]Da ≲ [Ω, b, |Θ|]B[Ω, b, |Θ|](∆, b, Θ) ⊢ [Ω, b]Da ≲ [Ω, b]B[Ω, b](∆, b) ⊢ [Ω, b]Da ≲ [Ω, b]B[Ω]∆, b ⊢ [Ω]Da ≲ [Ω]B[Ω]∆ ⊢ [Ω]Da ≲ ∀b. [Ω]B[Ω]∆ ⊢ [Ω]Da ≲ [Ω](∀b. B)

By Lemma F.3
Given
By i.h.
Free variables in aD and B are declared in (Ω, b)
By context partitioning and thinning
By context substitution
By rule cs-forallR
By def. of substitution• CaseΓ[Da ], ▶bDS , bDS ⊢ B[b 7→ bDS ] ⪅ aD ⊣ ∆, ▶bDS , Θ
instr-forallLLΓ[Da ] ⊢ ∀b. B ⪅ aD ⊣ ∆∆, ▶bD, Θ −→ Ω, ▶bD, |Θ|By Lemma F.3
Γ[Da ], ▶bD, bDS ⊢ B[b 7→ bDS ] ⪅ aD ⊣ ∆, ▶bD, ΘPremiseD[Ω, ▶bD, |Θ|](∆, ▶bD, Θ) ⊢ [Ω, ▶bD, |Θ|](B[b 7→ bS ]) ≲ [Ω, ▶bD, |Θ|]Da

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

By i.h.

Consistent Subtyping for All

39:63

a
By distributivity of substitution[Ω]∆ ⊢ ([Ω]B)[b 7→ [Ω, ▶bD, |Θ|]bDS ] ≲ [Ω]DDFollows from def. of context application[Ω]∆ ⊢ [Ω, ▶bD, |Θ|]bS[Ω]∆ ⊢ ∀b. [Ω]B ≲ [Ω]Da
By rule cs-forallL and [Ω, ▶bD, |Θ|]bDS is a monotype[Ω]∆ ⊢ [Ω](∀b. B) ≲ [Ω]Da
By def. of substitution• The rest of the cases are similar to the above cases.
□
Theorem 7.3 (Soundness of Algorithmic Consistent Subtyping). If Γ ⊢ A ≲ B ⊣ ∆ where[Γ]A = A and [Γ]B = B and ∆ −→ Ω then [Ω]∆ ⊢ [Ω]A ≲ [Ω]B.
Proof. By induction on the derivation of consistent subtyping.
• Caseas-tvarΓ[a] ⊢ a ≲ a ⊣ Γ[a]a ∈ Γ[a]a ∈ [Ω](Γ[a])[Ω](Γ[a]) ⊢ a ≲ a[Ω](Γ[a]) ⊢ [Ω]a ≲ [Ω]aGiven
Follows from def. of context application
By rule cs-tvar
By def. of substitution• Caseas-evarΓ[Da ] ⊢ aD ≲ aD ⊣ Γ[Da][Ω]Da defined
Follows from def. of context application[Ω]∆ ⊢ [Ω]DaFollows from ∆ = [Γ]Da[Ω]∆ ⊢ [Ω]Da ≲ [Ω]Da By Lemma 7• Caseas-intΓ ⊢ Int ≲ Int ⊣ Γ
Immediate.
• CaseΓ ⊢ B 1 ≲ A1 ⊣ ΘΘ ⊢ [Θ]A2 ≲ [Θ]B 2 ⊣ ∆as-arrowΓ ⊢ A1 → A2 ≲ B 1 → B 2 ⊣ ∆Γ ⊢ B 1 ≲ A1 ⊣ Θ∆ −→ Ω
Θ −→ Ω[Ω]Θ ⊢ [Ω]B 1 ≲ [Ω]A1[Ω]∆ ⊢ [Ω]B 1 ≲ [Ω]A1Θ ⊢ [Θ]A2 ≲ [Θ]B 2 ⊣ ∆[Ω]∆ ⊢ [Ω]([Θ]A2 ) ≲ [Ω]([Θ]B 2 )[Ω]([Θ]A2 ) = [Ω]A2[Ω]([Θ]B 2 ) = [Ω]B 2[Ω]∆ ⊢ [Ω]A2 ≲ [Ω]B 2[Ω]∆ ⊢ [Ω]A1 → [Ω]A2 ≲ [Ω]B 1 → [Ω]B 2[Ω]∆ ⊢ [Ω](A1 → A2 ) ≲ [Ω](B 1 → B 2 )PremiseGiven
By Lemma E.3
By i.h.
By Lemma E.14
PremiseBy i.h.
By Lemma E.5
By Lemma E.5
By above equalities
By rule cs-arrow
By def. of substitution

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:64

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers• CaseΓ, a ⊢ A ≲ B ⊣ ∆, a, Θ
as-forallRΓ ⊢ A ≲ ∀a. B ⊣ ∆Γ, a −→ ∆, a, ΘΘ is soft∆ −→ Ω∆, a, Θ −→ Ω, a, |Θ|| {z }| {z }

By Lemma E.20
By Lemma E.6 (1) where ΓR = •Given
By Lemma F.3

Γ, a ⊢ A ≲ B ⊣ ∆, a, Θ[Ω ′]∆ ′ ⊢ [Ω ′]A ≲ [Ω ′]B[Ω ′]A = [Ω, a]A[Ω ′]B = [Ω, a]B[Ω ′]∆ ′ = [Ω, a](∆, a)[Ω, a](∆, a) ⊢ [Ω, a]A ≲ [Ω, a]B[Ω]∆, a ⊢ [Ω]A ≲ [Ω]B[Ω]∆ ⊢ [Ω]A ≲ ∀a. [Ω]B[Ω]∆ ⊢ [Ω]A ≲ [Ω](∀a. B)

Given
By i.h.
By Lemma F.2
By Lemma F.2
By Lemma E.16
By above equalities
By def. of substitution
By rule cs-forallR
By def. of substitution∆′• CaseΩ′Γ, ▶aDS , aDS ⊢ A[a 7→ aDS ] ≲ B ⊣ ∆, ▶aDS , Θ
as-forallLLΓ ⊢ ∀a. A ≲ B ⊣ ∆Let Ω ′ = Ω, ▶aDS , |Θ|∆ −→ Ω∆, ▶aDS , Θ −→ Ω ′Γ, ▶aDS , aDS ⊢ A[a 7→ aDS ] ≲ B ⊣ ∆, ▶aDS , Θ[Ω ′](∆, ▶aDS , Θ) ⊢ [Ω ′](A[a 7→ aDS ]) ≲ [Ω ′]B[Ω ′]B = [Ω, a]B[Ω](∆, ▶aDS , Θ) ⊢ [Ω ′]A[a 7→ [Ω ′]Da S ] ≲ [Ω]B[Ω](∆, ▶aDS , Θ) ⊢ [Ω ′]DaS[Ω](∆, ▶aDS , Θ) ⊢ ∀a. [Ω ′]A ≲ [Ω]B[Ω]∆ ⊢ ∀a. [Ω]A ≲ [Ω]B[Ω]∆ ⊢ [Ω](∀a. A) ≲ [Ω]BGiven
By Lemma F.3
PremiseBy i.h.
By Lemma F.2
By distributivity of substitution
Follows from def. of context application
By rule cs-forallL
By context partitioning
By def. of substitution• Caseas-sparΓ⊢S≲S⊣Γ
Immediate from rule cs-spar.
• Caseas-gparΓ⊢G≲G⊣Γ
Immediate from rule cs-gpar.
• CaseΓ ⊢ ⋆ ≲ C ⊣ contaminate(Γ, C)

as-unknownLL

Immediate from rule cs-unknownLL.
• CaseΓ ⊢ C ≲ ⋆ ⊣ contaminate(Γ, C)

as-unknownRR

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:65

Immediate from rule cs-unknownRR.
• CaseaD < fv(A)Γ[Da ] ⊢ aD ⪅ A ⊣ ∆as-instLΓ[Da ] ⊢ aD ≲ A ⊣ ∆Γ[Da ] ⊢ aD ⪅ A ⊣ ∆[Ω]∆ ⊢ [Ω]Da ≲ [Ω]APremise
By Theorem 7.2• CaseaD < fv(A)Γ[Da ] ⊢ A ⪅ aD ⊣ ∆as-instRΓ[Da ] ⊢ A ≲ aD ⊣ ∆Similar to the case for rule as-instL.
□

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:66G

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

SOUNDNESS OF TYPING

Note: We use ♦ to improve readability when the conclusion has several parts.
Lemma G.1 (Matching Extension). If Γ ⊢ A ▷ A1 → A2 ⊣ ∆ then Γ −→ ∆.
Proof. By induction on the given derivation.
• CaseΓ, aDS ⊢ A[a 7→ aDS ] ▷ A1 → A2 ⊣ ∆Γ ⊢ ∀a. A ▷ A1 → A2 ⊣ ∆am-forallL

By i.h., we have Γ, aDS −→ ∆. By Lemma E.11, we have Γ −→ ∆.
• CaseΓ ⊢ A1 → A2 ▷ A1 → A2 ⊣ Γam-arrImmediate by Lemma E.2.
• CaseΓ ⊢⋆▷⋆→⋆⊣ Γ

am-unknown

Immediate by Lemma E.2.
• CaseΓ[Da ] ⊢ aD ▷ aD1 → aD2 ⊣ Γ[Da 1 , aD2 , aD = aD1 → aD2 ]am-varBy applying Lemma E.8 twice, we have Γ[Da ] −→ Γ[Da 1 , aD2 , aD]. By Lemma E.7, we haveΓ[Da 1 , aD2 , aD] −→ Γ[Da 1 , aD2 , aD = aD1 → aD2 ]. By Lemma E.3, we have Γ[Da ] −→ Γ[Da 1 , aD2 , aD =
aD1 → aD2 ].
□Lemma G.2 (Typing Extension). If Γ ⊢ e ⇒ A ⊣ ∆ or Γ ⊢ e ⇐ A ⊣ ∆ then Γ −→ ∆.
Proof. By induction on the given derivation.
• Case(x : A) ∈ Γ
inf-varΓ⊢x ⇒A⊣Γ
Immediate by Lemma E.2.
• Case
inf-intΓ ⊢ n ⇒ Int ⊣ Γ
Immediate by Lemma E.2.
• CaseΓ, aDS , bDS , x : aDS ⊢ e ⇐ bDS ⊣ ∆, x : aDS , Θ
inf-lam2Γ ⊢ λx. e ⇒ aDS → bDS ⊣ ∆By i.h., we have Γ, aDS , bDS , x : aDS −→ ∆, x : aDS , Θ. By Lemma E.6, we have Γ, aDS , bDS −→ ∆. By
definition, we have Γ −→ Γ, aDS , bDS . By Lemma E.3 we have Γ −→ ∆.
• CaseΓ⊢AΓ, bDS , x : A ⊢ e ⇐ bDS ⊣ ∆, x : A, Θ
inf-lamann2Γ ⊢ λx : A. e ⇒ A → bDS ⊣ ∆By i.h., we have Γ, bDS , x : A −→ ∆, x : A, Θ. By Lemma E.6, we have Γ −→ ∆.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All• CaseΓ ⊢ e 1 ⇒ A ⊣ Θ1

39:67

Θ1 ⊢ [Θ1 ]A ▷ A1 → A2 ⊣ Θ2

Θ2 ⊢ e 2 ⇐ [Θ2 ]A1 ⊣ ∆inf-appΓ ⊢ e 1 e 2 ⇒ A2 ⊣ ∆By i.h., we have Γ −→ Θ1 , Θ2 −→ ∆. By Lemma G.1, we have Θ1 −→ Θ2 . By Lemma E.3 , wehave Γ −→ ∆.
• CaseΓ⊢AΓ ⊢e ⇐A⊣∆
inf-annoΓ ⊢e :A⇒A⊣∆
By i.h., we have Γ −→ ∆.
• CaseΓ, a ⊢ e ⇐ A ⊣ ∆, a, Θ
chk-genΓ ⊢ e ⇐ ∀a. A ⊣ ∆By i.h., we have Γ, a −→ ∆, a, Θ. By Lemma E.6 we have Γ −→ ∆.
• CaseΓ, x : A ⊢ e ⇐ B ⊣ ∆, x : A, Θ
chk-lamΓ ⊢ λx. e ⇐ A → B ⊣ ∆By i.h., we have Γ, x : A −→ ∆, x : A, Θ. By Lemma E.6 we have Γ −→ ∆.
• CaseΓ ⊢e ⇒A⊣ΘΘ ⊢ [Θ]A ≲ [Θ]B ⊣ ∆chk-subΓ ⊢e ⇐B ⊣∆By i.h., we have Γ −→ Θ. By Lemma E.20 we have Θ −→ ∆. By Lemma E.3 we have Γ −→ ∆.
□Theorem G.3 (Matching Soundness). If Γ ⊢ A ▷ A1 → A2 ⊣ ∆ where [Γ]A = A and ∆ −→ Ωthen [Ω]∆ ⊢ [Ω]A ▷ [Ω]A1 → [Ω]A2 .
Proof. By induction on the given derivation.
• CaseΓ, aDS ⊢ A[a 7→ aDS ] ▷ A1 → A2 ⊣ ∆Γ ⊢ ∀a. A ▷ A1 → A2 ⊣ ∆Γ, aDS ⊢ A[a 7→ aDS ] ▷ A1 → A2 ⊣ ∆∆ −→ Ω[Ω]∆ ⊢ [Ω](A[a 7→ aDS ]) ▷ [Ω]A1 → [Ω]A2[Ω]∆ ⊢ [Ω]A[a 7→ [Ω]Da S ] ▷ [Ω]A1 → [Ω]A2[Ω]∆ ⊢ [Ω]DaS[Ω]∆ ⊢ ∀a. [Ω]A ▷ [Ω]A1 → [Ω]A2[Ω]∆ ⊢ [Ω](∀a. A) ▷ [Ω]A1 → [Ω]A2

am-forallL

PremiseGiven
By i.h.
By distributivity of substitution
Follows from def. of context application
By rule m-forall
By def. of substitution• CaseΓ ⊢ A1 → A2 ▷ A1 → A2 ⊣ Γam-arrImmediate from rule m-arr.
• CaseΓ ⊢⋆▷⋆→⋆⊣ Γ

am-unknown

Immediate from rule m-unknown.
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:68Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers• CaseΓ[Da ] ⊢ aD ▷ aD1 → aD2 ⊣ Γ[Da 1 , aD2 , aD = aD1 → aD2 ]∆ −→ Ω[Ω]Da = [Ω]D
a 1 → [Ω]Da2[Ω]∆ ⊢ [Ω]D
a 1 → [Ω]Da 2 ▷ [Ω]D
a 1 → [Ω]Da2

am-varGiven
By def. of context application
By rule m-arr□

Theorem 7.4 (Soundness of Algorithmic Typing). Given ∆ −→ Ω:(1) If Γ ⊢ e ⇒ A ⊣ ∆ then ∃e ′ such that [Ω]∆ ⊢ e ′ : [Ω]A and ⌊e⌋ = ⌊e ′⌋.
(2) If Γ ⊢ e ⇐ A ⊣ ∆ then ∃e ′ such that [Ω]∆ ⊢ e ′ : [Ω]A and ⌊e⌋ = ⌊e ′⌋.
Proof. By induction on the given derivation.
• Case(x : A) ∈ Γ
inf-varΓ⊢x ⇒A⊣Γ♦♦(x : A) ∈ Γ(x : A) ∈ ∆∆ −→ Ω(x : [Ω]A) ∈ [Ω]Γ[Ω]Γ ⊢ x : [Ω]A⌊x⌋ = ⌊x⌋

Premise∆=Ω
Given
By Lemma E.15
By rule var
By def. of erasure• Case
inf-intΓ ⊢ n ⇒ Int ⊣ Γ♦♦[Ω]Γ ⊢ n : Int⌊n⌋ = ⌊n⌋

By rule int
By def. of erasure• CaseΓ⊢AΓ, bDS , x : A ⊢ e ⇐ bDS ⊣ ∆, x : A, Θ
inf-lamann2Γ ⊢ λx : A. e ⇒ A → bDS ⊣ ∆Γ, aDS , x : A −→ ∆, x : A, Θ
Θ is soft∆ −→ Ω∆, x : A, Θ −→ Ω, x : A, |Θ|| {z }| {z }

By Lemma G.2
By Lemma E.6 where ΓR = •Given
By Lemma F.3

Γ, x : A ⊢ e ⇒ B ⊣ ∆, x : A, Θ[Ω ′]∆ ′ ⊢ e ′ : [Ω ′]bDS⌊e⌋ = ⌊e ′⌋[Ω ′]bDS = [Ω, x : A]bDS = [Ω]bDS[Ω ′]∆ ′ = [Ω]∆, x : [Ω]A[Ω]∆, x : [Ω]A ⊢ e ′ : [Ω]bDS[Ω]∆ ⊢ λx : [Ω]A. e ′ : [Ω]A → [Ω]bDS[Ω]A = A

PremiseBy i.h.
above
By Lemma F.2 and def. of substitution
By Lemma E.16 and def. of context substitution
By above equalities
By rule lamann
Type annotations cannot contain evars∆′Ω′

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

♦
♦

39:69

[Ω]∆ ⊢ λx : A. e ′ : [Ω]A → [Ω]bDS[Ω]∆ ⊢ λx : A. e ′ : [Ω](A → bDS )⌊λx : A. e ′⌋ = λx . ⌊e ′⌋ = λx . ⌊e⌋ = ⌊λx : A. e⌋

By above equality
By def. of substitution
By def. of erasure• CaseD x : aD ⊢ e ⇐ bD ⊣ ∆, x : aD, ΘΓ, aD, b,
inf-lamΓ ⊢ λx. e ⇒ aD → bD ⊣ ∆Γ, aDS , bDS , x : aDS −→ ∆, x : aDS , Θ
Γ, aDS , bDS −→ ∆
Θ is soft

By Lemma G.2
By Lemma E.6
Above∆ −→ Ω∆, x : aDS −→ Ω, x : [Ω]DaS∆, x : aDS , Θ −→ Ω, x : [Ω]Da , |Θ|| {z }|{z S }Given
By defBy Lemma F.3

Γ, aDS , bDS , x : aDS ⊢ e ⇐ bDS ⊣ ∆, x : aDS , Θ[Ω ′]∆ ′ ⊢ e ′ : [Ω ′]bDS⌊e⌋ = ⌊e ′⌋[Ω ′]bDS = [Ω]bDS[Ω ′]∆ ′ = [Ω]∆, x : [Ω]DaS′[Ω]∆, x : [Ω]Da S ⊢ e : [Ω]bDS[Ω]Da S is a monotype[Ω]∆ ⊢ λx. e ′ : [Ω]Da S → [Ω]bDS′[Ω]∆ ⊢ λx. e : [Ω](Da S → bDS )⌊λx . e⌋ = λx . ⌊e⌋ = λx . ⌊e ′⌋ = ⌊λx . e ′⌋PremiseBy i.h.
Above
By def. of context substitution
By def. of context substitution
By above equalitiesΩ is predicative
By rule lam
By def. of substitution
By def. of erasure

∆′

♦
♦

• CaseΓ ⊢ e 1 ⇒ A ⊣ Θ1Ω′

Θ1 ⊢ [Θ1 ]A ▷ A1 → A2 ⊣ Θ2

Θ2 ⊢ e 2 ⇐ [Θ2 ]A1 ⊣ ∆inf-appΓ ⊢ e 1 e 2 ⇒ A2 ⊣ ∆∆ −→ Ω
Θ1 −→ ΩΓ ⊢ e 1 ⇒ A ⊣ Θ1[Ω]Θ1 ⊢ e1′ : [Ω]A⌊e1′ ⌋ = ⌊e 1 ⌋[Ω]Θ1 = [Ω]∆[Ω]∆ ⊢ e1′ : [Ω]A
Θ2 ⊢ e 2 ⇐ [Θ2 ]A1 ⊣ ∆[Ω]∆ ⊢ e2′ : [Ω]A1⌊e2′ ⌋ = ⌊e 2 ⌋Θ1 ⊢ [Θ1 ]A ▷ A1 → A2 ⊣ Θ2[Ω]Θ2 ⊢ [Ω]([Θ1 ]A) ▷ [Ω]A1 → [Ω]A2[Ω]Θ2 = [Ω]∆[Ω]([Θ1 ]A) = [Ω]AGiven
By Lemmas G.1 to E.3
PremiseBy i.h.
above
By Lemma E.14
By above equality
PremiseBy i.h.
Above
Premise
By Theorem G.3
By Lemma E.14
By Lemma E.5

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:70Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers[Ω]∆ ⊢ [Ω]A ▷ [Ω]A1 → [Ω]A2[Ω]∆ ⊢ [Ω]A1 ≲ [Ω]A1♦ [Ω]∆ ⊢ e1′ e2′ : [Ω]A2♦ ⌊e 1′ e 2′ ⌋ = ⌊e 1′ ⌋ ⌊e 2′ ⌋ = ⌊e 1 ⌋ ⌊e 2 ⌋ = ⌊e 1 e 2 ⌋By above equalities
By Lemma 7
By rule app
By def. of erasure• CaseΓ⊢AΓ ⊢e ⇐A⊣∆
inf-annoΓ ⊢e :A⇒A⊣∆♦♦Γ ⊢e ⇐A⊣∆[Ω]∆ ⊢ e ′ : [Ω]A⌊e⌋ = ⌊e ′⌋⌊e : A⌋ = ⌊e⌋ = ⌊e ′⌋PremiseBy i.h.,Above
By above equality and the def. of erasure• CaseΓ, a ⊢ e ⇐ A ⊣ ∆, a, Θ
chk-genΓ ⊢ e ⇐ ∀a. A ⊣ ∆∆ −→ Ω∆, a −→ Ω, a
Γ, a −→ ∆, a, ΘΘ is soft∆, a, Θ −→ Ω, a, |Θ|| {z }| {z }Given
By defBy Lemma G.2
By Lemma E.6
By Lemma F.3

Γ, a ⊢ e ⇐ A ⊣ ∆, a, Θ[Ω ′]∆ ′ ⊢ e ′ : [Ω ′]A⌊e⌋ = ⌊e ′⌋[Ω ′]A = [Ω]A[Ω ′]∆ ′ = [Ω]∆, a[Ω]∆, a ⊢ e ′ : [Ω]A[Ω]∆ ⊢ e ′ : ∀a. [Ω]A[Ω]∆ ⊢ e ′ : [Ω](∀a. A)

PremiseBy i.h.,Above
By Lemma F.2
By Lemma E.16 and def. of context substitution
By above equalities
By rule gen
By def. of substitution

∆′

♦

♦

Ω′

• CaseΓ, x : A ⊢ e ⇐ B ⊣ ∆, x : A, Θ
chk-lamΓ ⊢ λx. e ⇐ A → B ⊣ ∆∆ −→ Ω∆, x : A −→ Ω, x : [Ω]AΓ, x : A −→ ∆, x : A, Θ
Θ is soft∆, x : A, Θ −→ Ω, x : [Ω]A, |Θ|| {z }
|
{z
}

Given
By defBy Lemma G.2
By Lemma E.6
By Lemma F.3

Γ, x : A ⊢ e ⇐ B ⊣ ∆, x : A, Θ[Ω ′]∆ ′ ⊢ e ′ : [Ω ′]B⌊e⌋ = ⌊e ′⌋[Ω ′]B = [Ω]B[Ω ′]∆ ′ = [Ω]∆, x : [Ω]APremiseBy i.h.,Above
By Lemma F.2
By Lemma E.16 and def. of context substitution∆′Ω′

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

♦
♦

39:71

[Ω]∆, x : [Ω]A ⊢ e ′ : [Ω]B[Ω]∆ ⊢ λx : [Ω]A. e ′ : [Ω]A → [Ω]B[Ω]∆ ⊢ λx : [Ω]A. e ′ : [Ω](A → B)
⌊λx . e⌋ = λx . ⌊e⌋ = λx . ⌊e ′⌋ = ⌊λx : [Ω]A. e ′⌋By above equalities
By rule lamann
By def. of substitution
By the def. of erasure• CaseΓ ⊢e ⇒A⊣ΘΘ ⊢ [Θ]A ≲ [Θ]B ⊣ ∆chk-subΓ ⊢e ⇐B ⊣∆♦♦Θ ⊢ [Θ]A ≲ [Θ]B ⊣ ∆Θ −→ ∆∆ −→ Ω
Θ −→ ΩΓ ⊢e ⇒A⊣Θ[Ω]Θ ⊢ e ′ : [Ω]A⌊e⌋ = ⌊e ′⌋[Ω]Θ = [Ω]∆[Ω]∆ ⊢ e ′ : [Ω]A[Ω]∆ ⊢ [Ω]([Θ]A) ≲ [Ω]([Θ]B)[Ω]([Θ]A) = [Ω]A[Ω]([Θ]B) = [Ω]B[Ω]∆ ⊢ [Ω]A ≲ [Ω]B[Ω]∆ ⊢ (e ′ : [Ω]B) : [Ω]B⌊(e ′ : [Ω]B)⌋ = ⌊e ′⌋ = ⌊e⌋PremiseBy Lemma E.20
Given
By Lemma E.3
PremiseBy i.h.,Above
By Lemma E.14
By above equality
By Theorem 7.3
By Lemma E.5
By Lemma E.5
By above equalities
By def. annotation
By def. erasure□

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:72
H

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

COMPLETENESS OF CONSISTENT SUBTYPING

Theorem 7.5 (Instantiation Completeness). Given Γ −→ Ω and A = [Γ]A and aD < unsolved(Γ)
and aD < fv(A):a ≲ [Ω]A then there are ∆, Ω ′ such that Ω −→ Ω ′ and ∆ −→ Ω ′ and Γ ⊢ aD ⪅(1) If [Ω]Γ ⊢ [Ω]DA ⊣ ∆.
(2) If [Ω]Γ ⊢ [Ω]A ≲ [Ω]Da then there are ∆, Ω ′ such that Ω −→ Ω ′ and ∆ −→ Ω ′ and Γ ⊢ A ⪅aD ⊣ ∆.
Proof. By mutual induction on the given derivation.
(1) We have [Ω]Γ ⊢ [Ω]Da ≲ [Ω]A. We case analyze the shape of A.
• Case A = ⋆, aD = aDS :[Ω]Γ ⊢ [Ω]Da S ≲ [Ω]⋆[Ω]⋆ = ⋆[Ω]Γ ⊢ [Ω]DaS ≲ ⋆
aDS < unsolved(Γ)Γ = ΓL , aDS , ΓR
ΓL , aDS , ΓR −→ Ω
Ω = ΩL , aDS = t, ΩR
ΓL −→ ΩLLet ∆ = ΓL , aDG , aDS = aDG , ΓR
and Ω ′ = ΩL , aDG = t, aDS = t, ΩR♦ Γ ⊢ aDS ⪅ ⋆ ⊣ ∆♦ ∆ −→ Ω ′♦ Ω −→ Ω ′Given
By above equality
Given
Above
Given
By Lemma E.6 and Ω is complete and [Ω]DaS ∈ CAbove

By rule instl-solveUS
By Lemmas E.9 and E.10
By Lemmas E.7 and E.8• Case A = ⋆, aD = aDG :[Ω]Γ ⊢ [Ω]DaG ≲ [Ω]⋆[Ω]⋆ = ⋆[Ω]Γ ⊢ [Ω]DaG ≲ ⋆
aDG < unsolved(Γ)Γ = Γ0 [DaG ]Let ∆ = Γ0 [DaG ] and Ω ′ = Ω♦ Γ ⊢ aDG ⪅ ⋆ ⊣ ∆♦ ∆ −→ Ω ′♦ Ω −→ Ω ′Given
By above equality
Given
Above
By rule instl-solveUG
Given
By Lemma E.2• Case A = bDG , aD = aDS :[Ω]Γ ⊢ [Ω]Da S ≲ [Ω]bDG[Ω]Γ ⊢ τ ≲ t
τ =t

Given
Let [Ω]Da S = τ and [Ω]bDG = t and Ω is predicative
By Lemma 8[Γ]bDG = bDGD
bG ∈ unsolved(Γ)

Given
Above

Now consider whether aDS is declared to the left of bDG .
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:73– Case Γ = Γ0 , aDS , Γ1 , bDG , Γ2♦♦♦

Let ∆ = Γ0 , aDG , aDS = aDG , Γ1 , bDG = aDG , Γ2
Γ ⊢ aDS ⪅ bDG ⊣ ∆Γ −→ ΩΩ = Ω0 , aDS = t, Ω1 , bDG = t, Ω2
Let Ω ′ = Ω0 , aDG = t, aDS = t, Ω1 , bDG = t, Ω2Ω −→ Ω ′∆ −→ Ω ′By rule instl-reachSG1
Given
By Lemma E.6
By Lemmas E.7 and E.8
By Lemmas E.9 and E.10

– Case Γ = Γ0 , bDG , Γ1 , aDS , Γ2♦♦♦

Let ∆ = Γ0 , bDG , Γ1 , aDS = bDG , Γ2
Γ ⊢ aDS ⪅ bDG ⊣ ∆∆ −→ ΩΩ −→ Ω

By rule instl-reachOther
By Lemma E.10
By Lemma E.2• Case A = bDS is similar to the above case.
• Case A = a:[Ω]Γ ⊢ [Ω]Da ≲ [Ω]a[Ω]Γ ⊢ [Ω]D
a≲a
[Ω]D
a=a
a is declared to the left of aD in ΩΓ −→ Ω
a is declared to the left of aD in Γ
Let Γ = Γ0 [a][Da]Let ∆ = Γ0 [a][Da = a]♦ Γ ⊢ aD ⪅ a ⊣ ∆♦ ∆ −→ Ω♦ Ω −→ ΩGiven
From [Ω]a = a
By inversion of rule cs-tvarΩ is well-formed
Given
By Lemma E.1

By rule instl-solveS or rule instl-solveG
By Lemma E.10
By Lemma E.2• Case A = A1 → A2 :[Ω]Γ ⊢ [Ω]Da ≲ [Ω]A1 → [Ω]A2[Ω]Da = τ1 → τ2[Ω]Γ ⊢ [Ω]A1 ≲ τ1[Ω]Γ ⊢ τ2 ≲ [Ω]A2
Γ = Γ0 [Da]Γ0 [Da ] −→ Γ0 [Da , aD , aD = aD → aD2 ]| 2 1 {z 1}Given
Ω is predicative
By inversion of rule cs-arrow
Above
From aD ∈ unsolved(Γ)Γ −→ ΩΩ = Ω0 [Da = τ0 ]Ω0 [Da = τ0 ] −→ Ω0 [D
a = τ2 , aD1 = τ1 , aD = aD1 → aD2 ]
| 2
{z
}

Given
From aD ∈ unsolved(Γ)[Ω]Γ = [Ω1 ]Γ1[Ω]A1 = [Ω1 ]A1
τ1 = [Ω1 ]D
a1

By Lemma E.13
By Lemma E.12
From def. of Ω1

Γ1Ω1

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:74

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers[Ω1 ]Γ1 ⊢ [Ω1 ]A1 ≲ [Ω1 ]D
a1
Γ1 ⊢ A1 ⪅ aD1 ⊣ ∆2∆2 −→ Ω2 and Ω1 −→ Ω2

By above equalities
By i.h.
Above[Ω]Γ = [Ω2 ]Γ2[Ω]A2 = [Ω2 ]A2 = [Ω2 ]([∆2 ]A2 )τ2 = [Ω2 ]D
a2[Ω2 ]∆2 ⊢ [Ω2 ]D
a 2 ≲ [Ω2 ]([∆2 ]A2 )∆2 ⊢ aD2 ⪅ [∆2 ]A2 ⊣ ∆Ω2 −→ Ω ′♦ ∆ −→ Ω ′♦ Γ0 [Da ] ⊢ aD ⪅ A1 → A2 ⊣ ∆♦ Ω −→ Ω ′By Lemma E.13
By Lemma E.12
By Ω1 −→ Ω2
By above equalities
By i.h.
Above
Above
By rule instl-arr
By Lemma E.3• Case A = Int:[Ω]Γ ⊢ [Ω]Da ≲ [Ω]Int[Ω]Int = Int[Ω]Γ ⊢ [Ω]Da ≲ Int[Ω]Da = IntaD ∈ unsolved(Γ)Γ = Γ0 [Da]Let ∆ = Γ0 [D
a = Int] and Ω ′ = ΩΓ0 [Da ] ⊢ aD ⪅ Int ⊣ ∆Γ −→ Ω
Γ0 [Da = Int] −→ ΩGiven
By above equalityΩ is predicative
Given
Above
By rule instl-solveS or rule instl-solveG
Given
By Lemma E.10

• Case A = ∀b. B:[Ω]Γ ⊢ [Ω]Da ≲ ∀b. [Ω]B[Ω]Da cannot be a quantifier[Ω]Γ, b ⊢ [Ω]Da ≲ [Ω]BGivenΩ is predicative
By inversion of rule cs-forallR♦[Ω]Γ, b = [Ω, b](Γ, b)[Ω]Da = [Ω, b]Da[Ω]B = [Ω, b]B[Ω, b](Γ, b) ⊢ [Ω, b]Da ≲ [Ω, b]B
Γ, b ⊢ aD ⪅ B ⊣ ∆0∆0 −→ Ω ′Ω, b −→ Ω ′Ω −→ Ω ′By def. of context substitution
By def. of substitution
By def. of substitution
By above equalities
By i.h.
Above
Above
By Lemma E.11
By Lemma E.18
By Lemma E.6
Above

♦
♦

Γ, b −→ ∆0∆0 = ∆, b, ∆ ′Γ −→ ∆∆ −→ Ω ′Γ ⊢ aD ⪅ ∀b. B ⊣ ∆By rule instl-forallR

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:75(2) Now we have [Ω]Γ ⊢ [Ω]A ≲ [Ω]Da . These cases are mostly symmetric. The one exception iswhen A = ∀b. B.
• Case A = ∀b. B:[Ω]Γ ⊢ ∀b. [Ω]B ≲ [Ω]D
a
Given
[Ω]D
a cannot be a quantifierΩ is predicative[Ω]Γ ⊢ τ
By inversion of rule cs-forallL[Ω]Γ ⊢ ([Ω]B)[b 7→ τ ] ≲ [Ω]Da
Above[Ω]Γ = [Ω, ▶bDS , bDS = τ ](Γ, ▶bDS , bDS )By def. of context application([Ω]B)[b 7→ τ ] = [Ω, ▶D , bDS = τ ](B[b 7→ bDS ])by def. of substitutionbS[Ω]Da = [Ω, ▶bDS , bDS = τ ]Da
By def. of substitutionDD[Ω, ▶D , bS = τ ](Γ, ▶D , bS ) ⊢ [Ω, ▶D , bDS = τ ](B[b 7→ bDS ]) ≲ [Ω, bDS = τ ]D
a
bS

bS

bS

By above equalitiesΓ, ▶bDS , bDS ⊢ B[b 7→ bDS ] ⪅ aD ⊣ ∆By i.h.
DΓ, ▶D , bS −→ ∆By Lemma E.18
bS

♦
♦
♦

∆ = ∆L , ▶bDS , ∆R
By Lemma E.6
Γ −→ ∆LAboveΩ, ▶bDS , bDS = τ −→ Ω ′AboveΩ ′ = ΩL , ▶bDS , ΩR
By Lemma E.6Ω −→ ΩL
Above∆L −→ ΩL
Lemma E.3
Γ ⊢ ∀b. B ⪅ aD ⊣ ∆L
By rule instr-forallLL□

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

[Γ]A

1 (B poly)

1 (B poly)

1 (B poly)

1 (B poly)

1 (B poly)aD⋆

A1 → A2

S

G

Impossible

Impossible

Impossible

2.Unknown

2.AEx.Int

Impossible

2.Ints1 (B poly)

1 (B poly)

2.PolyR

1 (B poly)a∀a .A′
R∀b .B ′

Impossible

Impossible

Impossible

2.BEx.G

2.BEx.S

2.BEx.Arrow

2.Unknown

1 (B unknown)

Impossible

1 (B unknown)

1 (B unknown)

1 (B unknown)

2.AEx.SameEx
2.AEx.OtherEx

Table 31. List of cases

2.Unknown

2.AEx.UVar

1 (B unknown)

1 (B unknown)⋆

1 (B unknown)[Γ]B

2.BEx.UVar

2.BEx.Int

Impossible
2.UVars

2.PolybD

2.Polya

Impossible

Impossible

2.Arrows

2.Unknown

2.AEx.Arrow

Impossible

Impossible

2.PolyB1 → B2

Impossible

2.S

Impossible

Impossible

2.AEx.S

Impossible

Impossible

2.PolyS

2.G

Impossible

Impossible

2.Unknown

2.AEx.G

Impossible

Impossible

2.PolyG

39:76
Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:77

Theorem 7.6 (Generalized Completeness of Consistent Subtyping). If Γ −→ Ω and Γ ⊢ A
and Γ ⊢ B and [Ω]Γ ⊢ [Ω]A ≲ [Ω]B then there exist ∆ and Ω ′ such that ∆ −→ Ω ′ and Ω −→ Ω ′ andΓ ⊢ [Γ]A ≲ [Γ]B ⊣ ∆.
Proof. By induction on the given declarative derivation. We list all the possible cases in Table 31.
We first split on[Γ]B.
• Case 1 (B poly) : [Γ]B is polymorphic: [Γ]B = ∀b. B ′:B = ∀b. B 0
B ′ = [Γ]B 0[Ω]B = ∀b. [Ω]B 0[Ω]Γ ⊢ [Ω]A ≲ [Ω]B[Ω]Γ ⊢ [Ω]A ≲ ∀b. [Ω]B 0[Ω]Γ, b ⊢ [Ω]A ≲ [Ω]B 0[Ω]Γ, b = [Ω, b](Γ, b)[Ω]A = [Ω, b]A[Ω]B = [Ω, b]B[Ω, b](Γ, b) ⊢ [Ω, b]A ≲ [Ω, b]B 0
Γ, b ⊢ [Γ, b]A ≲ [Γ, b]B 0 ⊣ ∆ ′∆ ′ −→ Ω0′Ω, b −→ Ω0′
Γ, b ⊢ [Γ]A ≲ [Γ]B 0 ⊣ ∆ ′Γ is predicativeΓ is predicative
By def. of substitution
PremiseBy above equality
By Lemma D.1
By def. of substitution
By def. of substitution
By def. of substitution
By above equalities
By i.h.
Above
Above
By def. of substitution♦

Γ, b −→ ∆ ′∆ ′ = ∆, b, ΘΓ −→ ∆∆, b, Θ −→ Ω0′Ω0′ = Ω ′, b, ΩR∆ −→ Ω ′Ω, b −→ Ω ′, b, ΩRΩ −→ Ω ′By Lemma E.18
By Lemma E.6
Above
By ∆ ′ −→ Ω0′ and above equality
By Lemma E.6
Above
By above equality
By Lemma E.6♦

Γ, b ⊢ [Γ]A ≲ [Γ]B 0 ⊣ ∆, b, ΘΓ ⊢ [Γ]A ≲ ∀b. [Γ]B 0 ⊣ ∆Γ ⊢ [Γ]A ≲ ∀b. B ′ ⊣ ∆By above equality
By rule as-forallR
By above equality♦• Case 1 (B unknown) : [Γ]B = ⋆:[Ω]B = ⋆[Ω]Γ ⊢ [Ω]A ≲ ⋆[Ω]A ∈ C
Γ −→ Ω[Γ]A ∈ CΓ ⊢ [Γ]A ≲ ⋆ ⊣ contaminate(Γ, [Γ]A)There exists Ω ′ such that contaminate(Γ, [Γ]A) −→ Ω ′ and Ω −→ Ω ′

Given
Above
Given
Above
By rule as-unknownRR• Case 2.*: [Γ]B is not polymorphic. We split on the form of [Ω]A.
– Case 2.Poly : [Ω]A is polymorphic: [Γ]A = ∀a. A′:
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:78♦♦♦Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers
A = ∀a. A0A′ = [Γ]A0[Ω]A = ∀a. [Ω]A0[Ω]Γ ⊢ [Ω]A ≲ [Ω]B[Ω]Γ ⊢ ∀a. [Ω]A0 ≲ [Ω]B[Ω]Γ ⊢ ([Ω]A0 )[a 7→ τ ] ≲ [Ω]B[Ω]Γ ⊢ τΓ is predicativeΓ is predicative
By def. of substitution
PremiseBy above equality
By inversion on rule cs-forallLAbove[Ω]Γ = [Ω, aD = τ ](Γ, aD)([Ω]A0 )[a 7→ τ ] = [Ω, aD = τ ](A0 [a 7→ aD])[Ω]B = [Ω, aD = τ ]B[Ω, aD = τ ](Γ, aD) ⊢ [Ω, aD = τ ](A0 [a 7→ aD]) ≲ [Ω, aD = τ ]B
Γ, aD ⊢ [Γ, aD](A0 [a 7→ aD]) ≲ [Γ, aD]B ⊣ ∆∆ −→ Ω ′Ω, aD = τ −→ Ω ′Ω −→ Ω ′[Γ, aD](A0 [a 7→ aD]) = ([Γ]A0 )[a 7→ aD][Γ, aD]B = [Γ]BΓ, aD ⊢ ([Γ]A0 )[a 7→ aD] ≲ [Γ]B ⊣ ∆Γ ⊢ ∀a. ([Γ]A0 ) ≲ [Γ]B ⊣ ∆Γ ⊢ ∀a. A′ ≲ [Γ]B ⊣ ∆By def. of substitution
By def. of substitution
By def. of substitution
By above equalities
By i.h.
Above
Above
By Lemma E.11
By def. of substitution
By def. of substitution
By above equality
By rule as-forallLL
By above equality– Case 2.Unknown : [Γ]A = ⋆:[Ω]A = ⋆[Ω]Γ ⊢ ⋆ ≲ [Ω]B[Ω]B ∈ C
Γ −→ Ω[Γ]B ∈ CΓ ⊢ ⋆ ≲ [Γ]B ⊣ contaminate(Γ, [Γ]B)There exists Ω ′ such that contaminate(Γ, [Γ]B) −→ Ω ′ and Ω −→ Ω ′Obviously, what else?
Given
Above
Given
Above
By rule as-unknownLL– Case 2.AEx.* : [Γ]A is an existential variable: [Γ]A = aD. We split on the form of [Γ]B.
∗ Case 2.AEx.SameEx . [Γ]B is the same existential variable [Γ]B = aD:♦♦♦Γ ⊢ aD ≲ aD ⊣ ΓΓ ⊢ [Γ]A ≲ [Γ]B ⊣ Γ∆ −→ ΩΩ −→ Ω ′By rule as-evar
By above equality∆=Γ
By Lemma E.2 and Ω ′ = Ω∗ Case 2.AEx.OtherEx . [Γ]B is a different existential variable [Γ]B = bD where bD , aD:♦[Ω]A = [Ω]([Γ]A) = [Ω]DaD[Ω]B = [Ω]([Γ]B) = [Ω]b[Ω]Γ ⊢ [Ω]A ≲ [Ω]B[Ω]Γ ⊢ [Ω]Da ≲ [Ω]bDΓ ⊢ aD ⪅ bD ⊣ ∆∆ −→ Ω ′By Lemma E.5
By Lemma E.5
Given
By above equalities
By Theorem 7.5
Above

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All♦♦Ω −→ Ω ′Γ ⊢ aD ≲ bD ⊣ ∆Γ ⊢ [Γ]A ≲ [Γ]B ⊣ ∆

39:79
Above
By rule as-instL
By above equalities∗ Case 2.AEx.Int . We have [Γ]B = Int:♦♦♦Γ −→ Ω[Ω]B = Int = [Ω]Int[Ω]A = [Ω]([Γ]A) = [Ω]Da[Ω]Γ ⊢ [Ω]A ≲ [Ω]B[Ω]Γ ⊢ [Ω]Da ≲ [Ω]IntΓ ⊢ aD ⪅ Int ⊣ ∆∆ −→ Ω ′Ω −→ Ω ′Γ ⊢ aD ≲ Int ⊣ ∆Γ ⊢ [Γ]A ≲ [Γ]B ⊣ ∆Given
By def. of substitution
By Lemma E.5
Given
By above equalities
By Theorem 7.5
Above
Above
By rule as-instL
By above equalities∗ Case 2.AEx.UVar . We have [Γ]B = b. Similar to Case 2.AEx.Int .
∗ Case 2.AEx.Arrow . [Γ]B = B 1 → B 2 . We prove aD < fv([Γ]B). Suppose for a contradiction, that aD ∈ fv([Γ]B), then aD must be a subterm of [Γ]B, so is [Ω]Da a subterm of[Ω]([Γ]B). The latter is equal to [Ω]B, so [Ω]Da is a subterm of [Ω]B. Since [Γ]B = B 1 → B 2 ,then [Ω]B must have the form B 1′ → B 2′ . Therefore [Ω]Da must occur in either B 1′ or B 2′ .
But we have [Ω]Γ ⊢ [Ω]Da ≲ [Ω]B. That is , [Ω]Da cannot be a subterm of [Ω]B. This is acontradiction.
aD < fv([Γ]B)Γ −→ Ω[Ω]B = [Ω]([Γ]B)[Ω]Γ ⊢ [Ω]Da ≲ [Ω]B[Ω]Γ ⊢ [Ω]Da ≲ [Ω]([Γ]B)Γ ⊢ aD ⪅ [Γ]B ⊣ ∆♦ ∆ −→ Ω ′♦ Ω −→ Ω ′Γ ⊢ aD ≲ [Γ]B ⊣ ∆♦ Γ ⊢ [Γ]A ≲ [Γ]B ⊣ ∆Proved above
Given
By Lemma E.5
Given
By above equality
By Theorem 7.5
Above
Above
By rule cs-instL
By above equalities∗ Case 2.AEx.S and 2.AEx.S . Similar to Case 2.AEx.Int .
D We– Case 2.BEx.* . [Γ]A is not polymorphic and [Γ]B is an existential variable: [Γ]B = b.
split on the form of [Γ]A.
∗ Case 2.BEx.Int . Similar to Case 2.AEx.Unit .
∗ Case 2.BEx.UVar . Similar to Case 2.AEx.UVar .
∗ Case 2.BEx.Arrow . Similar to Case 2.AEx.Arrow .
∗ Case 2.BEx.S . Similar to Case 2.AEx.S .
∗ Case 2.BEx.G . Similar to Case 2.AEx.G .
We use the second part of Theorem 7.5 and apply rule as-instR.
– Case 2.Ints . [Γ]A = [Γ]B = Int:♦Γ ⊢ Int ≲ Int ⊣ Γ

By rule as-int
ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:80♦♦Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers
Γ −→ Ω∆ −→ Ω ′Ω −→ Ω ′Given∆=Γ
By Lemma E.2 and Ω ′ = Ω– Case 2.UVars . [Γ]A = [Γ]B = a:♦♦♦Γ⊢a≲a⊣ΓΓ −→ Ω∆ −→ Ω ′Ω −→ Ω ′By rule as-tvar
Given
∆=Γ
By Lemma E.2 and Ω ′ = Ω– Case 2.Arrows . Let [Γ]A = A1 → A2 and [Γ]B = B 1 → B 2 :♦♦♦Γ −→ Ω[Ω]A = [Ω]([Γ]A) = [Ω]A1 → [Ω]A2[Ω]B = [Ω]([Γ]B) = [Ω]B 1 → [Ω]B 2[Ω]Γ ⊢ [Ω]A ≲ [Ω]B[Ω]Γ ⊢ [Ω]B 1 ≲ [Ω]A1Γ ⊢ [Γ]B 1 ≲ [Γ]A1 ⊣ ΘΘ −→ Ω0Ω −→ Ω0Γ −→ Ω0Given
By Lemma E.5
By Lemma E.5
Given
PremiseBy i.h.
Above
Above
By Lemma E.3[Ω]Γ = [Ω0 ]Θ
[Ω]A2 = [Ω0 ]([Γ]A2 )[Ω]B 2 = [Ω0 ]([Γ]B 2 )[Ω]Γ ⊢ [Ω]A2 ≲ [Ω]B 2[Ω0 ]Θ ⊢ [Ω0 ]([Γ]A2 ) ≲ [Ω0 ]([Γ]B 2 )Θ ⊢ [Θ]([Γ]A2 ) ≲ [Θ]([Γ]B 2 ) ⊣ ∆∆ −→ Ω ′Ω0 −→ Ω ′By Lemma E.14
By Lemma E.5
By Lemma E.5
PremiseBy above equalities
By i.h.
Above
Above

Γ ⊢ [Γ](A1 → A2 ) ≲ [Γ](B 1 → B 2 ) ⊣ ∆Ω −→ Ω ′By rule as-arrow
By Lemma E.3– Case 2.S : [Γ]A = [Γ]B = S.
♦♦♦Γ⊢S≲S⊣ΓΓ −→ Ω∆ −→ Ω ′Ω −→ Ω ′By rule as-spar
Given
∆=Γ
By Lemma E.2 and Ω ′ = Ω– Case 2.G . Similar to Case 2.S .
□ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All
I

39:81

COMPLETENESS OF TYPING

Theorem 7.7 (Matching Completeness). Given Γ −→ Ω and Γ ⊢ A, if [Ω]Γ ⊢ [Ω]A ▷ A1 → A2
then there exist ∆, Ω ′, A′1 and A′2 such that Γ ⊢ [Γ]A ▷ A′1 → A′2 ⊣ ∆ and ∆ −→ Ω ′ and Ω −→ Ω ′ andA1 = [Ω ′]A′1 and A2 = [Ω ′]A′2 .
Proof. By induction on the given derivation. We split on [Γ]A.
• [Γ]A = ∀a. A′:♦♦♦

A = ∀a. A0A′ = [Γ]A0[Ω]A = ∀a. [Ω]A0[Ω]Γ ⊢ [Ω]A ▷ A1 → A2[Ω]Γ ⊢ ∀a. [Ω]A0 ▷ A1 → A2[Ω]Γ ⊢ ([Ω]A0 )[a 7→ τ ] ▷ A1 → A2[Ω]Γ ⊢ τ
Γ −→ Ω
Γ, aDS −→ Ω, aDS

Γ is predicativeΓ is predicative
By def. of substitution
Given
By above equality
By inversion
Above
Given
By def. of context extension[Ω]Γ = [Ω, aDS = τ ](Γ, aDS )([Ω]A0 )[a 7→ τ ] = [Ω, aDS = τ ](A0 [a 7→ aDS ])[Ω, aDS = τ ](Γ, aDS ) ⊢ [Ω, aDS = τ ](A0 [a 7→ aDS ]) ▷ A1 → A2
Γ, aDS ⊢ [Γ, aDS ](A0 [a 7→ aDS ]) ▷ A′1 → A′2 ⊣ ∆∆ −→ Ω ′ and Ω, aDS = τ −→ Ω ′A1 = [Ω ′]A′1 and A2 = [Ω ′]A′2[Γ, aDS ](A0 [a 7→ aDS ]) = ([Γ]A0 )[a 7→ aDS ]Γ, aDS ⊢ ([Γ]A0 )[a 7→ aDS ] ▷ A′1 → A′2 ⊣ ∆Γ ⊢ ∀a. [Γ]A0 ▷ A′1 → A′2 ⊣ ∆[Γ]A = ∀a. A′ = ∀a. [Γ]A0Γ ⊢ [Γ]A ▷ A′1 → A′2 ⊣ ∆By def. of context application
By def. of substitution
By above equalities
By i.h.
Above
Above
By def. of substitution
By above equality
By rule am-forallL
By above equalities
Above• [Γ]A = A′1 → A′2 :

♦
♦
♦
♦

[Ω]A = [Ω]([Γ]A) = [Ω]A′1 → [Ω]A′2[Ω]Γ ⊢ [Ω]A′1 → [Ω]A′2 ▷ A1 → A2
Let ∆ = Γ and Ω ′ = Ω[Ω]A′1 = A1 and [Ω]A′2 = A2
Γ ⊢ A′1 → A′2 ▷ A′1 → A′2 ⊣ Γ∆ −→ Ω ′Ω −→ Ω ′By Lemma E.5
Given

By rule am-arr
Given Γ −→ Ω
By Lemma E.2• [Γ]A = ⋆:

♦
♦
♦
♦

[Ω]A = [Ω]([Γ]A) = ⋆[Ω]Γ ⊢ ⋆ ▷ A1 → A2
Let ∆ = Γ and Ω ′ = Ω
A1 = ⋆ and A2 = ⋆Γ ⊢⋆▷⋆→⋆⊣ Γ∆ −→ Ω ′Ω −→ Ω ′By Lemma E.5
Given

By rule am-unknown
Given Γ −→ Ω
By Lemma E.2

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:82

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers• [Γ]A = aD:

♦
♦
♦
♦

Γ = Γ0 [Da][Ω]A = [Ω]([Γ]A) = [Ω]Da[Ω]Γ ⊢ [Ω]Da ▷ A1 → A2[Ω]Da = τ1 → τ2 and A1 = τ1 and A2 = τ2
Ω = Ω0 [Da = τ ′] and [Ω]τ ′ = τ1 → τ2
Let ∆ = Γ0 [D
a 1 , aD2 , aD = aD1 → aD2 ]Let Ω ′ = Ω0 [D
a 1 = τ1 , aD2 = τ2 , aD = aD1 → aD2 ]∆ −→ Ω ′Ω −→ Ω ′Γ0 [Da ] ⊢ aD ▷ aD1 → aD2 ⊣ ∆A1 = τ1 = [Ω ′]Da 1 and A2 = τ2 = [Ω ′]Da2

Since aD ∈ unsolved(Γ)
By Lemma E.5
GivenΩ is predicate
Above

By Lemma E.9 twice
By Lemma E.10 and Lemma E.9
By rule am-var
Above□

Theorem 7.8 (Completeness of Algorithmic Typing). Given Γ −→ Ω and Γ ⊢ A, if [Ω]Γ ⊢ e : A
then there exist ∆, Ω ′, A′ and e ′ such that ∆ −→ Ω ′ and Ω −→ Ω ′ and Γ ⊢ e ′ ⇒ A′ ⊣ ∆ and
A = [Ω ′]A′ and ⌊e⌋ = ⌊e ′⌋.
Proof. By induction on the given derivation.
• Case(x : A) ∈ [Ω]Γvar[Ω]Γ ⊢ x : A

♦
♦
♦
♦
♦

(x : A) ∈ [Ω]ΓΓ −→ Ω(x : A′ ) ∈ Γ where [Ω]A′ = [Ω]ALet ∆ = Γ and Ω ′ = Ω.
Γ −→ ΩΩ −→ ΩΓ ⊢ x ⇒ A′ ⊣ Γ[Ω]A′ = [Ω]A = A⌊x⌋ = ⌊x⌋

PremiseGiven
From def. of context application
Given
By Lemma E.2
By rule inf-var
A is well-formed in [Ω]ΓBy def. of erasure• Caseint[Ω]Γ ⊢ n : Int

♦
♦
♦
♦
♦

Let A′ = Int and ∆ = Γ and Ω ′ = Ω.
Γ −→ ΩΩ −→ Ω
Γ ⊢ n ⇒ Int ⊣ Γ[Ω]Int = Int⌊n⌋ = ⌊n⌋Given
By Lemma E.2
By rule inf-int
By def. of erasure• Case[Ω]Γ, x : A ⊢ e : B
lamann[Ω]Γ ⊢ λx : A. e : A → B

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

39:83

Let Ω0 = Ω, x : A.
[Ω0 ](Γ, x : A) = [Ω]Γ, x : A[Ω0 ](Γ, x : A) ⊢ e : B
Γ, x : A ⊢ e ′ ⇒ B 0 ⊣ ∆0∆0 −→ Ω ′
Ω0 −→ Ω ′B = [Ω ′]B 0⌊e⌋ = ⌊e ′⌋Γ, x : A −→ ∆0∆0 = ∆1 , x : A ′ , ∆2[∆1 ]A = [∆1 ]A′
Γ −→ ∆1
A = [∆1 ]A′
Γ, x : A ⊢ e ′ ⇒ B 0 ⊣ ∆1 , x : A, ∆2
Γ, x : A ⊢ e ′ ⇐ B 0 ⊣ ∆1 , x : A, ∆2

From def. of context application
By above equality and premise
By i.h.
Above
Above
Above
Above
By Lemma G.2
By Lemma E.6
Above
Above
A has no evar
By above equalities
By rule chk-sub♦∆1 , x : A′, ∆2 −→ Ω ′Ω ′ = Ω1 , x : A′′, Ω2[Ω1 ]A′ = [Ω1 ]A′′
∆1 −→ Ω1Ω, x : A −→ Ω1 , x : A′′, Ω2Ω −→ Ω1

By above equalities
By Lemma E.6
Above
Above
By above equalities
By Lemma E.6♦♦♦

Γ ⊢ λx. e ′ ⇐ A → B 0 ⊣ ∆1
Γ ⊢ (λx. e ′ ) : A → B 0 ⇒ A → B 0 ⊣ ∆1[Ω1 ](A → B 0 ) = A → [Ω ′]B 0 = A → B⌊λx : A. e⌋ = λx . ⌊e⌋ = λx . ⌊e ′⌋ = ⌊(λx. e ′ ) : A → B 0 ⌋rule chk-lam
rule inf-anno
From above equality
By def. of erasure♦• Case[Ω]Γ ⊢ e1 : A[Ω]Γ ⊢ A ▷ A1 → A2[Ω]Γ ⊢ e2 : A3[Ω]Γ ⊢ A3 ≲ A1
app[Ω]Γ ⊢ e1 e2 : A2[Ω]Γ ⊢ e1 : A
Γ −→ ΩΓ ⊢ e 1′ ⇒ A′ ⊣ Θ1
Θ1 −→ Ω0′
Ω −→ Ω0′A = [Ω0′ ]A′⌊e1 ⌋ = ⌊e 1′ ⌋PremiseGiven
By i.h.
Above
Above
Above
Above

[Ω]Γ ⊢ A ▷ A1 → A2[Ω]Γ = [Ω]Ω
= [Ω0′ ]Ω0′
= [Ω0′ ]Γ
= [Ω0′ ]Θ1[Ω0′ ]Θ1 ⊢ [Ω0′ ]A′ ▷ A1 → A2
Θ1 ⊢ [Θ1 ]A′ ▷ A′1 → A′2 ⊣ Θ2

PremiseBy Lemma E.17
By Lemma E.13
By Lemma E.17
By Lemma E.14
By above equalities
By Theorem 7.7

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

39:84♦♦♦♦♦

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers
Θ2 −→ Ω ′
Ω0′ −→ Ω ′A1 = [Ω ′]A′1
A2 = [Ω ′]A′2

Above
Above
Above
Above

[Ω]Γ ⊢ e2 : A3[Ω]Γ = [Ω]Ω
= [Ω ′]Ω ′= [Ω ′]Γ
= [Ω ′]Θ2[Ω ′]Θ2 ⊢ e2 : A3
Θ2 ⊢ e 2′ ⇒ A′3 ⊣ Θ3
Θ3 −→ Ω1′
Ω ′ −→ Ω1′
A3 = [Ω1′ ]A′3
⌊e2 ⌋ = ⌊e 2′ ⌋PremiseBy Lemma E.17
By Lemma E.13
By Lemma E.17
By Lemma E.14
By above equality
By i.h.
Above
Above
Above
Above

[Ω]Γ ⊢ A3 ≲ A1[Ω]Γ = [Ω]Ω
= [Ω1′ ]Ω1′
= [Ω1′ ]Γ
= [Ω1′ ]Θ3
A3 = [Ω1′ ]A′3
A1 = [Ω ′]A′1 = [Ω1′ ]A′1[Ω1′ ]Θ3 ⊢ [Ω1′ ]A′3 ≲ [Ω1′ ]A′1
Θ3 ⊢ [Θ3 ]A′3 ≲ [Θ3 ]A′1 ⊣ ∆[Θ3 ]A′1 = [Θ3 ]([Θ2 ]A1 )Θ2 ⊢ e 2′ ⇐ [Θ2 ]A′1 ⊣ ∆∆ −→ Ω2′Ω1′ −→ Ω2′Γ ⊢ e 1′ e 2′ ⇒ A′2 ⊣ ∆A2 = [Ω ′]A′2 = [Ω2′ ]A′2
Γ −→ Ω2′⌊e1 e2 ⌋ = ⌊e 1 ⌋ ⌊e 2 ⌋ = ⌊e 1′ ⌋ ⌊e 2′ ⌋ = ⌊e 1′ e 2′ ⌋PremiseBy Lemma E.17
By Lemma E.13
By Lemma E.17
By Lemma E.14
Above
By Lemma E.12
By above equalities
By Theorem 7.6
By Lemma E.5
By rule chk-sub
Above
Above
By rule inf-app
Lemma E.12
By Lemma E.3
By def. of erasure• Case[Ω]Γ, x : τ ⊢ e : Blam[Ω]Γ ⊢ λx. e : τ → B[Ω]Γ, x : τ ⊢ e : B[Ω]Γ, x : τ = [Ω, x : τ ](Γ, x : τ )[Ω, x : τ ](Γ, x : τ ) ⊢ e : B
Γ, x : τ ⊢ e ′ ⇒ B ′ ⊣ ∆ ′∆ ′ −→ Ω ′Ω, x : τ −→ Ω ′B = [Ω ′]B ′⌊e⌋ = ⌊e ′⌋Γ, x : τ −→ ∆ ′Given
By def. of context substitution
By above equality
By i.h.,
Above
Above
Above
Above
By Lemma G.2

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.

Consistent Subtyping for All

♦
♦
♦
♦
♦

39:85

∆ ′ = ∆, x : τ , Θ
Γ, x : τ ⊢ e ′ ⇒ B ′ ⊣ ∆, x : τ , ΘΓ ⊢ λx : τ . e ′ ⇒ τ → B ′ ⊣ ∆∆ −→ Ω ′Ω −→ Ω ′τ → B = τ → [Ω ′]B ′ = [Ω ′](τ → B ′ )⌊λx. e⌋ = λx . ⌊e⌋ = λx . ⌊e ′⌋ = ⌊λx : τ . e ′⌋By Lemma E.6
By above equality
By rule inf-lamann
By context extension
By context extension
By def. of substitution
By def. of erasure• Case[Ω]Γ, a ⊢ e : A
gen[Ω]Γ ⊢ e : ∀a. A

♦

♦
♦

♦
♦

[Ω]Γ, a ⊢ e : A[Ω]Γ, a = [Ω, a](Γ, a)[Ω, a](Γ, a) ⊢ e : A
Γ, a ⊢ e ′ ⇒ A′ ⊣ ∆ ′∆ ′ −→ Ω ′Ω, a −→ Ω ′A = [Ω ′]A′⌊e⌋ = ⌊e ′⌋Γ, a −→ ∆ ′∆ ′ = ∆, a, Θ
∆ −→ Ω ′Ω −→ Ω ′Γ, a ⊢ e ′ ⇒ A′ ⊣ ∆, a, Θ∆, a, Θ ⊢ [∆, a, Θ]A′ ≲ [∆, a, Θ]A′ ⊣ ∆, a, Θ
Γ, a ⊢ e ′ ⇐ A′ ⊣ ∆, a, ΘΓ ⊢ e ′ ⇐ ∀a. A′ ⊣ ∆Γ ⊢ e ′ : ∀a. A′ ⇒ ∀a. A′ ⊣ ∆∀a. A = ∀a.[Ω ′]A′ = [Ω ′](∀a. A′ )Given
By def. of context substitution
By above equality
By i.h.,
Above
Above
Above
Above
By Lemma G.2
By Lemma E.6
By context extension
By context extension
By above equality
By reflexivity of consistent subtyping
By rule chk-sub
By rule chk-gen
By rule inf-anno
By def. of substitution□

ACM Transactions on the Web, Vol. 9, No. 4, Article 39. Publication date: March 2010.