Consistent Subtyping for All
Ningning Xie , Xuan Bi, and Bruno C. d. S. Oliveira
The University of Hong Kong
{nnxie,xbi,bruno}@cs.hku.hk

Abstract. Consistent subtyping is employed in some gradual type systems to validate type conversions. The original definition by Siek andTaha serves as a guideline for designing gradual type systems with subtyping. Polymorphic types à 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 consistentsubtyping provides novel insights with respect 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 consistentsubtyping. We develop both declarative and (bidirectional) algorithmic
versions for the type system. We prove that the new calculus satisfies
all static aspects of the refined criteria for gradual typing, which aremechanically formalized using the Coq proof assistant.

1

Introduction

Gradual typing [21] is an increasingly popular topic in both programming language practice and theory. On the practical side there is a growing number ofprogramming languages adopting gradual typing. Those languages include Clojure [6], Python [27], TypeScript [5], Hack [26], and the addition of Dynamic toC# [4], to cite a few. On the theoretical side, recent years have seen a large bodyof research that defines the foundations of gradual typing [13, 8, 9], explores theiruse for both functional and object-oriented programming [21, 22], as well as its
applications to many other areas [24, 3].
A key concept in gradual type systems is consistency [21]. Consistency weakens type equality to allow for the presence of unknown types. In some gradualtype systems with subtyping, consistency is combined with subtyping to giverise to the notion of consistent subtyping [22]. Consistent subtyping is employed
by gradual type systems to validate type conversions arising from conventional
subtyping. One nice feature of consistent subtyping is that it is derivable fromthe more primitive notions of consistency and subtyping. As Siek and Taha [22]put it this shows that “gradual typing and subtyping are orthogonal and can be
combined in a principled fashion”. Thus consistent subtyping is often used as a
guideline for designing gradual type systems with subtyping.

2

Unfortunately, as noted by Garcia et al. [13], notions of consistency and/or
consistent subtyping “become more difficult to adapt as type systems get more
complex ”. In particular, for the case of type systems with subtyping, certain
kinds of subtyping do not fit well with the original definition of consistent subtyping by Siek and Taha [22]. One important case where such mismatch happens
is in type systems supporting implicit (higher-rank) polymorphism [18, 11]. It is
well-known that polymorphic types à la System F induce a subtyping relationthat relates polymorphic types to their instantiations [17, 16]. However Siek andTaha’s definition is not adequate for this kind of subtyping. Moreover the current
framework for Abstracting Gradual Typing (AGT) [13] also does not account forpolymorphism, with the authors acknowledging that this is one of the interesting
avenues for future work.
Existing work on gradual type systems with polymorphism does not use
consistent subtyping. The Polymorphic Blame Calculus (λB) [1] is an explicitly polymorphic calculus with explicit casts, which is often used as a target
language for gradual type systems with polymorphism. 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 is possible 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 andconversions are closer to implicit polymorphism. That is, in a conventional explicitly polymorphic calculus (such as System F), the primary notion is typeequality, where instantiation is not taken into account. Thus the types ∀a.a → a
and Int → Int are deemed incompatible. However in implicitly polymorphic calculi [18, 11] ∀a.a → a and Int → Int are deemed compatible, since the latter typeis an instantiation of the former. Therefore λB is in a sense a hybrid between
implicit and explicit polymorphism, utilizing type equality (à la System F) for
validating applications, and compatibility for validating casts.
An alternative approach to polymorphism has recently been proposed by
Igarashi et al. [14]. Like λB their calculus is explicitly polymorphic. However,in that work they employ type consistency to validate cast conversions, andforbid conversions from ∀a.a → a to Int → Int. This makes their casts closer
to explicit polymorphism, in contrast to λB. Nonetheless, there is still same
flavour of implicit polymorphism in their calculus when it comes to interactions
between dynamically typed and polymorphically typed code. For example, in
their calculus type consistency allows types such as ∀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 andconsistent 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 andTaha. The new definition of consistent subtyping can deal with polymorphism,
and preserves the orthogonality between consistency and subtyping. To slightly
rephrase Siek and Taha, the motto of our paper is that:

3

Gradual typing and polymorphism are orthogonal and can be combinedin a principled fashion.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), and that Igarashi et al.’s notion of typeconsistency 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 consistentsubtyping. The syntax-directed version of consistent subtyping is remarkably
simple and well-behaved, without the ad-hoc restriction operator [22]. Moreover, to further illustrate the generality 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 a (source-level) gradually typed
calculus for (predicative) implicit higher-rank 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 gradual typing,which is interesting for two reasons. On one hand, modern functional languages(such as Haskell) employ sophisticated type-inference algorithms that, aided bytype annotations, can deal with implicit higher-rank polymorphism. So a natural
question is how gradual typing can be integrated in such languages. On the other
hand, there is several existing work on integrating explicit polymorphism into
gradual typing [1, 14]. Yet no work investigates how to move such 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-rankpolymorphism. The new calculus brings the expressive power of full implicit
higher-rank polymorphic into a gradually typed source language. We prove that
our calculus satisfies all of the static aspects of the refined criteria for gradualtyping [25], while discussing some issues related with the dynamic guarantee.
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 and Taha, and can deal with polymorphism and top types.
• a syntax-directed version of consistent subtyping that is sound and complete with respect to our definition of consistent subtyping, but still
guesses polymorphic instantiations.
– Based on consistent subtyping, we present a declarative gradual type systemwith predicative implicit higher-rank polymorphism. We prove that our calculus satisfies the static aspects of the refined criteria for gradual typing [25],and is type-safe by a type-directed translation to λB, and thus hereditarily
preserves parametricity [2].
1Note here that we borrow Siek and Taha’s motto mostly to talk about the static
semantics. As Ahmed et al. [1] show there are several non-trivial interactions between
polymorphism and casts at the level of the dynamic semantics.

4

A <: BInt <: Int
B1 <: A1

Bool <: BoolA2 <: B2

A1 → A2 <: B1 → B2

Float <: Float

