Formalization of a Polymorphic Subtyping
Algorithm
Jinxu Zhao1 , Bruno C. d. S. Oliveira1 , and Tom Schrijvers2
1

The University of Hong Kong, {jxzhao,bruno}@cs.hku.hk
2
KU Leuven, tom.schrijvers@cs.kuleuven.be

Abstract. Modern functional programming languages such as Haskell
support sophisticated forms of type-inference, even in the presence of
higher-order polymorphism. Central to such advanced forms of typeinference is an algorithm for polymorphic subtyping. This paper formalizes an algorithmic specification for polymorphic subtyping in the
Abella theorem prover. The algorithmic specification is shown to be decidable, and sound and complete with respect to Odersky and Läufer’s
well-known declarative formulation of polymorphic subtyping.
While the meta-theoretical results are not new, as far as we know our
work is the first to mechanically formalize them. Moreover, our algorithm
differs from those currently in the literature by using a novel approachbased on worklist judgements. Worklist judgements simplify the propagation of information required by the unification process during subtyping.
Furthermore they enable a simple formulation of the meta-theoreticalproperties, which can be easily encoded in theorem provers.

1

Introduction

Most statically typed functional languages support a form of (implicit) parametric polymorphism [28]. Traditionally, functional languages have employedvariants of the Hindley-Milner [14, 23, 5] type system, which supports full typeinference without any type annotations. However the Hindley-Milner type system
only supports first-order polymorphism, where all universal quantifiers only occur at the top-level of a type. Modern functional programming languages such as
Haskell go beyond Hindley-Milner and support higher-order polymorphism. Withhigher-order polymorphism there is no restriction on where universal quantifiers
can occur. This enables more code reuse and more expressions to type-check,and has numerous applications [15, 12, 18, 17].
Unfortunately, with higher-order polymorphism full type-inference becomesundecidable [35]. To recover decidability some type annotations on polymorphic arguments are necessary. A canonical example that requires higher-order
polymorphism in Haskell is:
hpoly = (\f :: forall a. a -> a) -> (f 1, f ’c’)
The function hpoly cannot be type-checked in Hindley-Milner. The type of hpolyis (forall a. a -> a) -> (Int, Char). The single universal quantifier does

not appear at the top-level. Instead it is used to quantify a type variable a used in
the first argument of the function. Notably hpoly requires a type annotation for
the first argument (forall a. a -> a). Despite these additional annotations,the type-inference algorithm employed by GHC Haskell [16] preserves many ofthe desirable properties of Hindley-Milner. Like in Hindley-Milner type instantiation is implicit. That is, calling a polymorphic function never requires the
programmer to provide the instantiations of the type parameters.
Central to type-inference with higher-order polymorphism is an algorithm forpolymorphic subtyping. This algorithm allows us to check whether one type ismore general than another, which is essential to detect valid instantiations ofa polymorphic type. For example, the type forall a. a -> a is more generalthan Int -> Int. A simple declarative specification for polymorphic subtyping
was proposed by Odersky and Läufer [26]. Since then several algorithms havebeen proposed that implement it. Most notably, the algorithm proposed by Peyton Jones et al. [16] forms the basis for the implementation of type inferencein the GHC compiler. Dunfield and Krishnaswami [9] provided a very elegant
formalization of another sound and complete algorithm, which has also inspired
implementations of type-inference in some polymorphic programming languages(such as PureScript [30] or DDC [6]).
Unfortunately, while many aspects of programming languages and type systems have been mechanically formalized in theorem provers, there is little workon formalizing algorithms related to type-inference. The main exceptions to therule are mechanical formalizations of algorithm W and other aspects of traditional Hindler-Milner type-inference [24, 7, 8, 33, 11]. However, as far as we know,
there is no mechanisation of algorithms used by modern functional languages like
Haskell, and polymorphic subtyping included is no exception. This is a shame
because recently there has been a lot of effort in promoting the use of theorem provers to check the meta-theory of programming languages, e.g., throughwell-known examples like the POPLMark challenge [3] and the CompCert
project [21]. Mechanical formalizations are especially valuable for proving thecorrectness of the semantics and type systems of programming languages. Typeinference algorithms are arguably among the most non-trivial aspects of the implementations of programming languages. In particular the information discovery process required by many algorithms (through unification-like or constraintbased approaches), is quite subtle and tricky to get right. Moreover, extending
type-inference algorithms with new programming language features is often quitedelicate. Studying the meta-theory for such extensions would be greatly aided
by the existence of a mechanical formalization of the base language, which could
then be extended by the language designer.
Handling variable binding is particularly challenging in type inference, because the algorithms typically do not rely simply on local environments, butinstead propagate information across judgements. Yet, there is little work on
how to deal with these complex forms of binding in theorem provers. We believethat this is the primary reason why theorem provers have still not been widelyadopted for formalizing type-inference algorithms.
2

Type variables

a, b

Types
Monotypes
Contexts

A, B, C ::=
τ
::=
Ψ
::=

1 | a | ∀a.A | A → B
1 | a | τ1 → τ2
· | Ψ, aFig. 1. Syntax of Declarative System

This paper advances the state-of-the-art by formalizing an algorithm for polymorphic subtyping in the Abella theorem prover. We hope that this work encourages other researchers to use theorem provers for formalizing type-inference
algorithms. In particular, we show that the problem we have identified above
can be overcome by means of worklist judgments. These are a form of judgementthat turns the complicated global propagation of unifications into a simple local
substitution. Moreover, we exploit several ideas in the recent inductive formulation of a type-inference algorithm by Dunfield and Krishnaswami [9], which turnout to be useful for mechanisation in a theorem prover.
Building on these ideas we develop a complete formalization of polymorphic subtyping in the Abella theorem prover. Moreover, we show that the algorithm is sound, complete and decidable with respect to the well-known declarative formulation of polymorphic subtyping by Odersky and Läufer. While thesemeta-theoretical results are not new, as far as we know our work is the first to
mechanically formalize them.
In summary the contributions of this paper are:
– A mechanical formalization of a polymorphic subtyping algorithm.
We show that the algorithm is sound, complete and decidable in the Abella
theorem prover, and make the Abella formalization available online3 .
– Information propagation using worklist judgements: we employ worklists judgements in our algorithmic specification of polymorphic subtyping
to propagate information across judgements.