Int <: Float][li : Aii∈1...n+m ] <: [li : Ai∈1...ni? <: ?

A∼B
A∼A

A∼?

?∼A

A1 ∼ B1

Ai ∼ BiA2 ∼ B2

A1 → A2 ∼ B1 → B2

[li : Ai ] ∼ [li : Bi ]Fig. 1: Subtyping and type consistency in FOb?<:– We present a complete and sound bidirectional algorithm for implementing
the declarative system based on the design principle of Garcia and Cimini[12] and the approach of Dunfield and Krishnaswami [11].
– All of the metatheory of this paper, except some manual proofs for thealgorithmic type system, has been mechanically formalized in Coq2 .

2Background and Motivation

In this section we review a simple gradually typed language with objects [22],to introduce the concept of consistency subtyping. We also briefly talk about
the Odersky-Läufer type system for higher-rank types [17], which serves as theoriginal language on which our gradually typed calculus with implicit higherrank polymorphism is based.
2.1

Gradual Subtyping

Siek and Taha [22] developed a gradual typed 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 involvethe 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 the unknown type ? is neutral to subtyping, with only ? <: ?.
Both relations are found in Fig. 1.
A primary contribution of their work is to show that consistency and subtyping are orthogonal. To compose subtyping and consistency, Siek and Tahadefined consistent subtyping (written .) in two equivalent ways:
2

All supplementary materials are available at https://bitbucket.org/xieningning/
consistent-subtyping

5

Definition 1 (Consistent Subtyping à la Siek and Taha [22]).
– A . B if and only if A ∼ C and C <: B for some C.
– A . B if and only if A <: C and C ∼ B for some C.
Both definitions are non-deterministic because of the intermediate type C. To
remove non-determinism, they proposed a so-called restriction operator, written
A|B that masks off the parts of a type A that are unknown in a type B.
A|B = case A, B of | (−, ?) ⇒ ?
| A1 → A2 , B1 → B2 = A1 |B1 → A2 |B2| [l1 : A1 , ..., ln : An ], [l1 : B1 , ..., lm : Bm ] if n ≤ m ⇒ [l1 : A1 |B1 , ..., ln : An |Bn ]| [l1 : A1 , ..., ln : An ], [l1 : B1 , ..., lm : Bm ] if n > m ⇒[l1 : A1 |B1 , ..., lm : Am |Bm , ..., ln : An ]| otherwise ⇒ A

With the restriction operator, consistent subtyping is simply defined as A . B ≡A|B <: B|A . Then they proved that this definition is equivalent to Definition 1.
2.2

The Odersky-Lä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 Läufer [17].
One difference is that, for simplicity, we do not account for a let expression,as there is already existing work about gradual type systems with let expressions and let generalization (for example, see Garcia and Cimini [12]). Similar
techniques can be applied to our calculus to enable let generalization.
The syntax of the type system, along with the typing and subtyping judgments is given in Fig. 2. An implicit assumption throughout the paper is thatvariables in contexts are distinct. We save the explanations for the static semantics to Section 4, where we present our gradually typed version of the calculus.
2.3

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 fine-grained control over the static-todynamic spectrum, i.e., a program can be evolved by introducing more or lessprecise types as needed [13].
Haskell is a language that supports implicit higher-rank polymorphism, but
no gradual typing. Therefore some programs that are safe at run-time may berejected due to the conservativity of the type system. For example, consider thefollowing Haskell program adapted from Peyton Jones et al. [18]:foo :: ([Int], [Char])foo = let f x = (x [1, 2] , x [0 a0 , 0 b0 ]) in f reverse

6
Expressions
e ::= x | n | λx : A. e | λx. e | e e
TypesA, B ::= Int | a | A → B | ∀a.A
Monotypes τ, σ ::= Int | a | τ → σContexts
Ψ ::= ∅ | Ψ, x : A | Ψ, a
Ψ `OL e : A
Ψ, x : A `OL e : B

x:A∈Ψ
Ψ`

OL

x:A

Var

OL

Ψ`

Ψ `OL e1 : A1 → A2
OL

Ψ`

Nat

n : IntΨ `OL λx : A. e : A → B
Ψ `OL e : A1

Ψ `OL e2 : A1App

e1 e2 : A2

Ψ`Ψ, x : τ `OL e : BΨ `OL λx. e : τ → B

LamAnnΨ ` A1 <: A2OL

Sube : A2Ψ, a `OL e : A
LamΨ `OL e : ∀a.AGen

Ψ ` A <: B
a∈Ψ

Ψ `τ

Ψ ` a <: aCS-TVarΨ ` Int <: Int

Ψ , a ` A <: BΨ ` A <: ∀a.B

CS-IntΨ ` B1 <: A1
ForallRΨ ` A[a 7→ τ ] <: B
ForallLΨ ` ∀a.A <: BΨ ` A2 <: B2

Ψ ` A1 → A2 <: B1 → B2

CS-FunFig. 2: Syntax and static semantics of the Odersky-Läufer type system.

This program is rejected by Haskell’s type checker because Haskell implements
the Damas-Milner 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. Instead of rejecting the program outright, due tomissing type annotations, gradual typing provides a simple alternative by giving
x the unknown type (denoted ?). With such typing the same program type-checks
and produces ([2, 1], [0 b0 , 0 a0 ]). By running the program, programmers can gain
some additional insight about the run-time behaviour. Then, with such insight,
they can also give x a more precise type (∀a.[a] → [a]) a posteriori so thatthe program continues to type-check via implicit polymorphism and also grants
more static safety. In this paper, we envision such a language that combines thebenefits of both implicit higher-rank polymorphism and gradual typing.

3

Revisiting Consistent Subtyping

In this section we explore the design space of consistent subtyping. We startwith the definitions of consistency and subtyping for polymorphic types, and

7
Types
A, B ::= Int | a | A → B | ∀a.A | ?
Monotypes τ, σ ::= Int | a | τ → σContexts
Ψ ::= ∅ | Ψ, x : A | Ψ, a
A∼B
A∼A

A∼?

A1 ∼ B1?∼A

A2 ∼ B2A∼B

A1 → A2 ∼ B1 → B2

∀a.A ∼ ∀a.BΨ ` A <: B
Ψ , a ` A <: BΨ ` A <: ∀a.BΨ `τS-ForallRΨ ` A[a 7→ τ ] <: B
Ψ ` ∀a.A <: BΨ ` B1 <: A1
Ψ ` Int <: Int

S-Int

a∈Ψ
S-ForallLΨ ` a <: aS-TVarΨ ` A2 <: B2

Ψ ` A1 → A2 <: B1 → B2

S-Fun

Ψ ` ? <: ?

S-Unknown

Fig. 3: Syntax of types, consistency, and subtyping in the declarative system.

compare with some relevant work. We then discuss the design decisions involved
towards our new definition of consistent subtyping, and justify the new definition
by demonstrating its equivalence with that of Siek and Taha [22] and the AGT
approach [13] on simple types.
The syntax of types is given at the top of Fig. 3. 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 for the purpose of illustration. Note that 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 of type variable declarations and term variables.
3.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. [1] and type consistency by Igarashi et al. [14].
Consistency. The key observation here is that consistency is mostly a structural
relation, except that the unknown type ? can be regarded as any type. Following
this observation, we naturally extend the definition from Fig. 1 with polymorphic
types, as shown at the middle of Fig. 3. 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 generalizationof another by means of the subtyping judgment Ψ ` A <: B. Compared withthe subtyping rules of Odersky and Läufer [17] in Fig. 2, the only addition is8the neutral subtyping of ?. Notice that, in the rule S-ForallL, the universal
quantifier is only allowed to be instantiated with a monotype. The judgmentΨ ` τ checks all the type variables in τ are bound in the context Ψ . For spacereasons, we omit the definition. According to the syntax in Fig. 3, monotypes
do not include the unknown type ?. This is because if we were to allow theunknown 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 oftype ∀a.a → a to a function where the input type is supposed to be Int →Bool. However, as we might expect, ∀a.a → a is definitely not compatible with
Int → Bool. This does not hold in any polymorphic type systems without gradualtyping. So the gradual type system should not accept it either. (This is the socalled conservative extension property that will be made precise in Section 4.3.)
Importantly there is a subtle but crucial distinction between a type variable
and the unknown type, although they all 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 with any type,and additional type-checks have to be performed at runtime. On the other hand,a type variable 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 [1], the compatibility relation for polymorphic types is defined as follows:
A≺B
Comp-AllRA ≺ ∀X.B

A[X 7→ ?] ≺ BComp-AllL∀X.A ≺ B

Notice that, in rule Comp-AllL, the universal quantifier is always instantiatedto ?. However, this way, λ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. [14] 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 follows3 :A∼B∀a.A ∼ ∀a.B

A∼B

B 6= ∀a.B 0? ∈ Types(B)∀a.A ∼ B

Compared with our consistency definition in Fig. 3, their first rule is the sameas ours. The second rule says that a non ∀-type can be consistent with a ∀-typeonly if it contains ?. In this way, their type system is able to reject ∀a.a → a ∼3This is a simplified version.

9
∼

⊥

(? → Int) → Int<:

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

∼

∼

<:

(∀a.? → Int) → Int

Int → ?
<:

∀a.a

∼

(a)

⊥

(b)
⊥

∼

(((? → Int) → Int) → Bool) → (Int → ?)<:<:(((∀a.a → Int) → Int) → Bool) → (∀a.a)

∼

⊥

(c)

Fig. 4: Examples that break the original definition of consistent subtyping.

Int → Bool. However, in order to keep conservativity, they also reject ∀a.a → a ∼Int → Int, which is perfectly sensible in their setting (i.e., 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 andpolymorphically typed terms, both relations allow ∀a.a → Int to be related with
? → Int for example, which in our view, is some sort of (implicit) polymorphic
subtyping combined with type consistency, and that should be derivable by themore primitive notions in the type system (instead of inventing new relations).
One of our design principles is that subtyping and consistency is orthogonal, andcan be naturally superimposed, echoing the same opinion of Siek and Taha [22].
3.2

Towards Consistent Subtyping

With the definitions of consistency and subtyping, the question now is how tocompose these two relations so that two types can be compared in a way thattakes these two relations into account.
Unfortunately, the original definition of Siek and Taha (Definition 1) 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 way (first by applying consistency,
then subtyping), but not the other way, as shown in Fig. 4a. We use ⊥ to meanthat 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. 4b.
What is worse, if those two examples are composed in a way that those types
all appear co-variantly, then the resulting types cannot reach each other in either
way. For example, Fig. 4c shows such two types by putting a Bool type in the
middle, and neither definition of consistent subtyping works.

10
T1
<:
B

∼
.
∼

C

A
.

<:
T2

.

<:
T1

.

<:

<:

C

A
(a)

∼

∼

B
<:
T2

(b)

Fig. 5: Observations of consistent subtyping

Observations on Consistent Subtyping Based on Information Propagation. In
order to develop the 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 consistent subtyping 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 consistent subtyping is nottransitive because information can only be lost once (otherwise, any two types
are a consistent subtype of each other). Now consider a situation where we haveboth A <: B, and B . 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. 5a. A symmetrical observation is given in Fig. 5b:
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. 5a, 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 reachC through the original definition. A similar problem is shown in Fig. 5b.
However, it turns out that those two problems can be fixed using the same
strategy: instead of taking one-step subtyping and one-step consistency, our definition of consistent subtyping allows types to take one-step subtyping, one-step
consistency, and one more step subtyping. Specifically, A <: B ∼ T2 <: C (inFig. 5a) and C <: T1 ∼ B <: A (in Fig. 5b) have the same relation chain:subtyping, consistency, and subtyping.

11

A2

∼

<:
A1

A3

A2 = ((∀a.a → Int) → Int) → Bool) → (Int → Int)<:.

A1 = (((∀a.a → Int) → Int) → Bool) → (∀a.a)A4

A3 = ((∀a.? → Int) → Int) → Bool) → (Int → ?)A4 = (((? → Int) → Int) → Bool) → (Int → ?)Fig. 6: Example that is fixed by the new definition of consistent subtyping.

Definition of Consistent subtyping. From the above discussion, we are ready tomodify Definition 1, and adapt it to our notation:
Definition 2 (Consistent Subtyping).
Ψ ` A <: CC∼DΨ `A.BΨ ` D <: B

With Definition 2, Figure 6 illustrates the correct relation chain for the broken
example shown in Fig. 4c. At first sight, Definition 2 seems worse than the original: we need to guess two types! It turns out that Definition 2 is a generalizationof Definition 1, and they are equivalent in the system of Siek and Taha [22].
However, more generally, Definition 2 is compatible with polymorphic types.
Proposition 1 (Generalization of Consistent Subtyping).
– Definition 2 subsumes Definition 1.
– Definition 1 is equivalent to Definition 2 in the system of Siek and Taha.
3.3

Abstracting Gradual Typing

Garcia et al. [13] 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 of static 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 to their approach is the so-called concretization function. For simple types, a concretization
γ from gradual types to a set of static types4 is defined as follows:
Definition 3 (Concretization).
γ(Int) = {Int}γ(A → B) = γ(A) → γ(B)

γ(?) = {All static types}

Based on the concretization function, subtyping between static types can belifted to gradual types, resulting in the consistent subtyping relation:
f: B if and only if A1 <:Definition 4 (Consistent Subtyping in AGT). A <B1 for some A1 ∈ γ(A), B1 ∈ γ(B).
4For simplification, we directly regard type constructor → as a set-level operator.

12

Later they proved that this definition of consistent subtyping coincides withthat of Siek and Taha [22] (Definition 1). By Proposition 1, we can directly
conclude that our definition coincides with AGT:
f: B.
Proposition 2 (Equivalence to AGT on Simple Types). A . B iff A <However, AGT does not show how to deal with polymorphism (e.g. the interpretation of type variables) yet. Still, as noted by Garcia et al. [13], it is apromising 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 [7], where the static types A1 , B1 in Definition 4 can bealgorithmically computed by also accounting for top and bottom types.
3.4

Directed Consistency

Directed consistency [15] is defined in terms of precision and static subtyping:A0 v A

A <: B
A0 . B 0

B0 v BThe judgment A v B is read “A is less precise than B”. In their setting, precision
is defined for type constructors and subtyping for static types. If we interpret
this definition from AGT’s point of view, finding a more precise static type5
has the same effect as concretization. Namely, A0 v A implies A ∈ γ(A0 ) andB 0 v B implies B ∈ γ(B 0 ). Therefore we consider this definition as AGT-style.
From this perspective, this definition naturally coincides with Definition 2.
The value of their definition is that consistent subtyping is derived compositionally from static subtyping and precision. These are two more atomic relations.
At first sight, their definition looks very similar to Definition 2 (replacing v by<: and <: by ∼). Then a question arises as to which one is more fundamental. To
answer this, we need to discuss the relation between consistency and precision.
Relating Consistency and Precision. Precision is a partial order (anti-symmetricand transitive), while consistency is symmetric but not transitive. Nonetheless,precision and consistency are related by the following proposition:
Proposition 3 (Consistency and Precision).
– If A ∼ B, then there exists (static) C, such that A v C, and B v C.
– If for some (static) C, we have A v C, and B v C, then we have A ∼ B.
It may seem that precision is a more atomic relation, since consistency can bederived from precision. However, recall that consistency is in fact an equivalence
relation lifted from static types to gradual types. Therefore defining consistency
independently is straightforward, and it is theoretically viable to validate the5

The definition of precision of types is given in appendix.

13

definition of consistency directly. On the other hand, precision is usually connected with the gradual criteria [25], and finding a correct partial order thatadheres to the criteria is not always an easy task. For example, Igarashi et al.
[14] argued that term precision for System FG is actually nontrivial, leaving
the gradual guarantee of the semantics as a conjecture. Thus precision can bedifficult to extend to more sophisticated type systems, e.g. dependent types.
Still, it is interesting that those two definitions illustrate the correspondenceof different foundations (on simple types): one is defined directly on gradualtypes, and the other stems from AGT, which is based on static subtyping.
3.5

Consistent Subtyping Without Existentials

Definition 2 serves as a fine specification of how consistent subtyping should
behave in general. But it is inherently non-deterministic because of the twointermediate types C and D. As with Definition 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 therestriction operator to account for polymorphic types. The original restriction
operator is structural, meaning that it works for types of similar structures. But
for polymorphic types, two input types could have different structures due touniversal quantifiers, e.g, ∀a.a → Int and (Int → ?) → Int. If we try to mask
the first type using the second, it seems hard to maintain the information thata should be instantiated to a function while ensuring that the return type ismasked. There seems to be no satisfactory way to extend 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 backand revisit what the restriction operator actually does. For consistent subtyping,two input types could have unknown types in different positions, but we only
care about the known parts. What the restriction operator does is (1) erase thetype 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 we compare the types in boxes directly instead of through thelens of the restriction operator, we can observe that the consistent subtyping

14Ψ `A.BΨ, a ` A . B
Ψ ` A . ∀a.BΨ ` B1 . A1

Ψ `τCS-ForallRΨ `?.A

CS-ForallLΨ ` ∀a.A . B