2

Overview: Polymorphic Subtyping

This section introduces Odersky and Läufer declarative subtyping rules, anddiscusses the challenges in formalizing a corresponding algorithmic version. Thenthe key ideas of our approach that address those challenges are introduced.
2.1

Declarative Polymorphic Subtyping

In implicitly polymorphic type systems, the subtyping relation compares thedegree of polymorphism of types. In short, if a polymorphic type A can always
be instantiated to any instantiation of B, then A is “at least as polymorphic as”
B, or we just say that A is “more polymorphic than” B, or A ≤ B.
3

https://github.com/JimmyZJX/Abella-subtyping-algorithm

3

Ψ `A

Ψ `1

a∈Ψ

wfd unit

Ψ `a

Ψ `A

wfd varΨ `BΨ `A→BΨ, a ` A

wfd →Ψ ` ∀a.A

wfd ∀Ψ `A≤Ba∈ΨΨ `a≤a≤VarΨ `1≤1

Ψ `τ

≤Unit

Ψ ` [τ /a]A ≤ BΨ ` ∀a.A ≤ B≤∀LΨ ` B1 ≤ A1

Ψ ` A2 ≤ B2

Ψ ` A1 → A2 ≤ B1 → B2
Ψ, a ` A ≤ B
Ψ ` A ≤ ∀a.B

≤→

≤∀R

Fig. 2. Well-formedness of Declarative Types and Declarative Subtyping

There is a very simple declarative formulation of polymorphic subtyping due
to Odersky and Laüfer [26]. The syntax of this declarative system is shown in
Figure 1. Types, represented by A, B, C, are the unit type 1, type variables
a, b, universal quantification ∀a.A and function type A → B. We allow nested
universal quantifiers to appear in types, but not in monotypes. Contexts Ψ collecta list of type variables.
In Figure 2, we give the well-formedness and subtyping relation for the declarative system. The cases without universal quantifiers are handled by Rules ≤Var,≤Unit and ≤→. The subtyping rule for function types (≤→) is standard, being
contravariant on the argument types. Rule ≤∀R says that if A is a subtype of
B under the context extended with a, where a is fresh in A, then A ≤ ∀a.B.
Intuitively, if A is more general than the universally quantified type ∀a.B, thenA must instantiate to [τ /a]B for every τ .
Finally, the most interesting rule is ≤∀L, which instantiates ∀a.A to [τ /a]A,and concludes the subtyping ∀a.A ≤ B if the instantiation is a subtype of B.
Notice that τ is guessed, and the algorithmic system should provide the means tocompute this guess. Furthermore, the guess is a monotype, which rules out thepossibility of polymorphic (or impredicative) instantiation. The restriction to
monotypes and predicative instantiation is used by both Peyton Jones et al. [16]and Dunfield and Krishnaswami’s [9] algorithms, which are adopted by several
practical implementations of programming languages.
2.2

Finding Solutions for Variable Instantiation

The declarative system specifies the behavior of subtyping relations, but is notdirectly implementable: the rule ≤∀L requires guessing a monotype τ . The core
problem that an algorithm for polymorphic subtyping needs to solve is to findan algorithmic way to compute the monotypes, instead of guessing them. An
additional challenge is that the declarative rule ≤→ splits one judgment into
two, and the (partial) solutions found for existential variables when processing
the first judgment should be transfered to the second judgement.
4

Dunfield and Krishnaswami’s Approach An elegant algorithmic solution to computing the monotypes is presented by Dunfield and Krishnaswami [9]. Theiralgorithmic subtyping judgement has the form:Ψ `A≤BaΦA notable difference to the declarative judgement is the presence of a so-called
output context Φ, which refines the input context Ψ with solutions for existential
variables found while processing the two types being compared for subtyping.
Both Ψ and Φ are ordered contexts with the same structure. Ordered contexts
are particularly useful to keep track of the correct scoping for variables, and are anotable different to older type-inference algorithms [5] that use global unification
variables or constraints collected in a set.
Output contexts are useful to transfer information across judgements in Dunfield and Krishnaswami’s approach. For example, the algorithmic rule corresponding to ≤→ in their approach is:Ψ ` B1 <: A1 a Φ Φ ` [Φ]A2 <: [Φ]B2 a Φ0<:→
Ψ ` A1 → A2 <: B1 → B2 a Φ0
The information gathered by the output context when comparing the input typesof the functions for subtyping is transfered to the second judgement by becoming
the new input context, while any solution derived from the first judgment isapplied to the types of the second judgment.
Example If we want to show that ∀a.a → a is a subtype of 1 → 1, the declarative
system will guess the proper τ = 1 for Rule ≤∀L:·`1 ·`1→1≤1→1≤∀L· ` ∀a.a → a ≤ 1 → 1
Dunfield and Krishnaswami introduce an existential variable—denoted with α, β—whenever a monotype τ needs to be guessed. Below is a sample derivation of theiralgorithm; we omit the full set of algorithmic rules due to lack of space:
InstRSolveα`1≤αaα=1
α=1`1≤1`α=1α`α→α≤1→1aα=1· ` ∀a.a → a ≤ 1 → 1 a ·<:Unit<:→<:∀L

The first step applies Rule <:∀L, which introduces a fresh existential variable,α, and opens the left-hand-side ∀-quantifier with it. Next, Rule <:→ splits the
judgment in two. For the first branch, Rule InstRSolve satisfies 1 ≤ α by solving
α to 1, and stores the solution in its output context. The output context of thefirst branch is used as the input context of the second branch, and the judgment
is updated according to current solutions. Finally, the second branch becomesa base case, and Rule <:Unit finishes the derivation, makes no change to the
input context and propagates the output context back.
5

Dunfield and Krishnaswami’s algorithmic specification is elegant and contains
several useful ideas for a mechanical formalization of polymorphic subtyping.
For example ordered contexts and existential variables enable a purely inductive
formulation of polymorphic subtyping. However the binding/scoping structureof their algorithmic judgement is still fairly complicated and poses challenges
when porting their approach to a theorem prover.
2.3

The Worklist Approach

We inherit Dunfield and Krishnaswami’s ideas of ordered contexts, existential
variables and the idea of solving those variables, but drop output contexts. Instead our algorithmic rule has the form:Γ `Ω
where Ω is a list of judgments A ≤ B instead of a single one. This judgement
form, which we call worklist judgement, simplifies two aspects of Dunfield andKrishnaswami’s approach.
Firstly, as already stated, there are no output contexts. Secondly the form of
the ordered contexts become simpler. The transfer of information across judgements is simplified because all judgements share the input context. Moreover theorder of the judgements in the list allows information discovered when processing the earlier judgements to be easily transfered to the later judgements. In theworklist approach the rule for function types is:Γ ` B1 ≤ A1 ; A2 ≤ B2 ; Ω≤a →Γ ` A1 → A2 ≤ B 1 → B 2 ; ΩThe derivation of the previous example with the worklist approach is:
a nil

·`·
≤a unit· ` 1 ≤ 1; ·≤a solve ex
α ` 1 ≤ α; α ≤ 1; ·≤a →α ` α → α ≤ 1 → 1; ·≤a ∀L
· ` ∀a.a → a ≤ 1 → 1; ·To derive · ` ∀a.a → a ≤ 1 → 1 with the worklist approach, we first introduce
an existential variable and change the judgement to α ` α → α ≤ 1 → 1; ·. Then,
we split the judgment in two for the function types and the derivation comesto α ` 1 ≤ α; α ≤ 1; ·. When the first judgment is solved with α = 1, we
immediately remove α from the context, while propagating the solution as a
substitution to the rest of the judgment list, resulting in · ` 1 ≤ 1; ·, whichfinishes the derivation in two trivial steps.
With this form of eager propagation, solutions no longer need to be recordedin contexts, simplifying the encoding and reasoning in a proof assistant.
6

Type variables
Existential variables

a, b
α, β

Algorithmic types
Algorithmic context
Algorithmic judgments

A, B, C ::=
Γ
::=
Ω
::=

1 | a | α | ∀a.A | A → B· | Γ, a | Γ, α
· | A ≤ B; Ω

Γ `A

Γ `1

a∈Γ

wfa unit
Γ `A

Γ `a
Γ `B

Γ `A→Bwfa var

wfa →

α∈Γ
Γ `α
Γ, a ` AΓ ` ∀a.A

wfa exvar

wfa ∀Fig. 3. Syntax and Well-Formedness Judgement for the Algorithmic System.

Key Results Both the declarative and algorithmic systems are formalized in
Abella. We have proven 3 important properties for this algorithm: decidability,
ensuring that the algorithm always terminates; and soundness and completeness,showing the equivalence of the declarative and algorithmic systems.

3

A Worklist Algorithm for Polymorphic Subtyping

This section presents our algorithm for polymorphic subtyping. A novel aspectof our algorithm is the use of worklist judgments: a form of judgement thatfacilitates the propagation of information.
3.1

Syntax and Well-Formedness of the Algorithmic System

Figure 3 shows the syntax and the well-formedness judgement.
Existential Variables In order to solve the unknown types τ , the algorithmic system extends the declarative syntax of types with existential variables α. They
behave like unification variables, but are not globally defined. Instead, the ordered algorithmic context, inspired by Dunfield and Krishnaswami [9], defines
their scope. Thus the type τ represented by the corresponding existential variable is always bound in the corresponding declarative context Ψ .
Worklist Judgements The form of our algorithmic judgements is non-standard.
Our algorithm keeps track of an explicit list of outstanding work: the list Ω of(reified) algorithmic judgements of the form A ≤ B, to which a substitution canbe applied once and for all to propagate the solution of an existential variable.
Hole Notation To facilitate context manipulation, we use the syntax Γ [ΓM ] todenote a context of the form ΓL , ΓM , ΓR where Γ is the context ΓL , •, ΓR witha hole (•). Hole notations with the same name implicitly share the same ΓL andΓR . A multi-hole notation like Γ [α][β] means Γ1 , α, Γ2 , β, Γ3 .
7

Γ `Ω
a nil

Γ `·
Γ `Ω
Γ ` 1 ≤ 1; Ωa∈Γ≤a unitΓ `ΩΓ ` a ≤ a; Ωα∈Γ≤a varΓ ` B1 ≤ A1 ; A2 ≤ B2 ; ΩΓ ` A1 → A2 ≤ B1 → B2 ; Ωα freshΓ, α ` [α/a]A ≤ B; ΩΓ ` ∀a.A ≤ B; Ωα∈
/ FV (A) ∪ F V (B)

≤a ∀L