Ψ ` A2 . B2

Ψ ` A1 → A2 . B1 → B2

Ψ ` A[a 7→ τ ] . Ba∈ΨCS-FunCS-UnknownLΨ `a.aCS-TVarΨ `A.?

Ψ ` Int . Int

CS-Int

CS-UnknownR

Fig. 7: Consistent Subtyping for implicit polymorphism.

relation always holds between the unknown type and an arbitrary type. We caninterpret this observation directly from Definition 2: the unknown type is neutral
to subtyping (? <: ?), the unknown type is consistent with any type (? ∼ A),
and subtyping is reflexive (A <: A). Therefore, the unknown type is a consistentsubtype of any type (? . A), and vice versa (A . ?). Note that this interpretation provides a general recipe on how to lift 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 consistent subtyping relation directly, without resorting to subtyping
or consistency at all. The key idea is that we replace <: with . in Fig. 3, get
rid of rule S-Unknown and add two extra rules concerning ?, resulting in therules of consistent subtyping in Fig. 7. Of particular interest are the rules CSUnknownL and CS-UnknownR, both of which correspond to what we just
said: the unknown type is a consistent subtype of any type, and vice versa.
From now on, we use the symbol . to refer to the consistent subtyping relationin Fig. 7. What is more, we can prove that those two are equivalent6 :T heorem 1 Ψ ` A . B ⇔ Ψ ` A <: C, C ∼ D, Ψ ` D <: B for some C, D.

4

Gradually Typed Implicit Polymorphism

In Section 3 we introduced the consistent subtyping relation that accommodates
polymorphic types. In this section we continue with the development by giving adeclarative type system for predicative implicit polymorphism that employs theconsistent subtyping relation. The declarative system itself is already quite interesting as it is equipped with both higher-rank polymorphism and the unknown
type. The syntax of expressions in the declarative system is given below:
Expressions
6

e ::= x | n | λx : A. e | λx. e | e e

Theorems with T are those proved in Coq. The same applies to Lemmas.

15Ψ `e:As
Ψ, a ` e : Ax:A∈ΨΨ `x:AxVarΨ ` n : Int

Ψ, x : A ` e : BΨ ` λx : A. e : A → BΨ ` e1 : A

s1

n

Nat

s
λx : A. s

LamAnnΨ ` A . A1 → A2

Ψ ` e1 e2 : A2s

Ψ ` e : ∀a.AΛa.s

Ψ, x : τ ` e : BsΨ ` λx. e : τ → B
Ψ ` e2 : A3

s2

Gen

λx : τ. sLam

Ψ ` A3 . A1

(hA ,→ A1 → A2 i s1 ) (hA3 ,→ A1 i s2 )AppΨ ` A . A1 → A2Ψ `τΨ ` A[a 7→ τ ] . A1 → A2Ψ ` ∀a.A . A1 → A2

Ψ ` (A1 → A2 ) . (A1 → A2 )M-Arr

M-ForallΨ `?.?→?

M-Unknown

Fig. 8: Declarative typing

4.1

Typing in Detail

Figure 8 gives the typing rules for our declarative system (the reader is advised toignore the gray-shaded parts for now). Rule Var extracts the type of the variablefrom the typing context. Rule Nat 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 type checking the
body e. Gradual types and polymorphic types are introduced via annotations
explicitly. Rule Gen puts a fresh type variable a into the type context andgeneralizes the typing result A to ∀a.A. Rule App first infers the type of e1 ,then the matching judgment Ψ ` A . A1 → A2 extracts the domain type A1 andthe codomain type A2 from type A. The type A3 of the argument e2 is thencompared with A1 using the consistent subtyping judgment.
Matching. The matching judgment of Siek et al. [25] can be extended to polymorphic types naturally, resulting in Ψ ` A . A1 → A2 . In M-Forall, a monotype
τ is guessed to instantiate the universal quantifier a. This rule is inspired by theapplication judgment Φ ` A • e ⇒ C [11], which says that if we apply a term oftype A to an argument e, we get something of type C. If A is a polymorphic type,the judgment works by guessing instantiations until it reaches an arrow type.
Matching further simplifies the application judgment, since it is independent of
typing. Rule M-Arr and M-Unknown are the same as Siek et al. [25]. M-Arr
returns the domain type A1 and range type A2 as expected. If the input is ?,then M-Unknown returns ? as both the type for the domain and the range.