Γ `Ω

Γ ` α ≤ α; Ω≤a →b freshΓ, b ` A ≤ B; ΩΓ ` A ≤ ∀b.B; ΩΓ [α1 , α2 ] ` α1 → α2 ≤ A → B; [α1 → α2 /α]Ω
Γ [α] ` α ≤ A → B; Ωα∈
/ F V (A) ∪ F V (B)Γ [α1 , α2 ] ` A → B ≤ α1 → α2 ; [α1 → α2 /α]Ω
Γ [α] ` A → B ≤ α; ΩΓ [α][] ` [α/β]Ω
Γ [α][β] ` α ≤ β; ΩΓ [a][] ` [a/β]Ω
Γ [a][β] ` a ≤ β; ΩΓ [] ` [1/α]Ω
Γ [α] ` α ≤ 1; ΩΓ [α][] ` [α/β]Ω≤a solve exΓ [α][β] ` β ≤ α; ΩΓ [a][] ` [a/β]Ω≤a solve var

Γ [a][β] ` β ≤ a; ΩΓ [] ` [1/α]Ω≤a solve unit≤a exvarΓ [α] ` 1 ≤ α; Ω≤a ∀R≤a instL≤a instR≤a solve ex0≤a solve var0

≤a solve unit0

Fig. 4. Algorithmic Subtyping

3.2

Algorithmic Subtyping

The algorithmic subtyping judgement, defined in Figure 4, has the form Γ ` Ω,
where Ω collects multiple subtyping judgments A ≤ B. The algorithm treats Ω
as a worklist. In every step it takes one task from the worklist for processing,possibly pushes some new tasks on the worklist, and repeats this process until
the list is empty. This last and single base case is handled by Rule a nil. The
remaining rules all deal with the first task in the worklist. Logically we candiscern 3 groups of rules.
Firstly, we have five rules that are similar to those in the declarative system,
mostly just adapted to the worklist style. For instance, Rule ≤a → consumes
one judgment and pushes two to the worklist. A notable difference with thedeclarative Rule ≤∀L is that Rule ≤a ∀L requires no guessing of a type τ toinstantiate the polymorphic type ∀a.A, but instead introduces an existential
variable α to the context and to A. In accordance with the declarative system,8α1 ` ·a nil

α1 ` 1 ≤ 1; ·≤a unit

α1 , α2 ` α1 ≤ α2 ; 1 ≤ 1; ·≤a solve ex

α1 , α2 , β ` α1 ≤ β; β ≤ α2 ; 1 ≤ 1; ·≤a solve ex

α1 , α2 , β ` β → β ≤ α1 → α2 ; 1 ≤ 1; ·α, β ` β → β ≤ α; 1 ≤ 1; ·α ` ∀a. a → a ≤ α; 1 ≤ 1; ·α ` α → 1 ≤ (∀a. a → a) → 1; ·≤a →≤a instR
≤a ∀L
≤a →

stuck
α, b ` α ≤ b; ·?

α ` α ≤ ∀b. b; ·≤a ∀R

α ` 1 ≤ 1; α ≤ ∀b. b; ·≤a unitα ` 1 → α ≤ 1 → ∀b. b; ·≤a →· ` ∀a. 1 → a ≤ 1 → ∀b. b; ·

≤a ∀L

≤a ∀L

· ` ∀a. a → 1 ≤ (∀a. a → a) → 1; ·Fig. 5. Successful and Failing Derivations for the Algorithmic Subtyping Relation

where the monotype τ should be bound in the context Ψ , here α should only besolved to a monotype bound in Γ . More generally, for any algorithmic context
Γ [α], the algorithmic variable α can only be solved to a monotype that is wellformed with respect to ΓL .
Secondly, Rules ≤a instL and ≤a instR partially instantiate existential types
α, to function types. The domain and range of the new function type are undetermined: they are set to two fresh existential variables α1 and α2 . To make surethat α1 → α2 has the same scope as α, the new variables α1 and α2 are inserted
in the same position in the context where the old variable α was. To propagate
the instantiation to the remainder of the worklist, α is substituted for α1 → α2
in Ω. The occurs-check side-condition is necessary to prevent a diverging infinite
instantiation. For example 1 → α ≤ α would diverge with no such check.
Thirdly, in the remaining six rules an existential variable can be immediately
solved. Each of the six similar rules removes an existential variable from thecontext, performs a substitution on the remainder of the worklist and continues.
The algorithm on judgment list is designed to share the context across all
judgments. However, the declarative system does not share a single context in its
derivation. This gap is filled by strengthening and weakening lemmas of both systems, where most of them are straightforward to prove, except for the strengthening lemma of the declarative system, which is a little trickier.
Example We illustrate the subtyping rules through a sample derivation in theleft of Figure 5, which shows that that ∀a. a → 1 ≤ (∀a. a → a) → 1. Thus
the derivation starts with an empty context and a judgment list with only one
element.
In step 1, we have only one judgment, and that one has a top-level ∀ on
the left hand side. So the only choice is rule ≤a ∀L, which opens the universallyquantified type with an unknown existential variable α. Variable α will be solved
later to some monotype that is well-formed within the context before α. That is,
the empty context · in this case. In step 2, rule ≤a → is applied to the worklist,
splitting the first judgment into two. Step 3 is similar to step 1, where the left9hand-side ∀ of the first judgment is opened according to rule ≤a ∀L with a fresh
existential variable. In step 4, the first judgment has an arrow on the left handside, but the right-hand-side type is an existential variable. It is obvious that
α should be solved to a monotype of the form σ → τ . Rule instR implements
this, but avoids guessing σ and τ by “splitting” α into two existential variables,
α1 and α2 , which will be solved to some σ and τ later. Step 5 applies Rule≤a → again. Notice that after the split, β appears in two judgments. When thefirst β is solved during any step of derivation, the next β will be substituted bythat solution. This propagation mechanism ensures the consistent solution of thevariables, while keeping the context as simple as possible. Steps 6 and 7 solve
existential variables. The existential variable that is right-most in the context isalways solved in terms of the other. Therefore in step 6, β is solved in terms of
α1 , and in step 7, α2 is solved in terms of α1 . Additionally, in step 6, when β
is solved, the substitution [α1 /β] is propagated to the rest of the judgment list,
and thus the second judgment becomes α1 ≤ α2 . Steps 8 and 9 trivially finish
the derivation. Notice that α1 is not instantiated at the end. This means thatany well-scoped instantiation is fine.
A Failing Derivation We illustrate the role of ordered contexts through anotherexample: ∀a. 1 → a ≤ 1 → ∀b. b. From the declarative perspective, a should
be instantiated to some τ first, then b is introduced to the context, so that b ∈/F V (τ ). As a result, we cannot find τ such that τ ≤ b. The right of Figure 5 shows
the algorithmic derivation, which also fails due to the scoping—α is introduced
earlier than b, thus it cannot be solved to b.

4

Metatheory

This section presents the 3 main meta-theoretical results that we have provedin Abella. The first two are soundness and completeness of our algorithm withrespect to Odersky and Läufer’s declarative subtyping. The third result is ouralgorithm’s decidability.
4.1

Transfer to the Declarative System

To state the correctness of the algorithmic subtyping rules, Figure 6 introduces
two transfer judgements to relate the declarative and the algorithmic system.
The first judgement, transfer of contexts Γ → Ψ , removes existential variablesfrom the algorithmic context Γ to obtain a declarative context Ψ . The second
judgement, transfer of the judgement list Γ | ΩΩ 0 , replaces all occurrences ofexistential variables in Ω by well-scoped mono-types. Notice that this judgment
is not decidable, i.e. a pair of Γ and Ω may be related with multiple Ω 0 . However,if there exists some substitution that transforms Ω to Ω 0 , and each subtyping
judgment in Ω 0 holds, we know that Ω is potentially satisfiable.
The following two lemmas generalize Rule exvar from substituting the firstexistential variable to substituting any existential variable.
10

Γ →Ψ

·→·

Γ →Ψ

→·

Γ, a → Ψ, a

Γ |Ω

·|Ω

Ω

·

Γ |Ω
Γ, a | Ω

Ω0
Ω

0

Γ →Ψ

→var

Γ, α → Ψ
Ω0
Γ →Ψ

var

→exvarΨ `τ

Γ | [τ /α]Ω

Γ, α | Ω

Ω

0

Ω0

exvar

Fig. 6. Transfer Rules

Lemma 1 (Insert). If Γ → Ψ and Ψ ` τ and Γ, Γ1 | [τ /α]Ω
Γ, α, Γ1 | ΩΩ0.
Lemma 2 (Extract). If Γ, α, Γ1 | ΩΓ, Γ1 | [τ /α]Ω
Ω0.

Ω 0 , thenΩ 0 , then ∃τ s.t. Γ → Ψ, Ψ ` τ andIn order to match the shape of algorithmic subtyping relation for the following
proofs, we define a relation Ψ ` Ω for the declarative system, meaning that all
the declarative judgments hold under context Ψ .
Definition 1 (Declarative Subtyping Worklist).
Ψ ` Ω := ∀(A ≤ B) ∈ Ω, Ψ ` A ≤ B
4.2

Soundness

Our algorithm is sound with respect to the declarative specification. For any
derivation of a list of algorithmic judgments Γ ` Ω, we can find a valid transfer
Γ |ΩΩ 0 such that all judgments in Ω 0 hold in Ψ , with Γ → Ψ .
Theorem 1 (Soundness). If Γ ` Ω and Γ → Ψ , then there exists Ω 0 , s.t.
Γ |Ω
Ω 0 and Ψ ` Ω 0 .
The proof proceeds by induction on the derivation of Γ ` Ω, finished off byappropriate applications of the insertion and extraction lemmas.
4.3

CompletenessCompleteness of the algorithm means that any declarative derivation has analgorithmic counterpart.
Theorem 2 (Completeness). If Ψ ` Ω 0 and Γ → Ψ and Γ | ΩΓ ` Ω.
11Ω 0 , then

The proof proceeds by induction on the derivation of Ψ ` Ω 0 . As the declarative system does not involve information propagation across judgments, theinduction can focus on the subtyping derivation of the first judgment without
affecting other judgments. The difficult cases correspond to the ≤a instL and≤a instR rules. When the proof by induction on Ψ ` Ω 0 reaches the ≤→ case,the first declarative judgment has a shape like A1 → A2 ≤ B1 → B2 . One of thepossibile cases for the first corresponding algorithmic judgement is α ≤ A → B.
However, the case analysis does not indicate that α is fresh in A and B. Thus
we cannot apply Rule ≤a instL and make use of the induction hypothesis. The
following lemma helps us out in those cases: it rules out subtypings with infinite
types as solutions (e.g. α ≤ 1 → α) and guarantees that α is free in A and B.
Lemma 3 (Prune Transfer for Instantiation). If Ψ ` A1 → A2 ≤ B1 →B2 ; Ω 0 and Γ → Ψ and Γ | (α ≤ A → B; Ω)(A1 → A2 ≤ B1 → B2 ; Ω 0 ) ,then α ∈/ F V (A) ∪ F V (B).
A similar lemma holds for the symmetric case (A → B ≤ α; Ω).
4.4

Decidability