16

Note that matching saves us from having a subsumption rule (Sub in Fig. 2).
the subsumption rule is incompatible with consistent subtyping, since the latter
is not transitive. A discussion of a subsumption rule based on normal subtyping
can be found in the appendix.
4.2

Type-directed Translation

We give the dynamic semantics of our language by translating it to λB. Below
we show a subset of the terms in λB that are used in the translation:
Terms s ::= x | n | λx : A. s | Λa.s | s1 s2 | hA ,→ Bi s
A cast hA ,→ Bi s converts the value of term s from type A to type B. A castfrom A to B is permitted only if the types are compatible, written A ≺ B, as
briefly mentioned in Section 3.1. The syntax of types in λB is the same as ours.
The translation is given in the gray-shaded parts in Fig. 8. The only interesting case here is to insert explicit casts in the application rule. Note that there
is no need to translate matching or consistent subtyping, instead we insert thesource and target types of a cast directly in the translated expressions, thanks
to the following two lemmas:
Lemma 1 (. to ≺) If Ψ ` A . A1 → A2 , then A ≺ A1 → A2 .
Lemma 2 (. to ≺) If Ψ ` A . B, then A ≺ B.
In order to show the correctness of the translation, we prove that our translation always produces well-typed expressions in λB. By Lemmas 1 and 2, wehave the following theorem:
T heorem 2 (Type Safety) If Ψ ` e : As, then Ψ `B s : A.

Parametricity. An important semantic property of polymorphic types is relational parametricity [19]. The parametricity property says that all instances of apolymorphic function should behave uniformly. A classic example is a function
with the type ∀a.a → a. The parametricity property guarantees that a valueof 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 theunknown type ?, careful measures are to be taken to ensure parametricity. Thisis exactly the circumstance that λB was designed to address. Ahmed et al. [2]proved that λB satisfies relational parametricity. Based on their result, and by
T heorem 2, parametricity is preserved in our system.
Ambiguity from Casts. The translation does not always produce a unique target
expression. This is because when we guess a monotype τ in rule M-Foralland CS-ForallL, we could have different choices, which inevitably leads todifferent types. Unlike (non-gradual) polymorphic type systems [18, 11], thechoice of monotypes could affect runtime behaviour of the translated programs,
since they could appear inside the explicit casts. For example, the following shows

17