The third key result for our algorithm is decidability.
Theorem 3 (Decidability). Given any well-formed judgment list Ω under Γ ,it is decidable whether Γ ` Ω or not.
We have proven this theorem by means of a lexicographic group of induction
measurements h|Ω|∀ , |Γ |α , |Ω|→ i on the worklist Ω and algorithmic context Γ .
The worklist measures | · |∀ and | · |→ count the number of universal quantifiers
and function types respectively.
Definition 2 (Worklist Measures).
|1|∀ = |a|∀ = |α|∀ = 0|1|→ = |a|→ = |α|→ = 0|A → B|∀ = |A|∀ + |B|∀
|A → B|→ = |A|→ + |B|→ + 1|∀x.A|∀ = |A|+
1|∀x.A|→ = P|A|→∀P|Ω|∀ = A≤B∈Ω |A|∀ + |B|∀|Ω|→ = A≤B∈Ω |A|→ + |B|→
The context measure | · |α counts the number of unsolved existential variables.
Definition 3 (Context Measure).
| · |α = 0|Γ, a|α = |Γ |α|Γ, α|α = |Γ |α + 1

It is not difficult to see that all but two of the algorithm’s rules decrease oneof the three measures. The two exceptions are the Rules ≤a instL and ≤a instR;
both increment the number of existential variables and the number of function
types without affecting the number of universal quantifiers. To handle these rules,
we handle a special class of judgements, which we call instantiation judgementsΩi , separately. They take the form:
12Definition 4 (Ωi ).
Ωi := · | α ≤ A; Ωi0 | A ≤ α; Ωi0

where α ∈/ F V (A) ∪ F V (Ωi0 )

These instantiation judgements are these ones consumed and produced by theRules ≤a instL and ≤a instR. The following lemma handles their decidability.
Lemma 4 (Instantiation Decidability). For any context Γ and judgment
list Ωi , Ω, it is decidable whether Γ ` Ωi , Ω if both of the conditions hold1) ∀Γ 0 , Ω 0 s.t. |Ω 0 |∀ < |Ωi , Ω|∀ , it is decidable whether Γ 0 ` Ω 0 .
2) ∀Γ 0 , Ω 0 s.t. |Ω 0 |∀ = |Ωi , Ω|∀ and |Γ 0 |α = |Γ |α − |Ωi |, it is decidable whetherΓ 0 ` Ω0.
In other words, for any instantiation judgment prefix Ωi , the algorithm either
reduces the number of ∀’s or solves one existential variable per instantiation
judgment. The proof of this lemma is by induction on the measure 2∗|Ωi |→ +|Ωi |of the instantiation judgment list.
In summary, the decidability theorem can be shown through a lexicographic
group of induction measurements h|Ω|∀ , |Ω|α , |Ω|→ i. The critical case is that,whenever we encounter an instantiation judgment at the front of the worklist, werefer to Lemma 4, which reduces the number of unsolved variables by consumingthat instantiation judgment, or reduces the number of ∀-quantifiers. Other cases
are relatively straightforward.

5

The Choice of Abella

We have chosen the Abella (v2.0.5) proof assistant [10] to develop our formalization. Our development is only based on the reasoning logic of Abella, anddoes not make use of its specification logic. Abella is particularly helpful due toits built-in support for variable bindings, and its λ-tree syntax [22] is a form of
HOAS, which helps with the encoding and reasoning about substitutions. For
instance, the type ∀x.x → a is encoded as all (x\ arrow x a), where x\ arrow x a
is a lambda abstraction in Abella. An opening [b/x](x → a) is encoded as an application (x\ arrow x a) b, which can be simplified(evaluated) to arrow b a. Namesupply and freshness conditions are controlled by the ∇-quantifier. The expression nabla x, F means that x is a unique variable in F, i.e. it is different from anyother names occurring elsewhere. Such variables are called nominal constants.
They can be of any type, in other words, every type may contain unlimited
number of such atomic nominal constants.
Encoding of the Declarative System As a concrete example, our declarative context and well-formedness rules are encoded as follows.
Kind ty
Type iType alltype.
ty.
(ty → ty) → ty.

% the unit type
% forall-quantifier

13Type arrow ty → ty → ty.
Type bound ty → o.

% function type% variable collection in contexts

Define env : olist → prop by
env nil;nabla x, env (bound x :: E) := env E.
Define wft : olist → ty → prop by
wft E i;nabla x, wft (E x) x := nabla x, member (bound x) (E x);
wft E (arrow A B) := wft E A ∧ wft E B;
wft E (all A) := nabla x, wft (bound x :: E) (A x).

We use the type olist just as normal list of o with two constructors, namely
nil : olist and (::) : o → olist → olist, where o purely means “the element
type of olist”. The member : o → olist → prop relation is also pre-defined. The
second case of the relation wft states rule wfd var. The encoding (E x) basicallymeans that the context may contain x. If we write (E x) as E, then the context
should not contain x, and both wft E x and member (bound x) E make no sense.
Instead, we treat E : ty → olist as an abstract structure of a context, such asx\ bound x :: bound a :: nil. For the fourth case of the relation wft, the type∀x.A in our target language is expressed as (all A), and its opening A, (A x).
Encoding of the Algorithmic System In terms of the algorithmic system, notably,
Abella handles the ≤a instL and ≤a instR rules in a nice way:
% sub_alg_list : enva → [subty_judgment] → prop
Define subal : olist → olist → prop by
subal E nil;
subal E (subt i i :: Exp) := subal E Exp;% some cases omitted ...
% <: instL
nabla x, subal (E x) (subt x (arrow A B) :: Exp x) :=exists E1 E2 F, nabla x y z, append E1 (exvar x :: E2) (E x) ∧append E1 (exvar y :: exvar z :: E2) (F y z) ∧subal (F y z) (subt (arrow y z) (arrow A B) :: Exp (arrow y z));% <: instR is symmetric to <: instL, omitted here
% other cases omitted ...