two possible translations for the same source expression λx : ?. f x, where thetype of f is instantiated to Int → Int and Bool → Bool, respectively:f : ∀a.a → a ` (λx : ?. f x) : ? → Int(λx : ?. (h∀a.a → a ,→ Int → Inti f ) ( h? ,→ Inti x))
f : ∀a.a → a ` (λx : ?. f x) : ? → Bool
(λx : ?. (h∀a.a → a ,→ Bool → Booli f ) ( h? ,→ Booli x))

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 casterror (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 any
instantiation of a would be put inside 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 notmatch the guessed type. Note that this does not compromise the type safety ofthe translated expressions, since cast errors are part of the type safety guarantees.
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 the same meaning [20]. We argue that thedeclarative 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 the above example,
whatever the translation might be, applying λx : ?. f x to 3 either results in acast error, or produces 3, nothing else.
This discrepancy is due to the guessing nature of the declarative system. As
far as the declarative system is concerned, both Int → Int and Bool → Boolare equally acceptable. But this is not the case at runtime. The acute reader
may have found that the only appropriate choice is to instantiate f to ? → ?.
However, as specified by rule M-Forall in Fig. 8, we can only instantiate typevariables to monotypes, but ? is not a monotype! We will get back to this issue inSection 6.2 after we present the corresponding algorithmic system in Section 5.
4.3

Correctness Criteria

Siek et al. [25] present a set of properties that a well-designed gradual typing
calculus must have, which they call the refined criteria. Among all the criteria,
those related to the static aspects of gradual typing are well summarized by Cimini and Siek [8]. Here we review those criteria and adapt them to our notation.
We have proved in Coq that our type system satisfies all these criteria.
Lemma 3 (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

18– Monotonicity w.r.t. precision: for all Ψ, e, e0 , A, if Ψ ` e : A, and e0 v e,then Ψ ` e0 : B, and B v A for some B.
– Type Preservation of cast insertion: for all Ψ, e, A, if Ψ ` e : A, thenΨ `e:As, and Ψ `B s : A for some s.
– Monotonicity of cast insertion: for all Ψ, e1 , e2 , e01 , e02 , A, if Ψ ` e1 :A
e01 , and Ψ ` e2 : A
e02 , and e1 v e2 , then Ψ p Ψ ` e01 vB e02 .
The first criterion states that the gradual type system should be a conservative extension of the original system. In other words, a static program that is
typeable in the Odersky-Läufer type system if and only if it is typeable in thegradual type system. A static program is one that does not contain any type ?7 .
However since our gradual type system does not have the subsumption rule, it
produces more general types.
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 v B, which is given in the appendix. 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 v e2 means that e1
and e2 are the same program except that e2 has more unknown types.
The first two criteria are fundamental to gradual typing. They explain for example why these two programs (λx : Int. x + 1) and (λx : ?. x + 1) are typeable,
as the former is typeable in the Odersky-Läufer type system and the latter is aless-precise version of it.
The last two criteria relate the compilation to the cast calculus. The third
criterion is essentially the same as T heorem 2, given that a target expression
should always exist, which can be easily seen from Fig. 8. The last criterion
ensures that the translation must be monotonic over the precision relation v.
As for the dynamic guarantee, things become a bit murky for two reasons: (1)as we discussed before, our declarative system is incoherent in that the runtime
behaviour of the same source program can vary depending on the particulartranslation; (2) it is still unknown whether dynamic guarantee holds in λB. We
will have more discussion on the dynamic guarantee in Section 6.3.

5Algorithmic 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 thealgorithmic bidirectional system of Dunfield and Krishnaswami [11] (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 [12]. We
then prove that our algorithm is both sound and complete with respect to thedeclarative type system. Full proofs can be found in the appendix.
7

Note that the term static has appeared several times with different meanings.

19
Expressions
e ::= x | n | λx : A. e | λx. e | e e | e : A
Types
A, B ::= Int | a | b
a | A → B | ∀a.A | ?
Monotypes
τ, σ ::= Int | a | b
a|τ →σContexts
Γ, ∆, Θ ::= ∅ | Γ, x : A | Γ, a | Γ, b
a | Γ, ba=τComplete ContextsΩ ::= ∅ | Ω, x : A | Ω, a | Ω, b
a=τFig. 9: Syntax of the algorithmic systemΓ `A.Ba∆Γ [a] ` a . a a Γ [a]Γ ` Int . Int a Γ

ACS-Int

ACS-TVarΓ [ba] ` ba.ba a Γ [ba]

Γ `?.AaΓΓ ` B1 . A1 a Θ

ACS-UnknownL

Γ, a ` A . B a ∆, a, Θba∈/ fv (A)ACS-ForallRΓ [ba] ` ba/Aa∆Γ [ba] ` ba.Aa∆

Γ `A.?aΓACS-UnknownRΘ ` [Θ]A2 . [Θ]B2 a ∆Γ ` A1 → A2 . B1 → B2 a ∆Γ ` A . ∀a.B a ∆ACS-ExVar

ACS-InstL

ACS-FunΓ, ba ` A[a 7→ ba] . B a ∆Γ ` ∀a.A . B a ∆ba∈/ fv (A)ACS-ForallLΓ [ba] ` A / b
aa∆

Γ [b
a] ` A . baa∆

ACS-InstR

Fig. 10: Algorithmic consistent subtyping

Algorithmic Contexts. The algorithmic context Γ is an ordered list containing
declarations of type variables a and term variables x : A. Unlike declarative contexts, algorithmic contexts also contain declarations of existential type variablesba, which can be either unsolved (written ba) or solved to some monotype (written b
a = τ ). Complete contexts Ω are those that contain no unsolved existential
type variables. Figure 9 shows the syntax of the algorithmic system. Apart fromexpressions in the declarative system, we have annotated expressions e : A.
5.1

Algorithmic Consistent Subtyping and Instantiation

Figure 10 shows the algorithmic consistent subtyping rules. The first five rules
do not manipulate contexts. Rule ACS-Fun is a natural extension of its declarative counterpart. The output context of the first premise is used by the second
premise, and the output context of the second premise is the output context
of the conclusion. Note that we do not simply check A2 . B2 , but apply Θ toboth types (e.g., [Θ]A2 ). This is to maintain an important invariant that types
are fully applied under input context Γ (they contain no existential variables
already solved in Γ ). The same invariant applies to every algorithmic judgment.

20

Γ `b
a/Aa∆
Γ `τ
0

Γ, b
a, Γ ` ba / τ a Γ, b
a = τ, Γ 0Γ [ba] ` ba / ? a Γ [ba]InstLSolveInstLSolveUΓ [ba2 , b
a1 , ba=ba1 → ba2 ] ` A1 / b
a1 a Θ

Γ [ba][bb] ` ba/b
b a Γ [b
a][b
b=b
a]
Γ [b
a], b ` b
a / B a ∆, b, ∆0Γ [ba] ` ba / ∀b.B a ∆Θ`ba2 / [Θ]A2 a ∆Γ [ba] ` ba / A1 → A2 a ∆InstLReach

InstLAllRInstLArr

Fig. 11: Algorithmic instantiation

Rule ACS-ForallR looks similar to its declarative counterpart, except that
we need to drop the trailing context a, Θ from the concluding output context
since they become out of scope. Rule ACS-ForallL generates a fresh existential variable ba, and replaces a with b
a in the body A. The new existential variableb
a is then added to the premise’s input context. As a side note, when both types
are quantifiers, then either ACS-ForallR or ACS-ForallR could be tried.
In practice, one can apply ACS-ForallR eagerly. The last two rules together
check consistent subtyping with an unsolved existential variable on one side andan arbitrary type on the other side by the help of the instantiation judgment.
The judgment Γ ` b
a / A a ∆ defined in Fig. 11 instantiates unsolved existential variables. Judgment b
a / A reads “instantiate b
a to a consistent subtypeof A”. For space reasons, we omit its symmetric judgement Γ ` A / ba a ∆. Ruleb
InstLSolve and rule InstLReach set b
a to τ and b in the output context, respectively. Rule InstLSolveU is similar to ACS-UnknownR in that we put noconstraint on ba when it meets the unknown type ?. This design decision reflects
the point that type inference only produces static types [12]. We will get backto this point in Section 6.2. Rule InstLAllR is the instantiation version of rule
ACS-ForallR. The last rule InstLArr applies when ba meets a function type.
It follows that the solution must also be a function type. That is why, in the firstpremise, we generate two fresh existential variables b
a1 and b
a2 , and insert them
just before b
a in the input context, so that the solution of ba can mention them.
Note that A1 / b
a1 switches to the other instantiation judgment.
5.2

Algorithmic Typing

We now turn to the algorithmic typing rules in Fig. 12. The algorithmic system uses bidirectional type checking to accommodate polymorphism. Most ofthem are quite standard. Perhaps rule AApp (which differs significantly fromthat in the DK system) deserves attention. It relies on the algorithmic matching judgment Γ ` A . A1 → A2 a ∆. Rule AM-ForallL replaces a with a21Γ `e⇒Aa∆(x : A) ∈ ΓΓ `x⇒AaΓAVarΓ ` n ⇒ Int a ΓΓ, x : A ` e ⇒ B a ∆, x : A, Θ

Γ, b
a, b
b, x : ba`e⇐bb a ∆, x : b
a, Θ
ALamU
b
Γ ` λx. e ⇒ b
a→ba∆
Γ `A

Γ ` λx : A. e ⇒ A → B a ∆ALamAnnAΓ `e⇐Aa∆AAnnoΓ `e:A⇒Aa∆Γ ` e1 ⇒ A a Θ1ANat

Θ1 ` [Θ1 ]A . A1 → A2 a Θ2

Θ2 ` e2 ⇐ [Θ2 ]A1 a ∆AAppΓ ` e1 e2 ⇒ A2 a ∆Γ `e⇐Aa∆Γ, x : A ` e ⇐ B a ∆, x : A, ΘΓ ` λx. e ⇐ A → B a ∆Γ `e⇒AaΘΓ, a ` e ⇐ A a ∆, a, ΘALam

Γ ` e ⇐ ∀a.A a ∆AGenΘ ` [Θ]A . [Θ]B a ∆Γ `e⇐Ba∆ASubΓ ` A . A1 → A2 a ∆Γ, ba ` A[a 7→ ba] . A1 → A2 a ∆Γ ` ∀a.A . A1 → A2 a ∆Γ `?.?→?aΓ

AM-Forall

AM-UnknownΓ ` (A1 → A2 ) . (A1 → A2 ) a ΓΓ [bc] ` bc.ba→bb a Γ [b
a, b
b, b
c=b
a→b
b]

AM-Arr

AM-VarFig. 12: Algorithmic typing

fresh existential variable ba, thus eliminating guessing. Rule AM-Arr and AMUnknown correspond directly to the declarative rules. Rule AM-Var, which
has no corresponding declarative version, is similar to InstRArr/InstLArr:
we create ba and bb and add b
c=b
a → bb to the context.
5.3

Completeness and Soundness

We prove that the algorithmic rules are sound and complete with respect to thedeclarative specifications. We need an auxiliary judgment Γ −→ ∆ that captures
a notion of information increase from input contexts Γ to output contexts ∆ [11].
Soundness. Roughly speaking, soundness of the algorithmic system says thatgiven an expression e that type checks in the algorithmic system, there exists a22

corresponding expression e0 that type checks in the declarative system. However
there is one complication: e does not necessarily have more annotations than e0 .
For example, by ALam we have λx. x ⇐ (∀a.a) → (∀a.a), but λx. x itself cannot
have type (∀a.a) → (∀a.a) in the declarative system. To circumvent that, we add
an annotation to the lambda abstraction, resulting in λx : (∀a.a). x, which is
typeable in the declarative system with the same type. To relate λx. x andλx : (∀a.a). x, we erase all annotations on both expressions. The definition oferasure b·c is standard and thus omitted.
Theorem 1 (Soundness of Algorithmic Typing) Given ∆ −→ Ω,
1. If Γ ` e ⇒ A a ∆ then ∃e0 such that [Ω]∆ ` e0 : [Ω]A and bec = be0 c.
2. If Γ ` e ⇐ A a ∆ then ∃e0 such that [Ω]∆ ` e0 : [Ω]A and bec = be0 c.
Completeness. Completeness of the algorithmic system is the reverse of soundness: given a declarative judgment of the form [Ω]Γ ` [Ω] . . . , we want to getan algorithmic derivation of Γ ` · · · a ∆. It turns out that completeness 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 Ω 0 that extends both the output context ∆, and the given complete
context Ω. As with soundness, we need erasure to relate both expressions.
Theorem 2 (Completeness of Algorithmic Typing) Given Γ −→ Ω andΓ ` A, if [Ω]Γ ` e : A then there exist ∆, Ω 0 , A0 and e0 such that ∆ −→ Ω 0 andΩ −→ Ω 0 and Γ ` e0 ⇒ A0 a ∆ and A = [Ω 0 ]A0 and bec = be0 c.

6Discussion

6.1

Top Types

To demonstrate that our definition of consistent subtyping (Definition 2) is applicable to other features, we show how to extend our approach to Top types
with all the desired properties preserved.
In order to preserve the orthogonality between subtyping and consistency,
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 therequirement A static, the rule seems reasonable. However, an important pointis 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 the rule that> is consistent with >, which is actually included in the original reflexive ruleA ∼ A. For consistent subtyping, every type is a consistent subtype of >, forexample, Int → ? . >.
A static
S-TopΨ ` A <: >>∼>Ψ `A.>

CS-Top23

It is easy to verify that Definition 2 is still equivalent to that in Fig. 7 extended
with rule CS-Top. That is, T heorem 1 holds:
Proposition 4 (Extension with >). Ψ ` A . B ⇔ Ψ ` A <: C, C ∼ D,Ψ ` D <: B, for some C, D.
We extend the definition of concretization (Definition 3) with > by adding
another equation γ(>) = {>}. Note that Castagna and Lanvin [7] also have thisequation in their calculus. It is easy to verify that Proposition 2 still holds:
f: B.
Proposition 5 (Equivalent to AGT on >). A . B if only if A <Siek and Taha’s Definition of Consistent Subtyping Does Not Work for >. As theanalysis in Section 3.2, Int → ? . > only holds when we first apply consistency,
then subtyping. However we cannot find a type A such that Int → ? <: A andA ∼ >. Also we have a similar problem in extending the restriction operator:
non-structural masking between Int → ? and > cannot be easily achieved.
6.2

Interpretation of the Dynamic Semantics

In Section 4.2 we have seen an example where a source expression could produce two different target expressions with different runtime behaviour. As we
explained, this is due to the guessing nature of the declarative system, and fromthe typing point of view, no type is particularly better than others. However,in practice, this is not desirable. Let us revisit the same example, now from thealgorithmic point of view (we omit the translation for space reasons):f : ∀a.a → a ` (λx : ?. f x) ⇒ ? → b
a a f : ∀a.a → a, baCompared with declarative typing, which produces many types (? → Int, ? →Bool, and so on), the algorithm computes the type ? → b
a with b
a unsolved in the
output context. What can we know from the output context? The only thing weknow is that b
a is not constrained at all! However, it is possible to make a morerefined distinction between different kinds of existential variables. The first kindof existential variables are those that indeed have no constraints at all, as they
do not affect the dynamic semantics. The second kind of existential variables(as in this example) are those where the only constraint is that the variable wasonce compared with an unknown type [12].
To emphasize the difference and have better support for dynamic semantics,
we could have gradual variables in addition to existential variables, with the difference that only unsolved gradual variables are allowed to be unified with the
unknown type. An irreversible transition from existential variables to gradualvariables occurs when an existential variable is compared with ?. After the algorithm terminates, we can set all unsolved existential variables to be any (static)
type (or more precisely, as Garcia and Cimini [12], with static type parameters),
and all unsolved gradual variables to be ? (or gradual type parameters). However,this approach requires a more sophisticated declarative/algorithmic type systemthan the ones presented in this paper, where we only produce static monotypes

24in type inference. We believe this is a typical trade-off in existing gradual typesystems with inference [23, 12]. Here we suppress the complexity of dynamic
semantics in favour of the conciseness of static typing.
6.3

The Dynamic Guarantee

In Section 4.3 we mentioned that the dynamic guarantee is closely related tothe coherence issue. To aid discussion, we first give the definition of dynamic
guarantee as follows:
Definition 5 (Dynamic guarantee). Suppose e0 v e, ∅ ` e : A∅ ` e 0 : A0
s0 , if s ⇓ v, then s0 ⇓ v 0 and v 0 v v.

s and

The dynamic guarantee says that if a gradually typed program evaluates to avalue, then removing type annotations always produces a program that evaluates
to an equivalent value (modulo type annotations). Now apparently the coherence
issue of the declarative system breaks the dynamic guarantee. For instance:(λf : ∀a.a → a. λx : Int. f x) (λx. x) 3

(λf : ∀a.a → a. λx : ?. f x) (λx. x) 3

The left one evaluates to 3, whereas its less precise version (right) will give acast error if a is instantiated to Bool for example.
As discussed in Section 6.2, we could design a more sophisticated declarative/algorithmic type system where coherence is retained. However, even with acoherent source language, the dynamic guarantee is still a question. Currently,
the dynamic guarantee for our target language λB is still an open question. According to Igarashi et al. [14], the difficulty lies in the definition of term precisionthat preserves the semantics.

7

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 and polymorphism.
Gradual Typing The seminal paper by Siek and Taha [21] is the first to propose gradual typing. The original proposal extends the simply typed lambda
calculus by introducing the unknown type ? and replacing type equality with
type consistency. Later Siek and Taha [22] incorporated gradual typing into a
simple object oriented language, and showed that subtyping and consistency are
orthogonal – an insight that partly inspired our work. We show that subtyping
and consistency are orthogonal in a much richer type system with higher-rankpolymorphism. Siek et al. [25] proposed a set of criteria that provides important guidelines for designers of gradually typed languages. Cimini and Siek [8]introduced the Gradualizer, a general methodology for generating gradual typesystems from static type systems. Later they also develop an algorithm to generate dynamic semantics [9]. Garcia et al. [13] introduced the AGT approachbased on abstract interpretation.

25

Gradual Type Systems with Explicit Polymorphism Ahmed et al. [1] proposed
λB that extends the blame calculus [29] to incorporate polymorphism. The key
novelty of their work is to use dynamic sealing to enforce parametricity. Devriese et al. [10] proved that embedding of System F terms into λB is not fully
abstract. Igarashi et al. [14] also studied integrating gradual typing with parametric polymorphism. They proposed System FG , a gradually typed extensionof 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.
Gradual Type Inference Siek and Vachharajani [23] studied unification-based
type inference for gradual typing, where they show why three straightforward
approaches fail to meet their design goals. Their type system infers gradual types,
which results in a complicated type system and inference algorithm. Garcia
and Cimini [12] 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). However none of these works deals with higherranked implicit polymorphism.
Higher-rank Implicit Polymorphism Odersky and Läufer [17] introduced a typesystem for higher-rank types. Based on that, Peyton Jones et al. [18] developed
an approach for type checking higher-rank predicative polymorphism. Dunfield
and Krishnaswami [11] proposed a bidirectional account of higher-rank polymorphism, and an algorithm for implementing the declarative system, which serves
as a sole inspiration for our algorithmic system. The key difference, however, isthe integration of gradual typing. Vytiniotis et al. [28] defers static type errors toruntime, which is fundamentally different from gradual typing, where programmers can control over static or runtime checks by precision of the annotations.

8

Conclusion

In this paper, we present a generalized definition of consistent subtyping, which
is proved to be applicable to both polymorphic and top types. Based on the
new definition of consistent subtyping, we have developed a gradually typed
calculus with predicative implicit higher-rank polymorphism, and an algorithm
to implement it. As future work, we are interested to investigate if our results
can scale to real world languages and other programming language features.

Acknowledgements
We thank Ronald Garcia 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.

Bibliography[1] Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler.
Blame for all. In Proceedings of the 38th Symposium on Principles of Programming Languages, 2011.
[2] Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. Theorems for free for free: Parametricity, with and without types. In Proceedingsof the 22nd International Conference on Functional Programming, 2017.
[3] Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. A theory ofgradual effect systems. In Proceedings of the 19th International Conference
on Functional Programming, 2014.
[4] Gavin Bierman, Erik Meijer, and Mads Torgersen. Adding dynamic types
to c#. In Proceedings of the European Conference on Object-Oriented Programming, 2010.
[5] Gavin Bierman, Martı́n Abadi, and Mads Torgersen. Understanding typescript. In Proceedings of the 28th European Conference on Object-Oriented
Programming, 2014.
[6] Ambrose Bonnaire-Sergeant, Rowan Davies, and Sam Tobin-Hochstadt.
Practical optional types for clojure. In Programming Languages and Systems. 2016.
[7] Giuseppe Castagna and Victor Lanvin. Gradual typing with union andintersection types. Proc. ACM Program. Lang., 1(ICFP):41:1–41:28, August
2017.
[8] Matteo Cimini and Jeremy G. Siek. The gradualizer: A methodology andalgorithm for generating gradual type systems. In Proceedings of the 43rd
Symposium on Principles of Programming Languages, 2016.
[9] Matteo Cimini and Jeremy G. Siek. Automatically generating the dynamic
semantics of gradually typed languages. In Proceedings of the 44th Symposium on Principles of Programming Languages, 2017.
[10] Dominique Devriese, Marco Patrignani, and Frank Piessens. Parametricity versus the universal type. Proceedings of the ACM on Programming
Languages, 2(POPL):38, 2017.
[11] Joshua Dunfield and Neelakantan R Krishnaswami. Complete and easy
bidirectional typechecking for higher-rank polymorphism. In International
Conference on Functional Programming, 2013.
[12] Ronald Garcia and Matteo Cimini. Principal type schemes for gradual programs. In Proceedings of the 42nd Symposium on Principles of Programming
Languages, 2015.
[13] Ronald Garcia, Alison M Clark, and Éric Tanter. Abstracting gradual typing. In Proceedings of the 43rd Symposium on Principles of Programming
Languages, 2016.
[14] Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. On polymorphic gradual typing. In Proceedings of the 22nd International Conference on Functional Programming, 2017.

27[15] Khurram A. Jafery and Joshua Dunfield. Sums of uncertainty: Refinements
go gradual. In Proceedings of the 44th Symposium on Principles of Programming Languages, 2017.
[16] John C Mitchell. Polymorphic type inference and containment. In Logicalfoundations of functional programming, 1990.
[17] Martin Odersky and Konstantin Läufer. Putting type annotations to work.
In Proceedings of the 23rd Symposium on Principles of Programming Languages, 1996.
[18] Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark
Shields. Practical type inference for arbitrary-rank types. Journal of Functional Programming, 17(1):1–82, 2007.
[19] John C. Reynolds. Types, abstraction and parametric polymorphism. In
Proceedings of the IFIP 9th World Computer Congress, 1983.
[20] John C. Reynolds. The coherence of languages with intersection types.
In Proceedings of the International Conference on Theoretical Aspects ofComputer Software, 1991.
[21] Jeremy G. Siek and Walid Taha. Gradual typing for functional languages.
In Proceedings of the 2006 Scheme and Functional Programming Workshop,
2006.
[22] Jeremy G. Siek and Walid Taha. Gradual typing for objects. In European
Conference on Object-Oriented Programming, 2007.
[23] Jeremy G. Siek and Manish Vachharajani. Gradual typing with unificationbased inference. In Proceedings of the 2008 Symposium on Dynamic Languages, 2008.
[24] Jeremy G. Siek and Philip Wadler. The key to blame: Gradual typing meets
cryptography (draft), 2016.
[25] Jeremy G. Siek, Michael M Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In LIPIcs-Leibniz International
Proceedings in Informatics, 2015.
[26] Julien Verlaguet. Facebook: Analyzing php statically. In Proceedings ofCommercial Users of Functional Programming, 2013.
[27] Michael M. Vitousek, Andrew M. Kent, Jeremy G. Siek, and Jim Baker.
Design and evaluation of gradual typing for python. In Proceedings of the10th Symposium on Dynamic languages, 2014.
[28] Dimitrios Vytiniotis, Simon Peyton Jones, and José Pedro Magalhães.
Equality proofs and deferred type errors: A compiler pearl. In Proceedings ofthe 17th International Conference on Functional Programming, ICFP ’12,
New York, NY, USA, 2012.
[29] Philip Wadler and Robert Bruce Findler. Well-typed programs can’t beblamed. In Proceedings of the 18th European Symposium on Programming
Languages and Systems, 2009.