Thanks to the way Abella deals with nominal constants, the pattern subt x (arrow A B)
implicitly states that x ∈/ F V (A) ∧ x ∈/ F V (B). If the condition were not required, we would have encoded the pattern as subt x (arrow (A x) (B x)) instead.
5.1

Statistics and Discussion

Some basic statistics on our proof script are shown in Figure 7. The proof consists of 3627 lines of code with a total of 33 definitions and 267 theorems. We
have to mention that Abella provides few built-in tactics and does not support
user-defined ones, and we would reduce significant lines of code if Abella provided more handy tactics. Moreover, the definition of natural numbers, the plus
14

File(s)SLOC # of Theorems Description
olist.thm, nat.thm
303
55
Basic data structureshigher.thm, order.thm 164
15
Declarative systemhigher alg.thm
618
44
Algorithmic systemtrans.thm
411
46
Transfersound.thm
166
2Soundness theorem
depth.thm
143
12
Definition of depth
complete.thm
626
28
Lemmas and Completeness theorem
decidable.thm
1077
53
Lemmas and Decidability theorem
Total
3627
267
(33 definitions in total)
Fig. 7. Statistics for the proof scripts

operation and less-than relation are defined within our proof due to Abella’s lackof packages. However, the way Abella deals with name bindings is very helpful
for type system formalizations and substitution-intensive formalizations, such as
this one.

6

Related Work

Type Inference for Polymorphic Subtyping Higher-order polymorphism is a practical and important programming language feature. Due to the undecidabilityof type-inference for System F [35], different decidable partial type-inference
approaches were developed. The subtyping relation of this paper, originally proposed by Odersky and Laüfer [26], is predicative (∀’s only instantiate to monotypes), which is considered a reasonable and practical trade-off. There is also
work on partial impredicative type-inference algorithms [19, 20, 34]. However,unlike the predicative subtyping relation for System F, the subtyping for impredicative System F is undecidable [31]. Therefore such algorithms have tonavigate through the design space to impose restrictions that allow for a decidable algorithm. As a result such algorithms tend to be more complex, and areless adopted in practice.
Gundry et al. [13] revisited the Hindley-Milner type system. They make useof ordered contexts on the unification during type inference, and their algorithm
works differently from algorithm W. Dunfield and Krishnaswami [9] adopted
a similar idea on ordered contexts and presented an algorithmic approach forpredicative polymorphic subtyping that tracks the (partial) solutions of existential variables in the algorithmic context—this denotes a delayed substitutionthat is incrementally applied to outstanding work as it is encountered. Theiralgorithm comes with 40 pages of manual proofs on the soundness, completeness and decidability. We have tried to mechanize these proofs directly, but havenot been successful yet because most proof assistants do not naturally support
output contexts and their more complex ordered contexts. Their theorems havestatements that are more complex than those in the worklist approach. One of
the reasons for the added complexity is that, when the constraints are not strict15

enough, the algorithm may not instantiate all existential variables. However inorder to match the declarative judgement, all the unsolved variables should beproperly assigned. For example, their generalized completeness theorem is:
Theorem 4 (Generalized Completeness of Subtyping [9]).
If Ψ −→ Φ and Ψ ` A and Ψ ` B and [Φ]Ψ ` [Φ]A ≤ [Φ]B then there exist ∆and Φ0 such that ∆ −→ Φ0 and Φ −→ Φ0 and Ψ ` [Ψ ]A <: [Ψ ]B a ∆.
Here, the auxiliary relation Ψ −→ Ψ 0 extends a context Ψ to a context Ψ 0 .
This is used to extend the algorithm’s input and output contexts Ψ and ∆, with
with possibly unassigned existential variables, to a complete (i.e., fully-assigned)
contexts Φ and Φ0 suitable for the declarative specification.
While we are faced with a similar gap between algorithm and specification,
which we tackle with our transfer relations Γ → Ψ , our completeness statement
is much shorter because our algorithm does not return an output context whichneeds to be transferred. Moreover, we have cleanly encapsulated any substitutions to the worklist in the worklist transfer judgement Γ | ΩΩ0.
Peyton Jones et al. [16] developed a higher-rank predicative bidirectional
type system. They enriched their subtyping relations with deep skolemisation,
while other relations remain similar to ours. Their algorithm is unification-basedwith a structure similar to algorithm W’s.
Unification Algorithms Our algorithm works similarly to some unification algorithms that use a set of unification constraints and single-step simplificationtransitions. Some work [27, 1] adopts this idea in dependently typed inference
and reconstruction. These approaches collect a set of constraints and nondeterministically process one of them at a time. Those approaches consider various
forms of constraints, including term unification, context unification and solution
for meta-variables. In contrast, our algorithm is presented in a simpler form, using ordered (worklist) judgements, which is sufficient for the subtyping problem.
Formalizations of Type-Inference Algorithms in Theorem Provers The wellknown POPLMark challenge [3] has encouraged the development of new proof
assistant features for facilitating the development and verification of type systems. As a result, many theorem provers and packages now provide methods for
dealing with variable binding [2, 32, 4], and more and more type system designers
choose to formalize their proofs with these tools. Yet, difficulties with mechanising algorithmic aspects, like unification and constraint solving, have received
very little attention. Moreover, while most type system judgements only feature
local (input) contexts, which have a simple binding/scoping structure, many traditional type-inference algorithms require more complex binding structures with
output contexts.
Naraschewski and Nipkow [24] published the first formal verification of algorithm W in Isabelle/HOL [25]. The treatment of new variables is a little trickyin their formalization, while most other parts follow the structure of Damas’s
manual proof closely. Following Naraschewski and Nipkow other researchers [7, 8]
prove a similar result in Coq [29]. Nominal techniques [32] in Isabelle/HOL have16

also been used for a similar verification [33]. Moreover, Garrigue [11] mechanizeda type inference algorithm for Core ML extended with structural polymorphism
and recursion.

7

Conclusion and Future WorkIn this paper we have shown how to mechanise an algorithmic subtyping relation
for higher-order polymorphism, together with its proofs of soundness, completeness and decidability, in the Abella proof assistant. In ongoing work we areextending our mechanisation with a bidirectional type inference algorithm. The
main difficulty there is communicating the instantiations of existential variablesfrom the subtyping algorithm to the type inference. To make this possible we are
exploring a continuation passing style formulation, which generalises the worklist
approach. Another possible extension is to have the algorithm return an explicit
witness for the subtyping as part of type-directed elaboration into System F.

Acknowledgement
We sincerely thank the anonymous reviewers for their insightful 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
1. Abel, A., Pientka, B.: Higher-order dynamic pattern unification for dependent
types and records. In: International Conference on Typed Lambda Calculi andApplications. pp. 10–26. Springer (2011)
2. Aydemir, B., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineeringformal metatheory. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages. POPL ’08 (2008)
3. Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P.,
Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory
for the masses: The POPLmark challenge. In: The 18th International Conferenceon Theorem Proving in Higher Order Logics (2005)
4. Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics.
In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming. ICFP ’08 (2008)
5. Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’82 (1982)
6. Disciple Development Team: The Disciplined Disciple Compiler (2017),
http://disciple.ouroborus.net/
7. Dubois, C.: Proving ML type soundness within Coq. Theorem Proving in Higher
Order Logics pp. 126–144 (2000)
8. Dubois, C., Menissier-Morain, V.: Certification of a type inference tool for ML:
Damas–Milner within Coq. Journal of Automated Reasoning 23(3), 319–346 (1999)

17

9. Dunfield, J., Krishnaswami, N.R.: Complete and easy bidirectional typechecking
for higher-rank polymorphism. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. ICFP ’13 (2013)
10. Gacek, A.: The Abella interactive theorem prover (system description). In: Proceedings of IJCAR 2008. Lecture Notes in Artificial Intelligence (2008)
11. Garrigue, J.: A certified implementation of ML with structural polymorphism
and recursive types. Mathematical Structures in Computer Science 25(4), 867–
891 (2015)
12. Gill, A., Launchbury, J., Peyton Jones, S.L.: A short cut to deforestation. In: Proceedings of the Conference on Functional Programming Languages and Computer
Architecture. FPCA ’93 (1993)
13. Gundry, A., McBride, C., McKinna, J.: Type inference in context. In: Proceedingsof the Third ACM SIGPLAN Workshop on Mathematically Structured Functional
Programming. MSFP ’10 (2010)
14. Hindley, R.: The principal type-scheme of an object in combinatory logic. Transactions of the american mathematical society 146, 29–60 (1969)
15. Jones, M.P.: Functional programming with overloading and higher-order polymorphism. In: Advanced Functional Programming. Lecture Notes in Computer Science
925 (1995)
16. Jones, S.P., Vytiniotis, D., Weirich, S., Shields, M.: Practical type inference forarbitrary-rank types. Journal of functional programming 17(1), 1–82 (2007)
17. Lämmel, R., Jones, S.P.: Scrap your boilerplate: A practical design pattern forgeneric programming. In: Proceedings of the 2003 ACM SIGPLAN International
Workshop on Types in Languages Design and Implementation. TLDI ’03 (2003)
18. Launchbury, J., Peyton Jones, S.L.: State in Haskell. LISP and Symbolic Computation 8(4), 293–341 (1995)
19. Le Botlan, D., Rémy, D.: MLF: Raising ML to the power of system F. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional
Programming. ICFP ’03 (2003)
20. Leijen, D.: HMF: Simple type inference for first-class polymorphism. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming. ICFP ’08 (2008)
21. Leroy, X., et al.: The CompCert verified compiler. Documentation and users manual. INRIA Paris-Rocquencourt (2012)
22. Miller, D.: Abstract syntax for variable binders: An overview. In: CL 2000: Computational Logic. Lecture Notes in Artificial Intelligence (2000)
23. Milner, R.: A theory of type polymorphism in programming. Journal of computerand system sciences 17(3), 348–375 (1978)
24. Naraschewski, W., Nipkow, T.: Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning 23(3), 299–318 (1999)
25. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higherorder logic, vol. 2283. Springer Science & Business Media (2002)
26. Odersky, M., Läufer, K.: Putting type annotations to work. In: Proceedings of the
23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’96 (1996)
27. Reed, J.: Higher-order constraint simplification in dependent type theory. In: Proceedings of the Fourth International Workshop on Logical Frameworks and MetaLanguages: Theory and Practice. LFMTP ’09 (2009)
28. Reynolds, J.C.: Types, abstraction and parametric polymorphism. Information
Processing pp. 513–523 (1983)

18

29. The Coq development team: The Coq proof assistant (2017), https://coq.inria.fr/
30. The PureScript development team: PureScript (2017), http://www.purescript.org/
31. Tiuryn, J., Urzyczyn, P.: The subtyping problem for second-order types is undecidable. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science(1996)
32. Urban, C.: Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning
40(4), 327–356 (2008)
33. Urban, C., Nipkow, T.: Nominal verification of algorithm W. From Semantics toComputer Science. Essays in Honour of Gilles Kahn pp. 363–382 (2008)
34. Vytiniotis, D., Weirich, S., Peyton Jones, S.: FPH: First-class polymorphism for
Haskell. In: Proceedings of the 13th ACM SIGPLAN International Conference on
Functional Programming. ICFP ’08 (2008)
35. Wells, J.B.: Typability and type checking in system F are equivalent and undecidable. Annals of Pure and Applied Logic 98(1-3), 111–156 (1999)

19