Formalized Higher-Ranked Polymorphic Type Inference
Algorithms
byJinxu Zhao(赵锦煦)

A thesis submitted in partial fulfillment of the requirements forthe degree of Doctor of Philosophy
at The University of Hong Kong

July 2021

Abstract of thesis entitled“Formalized Higher-Ranked Polymorphic Type Inference Algorithms”
Submitted by
Jinxu Zhao
for the degree of Doctor of Philosophy
at The University of Hong Kong
in July 2021

Modern functional programming languages, such as Haskell or OCaml, use sophisticated formsof type inference. In the meantime, more and more object-oriented programming languages implement advanced type inference algorithms, which greatly reduces the number of redundant anduninteresting types written by programmers, including C++11, Java 10, and C# 3.0. While being
an important topic in the Programming Languages research, there is little work on the mechanization of the metatheory of type inference in theorem provers.
In particular, we are unaware of any complete formalization of the type inference algorithms
that are the backbone of modern programming languages. This thesis presents the first full mechanical formalizations of the metatheory for three higher-ranked polymorphic type inference
algorithms. Higher-ranked polymorphism is an advanced feature that enables more code reuseand has numerous applications, which is already implemented in languages like Haskell. All
three systems are based on the bidirectional type system by Dunfield and Krishnaswami (DK).
The DK type system has two variants, a declarative and an algorithmic one, that have been manually proven sound, complete, and decidable. While DK’s original formalization comes with very
well-written manual proofs, there are several missing details and some incorrect proofs, which
motivates us to fully formalize the metatheory in proof assistants.
Our first system focuses on the core problem in higher-ranked type inference algorithms —the subtyping relation. Our algorithm differs from those currently in the literature by using anovel approach based on worklist judgments. Worklist judgments simplify the propagation of
information required by the unification process during subtyping. Furthermore, they enable a
simple formulation of the meta-theoretical properties, which can be easily encoded in theorem
provers. We formally prove soundness, completeness, and decidability of the subtyping algorithm
w.r.t DK’s declarative specification.
The second system extends the first one with a type system. We present a mechanical formalization of DK’s declarative type system with a novel algorithmic system. This system further

unifies contexts with judgments, which precisely captures the scope of variables and simplifies
the formalization of scoping in a theorem prover. Besides, the use of continuation-passing-style
judgments allows simple formalization for inference judgments. We formally prove soundness,completeness, and decidability of the type inference algorithm. Despite the use of a different algorithm, we prove the same results as DK, although with significantly different proofs and proof
techniques.
The third system is based on the second one and extended with object-oriented subtyping. In
presence of object-oriented subtyping, meta-variables usually have multiple different solutions.
Therefore we present a backtracking-based algorithm that non-deterministically checks against
each possibility. We prove soundness w.r.t our specification, and also completeness under the
rank-1 restriction.
Since such type inference algorithms are quite subtle and have a complex metatheory, mechanical formalizations are an important advance in type-inference research. With machine-checked
proofs, there is little chance that any logical derivation goes wrong. In this thesis, all the properties
we declare are fully formalized in the Abella theorem prover.

An abstract of exactly 483 words

To my beloved parents and grandparents

Declaration
I declare that this thesis represents my own work, except where due acknowledgment is made,and that it has not been previously included in a thesis, dissertation or report submitted to this
University or to any other institution for a degree, diploma or other qualifications.

............................
Jinxu Zhao
July 2021iAcknowledgments
First, I would like to give my most sincere thanks to my supervisor Prof. Bruno C. d. S. Oliveira.
Six years ago, I was lucky to get a chance to exchange to HKU and took two courses taught by
Bruno, and both of them are quite challenging and interesting at the same time. Since then,I decided to explore more on programming languages and therefore applied for Bruno’s Ph.D.
student. It turns out to be a wise choice! Regular meetings with him are usually quite informative,
encouraging and fun. Bruno is a very patient person; he always provides professional suggestions
on how to proceed with the research when I get stuck or move in the wrong direction. In short,
I would never expect a better supervisor.
Collaborations in research have been unforgettable experiences. Prof. Tom Schrijvers offered
help on my type inference project, giving me invaluable ideas and suggestions on both research,
writing, and presentation. This piece of work contributes to the most recognized publications
during my Ph.D., which won the distinguished paper award in ICFP. I also participated in projectsof my colleagues Xuejing Huang and Yaoda Zhu, which are both challenging and interesting. I
learned a lot from you as well. I would like to thank everyone in the group, for your enlightening
seminars and discussions: Tomas Tauber, Huang Li, Xuan Bi, Haoyuan Zhang, Yanlin Wang, Yanpeng Yang, Weixin Zhang, Ningning Xie, Xuejing Huang, Yaoda Zhou, Baber Rehman, Mingqi
Xue, Yaozhu Sun, Wenjia Ye, Xu Xue, Chen Cui, Jinhao Tan.
Study and life in HKU were wonderful. Staff from various sections of the university are kind
and willing to help. I would like to also thank Dr. Francois Pottier, Prof. Chuan Wu, Prof. Ravi
Ramanathan for your detailed review and precious feedbacks on my thesis.
I would also like to thank my friends who study or work in Hong Kong. Discussions with Ge
Bai were always insightful and fun. Gatherings with high school classmates, including those who
visit Hong Kong for a short time, were memorable: Yunze Deng, Bintao Sun, Lu Lu, Tong Yu,
Junfeng Chen, Zhiyu Wan, Ran You, Yiyao Xu, Yiming Hu, Hengyun Zhou, Jinglong Zhao.
Last but not least, my family is always supporting and encouraging. My parents, grandparents,
uncles and aunts give me warm advice through my difficult times and on important decisions.
Above all, I would like to offer my grateful thanks to my wife Jingyu Zhao for your love, tolerance
and constant support. You are the one who understands me the best, for being classmates in
middle school and high school, and we are both Ph.D. candidates in HKU. Even when I feelii

desperate, the time spent with you is always delightful and encouraging. Life would be muchharder without you.

iii

Contents
Declarationi

Acknowledgmentsii

List of Figures

viii

List of Tablesx

I

Prologue

1

1

Introduction

2

1.1

Type Systems and Type Inference Algorithms . . . . . . . . . . . . . . . . . . .

2

1.1.1

Functional Programming and System F . . . . . . . . . . . . . . . . . .

4

1.1.2

Hindley-Milner Type System . . . . . . . . . . . . . . . . . . . . . . . .

5

1.1.3

Higher-Ranked Polymorphism . . . . . . . . . . . . . . . . . . . . . . .

6

1.1.4

Bidirectional Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7

1.1.5

Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

8

1.2

Mechanical Formalizations and Theorem Provers . . . . . . . . . . . . . . . . .

9

1.3

Contributions and Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

102

Background

13

2.1

Hindley-Milner Type System . . . . . . . . . . . . . . . . . . . . . . . . . . . .

13

2.1.1

Declarative System . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

13

2.1.2

Algorithmic System and Principality . . . . . . . . . . . . . . . . . . . .

15

Odersky-Läufer Type System . . . . . . . . . . . . . . . . . . . . . . . . . . . .

16

2.2.1

Higher-Ranked Types . . . . . . . . . . . . . . . . . . . . . . . . . . . .

17

2.2.2

Declarative System . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

17

2.2.3

Relating to HM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

20

Dunfield-Krishnaswami Bidirectional Type System . . . . . . . . . . . . . . . .

20

2.3.1

21

2.2

2.3

Declarative System . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

iv

Contents

2.4

MLsub . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

23

2.4.1

Types and Polar Types . . . . . . . . . . . . . . . . . . . . . . . . . . . .

23

2.4.2

Biunification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

25

IIHigher-Ranked Type Inference Algorithms

26

3

Higher-Ranked Polymorphism Subtyping Algorithm

27

3.1

Overview: Polymorphic Subtyping . . . . . . . . . . . . . . . . . . . . . . . . .

27

3.1.1

Declarative Polymorphic Subtyping . . . . . . . . . . . . . . . . . . . .

27

3.1.2

Finding Solutions for Variable Instantiation . . . . . . . . . . . . . . . .

28

3.1.3

The Worklist Approach . . . . . . . . . . . . . . . . . . . . . . . . . . .

30

A Worklist Algorithm for Polymorphic Subtyping . . . . . . . . . . . . . . . . .

31

3.2.1

Syntax and Well-Formedness of the Algorithmic System . . . . . . . . .

31

3.2.2

Algorithmic Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . .

32

Metatheory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

35

3.3.1

Transfer to the Declarative System . . . . . . . . . . . . . . . . . . . . .

35

3.3.2

Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

36

3.3.3

Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

36

3.3.4

Decidability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

37

The Choice of Abella . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

38

3.4.1

41

3.2

3.3

3.4

4

Statistics and Discussion . . . . . . . . . . . . . . . . . . . . . . . . . .

A Type-Inference Algorithm for Higher-Ranked Polymorphism

42

4.1

Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

43

4.1.1

DK’s Declarative System . . . . . . . . . . . . . . . . . . . . . . . . . . .

44

4.1.2

DK’s Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

46

4.1.3

Judgment Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

49

4.1.4

Single-Context Worklist Algorithm for Subtyping . . . . . . . . . . . . .

50

4.1.5

Algorithmic Type Inference for Higher-Ranked Types: Key Ideas . . . .

51

Algorithmic System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

52

4.2.1

Syntax and Well-Formedness . . . . . . . . . . . . . . . . . . . . . . . .

52

4.2.2

Algorithmic System . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

54

Metatheory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

60

4.3.1

Declarative Worklist and Transfer . . . . . . . . . . . . . . . . . . . . .

60

4.3.2

Non-Overlapping Declarative System . . . . . . . . . . . . . . . . . . .

62

4.3.3

Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

65

4.3.4

Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

66

4.2

4.3

v

Contents

4.4

5

4.3.5

Decidability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

67

4.3.6

Abella and Proof Statistics . . . . . . . . . . . . . . . . . . . . . . . . . .

70Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

73

4.4.1

Contrasting Our Scoping Mechanisms with DK’s . . . . . . . . . . . . .

73

4.4.2

Elaboration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

74

4.4.3

Lexically-Scoped Type Variables . . . . . . . . . . . . . . . . . . . . . .

75

Higher-Ranked Polymorphism with Object-Oriented Subtyping

77

5.1

Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

77

5.1.1

Type Inference in Presence of Subtyping . . . . . . . . . . . . . . . . . .

77

5.1.2

Judgment List and Eager Substitution . . . . . . . . . . . . . . . . . . .

79

5.1.3

Our Solution: Backtracking Algorithm . . . . . . . . . . . . . . . . . . .

80

5.2

Declarative System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

81

5.3

Backtracking Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

82

5.3.1

Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

82

5.3.2

Algorithmic Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . .

83

5.3.3

Algorithmic Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

86

Metatheory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

87

5.4.1

Declarative Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . .

88

5.4.2

Transfer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

90

5.4.3

Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

91

5.4.4

Partial Completeness of Subtyping: Rank-1 Restriction . . . . . . . . . .

92

5.4.5

Algorithmic Rank-1 Restriction (Partial Completeness) . . . . . . . . . .

92

5.4.6

Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

93

5.4.7

Formalization in the Abella Proof Assistant . . . . . . . . . . . . . . . .

94

Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

95

5.5.1

A Complete Algorithm Under Monotype Guessing Restrictions . . . . .

95

5.5.2

Lazy Substitution and Non-terminating Loops . . . . . . . . . . . . . . .

96

5.4

5.5

III Related Work

99

6

100

Related Work
6.1

6.2

Higher-Ranked Polymorphic Type Inference Algorithms . . . . . . . . . . . . . 100
6.1.1

Predicative Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . 100

6.1.2

Impredicative Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . 101

Type Inference Algorithms with Subtyping . . . . . . . . . . . . . . . . . . . . . 103

vi

Contents

6.3

6.4

Techniques Used in Type Inference Algorithms . . . . . . . . . . . . . . . . . . 104
6.3.1

Ordered Contexts in Type Inference . . . . . . . . . . . . . . . . . . . . 104

6.3.2

The Essence of ML Type Inference . . . . . . . . . . . . . . . . . . . . . 104

6.3.3

Lists of Judgments in Unification . . . . . . . . . . . . . . . . . . . . . . 104

Mechanical Formalization of Polymorphic Type Systems . . . . . . . . . . . . . 105

IV Epilogue

106

7

107

Conclusion and Future Work
7.1

Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107

7.2

Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108

Bibliography

112

vii

List of Figures
2.1

HM Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

14

2.2

HM Type System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

14

2.3

Syntax of Odersky-Läufer System . . . . . . . . . . . . . . . . . . . . . . . . . .

18

2.4

Well-formedness of types in the Odersky-Läufer System . . . . . . . . . . . . . .

18

2.5

Subtyping of the Odersky-Läufer System . . . . . . . . . . . . . . . . . . . . . .

19

2.6

Typing of the Odersky-Läufer System . . . . . . . . . . . . . . . . . . . . . . . .

19

2.7

Syntax of Declarative System . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

21

2.8

Declarative Well-formedness and Subtyping . . . . . . . . . . . . . . . . . . . .

22

2.9

Declarative Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

23

2.10 Types of MLsub . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

24

3.1

Syntax of Declarative System . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

28

3.2

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

28

3.3

Syntax and Well-Formedness judgment for the Algorithmic System. . . . . . . .

32

3.4

Algorithmic Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

33

3.5

A Success Derivation for the Algorithmic Subtyping Relation . . . . . . . . . . .

34

3.6

A Failing Derivation for the Algorithmic Subtyping Relation . . . . . . . . . . .

34

3.7

Transfer Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

36

3.8

Statistics for the proof scripts . . . . . . . . . . . . . . . . . . . . . . . . . . . .

40

4.1

Syntax of Declarative System (Extends Figure 3.1) . . . . . . . . . . . . . . . . .

44

4.2

Declarative Well-formedness and Subtyping . . . . . . . . . . . . . . . . . . . .

44

4.3

Declarative Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

45

4.4

Extended Syntax and Well-Formedness for the Algorithmic System . . . . . . . .

53

4.5

Algorithmic Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

55

4.6

A Sample Derivation for Algorithmic Typing . . . . . . . . . . . . . . . . . . . .

60

4.7

Declarative Worklists and Instantiation . . . . . . . . . . . . . . . . . . . . . . .

60

4.8

Declarative Transfer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

61

4.9

Context Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

63

4.10 Worklist measures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

68

4.11 Worklist Update . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

69

viii

List of Figures

5.1

Declarative Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

81

5.2

Declarative Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

81

5.3

Declarative Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

82

5.4

Algorithmic Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

83

5.5

Algorithmic Garbage Collection and Subtyping . . . . . . . . . . . . . . . . . .

84

5.6

Algorithmic Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

87

5.7

Declarative Worklists and Instantiation . . . . . . . . . . . . . . . . . . . . . . .

91

5.8

Declarative Transfer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

91

ix

List of Tables
4.1

Statistics for the proof scripts . . . . . . . . . . . . . . . . . . . . . . . . . . . .

71

4.2

Translation Table for the Proof Scripts . . . . . . . . . . . . . . . . . . . . . . .

72

5.1

Statistics for the proof scripts . . . . . . . . . . . . . . . . . . . . . . . . . . . .

94

xPart I
Prologue11 Introduction
1.1 Type Systems and Type Inference Algorithms
Statically typed programming languages are widely used nowadays. Programs are categorized byvarious types before they are compiled and executed. Type errors caught before execution usuallyindicate potential bugs, letting the programmers realize and correct such errors in advance.
In the early stages, programming languages like Java (before 1.5) were built on a simple type system, where only features like primitive types, explicitly-typed functions, and non-generic classes
are supported. People soon realized the need to generalize similar programs that have different
types when used. For example, a simple way to define a function that swaps the first two items in
an integer array isvoid swap2(int[] arr) {int t = arr[0];arr[0] = arr[1];arr[1] = t;}
Similarly, the swap function for a float array can be defined as
void swap2(float[] arr) {float t = arr[0];arr[0] = arr[1];arr[1] = t;}which mostly shares the same body with the above definition for integer array, except that thetype of element in the array changes from int to float. If such functionality is a commonlyused one, such as the sorting function, we definitely want to define it once and use it on many
types, such as int, float, double, String, etc. Luckily, later versions of Java (1.5 and above) provides
a way to define a generic function that accepts input of different types:<T> void swap2_generic(T[] arr) {2

1 Introduction

T t = arr[0];arr[0] = arr[1];arr[1] = t;}where T denotes a generic type that programmers may arbitrarily pick. The swap2_genericfunction utilizes the feature of Java’s type system, generics, to improve modularity. The following
program invokes the generic function (suppose we defined the swap2_generic function in a
Utils class as a static method)
Double[] arr = new Double[2];arr[0] = 1.0; arr[1] = 2.0;
Utils.<Double>swap2_generic(arr);
System.out.println(arr[0] + " " + arr[1]);However, the type parameter <Double> seems a bit redundant: given the type of arr is Double[],the generic variable T can only be Double. In fact, with the help of type inference, we can simply
write
Utils.swap2_generic(arr);
to call the function. When compiling the above code, type inference algorithms help programmers to fill in the missing type automatically, thus saving them from writing redundant code.
From the example above, we learn that the generics of Java together with type inference algorithms used in the compiler help programmers to write generic functions, given that the functionality is generic in nature. In other words, good features introduced to type systems accept
more meaningful programs.
On the other hand, being able to accept all syntactically correct programs, as dynamicallytyped programming languages do, is not desirable as well. Ill-typed programs are easy to writeby mistake, like "3" / 3; or even well-typed programs with ambiguous/unexpected meaning
like "3" + 4 + 5 (for someone who is not familiar with the conventions, she might think thisevaluates to ”39”). Or even more commonly seen in practice, an accidentally misspelled variablename does not cause a runtime error until the line of code is actually executed. Type systems aredesigned to prevent such problems from happening, therefore statically-typed languages ensure
type-safety, or “well-typed programs cannot go wrong”. Type inference algorithms that comealong with modern type systems help eliminate trivial or redundant parts of programs to improvethe conciseness.

3

1 Introduction

1.1.1 Functional Programming and System F
Nowadays, more and more programming languages support the functional programming paradigm,
where functions are first-class citizens, and programs are mostly constructed with function applications. Functional programming originates from the lambda calculus [Church 1932]. The
simply-typed lambda calculus [Church 1941] extends the lambda calculus with a simple static
type checking algorithm, preventing ill-typed programs before actual execution. However, thesystem does not allow polymorphic functions and thus is quite tedious to express higher-level
logic.
In order to improve the expressiveness of functional programming languages, System F [Girard
1971, 1972; Reynolds 1974] introduces polymorphism via the universal quantifier ∀ for types
and the Λ binder (to introduce type-level functions) for expressions. For example, the identity
function that can range over any type of the form A → A can be encoded in System F:
id = Λa. λx : a. x : ∀a. a → a
To enjoy the polymorphism of such a function, one needs to first supply a type argument likeid @Int (we use the @ sign to denote a type-level application), so that the polymorphic function
is instantiated with a concrete type.
Implicit Parametric Polymorphism Although being much more expressive than simplytyped systems, plain System F is still tedious to use. It feels a bit silly to write id @Int 3 comparedwith id 3, because the missing type is quite easy to figure out, in presence of the argument, which
is of type Int and should represent a for the function application at the same time. With implicit
parametric polymorphism [Milner 1978], type arguments like @Int are not written by the programmer explicitly, in contrast, it is the type inference algorithm’s responsibility to guess them.
Practically speaking, in Java we can define the identity function as well,<T> T id(T x) {return x;}
And we typically use the function without specifying the type parameters, because the type systemalready supports implicit parametric polymorphism:
int n = id(3);String s = id("3");Theoretically speaking, it is unfortunate that there does not exist such a perfect algorithm that
can automatically guess missing type applications for every possible System F program [Tiuryn

41 Introduction

and Urzyczyn 1996]. For example, the following expression is ambiguous when the implicit typeargument is not given:f = (choose : ∀a. a → a → a) (id : ∀b. b → b)
It is unclear how the type variable is instantiated during the polymorphic application: one possibility is that a is chosen to be the type of id, or ∀b. b → b, resulting in the type (∀b. b → b) →(∀b. b → b) (Note that we cannot express this type in programming languages like Java, simply
because the ∀ quantifiers do not appear at the top level, and its type system is already a restrictedversion of System F). However, another valid type is ∀b. (b → b) → (b → b), which is obtainedby first instantiating id with a fresh type variable b, and generalizing the type after calculating thetype of the application. Furthermore, between the two possible types, neither one is better: there
exist programs that type check under either one of them and fail to type check under the other.
The fact that implicit parametric algorithm for full System F is impossible motivates people
to discover restrictions on the type system under which type inference algorithms are capable ofguessing the best types.

1.1.2 Hindley-Milner Type System
The Hindley-Milner (henceforth denoted as HM) type system [Damas and Milner 1982; Hindley
1969; Milner 1978] restricts System F types to type schemes, or first-order polymorphism, wherepolymorphic types can only have universal quantifiers in the top level. For example, ∀a b. (a →b) → a → b is allowed, but not (∀b. b → b) → (∀b. b → b). The type system of many
programming languages like Java adopts the idea from HM, where generics is a syntax to express
polymorphic types in HM: all the generic variables must be declared at the top level before thefunction return type. An important property of the HM type inference algorithm is principality,
where any unannotated program can be inferred to a most general type within its type system.
This supports full type-inference without any type annotations.
For example, the following functiong = λx. λy. x
can be assigned to types Int → Bool → Int, Int → Int → Int or infinitely many others. The
HM inference algorithm will infer a more general type ∀a. ∀b. a → b → a. In order to use the51 Introduction
function as the types mentioned above, a more-general-than relation ≤ is used to describe thatthe polymorphic type can be instantiated to more concrete types:∀a. ∀b. a → b → a ≤ Int → Bool → Int∀a. ∀b. a → b → a ≤ Int → Int → Int∀a. ∀b. a → b → a ≤ ∀a. a → a → a
Predicativity In the HM system, ∀ quantifiers can appear only on the top level, type instantiations will always be monotypes, i.e. types without the ∀ quantifier. We refer to such a system aspredicative. In contrast, System F does not restrict the types to instantiate, thus being an impredicative system. An important challenge is that full type inference for impredicative polymorphism
is known to be undecidable [Wells 1999]. There are works that focus on practical inference of impredicative systems [Emrich et al. 2020; Le Botlan and Rémy 2003; Leijen 2008; Serrano et al.
2020, 2018; Vytiniotis et al. 2008]. However, throughout this work, we study predicative typesystems only.

1.1.3 Higher-Ranked Polymorphism
As functional languages evolved, the need for more expressive power has motivated language
designers to look beyond HM, where there is still one obvious weakness that prevents some useful programs to type check: HM only have types of rank-1, since all the ∀’s appear on the top
level. Thus one expected feature is to allow higher-ranked polymorphism where polymorphic types
can occur anywhere in a type signature. This enables more code reuse and more expressions totype check, and has numerous applications [Gill et al. 1993; Jones 1995; Lämmel and Jones 2003;
Launchbury and Peyton Jones 1995].
One of the interesting examples is the ST monad [Launchbury and Peyton Jones 1994] of
Haskell, where the runST function is only possible to express in a rank-2 type system:
runST :: ∀a. (∀s. ST s a) → a
The type is rank-2 because of the inner ∀ quantifier in the argument position of the type. Such atype encapsulates the state and makes sure that program states from different computation threads
do not escape their scopes, otherwise the type checker should reject in advance.
In order to support higher-ranked types, we need to extend the type system of HM, but not
taking a too big step since type inference for full System F would be impossible. A simple polymorphic subtyping relation proposed by Odersky and Läufer [1996] extends the HM system byallowing higher-ranked types, but instantiations are still limited to monotypes, thus the systemremains predicative.

6

1 Introduction

1.1.4 Bidirectional Typing
In order to improve the expressiveness for higher-ranked systems, some type annotations arenecessary to guide type inference. In response to this challenge, several decidable type systems
requiring some annotations have been proposed [Dunfield and Krishnaswami 2013; Le Botlan
and Rémy 2003; Leijen 2008; Peyton Jones et al. 2007; Serrano et al. 2018; Vytiniotis et al. 2008].
As an example,
hpoly = λ(f : ∀a. a → a). (f 1, f ′ c′ )the type of hpoly is (∀a. a → a) → (Int, Char), which is a rank-2 type and is not typeable in
HM. Notably (and unlike Hindley-Milner) the lambda argument f requires a polymorphic type
annotation. This annotation is needed because 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 thefunction.
One of the key features that improve type inference algorithms with type annotations is bidirectional typing [Pierce and Turner 2000], a technique that combines two modes of typing: typechecking, which checks an expression against a given type, and type synthesis (inference), which
infers a type from an expression. Bidirectional typing is quite useful when the language supports
type annotations, because those “hints” are handled with the checking mode. With bidirectional
type-checking the typing judgment has two modes. In the checking mode Γ ⊢ e ⇐ A both e
and A are inputs: i.e. we check whether expression e has some type A. In the synthesis modeΓ ⊢ e ⇒ A only e is an input: we need to calculate the output type A from the input expression e.
It is clear that, with less information, the synthesis mode is more difficult to implement than the
checking mode. Therefore, bidirectional type checking with type annotations provides a way forthe programmer to guide the type inference algorithm when the expression is tricky to analyse,
especially in the case where higher-ranked types are involved. In addition, bidirectional typing
algorithms improve the quality of error messages in practice, due to the fact that they report errors
in a relatively local range, compared with global unification algorithms.
Two closely related type systems that support predicative higher-ranked type inference were
proposed by Peyton Jones et al. [Peyton Jones et al. 2007] and Dunfield and Krishnaswami [Dunfield and Krishnaswami 2013] (henceforth denoted as DK). These type systems are popular among
language designers and their ideas have been adopted by several modern functional languages, including Haskell, Unison [Chiusano and Bjarnason 2015] and PureScript [Freeman 2017] among
others.
DK developed a higher-ranked global bidirectional type system based on the declarative system
by Odersky and Läufer [Odersky and Läufer 1996]. Beyond the existing works, they introduce
a third form of judgment, the application inference A • e ⇒⇒ C, where the function type A
and argument expression e are input, and type C is the output representing the result type of the7

1 Introduction

function application (f :: A) e. Note that f does not appear in this relation, and one can tell theprocedure for type checking application expressions from the shape of the judgment — firstly,
the type of the function is inferred to A; then the application inference judgment is reduced toa checking judgment to verify if the argument e checks against the argument part of A; finally,
output the return part of A. Formally, the rules implement the procedure we described above:Ψ ⊢ e1 ⇒ A Ψ ⊢ A • e2 ⇒⇒ C
Ψ ⊢ e1 e2 ⇒ C

Decl→EΨ⊢e⇐AΨ ⊢ A → C • e ⇒⇒ C

Decl→AppThe use of application inference judgment avoids implicit instantiations of types like HM, instead,when the function type A is a polymorphic type, it is explicitly instantiated by the application
inference until it becomes a function type:Ψ⊢τΨ ⊢ [τ /a]A • e ⇒⇒ C

Ψ ⊢ ∀a. A • e ⇒⇒ C

Decl∀AppAs a result, DK is in a more syntax-directed system compared with HM-like systems.
DK also provided an elegant formalization of their sound and complete algorithm, which has
also inspired implementations of type inference in some polymorphic programming languages(such as PureScript [Freeman 2017] or DDC [Disciple Development Team 2017]).
The focus of this thesis is also on predicative implicit higher-ranked bidirectional type inference
algorithms.

1.1.5 Subtyping
The term “subtyping” is used as two slightly different concepts in this thesis. One of them refers
to the polymorphic subtyping relation used in polymorphic type systems, which compares thedegree of polymorphism between types, i.e. the more-general-than relation. Chapters 3 and 4
only focus on this type of subtyping relation. The other one is the subtyping usually seen in objectoriented programming, where there are some built-in or user-defined type conversion rules.
Type system in presence of object-oriented-style subtyping allows programmers to abstract
functionalities inside a class and thus benefit from another form of polymorphism. Introduced
by Cardelli [1988]; Mitchell [1984]; Reynolds [1985], subtyping is studied for explicitly typed
programs. Compared with functional programming languages, mainstream object-oriented languages lacks competitive type inference algorithms. We will further introduce object-oriented
subtyping as a feature in Chapter 5, where we also introduce the top and bottom types as theminimal support for subtyping.

8

1 Introduction

1.2 Mechanical Formalizations and Theorem Provers
Although type inference is important in practice and receives a lot of attention in academic research, there is little work on mechanically formalizing such advanced forms of type inference intheorem provers. The remarkable exception is work done on the formalization of certain partsof Hindley-Milner type inference [Dubois 2000; Dubois and Menissier-Morain 1999; Garrigue
2015; Naraschewski and Nipkow 1999; Urban and Nipkow 2008]. However, there is still noformalization of the higher-ranked type systems that are employed by modern languages like
Haskell. This is at odds with the current trend of mechanical formalizations in programming
language research. In particular, both the POPLMark challenge [Aydemir et al. 2005] and CompCert [Leroy et al. 2012] have significantly promoted the use of theorem provers to model various aspects of programming languages. Today, papers in various programming language venues
routinely use theorem provers to mechanically formalize: dynamic and static semantics and theircorrectness properties [Aydemir et al. 2008], compiler correctness [Leroy et al. 2012], correctness of
optimizations [Bertot et al. 2006], program analysis [Chang et al. 2006] or proofs involving logicalrelations [Abel et al. 2018].
Motivations for Mechanical Formalizations. The main argument for mechanical formalizations is a simple one. Proofs for programming languages tend to be long, tedious, anderror-prone. In such proofs, it is very easy to make mistakes that may invalidate the whole development. Furthermore, readers and reviewers often do not have time to look at the proofs
carefully to check their correctness. Therefore errors can go unnoticed for a long time. In fact,manual proofs are commonly observed to have flaws that invalidate the claimed properties. For
instance, Klein et al. [2012] reproduced the proofs of nine ICFP 2009 papers in Redex, and foundproblems in each one of them. We also found false lemmas and incorrect proofs in DK’s manual proof [Dunfield and Krishnaswami 2013]. Mechanical formalizations provide, in principle, anatural solution for these problems. Theorem provers can automatically check and validate theproofs, which removes the burden of checking from both the person doing the proofs as well as
readers or reviewers.
Moreover, extending type-inference algorithms with new programming language features isoften quite delicate. Studying the meta-theory for such extensions would be greatly aided by theexistence of a mechanical formalization of the base language, which could then be reused andextended by the language designer. Compared with manual proofs which may take a long time
before one can fully understand every detail, theorem provers can quickly point out proofs thatare invalidated after extensions.

91 Introduction

Challenges in Variable Binding and Abella. Handling variable binding is particularly
challenging in type inference, because the algorithms typically do not rely simply on local environments, but instead propagate information across judgments. Yet, there is little work on how todeal with these complex forms of binding in theorem provers. We believe that this is the primaryreason why theorem provers have still not been widely adopted for formalizing type-inference
algorithms.
The Abella theorem prover [Gacek 2008] is one that specifically eases formalization onbinders.
Two common treatments of binding are to use the De Bruijn indices [de Bruijn 1972] and thenominal logic framework of Pitts [Pitts 2003]. In contrast, Abella uses the abstraction operator
in a typed λ-calculus to encode binding. Its λ-tree syntax, or HOAS, and features including the∇ quantifier and higher-order unification, allow for better experiences than using Coq libraries
utilizing other approaches. In practice, Abella uses the ∇ (nabla) quantifier and nominal constants to help quantify a “fresh” variable during formalization. For example, the common typechecking rulee⇐Aa freshe ⇐ ∀a. A
is encoded as
check E (all A) := nabla a, check E (A a)in Abella, where the ∇ quantifier introduces a fresh type variable a and later use it to “open” thebody of ∀a. A.
Throughout the thesis, all the type systems and declared properties are mechanically formalized
in Abella.

1.3 Contributions and Outline
Contributions In this thesis, we propose variants of type inference algorithms for higherranked polymorphic type systems and formalize each of them in the Abella theorem prover. It
is the first work on higher-ranked type inference that comes with mechanical formalizations. In
summary, the main contributions of this thesis are:• Chapter 3 presents a predicative polymorphic subtyping algorithm.
– We proved that our algorithm is sound, complete, and decidable with respect to OL’s
higher-ranked subtyping specification in the Abella theorem prover. And we are thefirst to formalize the meta-theoretical results of a polymorphic higher-ranked subtyping algorithm.

10

1 Introduction– Similar to DK’s algorithm, we employ an ordered context to collect type variables
and existential variables (used as placeholders for guessing monotypes). However,
our unification process is novel. DK’s algorithm solves variables on-the-fly and communicates the partial solutions through an output context. In contrast, our algorithm
collects a list of judgments and propagate partial solutions across them via eager substitutions. Such technique eliminates the use of output contexts, and thus simplifies
the metatheory and makes mechanical formalizations easier. Besides, using only asingle context keeps the definition of well-formedness simple, resulting in an easy
and elegant algorithm.
• Chapter 4 presents a new bidirectional higher-ranked typing inference algorithm based on
DK’s declarative system.
– We are the first to present a full mechanical formalization for a type inference algorithm of higher-ranked type system. The soundness, completeness, and decidability
are shown in the Abella theorem prover, with respect to DK’s declarative system.
– We propose worklist judgments, a new technique that unifies ordered contexts andjudgments. This enables precise scope tracking of variables in judgments and avoids
the duplication of context information across judgments in worklists. Similar to theprevious algorithm, partial solutions are propagated across judgments in a single list
consist of both variable bindings and judgments. Nevertheless, the unification ofworklists and contexts exploits the fact that judgments are usually sharing a large partof common information. And one can easily tell when a variable is no longer referredto.
– Furthermore, we support inference judgments so that bidirectional typing can be encoded as worklist judgments. The idea is to use a continuation passing style to enable
the transfer of inferred information across judgments.
• Chapter 5 further extends the higher-ranked system with object-oriented subtyping.
– We propose a bidirectional declarative system extended with the top and bottom types
and relevant subtyping and typing rules. Several desirable properties are satisfied andmechanically proven.
– A new backtracking-based worklist algorithm is presented and proven to be soundwith respect to our declarative specification in the Abella theorem prover. Extended
with subtyping relations of the top and bottom types, simple solutions such as ⊤ or ⊥satisfies subtyping constraints in parallel with other solutions witch does not involve
object-oriented subtyping. Our backtracking technique is specifically well-suited forthe non-deterministic trial without missing any of them.

11

1 Introduction– We also formalize the rank-1 restriction of subtyping relation, and proved that ouralgorithmic subtyping is complete under such restriction.
Prior Publications. This thesis is partially based on the publications by the author [Zhao et al.
2018, 2019], as indicated below.
Chapter 3: Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018. “Formalization of
a Polymorphic Subtyping Algorithm”. In International Conference on Interactive Theorem
Proving (ITP).
Chapter 4: Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. “A Mechanical
Formalization of Higher-Ranked Polymorphic Type Inference”. In International Conference
on Functional Programming (ICFP).
Mechanized Proofs. All proofs in this thesis is mechanically formalized in the Abella theorem prover and are available online:
Chapter 3: https://github.com/JimmyZJX/Abella-subtyping-algorithm
Chapter 4: https://github.com/JimmyZJX/TypingFormalization
Chapter 5: https://github.com/JimmyZJX/Dissertation/tree/main/src

12

2 BackgroundIn this chapter, we introduce some highly related type systems. They are basic concepts andshould help the reader understand the rest of the thesis better. Section 2.1 introduces the HindleyMilner type system [Damas and Milner 1982; Hindley 1969; Milner 1978], a widely used systemthat supports rank-1 (prenex) polymorphism. Section 2.2 presents the Odersky-Läufer type system, which is an extension of the Hindley-Milner by allowing higher-ranked types. Section 2.3
describes the Dunfield-Krishnaswami bidirectional type system, a bidirectional type system thatfurther extends Odersky-Läufer’s. Finally, in Section 2.4 we introduce one of the recent advancements in the ML family, namely the MLsub type system, which integrates object-oriented subtyping with the Hindley-Milner type inference.

2.1 Hindley-Milner Type System
The Hindley-Milner type system, hereafter called “HM” for short, is a classical lambda calculus with parametric polymorphism. Thanks to its simple formulation and powerful inference
algorithm, many modern functional programming languages are still using HM as their base,including the ML family and Haskell. The system is also known as Damas–Milner or Damas–
Hindley–Milner. Hindley [Hindley 1969] and Milner [Milner 1978] independently discovered
algorithms for the polymorphic typing problem and also proved the soundness of their algorithms, despite that there are slight differences in the expressiveness— Milner’s system supports
let-generalization. Later on, Damas and Milner [1982] proved the completeness of their algorithm.

2.1.1 Declarative System
Syntax The declarative syntax is shown in Figure 2.1. The HM types are consist of polymorphic
types (or type schemes) and monomorphic types. A polymorphic type contains zero or more
universal quantifiers only at the top level. When no universal quantifier occurs, the type belongs
to a mono-type. Mono-types are constructed by a unit type 1, a type variable a, or a function type
τ1 → τ2 .
Expressions e includes variables x, literals (), lambda abstractions λx. e, applications e1 e2 andthe let expression let x = e1 in e2 . A context Ψ is a collection of type bindings for variables.

13

2 Background

Type variablesa, bτ | ∀a. σ

Types

σ

::=

Monotypesτ::= 1 | a | τ1 → τ2

Expressionse::=x | () | λx. e | e1 e2 | let x = e1 in e2

ContextsΨ::=· | Ψ, x : σ

Figure 2.1: HM Syntax

σ1 ⊑ σ2 HM Type Instantiation
τ ′ = [τ /a]τb∈
/ FV(∀a. τ )∀a. τ ⊑ ∀b. τ ′HM-TInst

Ψ ⊢HM e : σ HM Typing(x : σ) ∈ ΨΨ ⊢HM x : σ

HM-VarΨ ⊢HM () : 1

Ψ, x : τ1 ⊢HM e : τ2

HM-UnitΨ ⊢HM e1 : τ1 → τ2

Ψ ⊢HM λx. e : τ1 → τ2

Ψ ⊢HM e2 : τ1

HM-AppΨ ⊢HM e1 e2 : τ2
Ψ ⊢HM e1 : σΨ, x : σ ⊢HM e2 : τΨ ⊢HM let x = e1 in e2 : τΨ ⊢HM e : σa∈/ FV(Ψ)Ψ ⊢HM e : ∀a. σ

HM-LetΨ ⊢HM e : σ1

HM-Gen

HM-Absσ1 ⊑ σ2Ψ ⊢HM e : σ2

HM-InstFigure 2.2: HM Type System

Type Instantiation The relations between types are described via type instantiations. The ruleshown to the top of Figure 2.2 checks if ∀a. τ is a generic instance of ∀b. τ ′ . This relation is valid
when τ ′ = [τ /a]τ for a series of mono-types τ and each variable in b is not free in ∀a. τ .
For example,∀a. a → a ⊑ 1 → 1
is obtained by the substitution [1/a], and∀a. a → a ⊑ ∀b. (b → b) → (b → b)
substitutes a by b → b, and generalizes b after the substitution.

14

2 Background
Typing The typing relation Ψ ⊢HM e : σ synthesizes a type σ for an expression e under thecontext Ψ. Rule HM-Var looks up the binding of a variable x in the context. Rule HM-Unit always
gives the unit type 1 to the unit expression (). For a lambda abstraction λx. e, Rule HM-Absguesses its input type (τ1 ) and computes the type of its body (τ2 ) as the return type. Rule HM-App
eliminates a function type by an application e1 e2 , where the argument type must be the same as
the input type of the function, and the type of the whole application is τ2 .
Rule HM-Let is also referred to as let-polymorphism. In (untyped) lambda calculus, let x =e1 in e2 behaves the same as (λx. e2 ) e1 . However, the HM let rule derives the type of e1 first, andbinds the polymorphic type into the context before e2 . This enables polymorphic expressions to
be reused multiple times in different instantiated types.
Rules HM-Gen and HM-Inst change the type of an expression at any time during the derivation.
Rule HM-Gen generalizes over fresh type variables a. Rule HM-Inst, as opposed to generalization,
specializes a type according to the type instantiation relation.
The type system of HM supports implicit instantiation through Rule HM-Inst. This means thatany expression (function) that has a polymorphic type can be automatically instantiated with aproper monotype for any reasonable application. The fact that only monotypes are guessed indicates that the system is predicative. In contrast, an impredicative system might guess polymorphic
types. Unfortunately, type inference on impredicative systems is undecidable [Wells 1999]. In thisthesis, we focus on predicative systems only.

2.1.2 Algorithmic System and Principality
Syntax-Directed System The declarative system is not fully syntax-directed due to Rules
HM-Gen and HM-Inst, which can be applied to any expression. A syntax-directed system canbe obtained by replacing Rules HM-Var and HM-Let by the following rules:Ψ ⊢HM e1 : σa = FV(σ) − FV(Ψ)(x : σ) ∈ Ψσ⊑τΨ ⊢SHM x : τ

HM-Var-InstΨ, x : ∀a. σ ⊢HM e2 : τΨ ⊢SHM let x = e1 in e2 : τ

HM-Let-Gen

A generalization on σ, the synthesized type of e1 , is added to Rule HM-Let, since it is the source
place where a polymorphic type is generated. However, a too generalized type might reject applications due to its shape, therefore, an instantiation procedure is added to eliminate all the universal quantifiers on Rule HM-Var. We omit Rules HM-Unit, HM-Abs, and HM-App for the syntaxdirected system Ψ ⊢SHM . The following property shows that the new system is (almost) equivalent
to the original declarative system.

15

2 Background

Theorem 2.1 (Equivalence of Syntax-Directed System).
1. If Ψ ⊢SHM e : σ then Ψ ⊢HM e : σ
2. If Ψ ⊢HM e : σ then Ψ ⊢HM e : τ , and ∀a. τ ⊑ σ, where a = FV(τ ) − FV(Ψ).
Type Inference Algorithm Although being syntax-directed solves some problems, the rules
still require some guessings, including Rules HM-Abs and HM-Var-Inst. Proposed by Milner[1978], Algorithm W, an inference algorithm of the HM type system based on unification, is
proven to be sound and complete w.r.t the declarative specifications.
Theorem 2.2 (Algorithmic Completeness (Principality)). If Ψ ⊢HM e : σ, then W computes a
principal type scheme σp , i.e.
1. Ψ ⊢HM e : σp
2. σp ⊑ σ.
Note that both the above theorems are not formalized by the author. The reader may refer toan existing formalization of algorithm W, for example, [Naraschewski and Nipkow 1999].

2.2 Odersky-Läufer Type System
The HM type system is simple, powerful, and easy-to-use. However, it only accepts types ofrank-1, i.e. the ∀ quantifier can only appear in the top-level. In practice, there are cases where
higher-ranked types are needed. The rank-1 limitation prevents those programs from type checkand thus loses expressiveness. The problem is that full type inference for System F is proven to be
undecidable [Wells 1999]. Odersky and Läufer [1996] then proposed a system where programmers can make use of type annotations to guide the type system, especially on higher-ranked
types. This extension of HM preserves nice properties of HM, while accepting higher-ranked
types to be checked with the help of the programmers.
For example, consider the following function definition
λf. (f 1, f ′ c′ )This is not typeable in HM, because the argument of the lambda abstraction, f , is applied toboth an integer and a character, which means that it should be of a polymorphic unknown type,thus the type of the lambda abstraction cannot be inferred by the HM type system. This seems
reasonable, since there are several polymorphic types that fit the function, for example,
λf. (f 1, f ′ c′ ) :: (∀a. a → a) → (Int, Char)16

2 Backgroundλf. (f 1, f ′ c′ ) :: (∀a. a → Int) → (Int, Int)
The solution is also natural: if the programmer may pick the type of argument she wants, thetype system can figure out the rest. By adding type annotation on f , OL now accepts the definition
λ(f : ∀a. a → a). (f 1, f ′ c′ )and infers type (∀a. a → a) → (Int, Char).
In what follows, we will first formally define the rank of a type, and then introduce the declarative system of OL, finally discuss the relationship between OL and HM.

2.2.1 Higher-Ranked Types
The rank of a type represents how deep a universal quantifier appears at the contravariant position [Kfoury and Tiuryn 1992]. Formally speaking,

Rank 0 / Monotypes
Rank k(k ≥ 1), Polytypes

τ, σ 0 ::= 1 | a | τ1 → τ2
σk::=σ k−1 | σ k−1 → σ k | ∀a. σ k

The following example illustrates what rank a type belongs to:

1 → 1 Rank 0∀a. a → a Rank 1
1 → ∀a. a → a Rank 1(∀a. a → a) → (∀a. a → a) Rank 2
According to the definition, monotypes are types that does not contain any universal quantifier.
In the HM type system, all polymorphic types have rank 1.

2.2.2 Declarative System
The syntax of Odersky-Läufer system is shown in Figure 2.3. There are several differences compared to the HM system.
First, polymorphic types can be of arbitrary rank, i.e. the forall quantifier may occur at any
part of a type. Yet, mono-type remains the same definition as HM’s.
Second, expressions now allows annotations e : σ and (argument) annotated lambda functions
λx : σ. e. Annotations on expressions help guide the type system properly, acting as a machine-17

2 Background

Type variables

a, b

Types

σ

::= 1 | a | σ1 → σ2 | ∀a. σ

Monotypesτ::= 1 | a | τ1 → τ2

Expressionse::=x | () | λx : σ. e | e : σ | λx. e | e1 e2 | let x = e1 in e2

ContextsΨ::=· | Ψ, x : σ | Ψ, aFigure 2.3: Syntax of Odersky-Läufer SystemΨ ⊢OL 1Ψ ⊢OL σ1a∈Ψ

OL-WF-UnitΨ ⊢OL σ2Ψ ⊢OL σ1 → σ2Ψ ⊢OL aOL-WF-Arr

OL-WF-TVarΨ, a ⊢OL σΨ ⊢OL ∀a. σ

OL-WF-Forall

Figure 2.4: Well-formedness of types in the Odersky-Läufer System

checked document by the programmers. By annotating the argument of a lambda function with apolymorphic type σ, one may encode a function of higher rank in this system compared to HM’s.
Finally, contexts consist of not only variable bindings, but also type variable declarations. Here
we adopt a slightly different approach than the original work [Odersky and Läufer 1996], which
does not track type variables explicitly in a context. Such explicit declarations reduce formalization difficulties, especially when dealing with freshness conditions or variable name encodings.
This also enables us to formally define the well-formedness of types, shown in Figure 2.4.
Subtyping The subtyping relation, defined in Figure 2.5, is more powerful than that (type instantiation) of HM. It compares the degree of polymorphism between two types. Essentially, if
A can always be instantiated to match any instantiation of B, then A is “at least as polymorphic as” B. We also say that A is “more polymorphic than” B and write A ≤ B. In contrast
to HM’s subtyping, higher-ranked types can be compared thanks to Rule OL-SUB-Arr; functions
are contravariant on argument types and covariant on return types.
Subtyping rules OL-SUB-Var, OL-SUB-Unit handle simple cases that do not involve universal
quantifiers. Rule OL-SUB-∀R states that if A is a subtype of B in the context Ψ, a, where a is freshin A, then A ≤ ∀a. B. Intuitively, if A is more general than ∀a. B (where the universal quantifier
already indicates that ∀a. B is a general type), then A must instantiate to [τ /a]B for every τ .
The most interesting rule is OL-SUB-∀L. If some instantiation of ∀a. A, [τ /a]A, is a subtype ofB, then ∀a. A ≤ B. The monotype τ we used to instantiate a is guessed in this declarative rule,18

2 BackgroundΨ ⊢OL 1 ≤ 1a∈Ψ

OL-SUB-UnitΨ ⊢OL σ1′ ≤ σ1Ψ ⊢OL a ≤ aΨ ⊢OL σ2 ≤ σ2′Ψ ⊢OL σ1 → σ2 ≤ σ1′ → σ2′Ψ ⊢OL [τ /a]σ ≤ σ ′Ψ ⊢OL τΨ ⊢OL ∀a. σ ≤ σ ′OL-SUB-Var

OL-SUB-Arr

Ψ, a ⊢OL σ ≤ σ ′OL-SUB-∀LΨ ⊢OL σ ≤ ∀a. σ ′OL-SUB-∀R

Figure 2.5: Subtyping of the Odersky-Läufer System(x : σ) ∈ ΨΨ ⊢OL x : σΨ ⊢OL τOL-VarΨ ⊢OL () : 1

Ψ, x : τ ⊢OL e : σΨ ⊢OL e1 e2 : σ2

OL-AppΨ, a ⊢OL e : σΨ ⊢OL e : ∀a. σ

Ψ, x : σ1 ⊢OL e2 : σ2Ψ ⊢OL let x = e1 in e2 : σ2Ψ ⊢OL e : σ1Ψ ⊢OL (e : σ) : σΨ ⊢OL λx : σ1 . e : σ1 → σ2Ψ ⊢OL e2 : σ1Ψ ⊢OL e1 : σ1Ψ ⊢OL e : σΨ, x : σ1 ⊢OL e : σ2

OL-LamΨ ⊢OL λx. e : τ → σΨ ⊢OL e1 : σ1 → σ2

OL-UnitΨ ⊢OL σ1 ≤ σ2Ψ ⊢OL e : σ2

OL-Anno
OL-LamAnno
OL-Gen

OL-Let

OL-SubFigure 2.6: Typing of the Odersky-Läufer Systembut the algorithmic system does not guess and defers the instantiation until it can determine themonotype deterministically. The fact that τ is a monotype rules out the possibility of polymorphic (or impredicative) instantiation. However this restriction ensures that the subtyping relation remains decidable. Allowing an arbitrary type (rather than a monotype) in rule OL-SUB-∀L
is known to give rise to an undecidable subtyping relation [Chrząszcz 1998]. Peyton Jones et al.
[2007] also impose the restriction of predicative instantiation in their type system. Both systems
are adopted by several practical programming languages.
Note that when we introduce a new binder in the premise, we implicitly pick a fresh one, which
is made possible by renaming according to alpha-equivalence. This applies to rules OL-SUB-∀R
here. We follow this implicit freshness condition and omit it throughout the whole thesis.
Typing The type system of Odersky-Läufer, shown in Figure 2.6, extends HM’s type system inthe following aspects.

19

2 Background

Rule OL-Lam now accepts polymorphic return type, because such type is well-formed. The
guess on parameter types is still limited to monotypes like HM’s. However, if a parameter type is
specified in advance, the type system accepts polymorphic argument type with rule OL-LamAnno.
Functions of arbitrary rank can be encoded through proper annotations. The application andlet-generalization rules also accept polymorphic return types.
Rule OL-Gen encodes the generalization rule of HM in a different way under explicit type variable declarations. A fresh type variable is introduced into the context before the type of expression
e is calculated. Then we conclude that e has a polymorphic type by generalizing the type variable.
For example, the type of the identity function is derived as follows(x : a) ∈ (·, a, x : a)·, a ⊢OL a·, a, x : a ⊢OL x : a·, a ⊢OL λx. x : a → a· ⊢OL λx. x : ∀a. a → a

OL-Var
OL-LamOL-GenThe subsumption rule OL-Sub converts the type of an expression with the help of the subtyping
relation.

2.2.3 Relating to HM
The OL type system accepts higher-ranked types, but it only tries to instantiate monotypes like
HM. Therefore, conservatively extends HM, such that every typed expression in HM is also typed
in OL. In the meantime, all the “guessing” jobs OL needs to do remains in instantiating monotypes, thus the algorithm can be extended directly from any one for HM. Formally speaking,type inference for both systems can be reduced to a problem of solving certain forms of unification constraints, including equalities, conjunctions, universal and existential quantifiers, andlet-generalizations.

2.3 Dunfield-Krishnaswami Bidirectional Type System
Bidirectional typing is popular among new type systems. Compared with the ML-style systems,
bidirectional typing additionally makes use of checking mode, which checks an expression against
a known type. This is especially helpful in dealing with unannotated lambda functions, and when
the type of the function can be inferred from the neighbor nodes in the syntax tree. For example,
λf. (f 1, f ′ c′ ) : (∀a. a → a) → (Int → Char)20

2 Background

Type variables
Types
Monotypes
Expressions
Contexts

a, b
A, B, C
τ, σ
e
Ψ

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

1 | a | ∀a. A | A → B
1|a|τ →σx | () | λx. e | e1 e2 | (e : A)
· | Ψ, a | Ψ, x : A

Figure 2.7: Syntax of Declarative System

is typeable in higher-ranked bidirectional systems, as the outer type annotation may act as if boththe argument type and return type of the lambda is given. The Dunfield-Krishnaswami typesystem [Dunfield and Krishnaswami 2013], hereafter referred to as DK, extends the OL system
by exploiting bidirectional typing. In this section, we only introduce the declarative system andleave the discussion of their algorithmic system to Chapters 3 and 4.

2.3.1 Declarative System
Syntax. The syntax of DK’s declarative system [Dunfield and Krishnaswami 2013] is shownin Figure 2.7. A declarative type A is either the unit type 1, a type variable a, a universal quantification ∀a. A or a function type A → B. Nested universal quantifiers are allowed for types,
but monotypes τ do not have any universal quantifier. Terms include a unit term (), variables x,
lambda-functions λx. e, applications e1 e2 and annotations (e : A). Contexts Ψ are sequencesof type variable declarations and term variables with their types declared x : A.
Well-formedness Well-formedness of types and terms is shown at the top of Figure 2.8. The
rules are standard and simply ensure that variables in types and terms are well-scoped.
Declarative Subtyping The bottom of Figure 2.8 shows DK’s declarative subtyping judgment
Ψ ⊢ A ≤ B, which was adopted from Odersky and Läufer [1996]. Since it is exactly the samewith OL’s subtyping relation, we refer to Section 2.2 for detailed discussion.
Declarative Typing The bidirectional type system, shown in Figure 2.9, has three judgments.
The checking judgment Ψ ⊢ e ⇐ A checks expression e against the type A in the context Ψ. The
synthesis judgment Ψ ⊢ e ⇒ A synthesizes the type A of expression e in the context Ψ. The
application judgment Ψ ⊢ A • e ⇒⇒ C synthesizes the type C of the application of a function oftype A (which could be polymorphic) to the argument e.
Many rules are standard. Rule DeclVar looks up term variables in the context. Rules Decl1I
and Decl1I⇒ respectively check and synthesize the unit type. Rule DeclAnno synthesizes theannotated type A of the annotated expression (e : A) and checks that e has type A. Checking an

21

2 BackgroundΨ ⊢ A Well-formed declarative type
Ψ⊢1

a∈Ψ

wfd unitΨ⊢aΨ⊢A

wfd var

Ψ⊢B

Ψ⊢A→B

Ψ, a ⊢ A

wfd →Ψ ⊢ ∀a.Awfd ∀Ψ ⊢ e Well-formed declarative expression
x:A∈Ψ

wfd tmvar

Ψ⊢xΨ ⊢ e1Ψ ⊢ e2Ψ ⊢ e1 e2Ψ ⊢ ()

wfd tmunitΨ⊢A

wfd appΨ, x : A ⊢ eΨ ⊢ λx. eΨ⊢eΨ ⊢ (e : A)

wfd abs

wfd annoΨ ⊢ A ≤ B Declarative subtyping
a∈Ψ
Ψ⊢a≤a

≤Var

Ψ⊢1≤1

Ψ⊢τ

≤Unit

Ψ ⊢ [τ /a]A ≤ BΨ ⊢ ∀a. A ≤ B≤∀LΨ ⊢ B 1 ≤ A1

Ψ ⊢ A2 ≤ B 2

Ψ ⊢ A1 → A2 ≤ B1 → B2
Ψ, b ⊢ A ≤ B
Ψ ⊢ A ≤ ∀b. B

≤→

≤∀R

Figure 2.8: Declarative Well-formedness and Subtyping

expression e against a polymorphic type ∀a. A in the context Ψ succeeds if e checks against A inthe extended context (Ψ, a). The subsumption rule DeclSub depends on the subtyping relation,and changes mode from checking to synthesis: if e synthesizes type A and A ≤ B (A is morepolymorphic than B), then e checks against B. If a checking problem does not match any otherrules, this rule can be applied to synthesize a type instead and then check whether the synthesized
type entails the checked type. Lambda abstractions are the hardest construct of the bidirectional
type system to deal with. Checking λx. e against function type A → B is easy: we check the
body e against B in the context extended with x : A. However, synthesizing a lambda-function
is a lot harder, and this type system only synthesizes monotypes σ → τ .
Application e1 e2 is handled by Rule Decl→E, which first synthesizes the type A of the function e1 . If A is a function type B → C, Rule Decl→App is applied; it checks the argument e2
against B and returns type C. The synthesized type of function e1 can also be polymorphic, of
the form ∀a. A. In that case, we instantiate A to [τ /a]A with a monotype τ using according toRule Decl→I⇒. If [τ /a]A is a function type, Rule Decl→App proceeds; if [τ /a]A is anotheruniversal quantified type, Rule Decl→I⇒ is recursively applied.

22

2 BackgroundΨ⊢e⇐Ae checks against input type A.

Ψ⊢e⇒Ae synthesizes output type A.

Ψ ⊢ A • e ⇒⇒ C

Applying a function of type A to e synthesizes type C.

(x : A) ∈ Ψ
Ψ⊢x⇒A
Ψ⊢A

Ψ⊢e⇐A

Ψ ⊢ (e : A) ⇒ A

DeclVar

DeclAnno

Ψ, a ⊢ e ⇐ AΨ ⊢ e ⇐ ∀a. A

Decl∀IΨ, x : A ⊢ e ⇐ BΨ ⊢ λx. e ⇐ A → B

Decl→IΨ ⊢ e1 ⇒ A Ψ ⊢ A • e2 ⇒⇒ C
Ψ ⊢ e1 e2 ⇒ C

Ψ⊢e⇒A

Ψ⊢A≤B

Ψ⊢e⇐B
Ψ ⊢ () ⇐ 1
Ψ⊢τ

Decl1I

DeclSubΨ ⊢ () ⇒ 1

Ψ ⊢ [τ /a]A • e ⇒⇒ C

Ψ ⊢ ∀a. A • e ⇒⇒ C
Ψ⊢σ→τDecl∀AppΨ, x : σ ⊢ e ⇐ τΨ ⊢ λx. e ⇒ σ → τ
Decl→E

Decl1I⇒

Decl→I⇒Ψ⊢e⇐AΨ ⊢ A → C • e ⇒⇒ C

Decl→App

Figure 2.9: Declarative Typing

To conclude, DK employs a bidirectional declarative type system. The type system is mostly
syntax-directed, but there are still some guesses of monotypes that need to be resolved by analgorithm. We will continue to discuss DK’s algorithm in Chapters 3 and 4.

2.4 MLsub
Besides extending the HM type system with higher-ranked types and bidirectional type checking,another valuable direction is to support object-oriented subtyping. MLsub [Dolan and Mycroft
2017] is one of such systems. In presence of subtyping, type inference does not simply handle equality during unification. Therefore, types are extended with lattice operations to express
bounds properly. Furthermore, polar types are introduced to help separate input and output
types, which simplifies the type inference algorithm. Like HM’s type inference, MLsub always
infers a principal type.

2.4.1 Types and Polar Types
In comparison to the type system of HM, types (Figure 2.10) now include ⊤ and ⊥, as minimalcomponents to support subtyping. Besides, the least-upper-bound (⊔) and greatest-lower-bound(⊓) lattice operations are used to represent a bound expressed by two types. For finite types, a

23

2 Background

Types
Positive Types
Negative Types

τ
::=
+
τ
::=
τ − ::=

1 | a | ⊤ | ⊥ | τ 1 → τ2 | τ 1 ⊔ τ 2 | τ 1 ⊓ τ 2
1 | a | ⊥ | τ1− → τ2+ | τ1+ ⊔ τ2+
1 | a | ⊤ | τ1+ → τ2− | τ1− ⊓ τ2−

Figure 2.10: Types of MLsub

distributive lattice can be defined via a set of equivalence classes of ≡ [Dolan and Mycroft 2017].
The most interesting equations are the distributivity rule and rules for function types:
τ1 ⊔ (τ2 ⊓ τ3 ) ≡ (τ1 ⊔ τ2 ) ⊓ (τ1 ⊔ τ3 )
τ1 ⊓ (τ2 ⊔ τ3 ) ≡ (τ1 ⊓ τ2 ) ⊔ (τ1 ⊓ τ3 )(τ1 → τ2 ) ⊔ (τ1′ → τ2′ ) ≡ (τ1 ⊓ τ1′ ) → (τ2 ⊔ τ2′ )(τ1 → τ2 ) ⊓ (τ1′ → τ2′ ) ≡ (τ1 ⊔ τ1′ ) → (τ2 ⊓ τ2′ )The partial order τ1 ≤ τ2 is defined as τ1 ⊔ τ2 ≡ τ2 or τ1 ⊓ τ2 ≡ τ1 . ⊤ and ⊥ are the leastand greatest types. The above rules on function types imply the usual subtyping rule for function
types, considering the definition of partial order:
τ1′ ≤ τ1

τ2 ≤ τ2′

τ1 → τ2 ≤ τ1′ → τ2′
Type schemes are not defined as the usual σ. Instead, a monotype τ already represents a typescheme by omitting the ∀ quantifiers—all the free type variables are implicitly generalized.
Recursive types play an important role regarding the principality of type inference, but we omit
them for simplicity.
Polar Types Polar types are restrictions on the lattice operations; they should not occur arbitrarily in any position. Specifically, function outputs consist of types (τ1 , τ2 ) from different
branches, resulting in τ1 ⊔ τ2 ; a function input might be used in various ways (under different
constraints), thus τ1 ⊓ τ2 is more suitable. In summary, ⊔ only arises in return types, while ⊓only arises in argument types. Figure 2.10 formally defines the restriction, where positive types
τ + describe return types, and negative types τ − describe argument types.
An important consequence is that all the constraints are of the form τ + ≤ τ − , which represents
the subtyping relation when using an output expression in a function application as an argument.
The following subtyping rules involving the lattice operations reflects their basic properties:
τ1+ ≤ τ −

τ + ≤ τ1−

τ2+ ≤ τ −

τ + ≤ τ2−τ − ≤ τ1− ⊓ τ2−

τ1+ ⊔ τ2+ ≤ τ −24.

2 Background
Interestingly, the polar subtyping judgments avoids difficult judgments like τ1 ⊓ τ2 ≤ τ or τ ≤τ1 ⊔ τ2 through its syntactic restriction.

2.4.2 Biunification
Type inference for MLsub, similar to that for ML, is mainly a unification algorithm. However, inpresence of subtyping, equality-based unification loses information about subtyping constraints.
For the atomic constraint αb = τ where αb∈/ FV(τ ), the ML unification algorithm produces thesubstitution [τ /bα ]. In contrast, an MLsub atomic constraint might be αb ≤ τ , and the substitution[τ /bα ] treat the subtyping constraint as an equality constraint, which eliminates a whole set of
possibilities.
Luckily, lattices in MLsub helps express subtyping constraints on types directly. The constraintαb ≤ τ (bα∈
/ FV(τ )) may produce the substitution [bα ⊓ τ /bα ], since αb ⊓ τ ≤ τ . In the meantime,αb ⊓ τ does not lose any expressiveness: for any τ0 s.t. τ0 ≤ τ , picking αb = τ0 gives αb ⊓ τ = τ0 ,and the substitution [bα ⊓ τ /bα ] is equivalent to [τ0 /b
α ].
In presence of polar types, the biunification algorithm of MLsub produces a bisubstitution [bα⊓τ − /bα− ] against the constraint αb ≤ τ − , where only negative occurrences are substituted, keeping
polar types properly “polarized”. For example, a positive type αb →αb becomes (bα ⊓ τ −) → αbunder such substitution and remains a positive type. A more important fact is that this typeis equivalent to the constrained type scheme αb → αb with the constraint αb ≤ τ . Similarly, a
constraint like τ + ≤ α
b is reduced to a substitution [bα ⊔ τ + /b
α+ ].
For example, the choose function is typed ∀a. a → a → a in ML. However, MLsub might alsoinfer an equivalent type ∀a b. a → b → a ⊔ b. One can easily read the MLsub type in a form
where constraints are explicitly stated∀a b c. a → b → c where a ≤ c, b ≤ c.
Therefore, MLsub encodes the constraints directly onto types with the help of the lattice operations. Furthermore, a simplification step is taken after the type inference algorithm, reducing thesize and improving readablity of the type inferred.
As a result, biunification for MLsub extends unification for ML, accepting subtyping in addition
to type schemes, while maintaining principality.

25

Part II
Higher-Ranked Type Inference Algorithms

26

3 Higher-Ranked Polymorphism
Subtyping Algorithm
In this chapter, we present a new algorithm for polymorphic subtyping with mechanical formalizations in the Abella theorem prover. There is little work on formalizing type inference algorithms before, especially for higher-ranked systems, due to the fact that environments and variable bindings are tricky to mechanize in theorem provers. In order to overcome the difficulty informalization, we propose the novel algorithm by means of worklist judgments. Worklist judgments turn complicated global propagation of unification constraints into simple local substitutions. Moreover, we exploit several ideas in the recent inductive formulation of a type-inference
algorithm by Dunfield and Krishnaswami [2013], which turn out to be useful for mechanization
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 Läufer [1996]. While these meta-theoretical results are not new, as far as we know our workis the first to mechanically formalize them.

3.1 Overview: Polymorphic Subtyping
This section discusses Odersky and Läufer declarative subtyping rules further in depth, and identifies the challenges in formalizing a corresponding algorithmic version. Then the key ideas of ourapproach that address those challenges are introduced.

3.1.1 Declarative Polymorphic Subtyping
In implicitly polymorphic type systems, the subtyping relation compares the degree of polymorphism of types. In short, if a polymorphic type A can always be instantiated to any instantiationof B, then A is “at least as polymorphic as” B, or we just say that A is “more polymorphic than”
B, or A ≤ B.
There is a very simple declarative formulation of polymorphic subtyping due to Odersky and
Läufer [1996]. The syntax of this declarative system is shown in Figure 3.1. Types, represented27

3 Higher-Ranked Polymorphism Subtyping Algorithm

Type variables

a, b

Types
Monotypes
Contexts

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

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

Ψ⊢A
Ψ⊢1

a∈Ψ

wfd unitΨ⊢aΨ⊢A

wfd var

Ψ⊢B

Ψ⊢A→B

Ψ, a ⊢ A

wfd →Ψ ⊢ ∀a.A

wfd ∀

Ψ⊢A≤B
a∈Ψ
Ψ⊢a≤a

≤Var

Ψ⊢1≤1

Ψ⊢τ

≤Unit

Ψ ⊢ [τ /a]A ≤ BΨ ⊢ ∀a.A ≤ B

Ψ ⊢ B 1 ≤ A1

Ψ ⊢ A2 ≤ B 2

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

≤→

≤∀R

Figure 3.2: Well-formedness of Declarative Types and Declarative Subtyping

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 Ψ collect a list of type variables.
In Figure 3.2, we give the well-formedness and subtyping relation for the declarative system,
which is identical to the subtyping relation introduced in Subsection 2.3.1.

3.1.2 Finding Solutions for Variable Instantiation
The declarative system specifies the behavior of subtyping relations, but is not directly implementable: Rule ≤∀L requires guessing a monotype τ . The core problem that an algorithm forpolymorphic subtyping needs to solve is to find an 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 firstjudgment should be transfered to the second judgment.
It is worth mentioning that the problem of deciding subtyping of OL’s type system can be
reduced to first-order unification under a mixed prefix Miller [1992], where universal and existential quantifiers appears at the top level of constraints (equations). We further discuss anothersimpler algorithm by DK and present ours afterwards.

28

3 Higher-Ranked Polymorphism Subtyping Algorithm

Dunfield and Krishnaswami’s Approach An elegant algorithmic solution to computing
the monotypes is presented by Dunfield and Krishnaswami [2013]. Their algorithmic subtyping judgment has the form:
Ψ⊢A≤B⊣ΦA notable difference to the declarative judgment 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 samestructure. Ordered contexts are particularly useful to keep track of the correct scoping for variables, and are a notable difference to older type-inference algorithms [Damas and Milner 1982]
that use global unification variables or constraints collected in a set.
Output contexts are useful to transfer information across judgments in Dunfield and Krishnaswami’s approach. For example, the algorithmic rule corresponding to ≤→ in their approachis:Ψ ⊢ B1 <: A1 ⊣ Φ Φ ⊢ [Φ]A2 <: [Φ]B2 ⊣ Φ′
Ψ ⊢ A1 → A2 <: B1 → B2 ⊣ Φ′<:→

The information gathered by the output context when comparing the input types of the functions
for subtyping is transferred to the second judgment by becoming the new input context, while
any solution derived from the first judgment is applied 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 → 1b
Dunfield and Krishnaswami introduce an existential variable—denoted with αb , β—wheneveramonotype τ needs to be guessed. Below is a sample derivation of their algorithm:

α
b⊢1≤α
b⊣α
b=1

InstRSolveαb=1⊢1≤1⊣α
b=1

α
b⊢α
b→α
b≤1→1⊣αb=1· ⊢ ∀a.a → a ≤ 1 → 1 ⊣ ·<:Unit<:→<:∀L

The first step applies Rule <:∀L, which introduces a fresh existential variable, αb , and opens theleft-hand-side ∀-quantifier with it. Next, Rule <:→ splits the judgment in two. For the firstbranch, Rule InstRSolve satisfies 1 ≤ αb by solving α
b to 1, and stores the solution in its output

29

3 Higher-Ranked Polymorphism Subtyping Algorithm

context. The output context of the first 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 andpropagates the output context back.
Dunfield and Krishnaswami’s algorithmic specification is elegant and contains several usefulideas 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 structure of their algorithmic judgment is still fairly complicated andposes challenges when porting their approach to a theorem prover.

3.1.3 The Worklist Approach
We inherit Dunfield and Krishnaswami’s ideas of ordered contexts, existential variables and theidea 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 judgment form, which we callworklist judgment, simplifies two aspects of Dunfield and Krishnaswami’s approach.
Firstly, as already stated, there are no output contexts. Secondly, the form of the ordered contexts becomes simpler. The transfer of information across judgments is simplified because all
judgments share the input context. Moreover, the order of the judgments in the list allows information discovered when processing the earlier judgments to be easily transferred to the later
judgments. In the worklist approach the rule for function types is:Γ ⊢ B1 ≤ A1 ; A2 ≤ B2 ; Ω≤a →Γ ⊢ A1 → A2 ≤ B1 → B2 ; ΩThe derivation of the previous example with the worklist approach is:

·⊢·

a_nil

· ⊢ 1 ≤ 1; ·≤a unit

α
b⊢1≤α
b; α
b ≤ 1; ·≤a solve_ex

α
b⊢α
b→α
b ≤ 1 → 1; ·≤a →· ⊢ ∀a.a → a ≤ 1 → 1; ·

30

≤a ∀L

3 Higher-Ranked Polymorphism Subtyping Algorithm
To derive · ⊢ ∀a.a → a ≤ 1 → 1 with the worklist approach, we first introduce an existential
variable and change the judgment to α
b ⊢α
b →α
b ≤ 1 → 1; ·. Then, we split the judgment in
two for the function types and the derivation comes to αb ⊢ 1 ≤ αb; αb ≤ 1; ·. When the firstjudgment is solved with αb = 1, we immediately remove αb 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 recorded in contexts, simplifying the encoding and reasoning in a proof assistant.
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 andalgorithmic systems.

3.2 A Worklist Algorithm for Polymorphic Subtyping
This section presents our algorithm for polymorphic subtyping. A novel aspect of our algorithm isthe use of worklist judgments: a form of judgment that facilitates the propagation of information.

3.2.1 Syntax and Well-Formedness of the Algorithmic System
Figure 3.3 shows the syntax and the well-formedness judgment.
Existential Variables In order to solve the unknown types τ , the algorithmic system extends
the declarative syntax of types with existential variables α
b . They behave like unification variables,
but are not globally defined. Instead, the ordered algorithmic context, inspired by Dunfield andKrishnaswami [2013], defines their scope. Thus the type τ represented by the corresponding
existential variable is always bound in the corresponding declarative context Ψ.
Worklist judgments The form of our algorithmic judgments is non-standard. Our algorithm
keeps track of an explicit list of outstanding work: the list Ω of (reified) algorithmic judgments ofthe form A ≤ B, to which a substitution can be applied once and for all to propagate the solutionof an existential variable.
Hole Notation To facilitate context manipulation, we use the syntax Γ[ΓM ] to denote a context of the form ΓL , ΓM , ΓR where Γ is the context ΓL , •, ΓR with a hole (•). Hole notations withb means
the same name implicitly share the same ΓL and ΓR . A multi-hole notation like Γ[bα ][β]b Γ3 .
Γ1 , αb , Γ2 , β,31

3 Higher-Ranked Polymorphism Subtyping Algorithm

Type variables
Existential variablesa, bαb , βbAlgorithmic types
Algorithmic context
Algorithmic judgments

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

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

Γ⊢A
Γ⊢1

a∈Γ

wfa unit

Γ⊢A

Γ⊢a
Γ⊢B

Γ⊢A→B

wfa var

wfa →

α
b∈Γ
Γ⊢α
b
Γ, a ⊢ AΓ ⊢ ∀a.A

wfa exvar

wfa ∀Figure 3.3: Syntax and Well-Formedness judgment for the Algorithmic System.

3.2.2 Algorithmic Subtyping
The algorithmic subtyping judgment, defined in Figure 3.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, andrepeats 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 can discern 3 groupsof 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 theworklist. A notable difference with the declarative Rule ≤∀L is that Rule ≤a ∀L requires no guessing of a type τ to instantiate the polymorphic type ∀a.A, but instead introduces an existential
variable α
b to the context and to A. In accordance with the declarative system, where the monotype τ should be bound in the context Ψ, here αb should only be solved to a monotype boundin Γ. More generally, for any algorithmic context Γ[bα ], the algorithmic variable αb can only besolved to a monotype that is well-formed with respect to ΓL .
Secondly, Rules ≤a instL and ≤a instR partially instantiate existential types α
b , to function
types. The domain and range of the new function type are undetermined: they are set to two
fresh existential variables α
b1 and α
b2 . To make sure that α
b1 → αb2 has the same scope as αb , thenew variables α
b1 and α
b2 are inserted in the same position in the context where the old variable αbwas. To propagate the instantiation to the remainder of the worklist, αb is substituted for α
b1 → αb2in Ω. The occurs-check side-condition is necessary to prevent a diverging infinite instantiation.
For example 1 → αb ≤αb would diverge with no such check. Note that the algorithm does not

32

3 Higher-Ranked Polymorphism Subtyping Algorithm
Γ⊢Ω
Γ⊢·
Γ⊢Ω
Γ ⊢ 1 ≤ 1; Ω≤a unita∈Γ≤a nilΓ⊢ΩΓ ⊢ a ≤ a; Ωαb∈Γ≤a var

Γ⊢α
b≤α
b; Ω

Γ ⊢ B1 ≤ A1 ; A2 ≤ B2 ; ΩΓ ⊢ A1 → A2 ≤ B1 → B2 ; Ωαb freshΓ, αb ⊢ [bα /a]A ≤ B; ΩΓ ⊢ ∀a.A ≤ B; Ωαb∈
/ FV(A) ∪ F V (B)

≤a ∀L

Γ⊢Ω

≤a exvar≤a →b freshΓ, b ⊢ A ≤ B; ΩΓ ⊢ A ≤ ∀b.B; ΩΓ[bα1 , αb2 ] ⊢ αb1 → αb2 ≤ A → B; [bα1 → α
b2 /b
α ]Ω
Γ[b
α] ⊢ αb ≤ A → B; Ωαb∈
/ F V (A) ∪ F V (B) Γ[bα1 , αb2 ] ⊢ A → B ≤ αb1 → αb2 ; [bα1 → α
b2 /b
α ]Ω
Γ[b
α] ⊢ A → B ≤ α
b; Ω

≤a ∀R

≤a instL≤a instRbΓ[bα ][] ⊢ [bα /β]Ω≤ solve_ex
b ⊢α
bΩ a
Γ[b
α ][β]b ≤ β;bΓ[bα ][] ⊢ [bα /β]Ω≤a solve_ex′bb
Γ[bα ][β] ⊢ β ≤ αb; ΩbΓ[a][] ⊢ [a/β]Ω≤ solve_varb ⊢ a ≤ β;bΩ a
Γ[a][β]b
Γ[a][] ⊢ [a/β]Ω≤a solve_var′bb
Γ[a][β] ⊢ β ≤ a; ΩΓ[] ⊢ [1/bα ]Ω
Γ[bα] ⊢ αb ≤ 1; ΩΓ[] ⊢ [1/bα ]Ω

≤a solve_unit

Γ[bα] ⊢ 1 ≤ αb; Ω≤a solve_unit′

Figure 3.4: Algorithmic Subtyping

choose to instantiate αb directly with A → B, since the type is not guaranteed to be a monotype,and such instantiation will be inconsistent with our predicative declarative system.
Thirdly, in the remaining six rules an existential variable can be immediately solved. Each of
the six similar rules removes an existential variable from the context, 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 bystrengthening 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.

33

3 Higher-Ranked Polymorphism Subtyping Algorithmαb1 ⊢ ·a_nil

αb1 ⊢ 1 ≤ 1; ·≤a unit≤a solve_exαb1 , αb2 ⊢ αb1 ≤ αb2 ; 1 ≤ 1; ·≤a solve_exbbαb1 , αb2 , β ⊢ αb1 ≤ β; βb ≤ α
b2 ; 1 ≤ 1; ·≤ →aαb1 , αb2 , βb ⊢ βb → βb ≤ α
b1 → αb2 ; 1 ≤ 1; ·≤a instRαb , βb ⊢ βb → βb ≤ α
b ; 1 ≤ 1; ·

≤a ∀L

α
b ⊢ ∀a. a → a ≤ α
b ; 1 ≤ 1; ·αb⊢αb → 1 ≤ (∀a. a → a) → 1; ·· ⊢ ∀a. a → 1 ≤ (∀a. a → a) → 1; ·

≤a →
≤a ∀L

Figure 3.5: A Success Derivation for the Algorithmic Subtyping Relation

stuck
αb, b ⊢ αb ≤ b; ·?

αb⊢αb ≤ ∀b. b; ·

≤a ∀R

α
b ⊢ 1 ≤ 1; αb ≤ ∀b. b; ·≤a unitαb⊢1→αb ≤ 1 → ∀b. b; ·≤a →· ⊢ ∀a. 1 → a ≤ 1 → ∀b. b; ·≤a ∀LFigure 3.6: A Failing Derivation for the Algorithmic Subtyping Relation

Example We illustrate the subtyping rules through a sample derivation in Figure 3.5, whichshows 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 universally quantified type with an unknown
existential variable α
b . Variable αb will be solved later to some monotype that is well-formed within
the context before α
b . 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 left-handside ∀ 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 hand side, but the right-hand-side type isan existential variable. It is obvious that αb should be solved to a monotype of the form σ → τ .
Rule instR implements this, but avoids guessing σ and τ by “splitting” αb into two existential
variables, α
b1 and αb2 , which will be solved to some σ and τ later. Step 5 applies Rule ≤a → again.
Notice that after the split, βb appears in two judgments. When the first βb is solved during any stepof the derivation, the next βb will be substituted by that solution. This propagation mechanism34

3 Higher-Ranked Polymorphism Subtyping Algorithm

ensures the consistent solution of the variables, 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
is always solved in terms of the other. Therefore in step 6, βb is solved in terms of αb1 , and in stepb7, α
b2 is solved in terms of αb1 . Additionally, in step 6, when βb is solved, the substitution [bα1 /β]

is propagated to the rest of the judgment list, and thus the second judgment becomes αb1 ≤ αb2 .
Steps 8 and 9 trivially finish the derivation. Notice that α
b1 is not instantiated at the end. Thismeans that any well-scoped instantiation is fine.
A Failing Derivation We illustrate the role of ordered contexts through another example:∀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 τ suchthat τ ≤ b. Figure 3.6 shows the algorithmic derivation, which also fails due to the scoping—b
α
is introduced earlier than b, thus it cannot be solved to b.

3.3 Metatheory
This section presents the three main meta-theoretical results that we have proved in Abella. The
first two are soundness and completeness of our algorithm with respect to Odersky and Läufer’s
declarative subtyping. The third result is our algorithm’s decidability.

3.3.1 Transfer to the Declarative System
To state the correctness of the algorithmic subtyping rules, Figure 3.7 introduces two transfer
judgments to relate the declarative and the algorithmic system. The first judgment, transfer ofcontexts Γ → Ψ, removes existential variables from the algorithmic context Γ to obtain a declarative context Ψ. The second judgment, transfer of the judgment list Γ | Ω ⇝ Ω′ , replaces all
occurrences of existential 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 Ω′ . However, if there exists
some substitution that transforms Ω to Ω′ , and each subtyping judgment in Ω′ holds, we knowthat Ω is potentially satisfiable.
The following two lemmas generalize Rule ⇝exvar from substituting the first existential variable to substituting any existential variable.
Lemma 3.1 (Insert). If Γ → Ψ and Ψ ⊢ τ and Γ, Γ1 | [τ /bα ]Ω ⇝ Ω′ , then Γ, αb , Γ1 | Ω ⇝ Ω′ .
Lemma 3.2 (Extract). If Γ, αb , Γ1 | Ω ⇝ Ω′ , then ∃τ s.t. Γ → Ψ, Ψ ⊢ τ and Γ, Γ1 | [τ /bα ]Ω ⇝Ω′ .

35

3 Higher-Ranked Polymorphism Subtyping Algorithm
Γ→Ψ
·→·

Γ→Ψ

→·

Γ, a → Ψ, a

→var

Γ→Ψ
Γ, α
b→Ψ

→exvarΓ | Ω ⇝ Ω′

·|Ω⇝Ω
Γ→Ψ

Γ | Ω ⇝ Ω′

⇝·

Ψ⊢τ

Γ, a | Ω ⇝ Ω′
Γ | [τ /bα ]Ω ⇝ Ω′Γ, αb | Ω ⇝ Ω′⇝var
⇝exvarFigure 3.7: Transfer Rules

In order to match the shape of algorithmic subtyping relation for the following proofs, we definea relation Ψ ⊢ Ω for the declarative system, meaning that all the declarative judgments hold undercontext Ψ.
Definition 1 (Declarative Subtyping Worklist).
Ψ ⊢ Ω := ∀(A ≤ B) ∈ Ω, Ψ ⊢ A ≤ B

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

3.3.3 CompletenessCompleteness of the algorithm means that any declarative derivation has an algorithmic counterpart.
Theorem 3.4 (Completeness). If Ψ ⊢ Ω′ and Γ → Ψ and Γ | Ω ⇝ Ω′ , then Γ ⊢ Ω.

36

3 Higher-Ranked Polymorphism Subtyping Algorithm
The proof proceeds by induction on the derivation of Ψ ⊢ Ω′ . As the declarative system does
not involve information propagation across judgments, the induction can focus on the subtyping
derivation of the first judgment without affecting other judgments. The difficult cases correspondto the ≤a instL and ≤a instR rules. When the proof by induction on Ψ ⊢ Ω′ reaches the ≤→case, the first declarative judgment has a shape like A1 → A2 ≤ B1 → B2 . One of the possible
cases for the first corresponding algorithmic judgment is αb ≤ A → B. However, the case analysis
does not indicate that αb 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. αb≤1→αb ) and guarantees that αb is free in A and B.
Lemma 3.5 (Prune Transfer for Instantiation). If Ψ ⊢ A1 → A2 ≤ B1 → B2 ; Ω′ and Γ → Ψand Γ | (bα ≤ A → B; Ω) ⇝ (A1 → A2 ≤ B1 → B2 ; Ω′ ) , then αb∈/ F V (A) ∪ F V (B).
A similar lemma holds for the symmetric case (A → B ≤ αb ; Ω).

3.3.4 Decidability
The third key result for our algorithm is decidability.
Theorem 3.6 (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⟨|Ω|∀ , |Γ|αb , |Ω|→ ⟩ 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|∀ = 0|a|∀ = 0|bα |∀ = 0|A → B|∀ = |A|∀ + |B|∀|∀x.A|∀ = |A|∀ + 1
P|Ω|∀ =
A≤B∈Ω |A|∀ + |B|∀
|1|→ = 0|a|→ = 0|b
α |→ = 0|A → B|→ = |A|→ + |B|→ + 1|∀x.A|→ = |A|→P|Ω|→ =
A≤B∈Ω |A|→ + |B|→37

3 Higher-Ranked Polymorphism Subtyping Algorithm
The context measure | · |αb counts the number of unsolved existential variables.
Definition 3 (Context Measure).
| · |αb = 0|Γ, a|αb = |Γ|αb|Γ, αb |αb = |Γ|αb + 1

It is not difficult to see that all but two of the algorithm’s rules decrease one of the three measures. The two exceptions are the Rules ≤a instL and ≤a instR; both increment the numberof 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 judgments, which we callinstantiation judgments Ωi , separately. They take the form:
Definition 4 (Ωi ).
Ωi := · | αb ≤ A; Ω′i | A ≤ αb ; Ω′iwhere αb∈
/ F V (A) ∪ F V (Ω′i )These instantiation judgments are these ones consumed and produced by Rules ≤a instL and≤a instR. The following lemma handles their decidability.
Lemma 3.7 (Instantiation Decidability). For any context Γ and judgment list Ωi , Ω, it is decidable
whether Γ ⊢ Ωi , Ω if both of the conditions hold1) ∀Γ′ , Ω′ s.t. |Ω′ |∀ < |Ωi , Ω|∀ , it is decidable whether Γ′ ⊢ Ω′ .
2) ∀Γ′ , Ω′ s.t. |Ω′ |∀ = |Ωi , Ω|∀ and |Γ′ |αb = |Γ|αb − |Ωi |, it is decidable whether Γ′ ⊢ Ω′ .
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 ⟨|Ω|∀ , |Ω|αb , |Ω|→ ⟩. The critical case is that, whenever we encounter an instantiation judgment at the front of the worklist, we refer to Lemma 3.7, which reduces the number of unsolved variables by consuming that instantiation judgment, or reduces the number of∀-quantifiers. Other cases are relatively straightforward.

3.4 The Choice of Abella
We have chosen the Abella (v2.0.5) proof assistant [Gacek 2008] to develop our formalization.
Although Abella takes a two-level logic approach, where the specification logic can be expressed38

3 Higher-Ranked Polymorphism Subtyping Algorithm

separately from the reasoning logic, we only make use of its reasoning logic, due to the difficulty of expressing our algorithmic rules with only the specification. Abella is particularly helpful due to its built-in support for variable bindings, and its λ-tree syntax [Miller 2000] is a formof HOAS, which helps with the encoding and reasoning about substitutions. For instance, thetype ∀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. Name supply 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 any other names occurring elsewhere. Such variables are called nominal constants. They
can be of any type, in other words, every type may contain an unlimited number of such atomic
nominal constants.
Encoding of the Declarative System As a concrete example, our declarative context (wellformedness relation) and well-formedness rules are encoded as follows.
Kind ty
type.
Type ity.
Type all ( ty → ty) → ty.
Type arrow ty → ty → ty.
Type bound ty → o.

% the unit type
% forall-quantifier% 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).

In the above code, we first define the syntax of types and contexts in our type system. A
type of our system has type ty, and the context is of type olist. 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”, and both are built-in types of Abella. The
member : o → olist → prop relation is also pre-defined.

Note that in Abella, the symbol (:= ) used in definitions is similar to the (:− ) symbol in Prolog, where we write the condition to its right and the conclusion to its left. The second case of
the relation wft states Rule wfd var. The encoding ( E x) basically means 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 and39

3 Higher-Ranked Polymorphism Subtyping AlgorithmFile(s)olist.thm, nat.thm
higher.thm, order.thm
higher_alg.thm
trans.thmsound.thm
depth.thm
complete.thm
decidable.thm
Total

SLOC
303
164
618
411
166
143
626
1077
3627

# of Theorems
55
15
44
46
2
12
28
53
267

Description
Basic data structures
Declarative system
Algorithmic system
Transfer
Soundness theorem
Definition of depth
Lemmas and Completeness theorem
Lemmas and Decidability theorem(33 definitions in total)

Figure 3.8: Statistics for the proof scripts
member (bound x) E make no sense. Instead, we treat E : ty → olist as an abstract structure ofa context, such as x\ 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 ...

In this piece of code, we use Exp to denote the worklist Ω. An algorithmic existential variable αbis constructed by applying the Abella term exvar to an actual nabla quantified variable. Thanks
to the way Abella deals with nominal constants, the pattern subt x ( arrow A B) implicitly statesthat x ∈/ F V (A) ∧ x ∈/ F V (B). If the condition were not required, we would have encoded thepattern as subt x ( arrow (A x) ( B x)) instead.

40

3 Higher-Ranked Polymorphism Subtyping Algorithm

3.4.1 Statistics and Discussion
Some basic statistics on our proof script are shown in Figure 3.8. 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 tactics1 Moreover, the definition of natural numbers, theplus operation and less-than relation are defined within our proof due to Abella’s lack of packages.
However, the way Abella deals with name bindings is very helpful for type system formalizations
and substitution-intensive formalizations, such as this one.

1

We do extend Abella with some handy tactics after this work, which boosts our development and reduce someboilerplate codes. One may find the modified version in https://github.com/JimmyZJX/abella.

41

4 A Type-Inference Algorithm forHigher-Ranked Polymorphism
This chapter presents the first fully mechanized formalization of the metatheory for higher-ranked
polymorphic type inference. Following the woirklist subtyping algorithm in the previous chapter,
we address several drawbacks and extend the technique to DK’s bidirectional type system [Dunfield and Krishnaswami 2013]. We chose DK’s type system because it is quite elegant, welldocumented and it comes with detailed manually written proofs. Furthermore, the system isadopted in practice by a few real implementations of functional languages, including PureScriptand Unison. The DK type system has two variants: a declarative and an algorithmic one. The twovariants have been manually proved to be sound, complete and decidable. We present a mechanical formalization in the Abella theorem prover [Gacek 2008] for DK’s declarative type systemusing a different algorithm.
Challenges While our initial goal was to formalize both DK’s declarative and algorithmic
versions, we faced technical challenges with the latter, prompting us to find an alternative formulation.
The first challenge that we faced were missing details as well as a few incorrect proofs andlemmas in DK’s formalization. While DK’s original formalization comes with very well-written
manual proofs, there are still several details missing. These complicate the task of writing a mechanically verified proof. Moreover, some proofs and lemmas are wrong and, in some cases, it is
not clear to us how to fix them.
Despite the problems in DK’s manual formalization, we believe that these problems do notinvalidate their work and that their results are still true. In fact we have nothing but praise for
their detailed and clearly written metatheory and proofs, which provided invaluable help to ourown work. We expect that for most non-trivial manual proofs similar problems exist, so thisshould not be understood as a sign of sloppiness on their part. Instead, it should be an indicatorthat reinforces the arguments for mechanical formalizations: manual formalizations are errorprone due to the multiple tedious details involved in them. There are several other examplesof manual formalizations that were found to have similar problems. For example, Klein et al.

42

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism[2012] mechanized formalizations in Redex for nine ICFP 2009 papers and all were found tohave mistakes.
Another challenge was variable binding. Type inference algorithms typically do not rely simply
on local environments but instead propagate information across judgments. While local environments are well-studied in mechanical formalizations, there is little work on how to deal with thecomplex forms of binding employed by type inference algorithms in theorem provers. To keep
track of variable scoping, DK’s algorithmic version employs input and output contexts to track
information that is discovered through type inference. However, modeling output contexts in atheorem prover is non-trivial.
Due to those two challenges, our work takes a different approach by refining and extending
the idea of worklist judgments in Chapter 3, where we mechanically formalized an algorithm forpolymorphic subtyping [Odersky and Läufer 1996]. The algorithm eliminates output contexts
compared to DK’s algorithm, and therefore the problem of variable binding is solved. Unfortunately, the subtyping algorithm cannot be naively extended to support the bidirectional typesystem. A key innovation in the new algorithm to be introduced in this chapter is how to adapt
the idea of worklist judgments to inference judgments, which are not needed for polymorphic
subtyping, but are necessary for type inference. The idea is to use a continuation passing style toenable the transfer of inferred information across judgments. A further refinement to the ideaof worklist judgments is the unification between ordered contexts [Dunfield and Krishnaswami
2013; Gundry et al. 2010] and worklists. This enables precise scope tracking of free variables injudgments. Furthermore it avoids the duplication of context information across judgments inworklists that occurs in other techniques [Abel and Pientka 2011; Reed 2009]. Despite the useof a different algorithm, we prove the same results as DK, although with significantly different
proofs and proof techniques. The calculus and its metatheory have been fully formalized in the
Abella theorem prover [Gacek 2008].

4.1 Overview
This section starts with a discussion on DK’s declarative type system. Then it introduces several
techniques that have been used in algorithmic formulations, and which have influenced our own
algorithmic design. Finally we introduce the novelties of our new algorithm. In particular the
support for inference judgments in worklist judgments, and a new form of worklist judgmentthat unifies ordered contexts and the worklists themselves.

43

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

Type variables
Types
Monotypes
Expressions
Contexts

a, b
A, B, Cτ, σe
Ψ

1 | a | ∀a. A | A → B
1|a|τ →σx | () | λx. e | e1 e2 | (e : A)
· | Ψ, a | Ψ, x : A

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

Figure 4.1: Syntax of Declarative System (Extends Figure 3.1)

Ψ ⊢ A Well-formed declarative type
Ψ⊢1

a∈Ψ

wfd unitΨ⊢aΨ⊢A

wfd var

Ψ⊢B

Ψ⊢A→B

Ψ, a ⊢ A

wfd →Ψ ⊢ ∀a.Awfd ∀Ψ ⊢ e Well-formed declarative expression
x:A∈Ψ

wfd tmvar

Ψ⊢xΨ ⊢ e1Ψ ⊢ e2Ψ ⊢ e1 e2Ψ ⊢ ()

wfd tmunitΨ⊢A

wfd appΨ, x : A ⊢ eΨ ⊢ λx. eΨ⊢eΨ ⊢ (e : A)

wfd abs

wfd annoΨ ⊢ A ≤ B Declarative subtyping
a∈Ψ
Ψ⊢a≤a

≤Var

Ψ⊢1≤1

Ψ⊢τ

≤Unit

Ψ ⊢ [τ /a]A ≤ BΨ ⊢ ∀a. A ≤ B≤∀LΨ ⊢ B 1 ≤ A1

Ψ ⊢ A2 ≤ B 2

Ψ ⊢ A1 → A2 ≤ B1 → B2
Ψ, b ⊢ A ≤ B
Ψ ⊢ A ≤ ∀b. B

≤→

≤∀R

Figure 4.2: Declarative Well-formedness and Subtyping

4.1.1 DK’s Declarative System
Subsection 2.3.1 introduces DK’s declarative subtyping and typing systems. We also duplicate therules here for the convenience of the reader.
Overlapping Rules A problem that we found in the declarative system is that some of the rules
overlap with each other. Declarative subtyping rules ≤∀L and ≤∀R both match the conclusionΨ ⊢ ∀a. A ≤ ∀a. B. In such a case, choosing ≤∀R first is always better, since we introduce
the type variable a to the context earlier, which gives more flexibility on the choice of τ . The
declarative typing rule DeclSub overlaps with both Decl∀I and Decl→I. However, we argue44

4 A Type-Inference Algorithm for Higher-Ranked PolymorphismΨ⊢e⇐Ae checks against input type A.

Ψ⊢e⇒Ae synthesizes output type A.

Ψ ⊢ A • e ⇒⇒ C

Applying a function of type A to e synthesizes type C.

(x : A) ∈ Ψ
Ψ⊢x⇒A
Ψ⊢A

Ψ⊢e⇐A

Ψ ⊢ (e : A) ⇒ A

DeclVar

DeclAnno

Ψ, a ⊢ e ⇐ AΨ ⊢ e ⇐ ∀a. A

Ψ ⊢ e1 ⇒ A Ψ ⊢ A • e2 ⇒⇒ C
Ψ ⊢ e1 e2 ⇒ C

Decl1IΨ ⊢ () ⇐ 1

DeclSubΨ ⊢ () ⇒ 1

Ψ ⊢ [τ /a]A • e ⇒⇒ C

Ψ ⊢ ∀a. A • e ⇒⇒ C

Decl→IΨ ⊢ λx. e ⇐ A → B

Ψ⊢A≤B

Ψ⊢e⇐B

Ψ⊢τ

Decl∀IΨ, x : A ⊢ e ⇐ B

Ψ⊢e⇒A

Ψ⊢σ→τ

Decl∀AppΨ, x : σ ⊢ e ⇐ τΨ ⊢ λx. e ⇒ σ → τ

Decl→I⇒Ψ⊢e⇐A

Decl→E

Decl1I⇒Ψ ⊢ A → C • e ⇒⇒ C

Decl→App

Figure 4.3: Declarative Typingthat more specific rules are always the best choices, i.e. Decl∀I and Decl→I should have higher
priority than DeclSub.
For example, Ψ ⊢ λx. x ⇐ ∀a. a → a succeeds if derived from Rule Decl∀I:Ψ, a, x : a ⊢ x ⇐ a
Ψ, a ⊢ λx. x ⇐ a → a

Decl→IΨ ⊢ λx. x ⇐ ∀a. a → a

Decl∀I,but fails when applied to DeclSub:
Impossible!
a∈/ FV(σ)Ψ, a ⊢ a ≤ σ
Ψ⊢σ→τ

Ψ, x : σ ⊢ e ⇐ τΨ ⊢ λx. x ⇒ σ → τ?

Ψ, a ⊢ τ ≤ a

Ψ, a ⊢ σ → τ ≤ a → a

Decl→I⇒Ψ ⊢ σ → τ ≤ ∀a. a → aΨ ⊢ λx. x ⇐ ∀a. a → a≤→≤∀R
DeclSub.

Rule Decl→I is also better at handling higher-order types. When the lambda-expression to
be inferred has a polymorphic input type, such as ∀a. a → a, DeclSub may not derive some45

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
judgments. For example, Ψ, id : ∀a. a → a ⊢ λf. f id (f ()) ⇐ (∀a. a → a) → 1 requires
the argument of the lambda-expression to be a polymorphic type, otherwise it could not be applied to both id and (). If Rule DeclSub was chosen for derivation, the type of its argument isrestricted by Rule Decl→I⇒, which is not a polymorphic type. By contrast, Rule Decl→I keeps
the polymorphic argument type ∀a. a → a, and will successfully derive the judgment.
We will come back to this topic in Section 4.3.2 and formally derive a system without overlapping rules.

4.1.2 DK’s Algorithm
DK’s algorithm version revolves around their notion of algorithmic context.
Algorithmic Contexts

Γ, ∆, Θ ::=· | Γ, a | Γ, x : A | Γ, αb | Γ, αb = τ | Γ, ▶αbIn addition to the regular (universally quantified) type variables a, the algorithmic context also
contains existential type variables α
b . These are placeholders for monotypes τ that are still to be
determined by the inference algorithm. When the existential variable is “solved”, its entry in thecontext is replaced by the assignment αb = τ . A context application on a type, denoted by [Γ]A,substitutes all solved existential type variables in Γ with their solutions on type A.
All algorithmic judgments thread an algorithmic context. They have the form Γ ⊢ . . . ⊣ ∆,where Γ is the input context and ∆ is the output context: Γ ⊢ A ≤ B ⊣ ∆ for subtyping,Γ ⊢ e ⇐ A ⊣ ∆ for type checking, and so on. The output context is a functional update of the
input context that records newly introduced existentials and solutions.
Solutions are incrementally propagated by applying the algorithmic output context of a previous task as substitutions to the next task. This can be seen in the subsumption rule:Γ⊢e⇒A⊣ΘΘ ⊢ [Θ]A ≤ [Θ]B ⊣ ∆Γ⊢e⇐B⊣∆

DK_Sub

The inference task yields an output context Θ which is applied as a substitution to the types A
and B before performing the subtyping check to propagate any solutions of existential variables
that appear in A and B.
Markers for scoping. The sequential order of entries in the algorithmic context, in combination with the threading of contexts, does not perfectly capture the scoping of all existential46

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
variables. For this reason the DK algorithm uses scope markers ▶αb in a few places. An example
is given in the following rule:Γ, ▶αb , αb ⊢ [bα /a]A ≤ B ⊣ ∆, ▶αb , ΘΓ ⊢ ∀a. A ≤ B ⊣ ∆DK_≤∀LTo indicate that the scope of αb is local to the subtyping check [bα /a]A ≤ B, the marker is pushed
onto its input stack and popped from the output stack together with the subsequent part Θ, which
may refer to αb . (Remember that later entries may refer to earlier ones, but not vice versa.) Thisway αb does not escape its scope.
One may suggest that the marker ▶αb is somewhat redundant, since αb already declares thescope. However, in the following rule,Γ[bα2 , αb1 , αb=αb1 → αb2 ] ⊢ A1 ≤ αb1 ⊣ ΘΘ⊢αb2 ≤ [Θ]A2 ⊣ ∆Γ[bα] ⊢ αb ≤ A1 → A2 ⊣ ∆DK_InstLArr

the algorithm introduces new existential variables right before αb . In such case, the marker ▶αb still
appears to the left of them. Without the marker, it will be difficult to recycle the new existential
variables α
b1 and α
b2 properly, which should have the same scope of αb and thus should be recycled
together with αb.
At first sight, the DK algorithm would seem to be a good basis for mechanization. After all, it
comes with a careful description and extensive manual proofs. Unfortunately, we ran into several
obstacles that have prompted us to formulate a different, more mechanization-friendly algorithm.
Broken Metatheory While going through the manual proofs of DK’s algorithm, we foundseveral problems. Indeed, two proofs of lemmas—Lemma 19 (Extension Equality Preservation)and Lemma 14 (Subsumption)— wrongly apply induction hypotheses in several cases. Fortunately, we have found simple workarounds that fix these proofs without affecting the appeals tothese lemmas.
More seriously, we have also found a lemma that simply does not hold: Lemma 29 (Parallel Admissibility)1 . This lemma is used to relate the algorithmic system and declarative system before
and after the instantiation procedure. We believe that the general idea of the lemma is correct, but
the statement may fail when the sensitive ordering of variables breaks the “parallelism” in somecorner cases. This lemma is a cornerstone of the two metatheoretical results of the algorithm,
soundness, and completeness with respect to the declarative system. In particular, both instanti1

Ningning Xie found the issue with Lemma 29 in 2016 on an earlier attempt to mechanically formalize DK’s algorithm. The authors acknowledged the problem after we contacted them through email. Although they briefly
mentioned that it should be possible to use a weaker lemma instead they did not go into details.

47

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

ation soundness (i.e. a part of subtyping soundness) and typing completeness directly require thebroken lemma. Moreover, Lemma 54 (Typing Extension) also requires the broken lemma and isitself used 13 times in the proof of typing soundness and completeness. Unfortunately, we have
not yet found a way to fix this problem.
In what follows, we briefly discuss the problem through counterexamples. False lemmas arefound in the manual proofs of DK’ two papers [Dunfield and Krishnaswami 2013] and [Dunfield
and Krishnaswami 2019].
• In the first paper, Lemma 29 on page 9 of its appendix says:
Lemma 4.1 (Parallel Admissibility of [Dunfield and Krishnaswami 2013]).
If ΓL −→ ∆L and ΓL , ΓR −→ ∆L , ∆R then:
1. ΓL , αb , ΓR −→ ∆L , αb , ∆R
2. If ∆L ⊢ τ ′ then ΓL , αb , ΓR −→ ∆L , αb = τ ′ , ∆R .
3. If ΓL ⊢ τ and ∆L ⊢ τ ′ and [∆L ]τ = [∆L ]τ ′ , then ΓL , αb = τ, ΓR −→ ∆L , αb =τ ′ , ∆R .
We give a counter-example to this lemma:b ∆L = β,b ∆R = ·, then both conditions · −→ βb and βb −→ βb hold,
Pick ΓL = ·, ΓR = β,bαbut the first conclusion αb , βb −→ β,b does not hold.

• In the second paper, as an extended work to the first paper, Lemma 26 on page 22 of its
appendix says:
Lemma 4.2 (Parallel Admissibility of [Dunfield and Krishnaswami 2019]).
If ΓL −→ ∆L and ΓL , ΓR −→ ∆L , ∆R then:
1. ΓL , αb : κ, ΓR −→ ∆L , αb : κ, ∆R
2. If ∆L ⊢ τ ′ : κ then ΓL , αb : κ, ΓR −→ ∆L , αb : κ = τ ′ , ∆R .
3. If ΓL ⊢ τ : κ and ∆L ⊢ τ ′ types and [∆L ]τ = [∆L ]τ ′ , then ΓL , αb : κ = τ, ΓR −→∆L , αb : κ = τ ′ , ∆R .
A similar counter-example is given:
Pick ΓL = ·, ΓR = βb : ?, ∆L = βb : ?, ∆R = ·, then both conditions · −→ βb : ? andβb : ? −→ βb : ? hold, but the first conclusion αb : κ, βb : ? −→ βb : ?, αb : κ does not hold.

48

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

Complex Scoping and Propagation Besides the problematic lemmas in DK’s metatheory,
there are other reasons to look for an alternative algorithmic formulation of the type system that ismore amenable to mechanization. Indeed, two aspects that are particularly challenging to mechanize are the scoping of universal and existential type variables, and the propagation of the instantiation of existential type variables across judgments. DK is already quite disciplined on theseaccounts, in particular compared to traditional constraint-based type-inference algorithms like
Algorithm W [Milner 1978] which features an implicit global scope for all type variables. Indeed,
DK uses its explicit and ordered context Γ that tracks the relative scope of universal and existential
variables and it is careful to only instantiate existential variables in a well-scoped manner.
Moreover, DK’s algorithm carefully propagates instantiations by recording them into the context and threading this context through all judgments. While this works well on paper, this approach is still fairly involved and thus hard to reason about in a mechanized setting. Indeed, theinstantiations have to be recorded in the context and are applied incrementally to each remaining
judgment in turn, rather than immediately to all remaining judgments at once. Also, as we havementioned above, the stack discipline of the ordered contexts does not mesh well with the useof output contexts; explicit marker entries are needed in two places to demarcate the end of an
existential variable’s scope. Actually, we found a scoping issue related to the subsumption rule
DK_Sub, which might cause existential variables to leak across judgments. In Section 4.4.1 wegive a detailed discussion.
The complications of scoping and propagation are compelling reasons to look for another algorithm that is easier to reason about in a mechanized setting.

4.1.3 Judgment Lists
To avoid the problem of incrementally applying a substitution to remaining tasks, we can findinspiration in the formulation of constraint solving algorithms. For instance, the well-known
unification algorithm by Martelli and Montanari [1982] decomposes the problem of unifying.

.

two terms s = t into a number of related unification problems between pairs of terms si = ti .
These smaller problems are not tackled independently, but kept together in a set S. The algorithm
itself is typically formulated as a small-step-style state transition system S ↣ S ′ that rewrites theset of unification problems until it is in solved form or until a contradiction has been found. For
instance, the variable elimination rule is written as:.

.

x = t, S ↣ x = t, [t/x]S

if x ̸∈ t and x ∈ S

Because the whole set is explicitly available, the variable x can be simultaneously substituted.
In the above unification problem, all variables are implicitly bound in the same global scope.
Some constraint solving algorithms for Hindley-Milner type inference use similar ideas, but are49

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

more careful tracking the scopes of variables [Pottier and Rémy 2005]. Recent unification algorithms for dependently-typed languages are also more explicit about scopes. For instance, Reed[2009] represents a unification problem as ∆ ⊢ P where P is a set of equations to be solved and∆ is a (modal) context. Abel and Pientka [2011] even use multiple contexts within a unification
problem. Such a problem is denoted ∆ ⊩ K where the meta-context ∆ contains all the typingsof meta-variables in the constraint set K. The latter consists of constraints like Ψ ⊢ M = N : C
that are equipped with their individual context Ψ. While accurately tracking the scoping of regular and meta-variables, this approach is not ideal because it repeatedly copies contexts when
decomposing a unification problem, and later it has to substitute solutions into these copies.

4.1.4 Single-Context Worklist Algorithm for Subtyping
As we have seen in Chapter 3, an algorithm based on worklist judgments is mechanized and shown
to be correct with respect to DK’s declarative subtyping judgment. This approach overcomes someproblems in DK’s algorithmic formulation by using a worklist-based judgment of the formΓ⊢Ω
where Ω is a worklist (or sequence) of subtyping problems of the form A ≤ B. The judgment
is defined by case analysis on the first element of Ω and recursively processes the worklist until
it is empty. Using both a single common ordered context Γ and a worklist Ω greatly simplifies
propagating the instantiation of type variables in one subtyping problem to the remaining ones.
Unfortunately, this work does not solve all problems. In particular, it has two major limitations
that prevent it from scaling to the whole DK system.
Scoping Garbage Firstly, the single common ordered context Γ does not accurately reflect thetype and unification variables currently in scope. Instead, it is an overapproximation that steadily
accrues variables, and only drops those unification variables that are instantiated. In other words,
Γ contains “garbage” that is no longer in scope. This complicates establishing the relation withthe declarative system.
No Inference Judgments Secondly, and more importantly, the approach only deals with ajudgment for checking whether one type is the subtype of another. While this may not be sodifficult to adapt to the checking mode of term typing Γ ⊢ e ⇐ A, it clearly lacks the functionality
to support the inference mode of term typing Γ ⊢ e ⇒ A. Indeed, the latter requires not only thecommunication of unification variable instantiations from one typing problem to another, butalso an inferred type.

50

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

4.1.5 Algorithmic Type Inference for Higher-Ranked Types: Key Ideas
Our new algorithmic type system builds on the work above, but addresses the open problems.
Scope Tracking We avoid scoping garbage by blending the ordered context and the worklist
into a single syntactic sort Γ, our algorithmic worklist. This algorithmic worklist interleaves (typeand term) variables with work like checking or inferring types of expressions. The interleaving
keeps track of the variable scopes in the usual, natural way: each variable is in scope of anythingin front of it in the worklist. If there is nothing in front, the variable is no longer needed and canbe popped from the worklist. This way, no garbage (i.e. variables out-of-scope) builds up.

Algorithmic judgment chainω ::=A ≤ B | e ⇐ A | e ⇒a ω | A • e ⇒⇒a ω

Algorithmic worklistΓ ::=· | Γ, a | Γ, αb | Γ, x : A | Γ ⊩ ωFor example, suppose that the top judgment of the following worklist checks the identity function against ∀a. a → a:Γ ⊩ λx. x ⇐ ∀a. a → a
To proceed, two auxiliary variables a and x are introduced to help the type checking:Γ, a, x : a ⊩ x ⇐ awhich will be satisfied after several steps, and the worklist becomes
Γ, a, x : a
Since the variable declarations a, x : a are only used for a judgment already processed, they canbe safely removed, leaving the remaining worklist Γ to be further reduced.
Our worklist can be seen as an all-in-one stack, containing variable declarations and subtyping/typing judgments. The stack is an enriched form of ordered context, and it has a similar variablescoping scheme.
Inference Judgments To express the DK’s inference judgments, we use a novel form of work
entries in the worklist: our algorithmic judgment chains ω. In its simplest form, such a judgment
chain is just a check, like a subtyping check A ≤ B or a term typecheck e ⇐ A. However, thenon-trivial forms of chains capture an inference task together with the work that depends on its
outcome. For instance, a type inference task takes the form e ⇒a ω. This form expresses that weneed to infer the type, say A, for expression e and use it in the chain ω by substituting it for the51

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

placeholder type variable a. Notice that such a binds a fresh type variable for the inner chain ω,
which behaves similarly to the variable declarations in the context.
Take the following worklist as an exampleαb ⊩ (λx. x) () ⇒a a ≤ αb, x : αb , βb ⊩ α
b ≤ βb ⊩ βb ≤ 1
There are three (underlined) judgment chains in the worklist, where the first and second judgment
chains (from the right) are two subtyping judgments, and the third judgment chain, (λx. x) () ⇒aa≤αb , is a sequence of an inference judgment followed by a subtyping judgment.
The algorithm first analyses the two subtyping judgments and will find the best solutions αb=b
β = 1 (please refer to Figure 4.5 for detailed derivations). Then we substitute every instance ofαb and βb with 1, so the variable declarations can be safely removed from the worklist. Now we
reduce the worklist to the following state· ⊩ (λx. x) () ⇒a a ≤ 1, x : 1
which has a term variable declaration as the top element. After removing the garbage term variable declaration from the worklist, we process the last remaining inference judgment (λx. x) () ⇒ ?,with the unit type 1 as its result. Finally, the last judgment becomes 1 ≤ 1, a trivial base case.

4.2 Algorithmic System
This section introduces a novel algorithmic system that implements DK’s declarative specification.
The new algorithm extends the idea of worklists in Chapter 3 in two ways. Firstly, unlike its
worklists, the scope of variables is precisely tracked and variables do not escape their scope. This isachieved by unifying algorithmic contexts and the worklists themselves. Secondly, our algorithm
also accounts for the type system (and not just subtyping). To deal with inference judgments thatarise in the type system we employ a continuation passing style to enable the transfer of inferred
information across judgments in a worklist.

4.2.1 Syntax and Well-Formedness
Figure 4.4 shows the syntax and well-formedness judgments used by the algorithm. Similarly
to the declarative system the well-formedness rules are unsurprising and merely ensure wellscopedness.
Existential Variables The algorithmic system inherits the syntax of terms and types fromthe declarative system. It only introduces one additional feature. In order to find unknown types

52

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

Existential variables αb , βbA, B, C ::= 1 | a | ∀a. A | A → B | αbAlgorithmic types

Algorithmic judgment chain ω::=A ≤ B | e ⇐ A | e ⇒a ω | A • e ⇒⇒a ω

Algorithmic worklist Γ::=· | Γ, a | Γ, αb | Γ, x : A | Γ ⊩ ωΓ ⊢ A Well-formed algorithmic typea∈Γ

wf_unit

Γ⊢1

Γ⊢A

Γ⊢a

Γ⊢B

Γ⊢A→B

α
b∈Γ

wf_varΓ, a ⊢ A

wf_→

wf_exvar

Γ⊢α
b

wf_∀

Γ ⊢ ∀a.AΓ ⊢ e Well-formed algorithmic expression
x:A∈Γ
Γ⊢x

wf_tmvarΓ ⊢ e1Γ ⊢ ()Γ ⊢ e2Γ ⊢ e1 e2Γ, x : A ⊢ e

wf_tmunitΓ ⊢ λx. eΓ⊢A

wf_appΓ⊢eΓ ⊢ (e : A)

wf_abswf_annoΓ ⊢ ω Well-formed algorithmic judgment
Γ⊢A

Γ⊢B

Γ⊢A≤B
Γ⊢e

Γ, a ⊢ ωΓ ⊢ e ⇒a ω

Γ⊢e

wf≤

Γ⊢e⇐A

Γ⊢A

wf⇒

Γ⊢A

wf⇐

Γ, a ⊢ ωΓ⊢eΓ ⊢ A • e ⇒⇒a ω

wf⇒⇒

wf Γ Well-formed algorithmic worklist

wf ·
wf Γ

wf·

wf Γ
wf Γ, aΓ⊢A

wf Γ, x : A

wf Γ

wfa

wf Γ, α
b

wf Γ

wfof

wfαb

Γ⊢ω

wf Γ ⊩ ωwfω

Figure 4.4: Extended Syntax and Well-Formedness for the Algorithmic System53

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

τ in the declarative system, the algorithmic system extends the declarative types A with existential
b They behave like unification variables, but their scope is restricted by their position
variables αb , β.
in the algorithmic worklist rather than being global. Any existential variable αb should only besolved to a type that is well-formed with respect to the worklist to which αb has been added. The
point is that the monotype τ , represented by the corresponding existential variable, is always wellformed under the corresponding declarative context. In other words, the position of αb ’s reflects
the well-formedness restriction of τ ’s.
Judgment Chains Judgment chains ω, or judgments for short, are the core components of ouralgorithmic type-checking. There are four kinds of judgments in our system: subtyping (A ≤ B),
checking (e ⇐ A), inference (e ⇒a ω) and application inference (A • e ⇒⇒a ω). Subtyping
and checking are relatively simple, since their result is only success or failure. However bothinference and application inference return a type that is used in subsequent judgments. We use acontinuation-passing-style encoding to accomplish this. For example, the judgment chain e ⇒a(a ≤ B) contains two judgments: first we want to infer the type of the expression e, and thencheck if that type is a subtype of B. The unknown type of e is represented by a type variable a,which is used as a placeholder in the second judgment to denote the type of e.
Worklist Judgments Our algorithm has a non-standard form. We combine traditional contexts and judgment(s) into a single sort, the worklist Γ. The worklist is an ordered collection ofboth variable bindings and judgments. The order captures the scope: only the objects that comeafter a variable’s binding in the worklist can refer to it. For example, [·, a, x : a ⊩ x ⇐ a] is
a valid worklist, but [· ⊩ x ⇐ a, x : a, a] is not (the underlined symbols refer to out-of-scope
variables).
Hole Notation We use the syntax Γ[ΓM ] to denote the worklist ΓL , ΓM , ΓR , where Γ is theworklist ΓL , •, ΓR with a hole (•). Hole notations with the same name implicitly share the samestructure ΓL and ΓR . A multi-hole notation splits the worklist into more parts. For example,b means Γ1 , αb Γ3 .
Γ[bα ][β]b , Γ2 , β,4.2.2 Algorithmic System
The algorithmic typing reduction rules, defined in Figure 4.5, have the form Γ −→ Γ′ . The
reduction process treats the worklist as a stack. In every step, it pops the first judgment fromthe worklist for processing and possibly pushes new judgments onto the worklist. The syntax
Γ −→∗ Γ′ denotes multiple reduction steps.

54

4 A Type-Inference Algorithm for Higher-Ranked PolymorphismΓ −→ Γ′Γ, a −→1 ΓΓ reduces to Γ′ .
Γ, αb −→2 ΓΓ, x : A −→3 ΓΓ ⊩ 1 ≤ 1 −→4 ΓΓ ⊩ a ≤ a −→5 ΓΓ⊩αb≤αb −→6 ΓΓ ⊩ A1 → A2 ≤ B1 → B2 −→7 Γ ⊩ A2 ≤ B2 ⊩ B1 ≤ A1
Γ ⊩ ∀a. A ≤ B −→8 Γ, αb ⊩ [bα /a]A ≤ B

when B ̸= ∀a. B ′Γ ⊩ A ≤ ∀b. B −→9 Γ, b ⊩ A ≤ B
Γ[bα] ⊩ αb ≤ A → B −→10 [bα1 → αb2 /bα ](Γ[bα1 , αb2 ] ⊩ αb1 → αb2 ≤ A → B)
when αb∈/ F V (A) ∪ F V (B)Γ[bα] ⊩ A → B ≤ αb −→11 [bα1 → αb2 /bα ](Γ[bα1 , αb2 ] ⊩ A → B ≤ αb1 → αb2 )b∈/ F V (A) ∪ F V (B)when αb ⊩αb
Γ[bα ][β]b ≤ βb −→12 [bα /β](Γ[bα ][])b ⊩ βb ≤ αb
Γ[bα ][β]b −→13 [bα /β](Γ[bα ][])b ⊩ a ≤ βb −→14 [a/β](Γ[a][])b
Γ[a][β]b ⊩ βb ≤ a −→15 [a/β](Γ[a][])b
Γ[a][β]b ⊩ 1 ≤ βb −→16 [1/β](Γ[])
bΓ[β]b ⊩ βb ≤ 1 −→17 [1/β](Γ[])
bΓ[β]Γ ⊩ e ⇐ B −→18 Γ ⊩ e ⇒a a ≤ Bwhen e ̸= λx. e′ and B ̸= ∀a. B ′Γ ⊩ e ⇐ ∀a. A −→19 Γ, a ⊩ e ⇐ AΓ ⊩ λx. e ⇐ A → B −→20 Γ, x : A ⊩ e ⇐ B
Γ[bα ] ⊩ λx. e ⇐ αb −→21 [bα1 → αb2 /bα ](Γ[bα1 , αb2 ], x : α
b1 ⊩ e ⇐ αb2 )Γ ⊩ x ⇒a ω −→22 Γ ⊩ [A/a]ω

when (x : A) ∈ ΓΓ ⊩ (e : A) ⇒a ω −→23 Γ ⊩ [A/a]ω ⊩ e ⇐ A
Γ ⊩ () ⇒a ω −→24 Γ ⊩ [1/a]ω
bΓ ⊩ λx. e ⇒a ω −→25 Γ, αb , βb ⊩ [bα → β/a]ω,x:αb ⊩ e ⇐ βb
Γ ⊩ e1 e2 ⇒a ω −→26 Γ ⊩ e1 ⇒b (b • e2 ⇒⇒a ω)Γ ⊩ ∀a. A • e ⇒⇒a ω −→27 Γ, αb ⊩ [bα /a]A • e ⇒⇒a ωΓ ⊩ A → C • e ⇒⇒a ω −→28 Γ ⊩ [C/a]ω ⊩ e ⇐ A
Γ[bα] ⊩ αb • e ⇒⇒a ω −→29 [bα1 → αb2 /bα ](Γ[bα1 , αb2 ] ⊩ αb1 → αb2 • e ⇒⇒a ω)
Figure 4.5: Algorithmic Typing55

4 A Type-Inference Algorithm for Higher-Ranked PolymorphismΓ −→∗ Γ∗−→ id

Γ −→ Γ1Γ1 −→∗ Γ′Γ −→∗ Γ′−→∗ step

In the case that Γ −→∗ · this corresponds to successful type checking.
Please note that when a new variable is introduced in the right-hand side worklist Γ′ , we implicitly pick a fresh one, since the right-hand side can be seen as the premise of the reduction.
Rules 1-3 pop variable declarations that are essentially garbage. Those variables are out of scope
for the remaining judgments in the worklist. All other rules concern a judgment at the front of
the worklist. Logically we can discern 6 groups of rules.
1. Algorithmic subtyping We have six subtyping rules (Rules 4-9) that are similar to theirdeclarative counterparts. For instance, Rule 7 consumes a subtyping judgment and pushes twoback to the worklist. Rule 8 differs from declarative Rule ≤∀L by introducing an existential variable α
b instead of guessing the monotype τ instantiation. Each existential variable is later solved
to a monotype τ with the same context, so the final solution τ of αb should be well-formed underΓ.
Worklist Variable Scoping Rules 8 and 9 involve variable declarations and demonstrate how
our worklist treats variable scopes. Rule 8 introduces an existential variable αb that is only visible
to the judgment [bα /a]A ≤ B. Reduction continues until all the subtyping judgments in front ofαb are satisfied. Finally we can safely remove αb since no occurrence of αb could have leaked into
the left part of the worklist. Moreover, the algorithm garbage-collects the αb variable at the righttime: it leaves the environment immediately after being unreferenced completely for sure.
Example Consider the derivation of the subtyping judgment (1 → 1) → 1 ≤ (∀a. 1 → 1) →1:· ⊢ (1 → 1) → 1 ≤ (∀a. 1 → 1) → 1−→7 · ⊩ 1 ≤ 1 ⊩ ∀a. 1 → 1 ≤ 1 → 1−→8 · ⊩ 1 ≤ 1, αb⊩1→1≤1→1−→7 · ⊩ 1 ≤ 1, αb⊩1≤1⊩1≤1−→4 · ⊩ 1 ≤ 1, αb⊩1≤1−→4 · ⊩ 1 ≤ 1, αb−→2 · ⊩ 1 ≤ 1
−→4 ·

56

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

First, the subtyping of two function types is split into two judgments by Rule 7: a covariant subtyping on the return type and a contravariant subtyping on the argument type. Then we apply
Rule 8 to reduce the ∀ quantifier on the left side. The rule introduces an existential variable αbto the context (even though the type ∀a. 1 → 1 does not actually refer to the quantified typevariable a). In the following 3 steps we satisfy the judgment 1 → 1 ≤ 1 → 1 by Rules 7, 4, and 4(again).
Now the existential variable αb , introduced before but still unsolved, is at the top of the worklist
and Rule 2 garbage-collects it. The process is carefully designed within the algorithmic rules:
when αb is introduced earlier by Rule 8, we foresee the recycling of αb after all the judgments(potentially) requiring α
b have been processed. Finally Rule 4 reduces one of the base cases andfinishes the subtyping derivation.
2. Existential decomposition. Rules 10 and 11 are algorithmic versions of Rule ≤→; they bothpartially instantiate αb to function types. The domain α
b1 and range α
b2 of the new function type are
not determined: they are fresh existential variables with the same scope as αb . We replace αb in theworklist with α
b1 , αb2 . To propagate the instantiation to the rest of the worklist and maintain wellformedness, every reference to α
b is replaced by α
b1 → αb2 . The occurs-check condition prevents
divergence as usual. For example, without it αb≤1→αb would diverge.
3. Solving existentials

Rules 12-17 are base cases where an existential variable is solved. They

all remove an existential variable and substitute the variable with its solution in the remaining
worklist. Importantly the rules respect the scope of existential variables. For example, Rule 12
states that an existential variable αb can be solved with another existential variable βb only if βboccurs after αb.
One may notice that the subtyping relation for simple types is just equivalence, which is true
according to the declarative system. The DK’s system works in a similar way.
4. Checking judgments. Rules 18-21 deal with checking judgments. Rule 18 is similar to
DeclSub, but rewritten in the continuation-passing-style. The side conditions e ̸= λx. e′ andB ̸= ∀a. B ′ prevent overlap with Rules 19, 20 and 21; this is further discussed at the end of thissection. Rules 19 and 20 adapt their declarative counterparts to the worklist style. Rule 21 is a
special case of Decl → I, dealing with the case when the input type is an existential variable,
representing a monotype function as in the declarative system (it must be a function type, since
the expression λx. e is a function). The same instantiation technique as in Rules 10 and 11 applies. The declarative checking rule Decl1I does not have a direct counterpart in the algorithm,
because Rules 18 and 24 can be combined to give the same result.

57

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

Rule 21 Design Choice The addition of Rule 21 is a design choice we have made to simplify
the side condition of Rule 18 (which avoids overlap). It also streamlines the algorithm and themetatheory as we now treat all cases where we can see that an existential variable should be instantiated to a function type (i.e., Rules 10, 11, 21 and 29) uniformly.
The alternative would have been to omit Rule 21 and drop the condition on e in Rule 18. The
modified Rule 18 would then handle Γ ⊩ λx. e ⇐ αb and yield Γ ⊩ λx. e ⇒a a ≤ α
b , whichbbbbb
would be further processed by Rule 25 to Γ, β1 , β2 ⊩ β1 → β2 ≤ α
b , x : β1 ⊩ e ⇐ βb2 . As asubtyping constraint between monotypes is simply equality, βb1 → βb2 ≤ αb must end up equatingbb
β1 → β2 with αb and thus have the same effect as Rule 21, but in a more roundabout fashion.

In comparison, DK’s algorithmic subsumption rule has no restriction on the expression e, andthey do not have a rule that explicitly handles the case λx. e ⇐ α
b . Therefore the only way
to check a lambda function against an existential variable is by applying the subsumption rule,
which further breaks into type inference of a lambda function and a subtyping judgment.
5. Inference judgments. Inference judgments behave differently compared with subtyping andchecking judgments: they return a type instead of only accepting or rejecting. For the algorithmic
system, where guesses are involved, it may happen that the output type of an inference judgment
refers to new existential variables, such as Rule 25. In comparison to Rule 8 and 9, where new variables are only referred to by the sub-derivation, Rule 25 introduces variables αb , βb that affect theremaining judgment chain. This rule is carefully designed so that the output variables are boundby earlier declarations, thus the well-formedness of the worklist is preserved, and the garbage will
be collected at the correct time. By making use of the continuation-passing-style judgment chain,
inner judgments always share the context with their parent judgment.
Rules 22-26 deal with type inference judgments, written in continuation-passing-style. Whenan inference judgment succeeds with type A, the algorithm continues to work on the inner-chain
ω by assigning A to its placeholder variable a. Rule 23 infers an annotated expression by changing
into checking mode, therefore another judgment chain is created. Rule 24 is a base case, where
the unit type 1 is inferred and thus passed to its child judgment chain. Rule 26 infers the type ofan application by firstly inferring the type of the function e1 , and then leaving the rest work to an
application inference judgment, which passes a, representing the return type of the application,
to the remainder of the judgment chain ω.
Rule 25 infers the type of a lambda expression by introducing α
b , βb as the input and output typesof the function, respectively. After checking the body e under the assumption x : α
b , the returnb
type might reflect more information than simply α
b → β through propagation when existential
variables are solved or partially solved. The variable scopes are maintained during the process:the assumption of argument type (x : αb ) is recycled after checking against the function body;b are only visible in the remaining chain
the existential variables used by the function type (bα , β)

58

4 A Type-Inference Algorithm for Higher-Ranked Polymorphismb[b
α → β/a]ω.
The recycling process of Rule 25 differs from DK’s corresponding rule significantly,
and we further discuss the differences in Section 4.4.1.
6. Application inference judgments Finally, Rules 27-29 deal with application inference judgments. Rules 27 and 28 behave similarly to declarative rules Decl∀App and Decl → App. Rule
29 instantiates α
b1 → αb to the function type αb2 , just like Rules 10, 11 and 21.
Example Figure 4.6 shows a sample derivation of the algorithm. It checks the application(λx. x) () against the unit type. According to the algorithm, we apply Rule 18 (subsumption),changing to inference mode. Type inference of the application breaks into two steps by Rule 26:
first we infer the type of the function, and then the application inference judgment helps to determine the return type. In the following 5 steps the type of the identity function, λx. x, is inferred
to be αb→αb : checking the body of the lambda function (Rule 25), switching from check mode
to inference mode (Rule 18), inferring the type of a term variable (Rule 22), solving a subtyping
judgment between existential variables (Rule 12) and garbage collecting the term variable x (Rule3).
After that, Rule 28 changes the application inference judgment to a check of the argument
against the input type αb and returns the output type α
b . Checking () against the existential variableαb solves α
b to the unit type 1 through Rules 18, 24 and 16. Immediately after αb is solved, thealgorithm replaces every occurrence of α
b with 1. Therefore the worklist remains 1 ≤ 1, which isfinished off by Rule 4. Finally, the empty worklist indicates the success of the whole derivation.
In summary, our type checking algorithm accepts (λx. x) () ⇐ 1.
Non-overlapping and Deterministic Reduction An important feature of our algorithmic
rules is that they are directly implementable. Indeed, although written in the form of reduction
rules, they do not overlap and are thus deterministic.
Consider in particular Rules 8 and 9, which correspond to the declarative rules ≤∀L and ≤∀R.
While those declarative rules both match the goal ∀a. A ≤ ∀b. B, we have eliminated this overlap
in the algorithm by restricting Rule 8 (B ̸= ∀a. B ′ ) and thus always applying Rule 9 to ∀a. A ≤∀b. B.
Similarly, the declarative rule DeclSub overlaps highly with the other checking rules. Its algorithmic counterpart is Rule 18. Yet, we have avoided the overlap with other algorithmic checking
rules by adding side-conditions to Rule 18, namely e ̸= λx. e′ and B ̸= ∀a. B ′ .
These restrictions have not been imposed arbitrarily: we formally prove that the restrictedalgorithm is still complete. In Section 4.3.2 we discuss the relevant metatheory, with the help of
a non-overlapping version of the declarative system.

59

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism· ⊩ (λx. x) () ⇐ 1−→18 · ⊩ (λx. x) () ⇒a a ≤ 1−→26 · ⊩ (λx. x) ⇒b (b • () ⇒⇒a a ≤ 1)−→25 ·, αb , βb ⊩ α
b → βb • () ⇒⇒a a ≤ 1, x : αb ⊩ x ⇐ βb−→18 ·, αb , βb ⊩ α
b → βb • () ⇒⇒a a ≤ 1, x : αb ⊩ x ⇒b b ≤ βb−→22 ·, αb , βb ⊩ α
b → βb • () ⇒⇒a a ≤ 1, x : αb⊩αb ≤ βb−→12 ·, αb⊩αb→αb • () ⇒⇒a a ≤ 1, x : αb−→3 ·, αb⊩αb→αb • () ⇒⇒a a ≤ 1−→28 ·, αb⊩αb ≤ 1 ⊩ () ⇐ αb−→18 ·, αb⊩αb ≤ 1 ⊩ () ⇒a a ≤ αb−→24 ·, αb⊩αb≤1⊩1≤αb−→16 · ⊩ 1 ≤ 1−→4 ·Figure 4.6: A Sample Derivation for Algorithmic Typing

Declarative worklistΩ ::=· | Ω, a | Ω, x : A | Ω ⊩ ω

Γ⇝Ω
Ω⇝Ω

⇝Ω

Γ instantiates to Ω.

Ω⊢τΩ, [τ /bα ]Γ ⇝ ΩΩ, αb, Γ ⇝ Ω⇝bαFigure 4.7: Declarative Worklists and Instantiation

4.3 Metatheory
This section presents the metatheory of the algorithmic system presented in the previous section.
We show that three main results hold: soundness, completeness and decidability. These three results have been mechanically formalized and proved in the Abella theorem prover [Gacek 2008].

4.3.1 Declarative Worklist and Transfer
To aid formalizing the correspondence between the declarative and algorithmic systems, we introduce the notion of a declarative worklist Ω, defined in Figure 4.7. A declarative worklist Ω has
the same structure as an algorithmic worklist Γ, but does not contain any existential variables αb.

60

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism∥Ω∥Judgment erasure.
∥·∥=·∥Ω, a∥ = ∥Ω∥, a∥Ω, x : A∥ = ∥Ω∥, x : A∥Ω ⊩ ω∥ = ∥Ω∥Ω −→ Ω′

Declarative transfer.

Ω, a −→ ΩΩ, x : A −→ ΩΩ ⊩ A ≤ B −→ Ω

when ∥Ω∥ ⊢ A ≤ BΩ ⊩ e ⇐ A −→ Ω

when ∥Ω∥ ⊢ e ⇐ AΩ ⊩ e ⇒a ω −→ Ω ⊩ [A/a]ω

when ∥Ω∥ ⊢ e ⇒ AΩ ⊩ A • e ⇒⇒a ω −→ Ω ⊩ [C/a]ω

when ∥Ω∥ ⊢ A • e ⇒⇒ C

Figure 4.8: Declarative Transfer

Worklist instantiation. The relation Γ ⇝ Ω expresses that the algorithmic worklist Γ can beinstantiated to the declarative worklist Ω, by appropriately instantiating all existential variables αbin Γ with well-scoped monotypes τ . The rules of this instantiation relation are shown in Figure 4.7
too. Rule ⇝b
α replaces the first existential variable with a well-scoped monotype and repeats theprocess on the resulting worklist until no existential variable remains and thus the algorithmic
worklist has become a declarative one. In order to maintain well-scopedness, the substitution isapplied to all the judgments and term variable bindings in the scope of αb.
Observe that the instantiation Γ ⇝ Ω is not deterministic. From left to right, there are infinitely many possibilities to instantiate an existential variable and thus infinitely many declarative
worklists that one can get from an algorithmic one. In the other direction, any valid monotype
in Ω can be abstracted to an existential variable in Γ. Thus different Γ’s can be instantiated to thesame Ω.
Lemmas 4.3 and 4.4 generalize Rule ⇝b
α from substituting the first existential variable to substituting any existential variable.
Lemma 4.3 (Insert). If ΓL , [τ /bα ]ΓR ⇝ Ω and ΓL ⊢ τ , then ΓL , αb , ΓR ⇝ Ω.
Lemma 4.4 (Extract). If ΓL , αb , ΓR ⇝ Ω , then there exists τ s.t. ΓL ⊢ τ and ΓL , [τ /bα ]ΓR ⇝ Ω.
Declarative transfer. Figure 4.8 defines a relation Ω −→ Ω′ , which transfers all judgmentsin the declarative worklists to the declarative type system. This relation checks that every judg-

61

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

ment entry in the worklist holds using a corresponding conventional declarative judgment. The
typing contexts of declarative judgments are recovered using an auxiliary erasure function ∥Ω∥ 2 .
The erasure function simply drops all judgment entries from the worklist, keeping only variable
and type variable declarations.

4.3.2 Non-Overlapping Declarative System
DK’s declarative system, shown in Figures 2.8 and 2.9, has a few overlapping rules. In contrast,
our algorithm has removed all overlap; at most one rule applies in any given situation. This discrepancy makes it more difficult to relate the two systems.
To simplify matters, we introduce an intermediate system that is still declarative in nature, but
has no overlap. This intermediate system differs only in a few rules from DK’s declarative system:
1. Restrict the shape of B in the rule ∀L subtyping rule:B ̸= ∀b. B ′Ψ⊢τΨ ⊢ [τ /a]A ≤ BΨ ⊢ ∀a. A ≤ B∀L′

2. Drop the redundant rule Decl1I, which can be easily derived by a combination of DeclSub,
Decl1I⇒ and ≤Unit:Ψ ⊢ () ⇒ 1

Decl1I⇒Ψ⊢1≤1Ψ ⊢ () ⇐ 1≤Unit
DeclSub

3. Restrict the shapes of e and A in the subsumption rule DeclSub:e ̸= λx. e′

A ̸= ∀a. A′

Ψ⊢e⇒A

Ψ⊢e⇐B

Ψ⊢A≤B

DeclSub′

The resulting declarative system has no overlapping rules and more closely resembles the algorithmic system, which contains constraints of the same shape.
We have proven soundness and completeness of the non-overlapping declarative system withrespect to the overlapping one to establish their equivalence. Thus the restrictions do not change
the expressive power of the system. Modification (2) is relatively easy to justify, with the derivation
given above: the rule is redundant and can be replaced by a combination of three other rules.
2

In the proof script we do not use the erasure function, for the declarative system and well-formedness judgments
automatically fit the non-erased declarative worklist just as declarative contexts.

62

4 A Type-Inference Algorithm for Higher-Ranked PolymorphismΨ′ ≤ Ψ
·≤·Ψ′ ≤ Ψ

CtxSubEmpty

Ψ′ , a ≤ Ψ, aΨ′ ≤ Ψ

Ψ ⊢ A′ ≤ A

Ψ′ , x : A′ ≤ Ψ, x : A

CtxSubTyVar
CtxSubTmVar

Figure 4.9: Context Subtyping

Modifications (1) and (3) require inversion lemmas for the rules that overlap. Firstly, Rule ∀Loverlaps with Rule ∀R for the judgment Ψ ⊢ ∀a. A ≤ ∀b. B. The following inversion lemma for
Rule ∀R resolves the overlap:
Lemma 4.5 (Invertibility of ∀R). If Ψ ⊢ A ≤ ∀a. B then Ψ, a ⊢ A ≤ B.
The lemma implies that preferring Rule ∀R does not affect the derivability of the judgment.
Therefore the restriction B ̸= ∀b. B ′ in ∀L′ is valid.
Secondly, Rule DeclSub overlaps with both Decl∀I and Decl→I. We have proven two inversion lemmas for these overlaps:
Lemma 4.6 (Invertibility of Decl∀I). If Ψ ⊢ e ⇐ ∀a. A then Ψ, a ⊢ e ⇐ A.
Lemma 4.7 (Invertibility of Decl→I). If Ψ ⊢ λx. e ⇐ A → B then Ψ, x : A ⊢ e ⇐ B.
These lemmas express that applying the more specific rules, rather than the more general rule
DeclSub, does not reduce the expressive power. The is required by the completeness lemma, as
the algorithmic system explicitly prioritize the more specific rules.
The proofs of the above two lemmas rely on an important property of the declarative system,
the subsumption lemma. To be able to formulate this lemma, Figure 4.9 introduces the context
subtyping relation Ψ ≤ Ψ′ . Context Ψ subsumes context Ψ′ if they bind the same variables in thesame order, but the types A of the term variables x in the former are subtypes of types A′ assigned
to those term variables in the latter. Now we can state the subsumption lemma:
Lemma 4.8 (Subsumption). Given Ψ′ ≤ Ψ:
1. If Ψ ⊢ e ⇐ A and Ψ ⊢ A ≤ A′ then Ψ′ ⊢ e ⇐ A′ ;2. If Ψ ⊢ e ⇒ B then there exists B ′ s.t. Ψ ⊢ B ′ ≤ B and Ψ′ ⊢ e ⇒ B ′ ;3. If Ψ ⊢ A • e ⇒⇒ C and Ψ ⊢ A′ ≤ A, then there exists C ′ s.t. Ψ ⊢ C ′ ≤ C andΨ′ ⊢ A′ • e ⇒⇒ C ′ .

63

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

This lemma expresses that any derivation in a context Ψ has a corresponding derivation in any
context Ψ′ that it subsumes.
While being written in a clear format and providing enough details, some proof is not fully
accepted by the proof assistant. Specifically for the subsumption lemma, we have tried to follow
DK’s manual proof, but we discovered several problems in their reasoning that we have been
unable to address. Fortunately we have found a different way to prove the lemma. A descriptionof the problem and our fix are discussed in-depth as follows.
In the appendix of DK’s paper [Dunfield and Krishnaswami 2013], the first two applicationsof induction hypotheses on page 22 are not accepted. Either of them seems to use a slightly
different “induction hypothesis” than the true one. In fact, we cannot think of simple ways to fix
the problem, since the induction hypothesis seems not strong enough for these two cases.
To fix the proof, we propose a new induction scheme by making use of our worklist measures.
Recall that |e|e measures term size; and the judgment measure counts checking as 2, inference as
1 and application inference as 3; and |A|∀ counts the number of ∀’s in a type.
Proof. The proof is by a nested mutual induction on the lexicographical order of the measures⟨|e|e , | · |⇔ , |A|∀ + |A′ |∀ ⟩,where the second measure simple give an natural number for each type of judgment: (1) checking
judgments (Ψ ⊢ e ⇐ A) count as 2; (2) inference judgments (Ψ ⊢ e ⇒ A) count as 1; and (3)application inference judgments (Ψ ⊢ e • A ⇒⇒ C) count as 3; and the third measure does
not apply to (case 2) since no A is used. Compared with DK’s, our third measure that counts
the degree of polymorphism fixes problems that occurred in DK’s proof: in both places, our new
induction hypothesis is more generalized.
All but two cases can be finished easily following the declarative typing derivation, and theproof shares a similar structure to DK’s. One tricky case related to Rule Decl∀I indicates that
A has the shape ∀a. A0 , thus the subtyping relation derives from either ≤∀L or ≤∀R. For eachof the case, the third measure |A|∀ + |A′ |∀ decreases (the ≤∀L case requires a type substitution
lemma obtaining Ψ ⊢ e ⇐ [τ /a]A0 from the typing derivation).
Another tricky case is Decl→I. When the subtyping relation is derived from ≤→, a simple
application of induction hypothesis finishes the proof. When the subtyping relation is derived
from ≤∀R, |A′ |∀ decreases, and thus the induction hypothesis finishes this case.
In short, we found a specific problem when trying to prove the subsumption lemma following
DK’s manual proof, yet we addressed the problem by using a slightly different induction scheme.

64

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

Three-Way Soundness and Completeness Theorems We now have three systems that canbe related: DK’s overlapping declarative system, our non-overlapping declarative system, and ouralgorithmic system. We have already established the first relation, that the two declarative systems
are equivalent. In what follows, we will establish the soundness of our algorithm directly against
the original overlapping declarative system. However, we have found that showing completenessof the algorithm is easier against the non-overlapping declarative system. Of course, as a corollary,it follows that our algorithm is also complete with respect to DK’s declarative system.

4.3.3 Soundness
Our algorithm is sound with respect to DK’s declarative system. For any worklist Γ that reduces
successfully, there is a valid instantiation Ω that transfers all judgments to the declarative system.

Theorem 4.9 (Soundness). If wf Γ and Γ −→∗ ·, then there exists Ω s.t. Γ ⇝ Ω and Ω −→∗ ·.
The proof proceeds by induction on the derivation of Γ −→∗ ·. Interesting cases are those
involving existential variable instantiations, including Rules 10, 11, 21 and 29. Applications ofLemmas 4.3 and 4.4 help analyse the full instantiation of those existential variables. For example,
when αb is solved to α
b1 → αb2 in the algorithm, applying the Extract lemma gives two instantiations α
b1 = σ and αb2 = τ . It follows that αb = σ → τ , which enables the induction hypothesis
and finishes the corresponding case. Some immediate corollaries which show the soundness for
specific judgment forms are:Corollary 4.10 (Soundness, single judgment form). Given wf Γ:
1. If Γ ⊩ A ≤ B −→∗ ·then there exist A′ , B ′ , Ω s.t. Γ ⊩ A ≤ B ⇝ Ω ⊩ A′ ≤ B ′ and ∥Ω∥ ⊢ A′ ≤ B ′ ;2. If Γ ⊩ e ⇐ A −→∗ ·then there exist A′ , Ω s.t. Γ ⊩ e ⇐ A ⇝ Ω ⊩ e ⇐ A′ and ∥Ω∥ ⊢ e ⇐ A′ ;3. If Γ ⊩ e ⇒a ω −→∗ · for any ωthen there exists Ω, ω ′ , A s.t. Γ ⇝ Ω and ∥Ω∥ ⊢ e ⇒ A;
4. If Γ ⊩ A • e ⇒⇒a ω −→∗ · for any ωthen there exists Ω, ω ′ , A′ , C s.t. Γ ⊩ A • e ⇒⇒a ω ⇝ Ω ⊩ A′ • e ⇒⇒a ω ′ and ∥Ω∥ ⊢A′ • e ⇒⇒ C.
It is also possible to express a even simpler form of corollary, where the judgments consist of
declarative expressions and types.

65

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

Corollary 4.11 (Soundness, declarative form). Given wf Ψ:
1. If Ψ ⊩ A ≤ B −→∗ · then Ψ ⊢ A ≤ B;
2. If Ψ ⊩ e ⇐ A −→∗ · then Ψ ⊢ e ⇐ A;
3. If Ψ ⊩ e ⇒a ω −→∗ · then there exists A s.t. Ψ ⊢ e ⇒ A;
4. If Ψ ⊩ A • e ⇒⇒a ω −→∗ · then there exists C s.t. Ψ ⊢ A • e ⇒⇒ C.

4.3.4 CompletenessThe completeness of our algorithm means that any derivation in the declarative system has analgorithmic counterpart. We explicitly relate between an algorithmic context Γ and a declarative
context Ω to avoid potential confusion.
Theorem 4.12 (Completeness). If wf Γ and Γ ⇝ Ω and Ω −→∗ ·, then Γ −→∗ ·.
We prove completeness by induction on the derivation of Ω −→∗ · and use the non-overlapping
declarative system. Since the declarative worklist is reduced judgment by judgment (shown in
Figure 4.8), the induction always analyses the first judgment by a small step. As the algorithmic
system introduces existential variables, a declarative rule may correspond to multiple algorithmic
rules, and thus we analyse each of the possible cases.
Most cases are relatively easy to prove. The Insert and Extract lemmas are applied when thealgorithm uses existential variables, but transferred to a monotype for the declarative system, suchas Rules 6, 8, 10, 11, 12-17, 21, 25, 27 and 29.
Algorithmic Rules 10 and 11 require special treatment. When the induction reaches the ≤→case, the first judgment is of shape A1 → A2 ≤ B1 → B2 . One of the corresponding algorithmic
judgments is αb ≤ A → B. However, the case analysis does not imply that αb is fresh in A andB, therefore Rule 10 cannot be applied and the proof gets stuck. The following lemma helps us
out in those cases: the success in declarative subtyping indicates the freshness of αb in A and B in
its corresponding algorithmic judgment. In other words, the declarative system does not accept
infinite types. A symmetric lemma holds for A → B ≤ αb.
Lemma 4.13 (Prune Transfer for Instantiation). If (Γ ⊩ αb ≤ A → B) ⇝ (Ω ⊩ C ≤ A1 → B1 )and ∥Ω∥ ⊢ C ≤ A1 → B1 , then αb∈/ F V (A) ∪ F V (B).
The following corollary is derived immediately from Theorem 4.12.
Corollary 4.14 (Completeness, single judgment form). Given wf Γ containing no judgments:
1. If Ω ⊢ A′ ≤ B ′ and Γ ⊩ A ≤ B ⇝ Ω ⊩ A′ ≤ B ′then Γ ⊩ A ≤ B −→∗ ·;66

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
2. If Ω ⊢ e ⇐ A′ and Γ ⊩ e ⇐ A ⇝ Ω ⊩ e ⇐ A′
then Γ ⊩ e ⇐ A −→∗ ·;3. If Ω ⊢ e ⇒ A and Γ ⊩ e ⇒a 1 ≤ 1 ⇝ Ω ⊩ e ⇒a 1 ≤ 1then Γ ⊩ e ⇒a 1 ≤ 1 −→∗ ·;4. If Ω ⊢ A′ • e ⇒⇒ C and Γ ⊩ A • e ⇒⇒a 1 ≤ 1 ⇝ Ω ⊩ A′ • e ⇒⇒a 1 ≤ 1then Γ ⊩ A • e ⇒⇒a 1 ≤ 1 −→∗ ·.
Similar to soundness, we also provide a simpler corollary of completeness for declarative types
and expressions.
Corollary 4.15 (Completeness, declarative form). Given wf Ψ:
1. If Ψ ⊢ A ≤ B then Ψ ⊩ A ≤ B −→∗ ·;2. If Ψ ⊢ e ⇐ A then Ψ ⊩ e ⇐ A −→∗ ·;3. If Ψ ⊢ e ⇒ A then Ψ ⊩ e ⇒a 1 ≤ 1 −→∗ ·;4. If Ψ ⊢ A • e ⇒⇒ C then Ψ ⊩ A • e ⇒⇒a 1 ≤ 1 −→∗ ·.

4.3.5 Decidability
Finally, we show that our algorithm is decidable:
Theorem 4.16 (Decidability). Given wf Γ, it is decidable whether Γ −→∗ · or not.
Our decidability proof is based on a lexicographic group of induction measures⟨|Γ|e , |Γ|⇔ , |Γ|∀ , |Γ|αb , |Γ|→ + |Γ|⟩ on the worklist Γ. Formal definitions of these measures canbe found in Figure 4.10. The first two, | · |e and | · |⇔ , measure the total size of terms and thetotal difficulty of judgments, respectively. In the latter, check judgments count for 2, inference
judgments for 1 and function inference judgments for 3. Another two measures, | · |∀ and | · |→ ,count the total number of universal quantifiers and function types, respectively. Finally, | · |αbcounts the number of existential variables in the worklist, and | · | is simply the length of theworklist.
It is not difficult to see that all but two algorithmic reduction rules decrease the group of measures. (The result of Rule 29 could be directly reduced by Rule 28, which decreases the measures.)
The two exceptions are Rules 10 and 11. Both rules increase the number of existential variables
without decreasing the number of universal quantifiers. However, they are both immediately
followed by Rule 7, which breaks the subtyping problem into two smaller problems of the formαb ≤ A and A ≤ αb which we call instantiation judgments.

67

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism|Γ|e , |ω|e , |e|e Size measure.
|Γ|e =

X|Γ|∀ , |ω|∀ , |A|∀ Polymorphism measure.

|ω|e|Γ|⇔ =

ω∈Γ

X

|ω|∀

ω∈Γ

|A ≤ B|e = 0|A ≤ B|∀ = |A|∀ + |B|∀|e ⇐ A|e = |e|e|e ⇐ A|∀ = |A|∀|e ⇒ ω|e = |e|e + |ω|e|e ⇒ ω|∀ = |ω|∀|A • e ⇒⇒a ω|e = |e|e + |ω|e|A • e ⇒⇒a ω|∀ = |A|∀ + |ω|∀|x|e = |()|e = 1|1|∀ = |a|∀ = |bα |∀ = 1|λx. e|e = |e|e + 1|A → B|∀ = |A|∀ + |B|∀|e1 e2 |e = |e1 |e + |e2 |e + 1|∀a. A|∀ = |A|∀ + 1|e : A|e = |e|e + 1|Γ|→ , |ω|→ , |A|→ Function measure.

|Γ|⇔ , |ω|⇔ Judgment measure.
|Γ|⇔ =

X|Γ|→ =

|ω|e

X

|ω|∀

ω∈Γ

|A ≤ B|∀ = |A|∀ + |B|∀ω∈Γ|A ≤ B|⇔ = 0|e ⇐ A|∀ = |A|∀|e ⇐ A|⇔ = 2|e ⇒ ω|∀ = |ω|∀|e ⇒ ω|⇔ = |ω|⇔ + 1|A • e ⇒⇒a ω|∀ = |A|∀ + |ω|∀|A • e ⇒⇒a ω|⇔ = |ω|⇔ + 3|1|→ = |a|→ = |b
α |→ = 1|A → B|→ = |A|→ + |B|→ + 1|Γ|αb Existential measure.

|∀a. A|→ = |A|→|Γ|αb = #αb ∈ΓFigure 4.10: Worklist measures

We now show that entirely reducing these smaller problems leaves the worklist in a state withan overall smaller measure. Our starting point is a worklist Γ, Γi where Γi are instantiation judgments.
Γi := · | Γi , αb ≤ A | Γi , A ≤ αbwhere αb∈
/ F V (A) ∪ F V (Γi )Fully reducing these instantiation judgments at the top of the worklist has a twofold impact.
Firstly, new entries may be pushed onto the worklist which are not instantiation judgments. This68

4 A Type-Inference Algorithm for Higher-Ranked PolymorphismΓ * Γ′

Γ*Γ

* id|A|∀ = 0

ΓL , [A/bα ]ΓR * Γ′ΓL , αb , ΓR * Γ′Γ updates to Γ′ .
* solveΓL , αb , ΓR * Γ′ΓL , ΓR * Γ′*αbFigure 4.11: Worklist Update

only happens when Γi contains a universal quantifier that is reduced by Rule 8 or 9. The new
entries then are of the form Γ≤ :
Γ≤ := · | Γ≤ , a | Γ≤ , αb | Γ≤ , A ≤ B
Secondly, reducing the instantiation judgments may also affect the remainder of the worklist Γ,
by solving existing existentials and introducing new ones. This worklist update is captured in the
update judgment Γ * Γ′ defined in Figure 4.11. For instance, an existential variable instantiation, ΓL , αb , ΓR * ΓL , α
b1 , αb2 , [bα1 → αb2 /bα ]ΓR , can be derived as a combination of the threerules that define the update relation.
The good news is that worklist updates do not affect the three main worklist measures:
Lemma 4.17 (Measure Invariants of Worklist Extension). If Γ * Γ′ then |Γ|e = |Γ′ |e and |Γ|⇔ =|Γ′ |⇔ and |Γ|∀ = |Γ′ |∀ .
Moreover, we can characterize the reduction of the instantiation judgments as follows.
Lemma 4.18 (Instantiation Decidability). For any well-formed algorithmic worklist (Γ, Γi ):1) If |Γi |∀ = 0, then there exists Γ′
s.t. (Γ, Γi ) −→∗ Γ′ and |Γ′ |αb = |Γ|αb − |Γi | and Γ * Γ′ .
2) If |Γi |∀ > 0, then there exist Γ′ , Γ≤s.t. (Γ, Γi ) −→∗ (Γ′ , Γ≤ ) and |Γ≤ |∀ = |Γi |∀ − 1 and Γ * Γ′ .
Hence, reducing the instantiation judgment prefix Γi either decreases the number of universal
quantifiers or eliminates one existential variable per instantiation judgment. The proof of thislemma proceeds by induction on the measure 2 ∗ |Γi |→ + |Γi | of the instantiation judgment list
Γi .
Let us go back to the whole algorithm and summarize our findings. The decidability theorem
is shown through a lexicographic group of induction measures⟨|Γ|e , |Γ|⇔ , |Γ|∀ , |Γ|αb , |Γ|→ + |Γ|⟩69

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

which is decreased by nearly all rules. In the exceptional case that the measure does not decrease
immediately, we encounter an instantiation judgment at the top of the worklist. We can thenmake use of Lemma 4.18 to show that |Γ|αb or |Γ|∀ decreases when that instantiation judgment isconsumed or partially reduced. Moreover, Lemma 4.17 establishes that no higher-priority measure component increases. Hence, in the exceptional case we have an overall measure decreasetoo.
Combining all three main results (soundness, completeness and decidability), we conclude thatthe declarative system is decidable by means of our algorithm.
Corollary 4.19 (Decidability of Declarative Typing). Given wf Ω, it is decidable whether Ω −→∗ ·or not.

4.3.6 Abella and Proof Statistics
We have chosen the Abella (v2.0.7-dev 3 ) proof assistant [Gacek 2008] to develop our formalization. Abella is designed to help with formalizations of programming languages, due to its built-in
support for variable binding and the λ-tree syntax [Miller 2000], which is a form of HOAS. Nominal variables, or ∇-quantified variables, are used as an unlimited name supply, which supports
explicit freshness control and substitutions. Although Abella lacks packages, tactics and support
for modules, its higher-order unification and the ease of formalizing substitution-intensive relations are very helpful.
While the algorithmic rules are in a small-step style, the proof script rewrites them into a bigstep style for easier inductions. In addition, we do prove the equivalence of the two representations.
Statistics of the Proof The proof script consists of 7,977 lines of Abella code with a total of
60 definitions and 596 theorems. Figure 4.1 briefly summarizes the contents of each file. The files
are linearly dependent due to the limitations of Abella.
Translation Table for the Proof Scripts In the proof scripts, we use textual relational
definitions rather than the symbolic ones used in the paper. The mapping, shown in Table 4.2,
should be helpful for anyone who reads the script.

3

We use a development version because the developers just fixed a serious bug that accepts a simple proof of false,
which also affects our proof. Specifically, our scripts compile against commit 92829a of Abella’s GitHub repository.

70

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

Table 4.1: Statistics for the proof scripts

File(s)LOC#Thm

Description

olist.thm, nat.thm
typing.thm
decl.thmorder.thm
alg.thm

311
245
226
235
679

57
7
33
27
80

trans.thm

616

53

declTyping.thm

909

70

soundness.thm
depth.thm
dcl.thmcompleteness.thm
inst_decidable.thm
decidability.thm
smallStep.thm

1,107
206
380
1,124
837
983
119

78
14
12
61
45
57
2

Basic data structures
Declarative & algorithmic system, debug examples
Basic declarative properties
The | · |∀ measure; decl. subtyping strengthening
Basic algorithmic properties
Worklist instantiation and declarative transfer;
Lemmas 4.3, 4.4
Non-overlapping declarative system;
Lemmas 4.5, 4.6, 4.7, 4.8
Soundness theorem; aux. lemmas on transfer
The | · |→ measure; Lemma 4.13
Non-overlapping declarative worklist
Completeness theorem; aux. lemmas and relations
Other worklist measures; Lemma 4.18
Decidability theorem and corollary
The equivalence between big-step and small-step

Total

7,977

596

(60 definitions in total)71

typingtypingtypingtypingty, wft, wfta

tm, wftm

olist, wfj

judgment, wfjg

reduction

judge

tex

A

e

Ψ, Γ

ω

Γ −→ Γ′Γ −→∗ ·

Γ⇝Ω

72
inst_decidable
inst_decidable
inst_decidable

jExt

iexp

subExptmSize, tmSizeJ, tmSizel

m_judgeJ, m_judgenVarorder, orderJ, orderl

depth, depthJ, depthl

Γ * Γ′

ΓiΓ≤| · |e| · |⇔| · |αb| · |∀| · |→

order, decidability

order, inst_decidable

inst_decidable

decidability

declTyping, decidability

declTypingesub

Ψ′ ≤ Ψ

trans, dcl

dc, dclΩ −→∗ ·

transtypingsmallStep

File (.thm)

Abella textual relation

SymbolFunction measure for type, judgment chain or context

Polymorphism measure for type, judgment chain or context

Existential measure for context

Judgment measure for judgment chain or context

Size measure for term, judgment chain or context

subtyping judgments

instantiation judgments (Γ ⊢wf Γi )”Judgment extension”

Declarative context subtyping

Declarative chain representation”transfer existential variables”(judge Γ): a success reduction on Γ

Algorithmic reduction: paper version

Judgment chain and its well-formedness

olist is Abella’s built-in list type, i.e. [o]The ”term” type, (alg.) well-formedness

The ”type” type, decl./alg. well-formedness

Description

Table 4.2: Translation Table for the Proof Scripts

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

4.4 Discussion
This section discusses some insights that we gained from our work and contrasts the scoping
mechanisms we have employed with those in DK’s algorithm. We also discuss a way to improve
the precision of their scope tracking. Furthermore we discuss and sketch an extension of ouralgorithm with an elaboration to a target calculus, and discuss an extension of our algorithmwith scoped type variables [Peyton Jones and Shields 2004].

4.4.1 Contrasting Our Scoping Mechanisms with DK’s
A nice feature of our worklists is that, simply by interleaving variable declarations and judgment
chains, they make the scope of variables precise. DK’s algorithm deals with garbage collecting
variables in a different way: through type variable or existential variable markers (as discussed in
Section 4.1.2). Despite the sophistication employed in DK’s algorithm to keep scoping precise,
there is still a chance that unused existential variables leak their scope to an output context andaccumulate indefinitely. For example, the derivation of the judgment (λx. x) () ⇐ 1 is as follows...x ⇒ α
b ...

...α
b ≤ βb . . .

b x:α
Γ, α
b , β,b ⊢ x ⇐ βb ⊣ Γ1 , x : αb. . . () ⇐ αb ...

Γ ⊢ λx. x ⇒ α
b → βb ⊣ Γ1

Γ1 ⊢ αb→αb • () ⇒⇒ αb ⊣ Γ2Γ ⊢ (λx. x) () ⇒ αb ⊣ Γ2Γ2 ⊢ 1 ≤ 1 ⊣ Γ2
Γ ⊢ (λx. x) () ⇐ 1 ⊣ Γ, αb = 1, βb = αbb and Γ2 := (Γ, αbwhere Γ1 := (Γ, αb , βb = αb ) solves β,
b = 1, βb = αb ) solves both αb and β.
If the reader is not familiar with DK’s algorithm, he/she might be confused about the inconsistent types across judgment. As an example, (λx. x) () synthesizes α
b , but the second
premise of the subsumption rule uses 1 for the result. This is because a context application[Γ, αb = 1, βb = αb ]b
α = 1 happens between the premises.
The existential variables αb and βb are clearly not used after the subsumption rule, but according

to the algorithm, they are kept in the context until some parent judgment recycles a block ofvariables, or to the very end of a type inference task. In that sense, DK’s algorithm does notcontrol the scoping of variables precisely.

73

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

Two rules we may blame for not garbage collecting correctly are the inference rule for lambda
functions and an application inference rule:
b x:α
Γ, α
b , β,b ⊢ e ⇐ βb ⊣ ∆, x : αb, ΘΓ ⊢ λx. e ⇒ α
b → βb ⊣ ∆DK_→I⇒Γ, αb ⊢ [bα /a]A • e ⇒⇒ C ⊣ ∆Γ ⊢ ∀a. A • e ⇒⇒ C ⊣ ∆DK_∀App

In contrast, Rule 25 of our algorithm collects the existential variables right after the second judgment chain, and Rule 27 collects one existential variable similarly:bΓ ⊩ λx. e ⇒a ω −→25 Γ, αb , βb ⊩ [bα → β/a]ω,x:αb ⊩ e ⇐ βb
Γ ⊩ ∀a. A • e ⇒⇒a ω −→27 Γ, αb ⊩ [bα /a]A • e ⇒⇒a ω
It seems impossible to achieve a similar outcome in DK’s system by only modifying these tworules. Taking DK_→I⇒ as an example, the declaration or solution for αb and βb may be referred
to by subsequent judgments. Therefore leaving α
b and βb in the output context is the only choice,when the subsequent judgments cannot be consulted.
To fix the problem, one possible modification is on the algorithmic subsumption rule, as garbage
collection for a checking judgment is always safe:Θ ⊢ [Θ]A ≤ [Θ]B ⊣ ∆, ▶αb , ∆′Γ, ▶αb ⊢ e ⇒ A ⊣ ΘΓ⊢e⇐B⊣∆

DK_Sub

Here we employ the markers in a way they were originally not intended for. We create a dummy
fresh existential αb and add a marker to the input context of the inference judgment. After thesubtyping judgment is processed we look for the marker and drop everything afterwards. We
pick this rule because it is the only one where a checking judgment calls an inference judgment.
That is the point where our algorithm recycles variables—right after a judgment chain is satisfied.
After applying this patch, to the best of our knowledge, DK’s algorithm behaves equivalently to
our algorithm in terms of variable scoping. However, this exploits markers in a way they were notintended to be used and seems ad-hoc.

4.4.2 Elaboration
Type-inference algorithms are often extended with an associated elaboration. For example, for
languages with implicit polymorphism, it is common to have an elaboration to a variant of System
F [Reynolds 1983], which recovers type information and explicit type applications. Therefore anatural question is whether our algorithm can also accommodate such elaboration. While our74

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

algorithmic reduction does not elaborate to System F, we believe that it is not difficult to extend
the algorithm with a (type-directed) elaboration. We explain the rough idea as follows.
Since the judgment form of our algorithmic worklist contains a collection of judgments, elaboration expressions are also generated as a list of equal length to the number of judgments (notjudgment chains) in the worklist. As usual, subtyping judgments translate to coercions (denotedby f and represented by System F functions), all three other types of judgments translate to terms
in System F (denoted by t).
Let Φ be the elaboration list, containing translated type coercions and terms:
Φ ::= · | Φ, f | Φ, t
Then the form of our algorithmic judgment becomes:
Γ ,→ Φ
We take Rule 18 as an example, rewriting small-step reduction in a relational style,Γ ⊩ e ⇒a a ≤ B ,→ Φ, f, tΓ ⊩ e ⇐ B ,→ Φ, f t

Translation_18

As is shown in the conclusion of the rule, a checking judgment at the top of the worklist corresponds to a top element for elaboration. The premise shows that one judgment chain may relate
to more than one elaboration elements, instead, one single judgment relates to one elaborated
term. The outer judgment, being processed before inner ones, elaborates to the top element in
the elaboration list.
Moreover, existential variables need special treatment, since they may be solved at any point,
or be recycled if not solved within their scopes. If an existential variable is solved, we not only
propagate the solution to the other judgments, but also replace occurrences in the elaboration
list. If an existential variable is recycled, meaning that it is not constrained, we can pick any wellformed monotype as its solution. The unit type 1, as the simplest type in the system, is a good
choice.

4.4.3 Lexically-Scoped Type Variables
We have further extended the type system with the support for lexically-scoped type variables [Peyton Jones and Shields 2004]. Our Abella formalization for this extension proves all the metatheory
we discuss in Section 4.3.

75

4 A Type-Inference Algorithm for Higher-Ranked Polymorphism

From a practical point of view, this extension allows the implementation of a function to referto type variables from its type signature. For example,(λx. λy. (x : a)) : ∀a b. a → b → a
has an annotation (x : a) that refers to the type variable a in the type signature. This is not asurprising feature, since the declarative system already accepts similar programs
Ψ, a ⊢ e ⇐ AΨ ⊢ ∀a. AΨ ⊢ e ⇐ ∀a. A

Decl∀I
DeclAnnoΨ ⊢ (e : ∀a. A) ⇒ ∀a. A

The main issue is the well-formedness condition. Normally Ψ ⊢ (e : A) follows from Ψ ⊢ eand Ψ ⊢ A. However, when A = ∀a. A′ , the type variable a is not in scope at e, therefore Ψ ⊢ e
is not derivable. To address the problem, we add a new syntactic form that explicitly binds a typevariable simultaneously in a function and its annotation.
Expressionse ::=. . . | Λa. e : A

This new type-lambda syntax Λa. e : A actually annotates its body e with ∀a. A, while making
a visible inside the body of the function. The well-formedness judgments are extended accordingly:
Ψ, a ⊢ eΨ, a ⊢ AΨ ⊢ Λa. e : A

Γ, a ⊢ ewfd ΛΓ, a ⊢ AΓ ⊢ Λa. e : A

wf_Λ

Corresponding rules are introduced for both the declarative system and the algorithmic system:
Ψ, a ⊢ A Ψ, a ⊢ e ⇐ AΨ ⊢ Λa. e : A ⇒ ∀a. A

DeclΛ

Γ ⊩ Λa. e : A ⇒b ω −→30 Γ ⊩ [(∀a. A)/b]ω, a ⊩ e ⇐ A
In practice, programmers would not write the syntax Λa. e : A directly. The ScopedTypeVariables extension of Haskell is effective only when the type signature is explicitly universallyquantified (which the compiler translates into an expression similar to Λa. e : A); otherwise theprogram means the normal syntax e : ∀a. A and may not later refer to the type variable a.
We have proven all three desired properties for the extended system, namely soundness, completeness and decidability.

76

5 Higher-Ranked Polymorphism with
Object-Oriented Subtyping
5.1 Overview
In this chapter, we present a worklist algorithm that further supports subtyping, by introducing
the top and bottom types. Such type inference algorithms are known to be hard to design, due tothe complication of unifying variables under subtyping inequality rather than equality. Therefore,
algorithmic existential variables that appear in subtyping judgments might have more solutions
than before, and the eager substitution rules miss some possibilities. Our new backtracking algorithm extends the existing one by some overlapping rules that non-deterministically try different
sorts of solutions instead of a single sort, improving the rate of success guessing.
Formalization of the algorithm in the Abella theorem prover shows soundness of the algorithmwith respect to our declarative specification. Although the backtracking algorithm is still incomplete in some corner cases, the proof script indicates that the only source of incompleteness comesfrom higher-ranked subtyping relations. Following that discovery, we formally proved partial
completeness of our subtyping algorithm under the rank-1 restriction, and is at least comparable
to local type inference algorithms.

5.1.1 Type Inference in Presence of Subtyping
In all previous chapters, “subtyping” refers to a relationship that compares the degree of polymorphism between two types. In addition to that, we also include the top and bottom types. Both of
the types have practical uses, especially in object-oriented programming languages. The top type,⊤, is the super type of any type, i.e. any type is more general than ⊤ and thus can be considered
as an instance of type ⊤. In typical object-oriented programming languages, the Object class, as
the base class of any class, is the ⊤ type. In contrast, the bottom type, ⊥, is dual to ⊤. An instanceof ⊥ can be cast to a value of any type, which is also viewed as the uninhabited type therefore one
cannot find any value that has the ⊥ type. However, there are few exceptions. One of them is anull pointer value ((void *) in C++, for example). Another practical use for bottom types
is for exceptions. The type Exception → ⊥ given to the raise function may pass type checkers
naturally. The type Exception → ∀a. a is also a reasonable choice, which in fact reveals that ⊥77

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping
behaves almost identically as ∀a. a. From the theoretical point of view, both of them represent“falsity”.
A number of systems and algorithms are proposed for type inference with subtyping. Since
subtyping constraints cannot be easily reduced in presence of subtyping, it is natural to extend
the syntax of types so that unsolved constraints are carried with them, and the idea is studied byprevious work [Eifrig et al. 1995b; Trifonov and Smith 1996]. For example, the following function
select p v d = if (p v) then v else d
is inferred to have the type(α → bool) → α → β → γ | α ≤ γ, β ≤ γHowever, this representation usually contains a large set of constraints, which might confuse programmers. Besides, subtyping comparison between constraint types may introduce additionaldifficulty for programmers to understand, which weakens its practical use.
MLsub MLsub [Dolan and Mycroft 2017], as introduced in Section 2.4, is based on a type system with lattices and polar types. Inspired by [Pottier 1998], they separated input and output
types into polar types, which greatly simplifies the subtyping judgment. With the further helpof their biunification algorithm, constraints are no longer carried with types, instead they are
expressed directly on types. For example, the select function defined above has type(α → bool) → α → β → α ⊔ βin MLsub. The ⊔ symbol in the output type indicates that any of the types might be returned when
executed. On the other hand, the ⊓ symbol might occur on an input type, when that argument isused as different types, meaning that the type must be able to convert to all these types.
Nevertheless, there are still drawbacks in practice. Firstly, the type inference algorithm produces types that have comparable sizes to previous systems with constraint types. Although asimplification algorithm is provided, it is not guaranteed to produce the most simple form.
Secondly, MLsub always infers an expression and returns its principal type, but some of thetypes are not easy to understand. For example, the twice function defined as
twice f x = f (f x)
has type (α ⊔ β → α) → β → α, where normally people might expect (α → α) → α → α.
Thirdly, MLsub tries to infer on almost every possible expression, even those that might justbe a mistake made by the programmer. For instance, the function78

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

positive f x = if x > 0 then f x else f 0
always checks the positivity of x before applying to f. However, a slight mistake is made in thefollowing definition
positive' f x = if x > 0 then f x else fthen the algorithm might still accept the program by giving the type:α ⊓ (β → α) → β ⊓ int → α
Type inference algorithms, as logical tools that help people program, should accept good programs and reject bad ones. Typically, such a function is considered to be badly-written, but unfortunately, MLsub accepts it without giving any warnings.

5.1.2 Judgment List and Eager Substitution
The judgment list algorithm we discussed in the last chapter treats subtyping judgments mainly
as unification. However, the algorithm may lose some solutions when top and bottom types are
introduced. For example, the judgment αb ≤ 1 has the best solution αb := 1 in the previous
system, but now αb := ⊥ should also be allowed. As a result, several subtyping judgments cannot
be reduced easily with a single eager substitution.
Similar incompleteness also affects the instantiation and existential variable solving rules
Γ[bα] ⊩ αb ≤ A → B −→10 [bα1 → αb2 /bα ](Γ[bα1 , αb2 ] ⊩ αb1 → αb2 ≤ A → B)
b ⊩α
b
Γ[b
α ][β]b ≤ βb −→12 [bα /β](Γ[bα ][])The instantiation judgment αb ≤ A → B immediately split αb into α
b1 → αb2 , which is no longer
the case — α
b can also be ⊥.

b is even more problemThe rule that solves one existential variable against another, αb ≤ β,

atic, because the shapes of the instantiations of both existential variables are unknown, there areinfinitely many possibilities if no additional constraints present. For example, if α
b is finally instantiated to Int → Int, then βb may be solved to the same type as αb , or other types that satisfy thesubtyping relationship, including Int → ⊤, ⊥ → Int or ⊥ → ⊤. What’s worse, given only thisb we have no assumption on both existential variables.
single subtyping judgment αb ≤ β,
Theoretically speaking, if we extend the type system with ⊤ and ⊥ types, the definition ofmonotypes becomesτ ::= 1 | ⊥ | ⊤ | τ → τ | a79

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping, which causes the subtyping problem to be undecidable Su et al. [2002]. Therefore, it is impossible
to derive a complete algorithm for the declarative system, and we try to keep the algorithm complete for common usages of polymorphism, but pose restrictions in some higher-ranked cases.

5.1.3 Our Solution: Backtracking Algorithm
After examining the examples where the worklist algorithm behaves incompletely, we propose
some improvements to the worklist algorithm to accept some simple cases. We have observedthat subtyping judgments like αb ≤ A and A ≤ αb have trivial solutions αb := ⊥ and αb := ⊤
respectively, thus we can try these simple solutions before the more complicated analysis.
For example, for the judgment list Γ ⊩ αb ≤ A → B, we first assign αb := ⊥ and continue
to check other judgments. If the judgment reduction succeeds, then we know that αb := ⊥ is apossible solution. If the reduction failed, we continue to try the other possibility according to theprevious instantiation rule by splitting αb into two existential variables α
b1 and α
b2 . The proceduremust keep track of all backtracking points until type-checking the whole program. Note that for
the reduced judgment α
b1 → αb2 ≤ A → B, αb1 and α
b2 might be solved to ⊤ or ⊥.
For the type system, there are also interesting changes to both the declarative system and algorithmic system. Two algorithmic typing rules also adopt the backtracking approach:• The checking judgment e ⇐ αb now has a trivial solution αb := ⊤, because e ⇐ ⊤ shouldbe accepted for any (well-formed) expression.
• The introduction of top and bottom types comes with another new declarative rule ⊥•e ⇒⇒⊥. Therefore the application inference judgment αb • e ⇒⇒a ω can be satisfied by αb := ⊥,
with output ⊥ applied to the rest of the judgment chain ω.
By applying the above modifications, the algorithm remains sound w.r.t our new declarative
system, and at the same time, we address most issues regarding the top and bottom types, obtaining a more complete algorithm. Furthermore, we formally verified that the subtyping algorithmb a naive
is complete under the rank-1 restriction. However, for rank-2 judgments like αb ≤ β,
complete algorithm would traverse an infinitely large tree of possibilities and diverge for someset of constraints.
Following the formal statements, we conclude that the backtracking algorithm is complete under a rank-1 restriction, but not always on the general higher-ranked settings. In those settings,
our algorithm only consider the equality case and ignore any other possibilities. In another perspective, our algorithm does not try to solve completely when parametric polymorphism andsubtyping polymorphism occur at the same time. This is not theoretically satisfactory, but we argue that this handles most common programs, and the programmer may use annotation to guidethe inference algorithm with the real type he intends to instantiate.

80

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

Type variables
Types

a, b
A, B, C ::= 1 | ⊤ | ⊥ | a | ∀a. A | A → B

Monotypesτ::= 1 | ⊤ | ⊥ | a | τ1 → τ2

Expressionse::=x | () | λx. e | e1 e2 | (e : A)

ContextΨ::=· | Ψ, a | Ψ, x : A

Figure 5.1: Declarative Syntax

Ψ⊢A≤B
a∈Ψ
Ψ⊢a≤a

≤Var

Ψ⊢1≤1

Ψ⊢τ

≤Unit

Ψ ⊢ [τ /a]A ≤ BΨ ⊢ ∀a. A ≤ B
A≤⊤Ψ ⊢ B 1 ≤ A1

Ψ ⊢ A1 → A2 ≤ B1 → B2
Ψ, b ⊢ A ≤ B

≤∀L

≤Top

Ψ ⊢ A2 ≤ B 2

Ψ ⊢ A ≤ ∀b. B
⊥≤A

≤→

≤∀R

≤Bot

Figure 5.2: Declarative Subtyping

5.2 Declarative System
Syntax The syntax of the declarative system, shown in Figure 5.1, is similar to the previous
systems by having a primitive type 1, type variables a, polymorphic types ∀a. A and function
types A → B. Additionally, top and bottom types are introduced to the type system.
The well-formedness formalization of the system is standard and almost identical to the previous systems, therefore we omit the formal definitions.
Declarative Subtyping Shown in Figure 5.2, the declarative subtyping extends the polymorphic subtyping relation originally proposed by Odersky and Läufer [1996] by adding Rules ≤Topand ≤Bot, defining the properties of the ⊤ and ⊥ types, respectively. Although the new rules
seem quite simple, they may increase the uncertainty of polymorphic instantiations. For example,
the subtyping judgment∀a. a → a ≤ ⊥ → ⊤accepts any well-formed instantiation on the polymorphic type ∀a. a → a.

81

5 Higher-Ranked Polymorphism with Object-Oriented SubtypingΨ⊢e⇐Ae checks against input type A.

Ψ⊢e⇒Ae synthesizes output type A.

Ψ ⊢ A • e ⇒⇒ C

Applying a function of type A to e synthesizes type C.

(x : A) ∈ Ψ
Ψ⊢x⇒A
Ψ⊢A

Ψ⊢e⇐A

Ψ ⊢ (e : A) ⇒ A
Ψ ⊢ () ⇐ 1

Ψ ⊢ e ⇐ ∀a. A

DeclAnnoΨ⊢e⇐⊤Decl∀IΨ, x : A ⊢ e ⇐ BΨ ⊢ λx. e ⇐ A → BΨ ⊢ e1 e2 ⇒ C

Ψ ⊢ () ⇒ 1

DeclSub

Decl1I⇒

Ψ⊢e

Decl⊤

Ψ⊢τ

Ψ ⊢ ⊥ • e ⇒⇒ ⊥

Ψ ⊢ [τ /a]A • e ⇒⇒ C

Ψ ⊢ ∀a. A • e ⇒⇒ C
Ψ⊢σ→τDecl→IΨ ⊢ e1 ⇒ A Ψ ⊢ A • e2 ⇒⇒ C

Ψ⊢A≤B

Ψ⊢e⇐B

Ψ⊢e

Decl1IΨ, a ⊢ e ⇐ A

Ψ⊢e⇒A

DeclVarDecl→E

Decl∀AppΨ, x : σ ⊢ e ⇐ τΨ ⊢ λx. e ⇒ σ → τ

Decl⊥App

Decl→I⇒Ψ⊢e⇐AΨ ⊢ A → C • e ⇒⇒ C

Decl→App

Figure 5.3: Declarative Typing

Declarative Typing The declarative typing rules, shown in Figure 5.3, extend DK’s higherranked type system in order to support the top and bottom types. Rule Decl⊤ allows any wellformed expression to check against ⊤. Rule Decl⊥App returns the ⊥ type when a function of⊥ type is applied to any argument. All other rules remain exactly the same as the system ofChapters 3 and 4.
It’s worth mentioning that the design of the two new rules is driven by the subsumption property described in Section 5.4.1. They maintain the property in presence of a more powerful declarative subtyping, and we will discuss further later in that part.

5.3 Backtracking Algorithm
5.3.1 Syntax
The algorithmic syntax is shown in Figure 5.4. Compared with the declarative system, existential
variables αb , βb are used as placeholders for unsolved mono-types. The judgment chain ω andworklist context Γ are defined in the same way as that of Chapter 4.
The well-formedness definition for worklist context remains the same as that of Chapter 4. The
hole notation is also inherited.

82

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

Existential variables αb , βb
Types

A, B, C ::= 1 | ⊤ | ⊥ | a | ∀a. A | A → B | αbAlgorithmic judgment chain ω::=A ≤ B | e ⇐ A | e ⇒a ω | A • e ⇒⇒a ω

Algorithmic worklist Γ::=· | Γ, a | Γ, αb|Γ⊩ωFigure 5.4: Algorithmic Syntax

The Solve Notation We define a set of auxiliary substitution functions in the form {bα := τA }to improve readability of our algorithmic definitions. Basically it refers to a global substitution
when solving an existential variable.
A detailed definition of the notation is shown as follows:{b
α := τ } (ΓL , αb , ΓR ) = ΓL , [τ /bα ]ΓRτ = 1, ⊤, ⊥ or ab (ΓL , αb α ]ΓR{b
α := β}b , ΓR ) = ΓL , [β/bβb ∈ ΓL{b
α := αb1 → αb2 } (ΓL , αb , ΓR ) = ΓL , α
b1 , αb2 , [bα1 → αb2 /bα ]ΓR5.3.2 Algorithmic Subtyping
Figure 5.5 describes the algorithmic rules for subtyping. The relation is stated in a small-step“reduction” form, i.e. in each step, the worklist is analysed from the right-hand-side and reduced
according to the top judgment. The overall procedure succeeds iff the worklist eventually reduces
to · (the empty worklist).
We categorize them into 7 groups according to their behavior:
1. Rules 1-3 are basic garbage collection rules. Given that the worklist Γ is well-formed, noreference of a variable should occur before its declaration. Therefore removing the declaration in the top position does not break well-formedness.
An existential variable that is unsolved in the top position indicates that it is not constrained, thus picking any well-formed mono-type as its solution is acceptable. In ouralgorithmic formalization, we simply drop the existential variable.
2. Rules 4-10 directly correspond to the declarative subtyping rules. With no top-level existential variables, there is nothing to guess immediately, and thus the algorithm behaves
just like the declarative system.
3. Rule 11 is a base case in the algorithmic system. The declarative reflexivity property suggests that any solution is acceptable, thus the judgment holds without any constraint.

83

5 Higher-Ranked Polymorphism with Object-Oriented SubtypingΓ −→ Γ′ Γ reduces to Γ′ .
Γ, a −→1 ΓΓ, αb −→2 ΓΓ, x : A −→3 ΓΓ ⊩ 1 ≤ 1 −→4 ΓΓ ⊩ a ≤ a −→5 ΓΓ ⊩ A1 → A2 ≤ B1 → B2 −→6 Γ ⊩ A2 ≤ B2 ⊩ B1 ≤ A1
Γ ⊩ ∀a.A ≤ B −→7 Γ, αb ⊩ [bα /a]A ≤ B
Γ ⊩ A ≤ ∀b.B −→8 Γ, b ⊩ A ≤ B
Γ ⊩ A ≤ ⊤ −→9 ΓΓ ⊩ ⊥ ≤ B −→10 ΓΓ[bα] ⊩ αb≤αb −→11 ΓΓ[bα] ⊩ A ≤ αb −→12 {bα := ⊤} Γ[bα]Γ[bα] ⊩ αb ≤ A −→13 {bα := ⊥} Γ[bα]Γ[bα] ⊩ αb ≤ A → B −→14 {bα := αb1 → αb2 } (Γ[bα] ⊩ αb ≤ A → B)
when αb∈/ F V (A → B)
Γ[bα] ⊩ A → B ≤ αb −→15 {bα := αb1 → αb2 } (Γ[bα] ⊩ A → B ≤ αb)when αb∈/ F V (A → B)b ⊩ a ≤ βb −→16 {βb := a} Γ[a][β]bΓ[a][β]b ⊩ βb ≤ a −→17 {βb := a} Γ[a][β]bΓ[a][β]b ⊩ 1 ≤ βb −→18 {βb := 1} Γ[β]b
Γ[β]b ⊩ βb ≤ 1 −→19 {βb := 1} Γ[β]
b
Γ[β]
b ⊩α
b
Γ[b
α ][β]b ≤ βb −→20 {βb := αb } Γ[bα ][β]b ⊩ βb ≤ αb
Γ[bα ][β]b −→21 {βb := αb } Γ[bα ][β]
Figure 5.5: Algorithmic Garbage Collection and Subtyping

4. Rules 12-13 are important rules that require backtracking techniques for implementation.
These rules overlap with all the remaining rules when solving an existential variable. In

84

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping
other words, they simply try if ⊤ or ⊥ satisfies the constraints in parallel with other possibilities.
5. Rules 14-15 compares an existential variable α
b with a function type, resulting in solving
the α
b by αb1 → αb2 . The freshness condition rules out the possibility when there is a cyclic
dependency. For example, the judgment
α
b≤1→α
b
is satisfied with either of these solutions to αb:⊥, 1 → ⊥, ⊤ → ⊥, 1 → 1 → ⊥, . . .
However, we argue that comparing α
b with a function type that contains αb itself is hardly
useful in practice, and most of the solutions are meaningless. It would be nice if we may
develop a complete algorithm or weaken the specification to reject such cases, but in thiswork, we choose to simply propose an incomplete algorithm, where in this example, onlythe ⊥ solution is considered with Rule 13. The condition of Rule 14 rejects the judgment
for further analysis and thus does not produce more solutions. This is one source of incompleteness of our algorithm with respect to the declarative specification.
6. Rules 16-19 solve existential variables against a type variable or the unit type. For instance,
the judgment
αb≤1
only has two solutions: α
b = 1 or αb = ⊥. In similar cases, one of the solutions is produced
by Rule 12 or 13, and the other one is given by one of the rules in this group. Additional
well-formedness checks are performed when type variables are encountered; a solution toan existential variable must be well-formed in the context before the existential variable isdefined.
7. Rules 20-21 deal with subtyping judgments that compare two different existential variables.
The only difference between them is the variable order. Similar to the type variable case in
the previous group, existential variables must solve to another one defined earlier. With
Rules 12, 13, 20 and 21, a judgment likeαb ≤ βb85

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

could possibly give any of the following solutions:αb = βb (or βb = αb ) or αb = ⊥ or βb = ⊤Those are good attempts, but unfortunately, they do not cover the complete set of possibilities. The following example worklistαb , βb ⊩ βb ≤ 1 → 1 ⊩ αb ≤ βbhas a solution αb = 1 → ⊤, βb = 1 → 1 missed by our algorithm. Similar situations happen
when the judgments are specifically ordered; if βb ≤ 1 → 1 is the top-most judgment, thealgorithm will not miss this solution.
Although such treatment for existential variable solving is incomplete in theory, the algorithm completely handles practical programs where unification is simply equality. For
other programs that exploit complex guessing involving subtyping, the programmer may
put type annotations when the type inference algorithm does not find the optimal solution.

5.3.3 Algorithmic Typing
The algorithmic typing rules are split into three groups, according to the category of the top-mostjudgment.
1. Checking mode. Rules 22-27 reduce top-level checking judgments. Rules 22, 23, 24 and26 directly reflect how the declarative system behaves. Rule 25 splits αb into α
b1 → αb2 tomimic the same logic as Rule 24, since a lambda expression must be of a function type.
Rule 27 is another backtracking rule, which overlaps with all other checking rules. Solving
αb to ⊤ in such case reflects the declarative rule Decl⊤ when the unknown type is ⊤. Furthermore, we eliminate the algorithmic counterpart of declarative rule Decl1I, because acombination of Rules 22 and 30 already accepts the judgment () ⇐ 1.
2. Inference mode. Rules 28-32 reduce inference judgments. Like the work presented in
Chapter 4, the encoding of the return type is by an explicit substitution on the binder ofa judgment chain. Rules 28, 29, 30 and 32 correspond to the declarative system straightb
forwardly. Rule 31 guesses an unannotated lambda with a mono function type αb → β.
Writing in a slightly different way may help improve readability:bΓ ⊩ λx. e ⇒a ω −→31′ Γ, αb , βb ⊩ [bα → β/a]ω
⊩ λx. e ⇐ α
b → βb86

5 Higher-Ranked Polymorphism with Object-Oriented SubtypingΓ −→ Γ′ Γ reduces to Γ′ (continued).
Γ ⊩ e ⇐ B −→22 Γ ⊩ e ⇒a a ≤ Bwhen e ̸= λx. e′ and B ̸= ∀a. B ′Γ ⊩ e ⇐ ∀a. A −→23 Γ, a ⊩ e ⇐ AΓ ⊩ λx. e ⇐ A → B −→24 Γ, x : A ⊩ e ⇐ B
Γ[bα ] ⊩ λx. e ⇐ αb −→25 {bα := αb1 → αb2 } Γ, x : α
b1 ⊩ e ⇐ αb2Γ ⊩ e ⇐ ⊤ −→26 ΓΓ[bα] ⊩ e ⇐ αb −→27 {bα := ⊤} Γ[bα]Γ ⊩ x ⇒a ω −→28 Γ ⊩ [A/a]ω

when (x : A) ∈ ΓΓ ⊩ (e : A) ⇒a ω −→29 Γ ⊩ [A/a]ω ⊩ e ⇐ A
Γ ⊩ () ⇒a ω −→30 Γ ⊩ [1/a]ω
bΓ ⊩ λx. e ⇒a ω −→31 Γ, αb , βb ⊩ [bα → β/a]ω,x:αb ⊩ e ⇐ βb
Γ ⊩ e1 e2 ⇒a ω −→32 Γ ⊩ e1 ⇒b (b • e2 ⇒⇒a ω)Γ ⊩ ∀a. A • e ⇒⇒a ω −→33 Γ, αb ⊩ [bα /a]A • e ⇒⇒a ωΓ ⊩ A → C • e ⇒⇒a ω −→34 Γ ⊩ [C/a]ω ⊩ e ⇐ AΓ ⊩ ⊥ • e ⇒⇒a ω −→35 Γ ⊩ [⊥/a]ωΓ[bα] ⊩ αb • e ⇒⇒a ω −→36 {bα := αb1 → αb2 } Γ ⊩ α
b1 → αb2 • e ⇒⇒a ωΓ[bα] ⊩ αb • e ⇒⇒a ω −→37 {bα := ⊥} Γ[bα ] ⊩ [⊥/a]ω
Figure 5.6: Algorithmic Typing

Rule 32 illustrates how the judgment chain works, with a continuation-passing-style encoding of the type inference task.
3. Application inference mode. Rules 33-37 reduce application inference judgments. Each ofthese judgments accepts an input function type and an argument expression and produces
the expected return type. Rules 33, 34 and 35 are direct translations from the declarative
rules. Rule 33, specifically, enables implicit parametric polymorphism via existential variable solving. Rules 36 and 37 deal with cases where a single existential variable αb behaves
as a function type. Rule 36 splits αb into a function unknown type α
b1 → αb2 . Rule 37 tries
the solution αb = ⊥ and returns the ⊥ type.

5.4 Metatheory
In this section we present several properties that are formally verified. For the declarative system,
the typing subsumption and subtyping transitivity lemmas are discussed in detail. The algorith-87

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

mic system is proven to be sound with respect to the declarative system via a transfer relation. A
partial completeness theorem is shown under the rank-1 restriction. We then briefly describe thechallenges we face when proving termination. Lastly, proof statistics of Abella are discussed.

5.4.1 Declarative Properties
The Typing Subsumption Lemma.

An important desired property for a type system is checking

subsumption, which says that any expression e can check against B if e checks against A andA ≤ B. Since our bidirectional type system defines the checking mode, inference mode andapplication inference mode mutually, we formalize the generalized typing subsumption.
First of all, we give the definition of worklist subtyping, which is used to further generalize thetyping subsumption lemma. This is necessary because rules like Decl→I will push the argument
type A into the context, thus when checking against a super type of A → B, say C → D, willcause the bind of x in the context to a subtype of A (since C ≤ A).
Definition 5 (Worklist Subtyping). Worklist subtyping compares the type of variables bound in
the worklist. Ψ <: Ψ′ iff each binding in Ψ is converted to one with a super type.

· <: ·
Ψ′ ⊢ A ≤ B

Ψ <: Ψ′<: nilΨ <: Ψ′Ψ, x : A <: Ψ′ , x : B

Ψ, a <: Ψ′ , a
<: of

<: ty

Ψ <: Ψ′Ψ ⊩ ω <: Ψ′ ⊩ ω<: ωA basic property of worklist subtyping is that they acts similarly when dealing with subtyping
between well-formed types.
Lemma 5.1 (Worklist Subtyping Equivalence).
Given Ψ <: Ψ′ , Ψ ⊢ A ≤ B ⇐⇒ Ψ′ ⊢ A ≤ B.
Finally, we give the statement of typing subsumption lemma, which is generalized by the worklist subtyping relation.
Lemma 5.2 (Typing Subsumption). Given Ψ <: Ψ′ ,1) If Ψ′ ⊢ e ⇐ A and Ψ′ ⊢ A ≤ B, then Ψ ⊢ e ⇐ B;
2) If Ψ′ ⊢ e ⇒ A, then ∃B s.t. Ψ′ ⊢ B ≤ A and Ψ ⊢ e ⇒ B.
3) If Ψ′ ⊢ C • e ⇒⇒ A and Ψ′ ⊢ D ≤ C, then ∃B s.t. Ψ′ ⊢ B ≤ A and Ψ ⊢ D • e ⇒⇒ B.
Proof. By induction on the following size measure (lexicographical order on a 3-tuple):88

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping• Checking (e ⇐ A): ⟨|e|, 1, |A|∀ + |B|∀ ⟩• Inference (e ⇒ A): ⟨|e|, 0, 0⟩• Application inference (A • e ⇒⇒ C): ⟨|e|, 2, |C|∀ + |D|∀ ⟩Most of the cases are straightforward. When rule ≤∀L is applied for the subtyping predicate likeΨ′ ⊢ A ≤ B, a mono-type substitution is performed on ∀a. A, resulting in [τ /a]A. Since τ is amono-type, the result type reduces the number of ∀’s, and thus reduces the size measure.
Interestingly, the two new declarative rules Decl⊤ and Decl⊥App are discovered when wewere trying to prove the property instead of before exploring the meta-theory. Given the typing
and subtyping judgments Ψ ⊢ e ⇐ A and Ψ ⊢ A ≤ ⊤, we should derive Ψ ⊢ e ⇐ ⊤ from thelemma, therefore Rule Decl⊤ is required, saying that any expression can be checked against the
top type. Note that here we do not include the condition e ⇐ A, since we may elaborate the term
to the top term which no longer refers to the original term.
Similarly, the most general type ⊥, being able to convert to any type due to Rule ≤Bot, can beconverted to any function type, or simply the most general one ⊤ → ⊥, which accepts any input
and returns the ⊥ type, resulting in the derivation Ψ ⊢ ⊥ • e ⇒⇒ ⊥. From the lemma we canalso derive that by Ψ ⊢ C • e ⇒⇒ A, Ψ ⊢ ⊥ ≤ C and Ψ ⊢ ⊥ ≤ A.
With the addition of Rules Decl⊤ and Decl⊥App, we can prove the typing subsumption
lemma. To the best of the author’s knowledge, they are the minimal set of rules that make thelemma hold.
Transitivity of Subtyping The transitivity lemma for declarative subtyping is a commonly
expected property. The proof depends on the following subtyping derivation size relation and an
auxiliary lemma.
Definition 6 (Subtyping Derivation Size).
|1 ≤ 1| = 0|a ≤ a| = 0|A ≤ ⊤| = 0|⊥ ≤ B| = 0|A1 → A2 ≤ B1 → B2 | = |B1 ≤ A1 | + |A2 ≤ B2 | + 1|∀a. A ≤ B| = |[τ /a]A ≤ B| + 1|A ≤ ∀a. B| = |A ≤ B| + 1

89

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping
Lemma 5.3 (Monotype Subtyping Substitution). If Ψ ⊢ τ and Ψ, a, ΨR ⊢ A ≤ B, thenΨ, [τ /a]ΨR ⊢ [τ /a]A ≤ [τ /a]B.
Proof. A routine induction on the subtyping relation Ψ, a, ΨR ⊢ A ≤ B finishes the proof.
Corollary 5.4 (Monotype Subtyping Substitution for Type Variables). If Ψ ⊢ τ and Ψ, a ⊢ A ≤B, then Ψ ⊢ [τ /a]A ≤ [τ /a]B.
The above lemma and corollary reveal the fact that a type variable occurred in the subtyping
relation represents an arbitrary well-formed monotype. And it also explains the difference intreatment of polymorphic types between Rules ≤∀L and ≤∀R: Rule ≤∀R is in fact equivalent to:∀τ s.t. Ψ ⊢ τ =⇒ Ψ ⊢ A ≤ [τ /b]BΨ ⊢ A ≤ ∀b. B≤∀R′

Finally, with the size measure defined and required lemma proven, we can obtain the transitivity lemma for declarative subtyping.
Lemma 5.5 (Subtyping Transitivity). If Ψ ⊢ A ≤ B and Ψ ⊢ B ≤ C then Ψ ⊢ A ≤ C.
Proof. Induction on the lexicographical order defined by ⟨|B|∀ , |A ≤ B| + |B ≤ C|⟩. Most
cases preserve the first element of the size measures |B|∀ , and are relatively easy to prove. The
difficult case is when B is a polymorphic type, when the conditions are Ψ ⊢ A ≤ ∀a. B andΨ ⊢ ∀a. B ≤ C. They are derived through rules ≤∀L and ≤∀R, respectively. Therefore, we haveΨ, a ⊢ A ≤ B and Ψ ⊢ [τ /a]B ≤ C. To exploit the induction hypothesis, the contexts should
be unified. By Corollary 5.4, Ψ ⊢ A ≤ [τ /a]B. Notice that the freshness condition is implicit
for rule ≤∀L. Clearly, |[τ /a]B|∀ < |∀a. B|∀ , i.e. the first size measure decreases. By induction
hypothesis we get Ψ ⊢ A ≤ C and finish this case.

5.4.2 Transfer
Follow the approach of Section 4.3, the transfer relation and the declarative instantiation relation
are defined in Figure 5.7.
Similarly, Lemmas 5.6 and 5.7 generalizing Rule ⇝b
α hold as well.
Lemma 5.6 (Insert). If ΓL , [τ /bα ]ΓR ⇝ Ω and ΓL ⊢ τ , then ΓL , αb , ΓR ⇝ Ω.
Lemma 5.7 (Extract). If ΓL , αb , ΓR ⇝ Ω , then there exists τ s.t. ΓL ⊢ τ and ΓL , [τ /bα ]ΓR ⇝ Ω.
Figure 5.8 defines a relation Ω −→ Ω′ , checking that every judgment entry in the worklist
holds using a corresponding declarative judgment.

90

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

Declarative worklistΩ ::=· | Ω, a | Ω, x : A | Ω ⊩ ω

Γ⇝Ω
Ω⇝Ω

⇝Ω

Γ instantiates to Ω.

Ω⊢τΩ, [τ /bα ]Γ ⇝ ΩΩ, αb, Γ ⇝ Ω⇝bαFigure 5.7: Declarative Worklists and Instantiation∥Ω∥

Judgment erasure.
∥·∥=·∥Ω, a∥ = ∥Ω∥, a∥Ω, x : A∥ = ∥Ω∥, x : A∥Ω ⊩ ω∥ = ∥Ω∥Ω −→ Ω′

Declarative transfer.

Ω, a −→ ΩΩ, x : A −→ ΩΩ ⊩ A ≤ B −→ Ω

when ∥Ω∥ ⊢ A ≤ BΩ ⊩ e ⇐ A −→ Ω

when ∥Ω∥ ⊢ e ⇐ AΩ ⊩ e ⇒a ω −→ Ω ⊩ [A/a]ω

when ∥Ω∥ ⊢ e ⇒ AΩ ⊩ A • e ⇒⇒a ω −→ Ω ⊩ [C/a]ω

when ∥Ω∥ ⊢ A • e ⇒⇒ C

Figure 5.8: Declarative Transfer

5.4.3 Soundness
Our algorithm is sound with respect to the declarative system. For any worklist Γ that reduces
successfully, there is a valid instantiation Ω that transfers all judgments to the declarative system.

Theorem 5.8 (Soundness). If wf Γ and Γ −→∗ ·, then there exists Ω s.t. Γ ⇝ Ω and Ω −→∗ ·.
Soundness is a basic desired property of a type inference algorithm, which ensures that thealgorithm is always producing valid declarative derivations when the judgments are accepted.

91

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

5.4.4 Partial Completeness of Subtyping: Rank-1 Restriction
The algorithm is incomplete due to the subtyping rules 14, 15, 20 and 21. However, subtyping iscomplete with respect to the declarative system in a rank-1 setting.
Declarative Rank-1 Restriction Rank-1 types are also named type schemes in the HindleyMilner type system.
Declarative Type Schemesσ ::=∀a. σ | τ

In other words, the universal quantifiers only appear in the top level of all polymorphic types.
For declarative subtyping, a judgment must be of form σ1 ≤ σ2 .

5.4.5 Algorithmic Rank-1 Restriction (Partial Completeness)
The algorithmic mono-types and type schemes are defined as following:
Algorithmic Mono-types
Algorithmic Type Schemes

τA::= 1 | ⊤ | ⊥ | a | A → B | αbσA ::=∀a. σA | τA

Starting from the declarative judgment σ1 ≤ σ2 , the algorithmic derivation might involve
different other kinds of judgments. The following derivation, as an example, shows how a rank-1
judgment derives.
· ⊩ ∀a. a → a ≤ ∀b. (b → b) → (b → b)−→8 b ⊩ ∀a. a → a ≤ (b → b) → (b → b)−→7 b, αb⊩αb→αb ≤ (b → b) → (b → b)−→6 b, αb⊩αb≤b→b⊩b→b≤αb−→ · · ·In this derivation, we begin from a judgment of the form σ ≤ σ. After Rule 8 is applied, thejudgment becomes σ ≤ τ , since the right-hand-side polymorphic type is reduced to a declarative mono-type. Then, Rule 7 introduces existential variables to the left-hand-side, resulting ina judgment like τA ≤ τ , or σA ≤ τ in a more general case. Finally, Rule 6 breaks a judgment
between functions into two sub-judgments, which swaps the positions of the argument types andcreates a judgment like τ ≤ τA . Notice that σA is not possible to occur to the right because thefunction type may not contain any polymorphic types as its argument type.

92

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

After a detailed analysis on the judgments derivations, we found that the only possible judgments that a rank-1 declarative subtyping judgment might step to belong to the following two
categories:σA ≤ σor τ ≤ σA

All the possible judgment types shown above fall into these categories. For example, τA ≤ τ is a
special form of σA ≤ σ, and τ ≤ τA belongs to τ ≤ σA .
An interesting observation is that αb ≤ βb does not belong to either category, neither does αb≤
A → B when αb ∈ FV(A → B). Therefore, in the rank-1 setting, both cases of incompletenessnever occur, and our algorithm is complete.
Theorem 5.9 (Completeness of Rank-1 Subtyping). Given Ψ ⊢ σ1 ≤ σ2 ,• If Γ ⊩ σA ≤ σ ⇝ Ψ ⊩ σ1 ≤ σ2then Γ ⊩ σA ≤ σ −→∗ ·;• If Γ ⊩ τ ≤ σA ⇝ Ψ ⊩ σ1 ≤ σ2then Γ ⊩ τ ≤ σA −→∗ ·.

5.4.6 Termination
The measure used in Chapter 4 no longer works because subtyping judgments likeαb≤⊥→⊤cause αb to split into α
b1 → αb2 , without solving any part of it, resulting in an increased number ofexistential variables and possibly increased complexity of the worklist through the size-increasing
substitution {bα := αb1 → αb2 }.
We have performed a large set of tests on generated subtyping judgments that are consist ofalgorithmic monotypes, and all judgments terminated within a reasonable number of derivation
depth. Unfortunately, we have not yet find any formal proof for the termination statement.
In some theoretical point of view, an algorithm should terminate on any valid input. However, there are programs that do not terminate, which we also consider them as an “algorithm”.
Therefore, we would still call our reduction procedure an algorithm, although the terminationargument has not been formally proven.

93

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

Table 5.1: Statistics for the proof scripts

File(s)LOC#Thm

Description

olist.thm, nat.thm
typing.thm
decl.thmorder.thm
alg.thm

311
273
241
274
699

57
7
33
27
82

trans.thm

635

53

declTyping.thm

1,087

76

soundness.thm
dcl.thmscheme.thm
completeness.thm

1,206
417
1,113
1,045

81
12
98
63

Basic data structures
Declarative & algorithmic system, debug examples
Basic declarative properties
The | · |∀ measure; decl. subtyping strengthening
Basic algorithmic properties
Worklist instantiation and declarative transfer;
Lemmas 4.3, 4.4
Non-overlapping declarative system;
Lemmas 4.5, 4.6, 4.7, 4.8
Soundness theorem; aux. lemmas on transfer
Non-overlapping declarative worklist
Type scheme (rank-1 restriction)
Completeness theorem; aux. lemmas and relations

Total

7,301

592

(48 definitions in total)

5.4.7 Formalization in the Abella Proof Assistant
We have chosen the Abella (v2.0.7-dev 1 ) proof assistant [Gacek 2008] to develop our formalization. Equipped with HOAS, Abella eases the formalization and proof tasks a lot compared withvarious libraries in Coq. Additionally, our algorithm heavily uses eager substitutions, and Abella
greatly simplifies relevant proofs thanks to its built-in substitution representation and higherorder unification algorithms.
The reader may find the source code of the proof at https://github.com/JimmyZJX/Dissertation/tree/main/src/Subtyping.
Statistics of the Proof The proof script consists of 7,301 lines of Abella code with a total of
48 definitions and 592 theorems. Figure 5.1 briefly summarizes the contents of each file. The files
are linearly dependent due to the limitations of Abella.

1

We use a forked version https://github.com/JimmyZJX/abella by only enhancing the Abella prover with ahandy “applys” tactic.

94

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

5.5 Discussion
5.5.1 A Complete Algorithm Under Monotype Guessing Restrictions
The incompleteness of the algorithm is mainly due to incomplete guesses for existential variableinstantiations when dealing with subtyping. For example, when reducing the algorithmic subtyping judgment
α
b≤α
b→1
we only consider the possibility αb := ⊥ and stop reducing because the judgment involves aself-reference. In fact, there are infinitely many valid solutions just in our type system, including
αb := ⊤ → ⊥ and αb := ⊤ → 1. The problem can be solved by introducing recursive types, which
may be used to represent a whole class of solutions, and recursive constraints can be solved witha single recursive type. However, the other type of incompleteness that comes fromαb ≤ βbis still not addressed.
We propose an alternative approach that requires little change to the type system by restricting
the declarative system. If the declarative system did not treat the bottom and top types as monotypes in the first place, the algorithm would not need to guess those types. Formally, if monotypes
are defined as follows,
Monotypes’

τ′

::=

1 | a | τ1 → τ 2then subtyping relation between monotypes is simply equality.
The incomplete examples mentioned above can be addressed now, judgments like αb≤αb→1can no longer instantiate αb to a function type, otherwise it will infinitely loop without emitting
b because theany valid solution; judgments like αb ≤ βb can now be safely treated as αb = β,
instantiations of αb and βb must be equal to each other. Formally speaking, we proved the following
lemma
Lemma 5.10 (Subtyping between Monotypes is Equality).
If Ψ ⊢ τ1′ ≤ τ2′ , then τ1′ = τ2′ .
which also holds for the system in Chapter 4, yet it does not hold for the system with subtyping
when monotypes are not restricted.
On the meantime, algorithmic subtyping rules 12 and 13, and typing rules 27 and 37 should be
removed from the algorithm under the monotype restriction, since these rules solve existential
variables to ⊤ or ⊥. Other than that, the algorithm remains unchanged. Note that after removing95

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

these rules, the algorithm no longer has overlapping rules, therefore backtracking is not needed
any more.
Following the proof techniques in Chapter 4, both soundness and completeness theorems are
successfully proven and also mechanized. Given that the algorithm reduces judgments in a similar
way to the one in the previous chapter, the result is not so surprising. However, it still reveals
two facts: firstly, if we do not try to guess any type involving subtyping relation (the top andbottom types in our case), the algorithm should remain simple and complete; secondly, although
the current algorithm for the system with subtyping is incomplete, all source of incompletenesscomes from subtyping relations.
The source code of the proof can be found at https://github.com/JimmyZJX/
Dissertation/tree/main/src/Subtyping_mono_restriction.

5.5.2 Lazy Substitution and Non-terminating Loops
In this subsection, we propose a possible way to fix the incompleteness issue for the subtyping
part of the algorithm and discuss its impact to the existing formalization.
As we have analysed before, one major source of incompleteness comes from Rules 20 and
21, where two different existential variables are compared. A natural idea is to delay the solving procedure until all the corresponding constraints are collected. Constraint collection can be
implemented by the following new worklist definition, where the existential variables also comewith a set of upper bounds and a set of lower bounds. Both of the bounds consist of algorithmic
mono-types that does not contain αb (similar to the occurs-check condition).

Algorithmic worklistΓ ::=· | Γ, a | Γ, τA ≤ αb ≤ τA | Γ ⊩ ω

Differences of Algorithmic Rules. In presence of the bound collections, the algorithm
behaves slightly differently on variable solving rules. Firstly, rules that eagerly solve existential
variables to the top or bottom type are discarded (Rules 12 and 13). Next, Rules 20 and 21 add thecorresponding existential variable as part of a bound rather than performing a global substitution.
Γ[bα ][L ≤ βb ≤ U ] ⊩ αb ≤ βb −→20′ Γ[bα ][L ∪ {bα } ≤ βb ≤ U ]Γ[bα ][L ≤ βb ≤ U ] ⊩ βb ≤ α
b −→21′ Γ[bα ][L ≤ βb ≤ U ∪ {b
α }]

96

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

Instantiation rules (Rules 14 and 15) also behave lazily in order not to lose completeness.
Γ[L ≤ αb ≤ U] ⊩ αb ≤ A → B −→14′Γ[bα1 , αb2 , L ≤ αb ≤ U ∪ {bα1 → αb2 }] ⊩ αb1 → αb2 ≤ A → B
Γ[L ≤ αb ≤ U] ⊩ A → B ≤ αb −→15′Γ[bα1 , αb2 , L ∪ {bα1 → αb2 } ≤ αb ≤ U] ⊩ A → B ≤ αb1 → αb2These new rules differ from the original ones: the two fresh existential variables representing afunction type α
b1 → αb2 now acts as a bridge between αb and A → B. The algorithm breaks the
judgment αb≤αb1 → αb2 into two sub-problems: αb≤αb1 → αb2 and α
b1 → αb2 ≤ A → B. And
it is not difficult to prove that the problems before and after such transformation are equivalent
to each other.
The change of existential variable declaration and solving mechanisms also result in the changeof the algorithmic rule for garbage collecting them. When αb is at the top of the worklist and thus
going to be recycled, we need to further check if it can actually be solved, by ensuring that lower
bounds are indeed subtypes of upper bounds: any type that is a subtype of αb should be a subtypeof any super type of αb . Note that the bounds should not contain αb.
Γ, {li }n ≤ αb ≤ {uj }m −→2′ Γ ⊩1≤i≤n,1≤j≤m li ≤ uj
The notion {li }n indicates that the bound collection is of length n; the notion⊩1≤i≤n,1≤j≤m li ≤ uj
is similar to the syntax of list-comprehension, which creates a list of judgments⊩ l1 ≤ u1 · · · ⊩ l1 ≤ um · · · ⊩ l2 ≤ u1 · · · ⊩ ln ≤ um
According to the transitivity of subtyping, this rule is sound: any valid instantiation of αb , denoted
ταb , indicates that the instantiation of li ≤ ταb and ταb ≤ uj holds, therefore the instantiation ofli ≤ uj holds for any 1 ≤ i ≤ n, 1 ≤ j ≤ m.
On the other hand, such check is sufficient. In other words, we can always find a proper solutionfor αb if any lower bound is a subtype of any upper bound. This is supported by the following
property on declarative monotypes:
Lemma 5.11 (Sufficient Bound Check for Monotypes).
Given collections of monotypes {li }n and {uj }m ,if Ψ ⊢ li ≤ uj holds for any 1 ≤ i ≤ n, 1 ≤ j ≤ m,then there exists τ s.t. Ψ ⊢ li ≤ τ and Ψ ⊢ τ ≤ ui for any 1 ≤ i ≤ n, 1 ≤ j ≤ m.

97

5 Higher-Ranked Polymorphism with Object-Oriented Subtyping

Impact of the New Algorithm. The new algorithm addresses the incompleteness issue thoroughly by re-designing in a lazy-substitution style. However, the algorithm might loop forever
due to the new version of instantiation rules. For example, the following derivation results in
infinite instantiations:αb , βb ⊩ αb ≤ 1 → βb ⊩ βb ≤ 1 → αb−→ αb , βb1 , βb2 , {} ≤ βb ≤ {βb1 → βb2 } ⊩ αb ≤ 1 → βb ⊩ βb1 → βb2 ≤ 1 → αb−→ · · ·−→ αb , {1} ≤ βb1 ≤ {}, {} ≤ βb2 ≤ {bα }, {} ≤ βb ≤ {βb1 → βb2 } ⊩ αb ≤ 1 → βb−→ · · ·A further analyse on the problem suggests that the loop dependencies are not detected andreduced smartly by the lazy algorithm: it insist too much on not missing any possible solutions.
By loop dependency we refer to the following pattern αb ≤ A → B where αb ∈ A → B In thebabove example, one can derive (by transitivity of subtyping) αb≤1→β≤1→1→αb whichforms a (indirect) loop dependency on αb.
By performing experimental implementations and randomly generated tests, we observe thatthe algorithm accepts more valid relations when there are no loop dependencies, but may be
trapped in infinite loops otherwise. We have also tried to formalize how a loop detection procedure might be used to help prevent the non-termination problem, but most of them turn out tobe rather complicated and hard to mechanically formalize.

98

Part III
Related Work99

6 Related Work
Throughout the thesis, we have already discussed much of the closest related work. In this section
we summarize the key differences and novelties, and discuss some other related work.

6.1 Higher-Ranked Polymorphic Type Inference Algorithms
6.1.1 Predicative Algorithms
Higher-ranked polymorphism is a convenient and practical feature of programming languages.
Since full type-inference for System F is undecidable [Wells 1999], various decidable partial typeinference algorithms were developed. The declarative formulation of subtyping in Chapters 3 and
4 (and later extended in Chapter 5), originally proposed by Odersky and Läufer [1996], is predicative: ∀’s only instantiate to monotypes. The monotype restriction on instantiation is consideredreasonable and practical for most programs, except for those that require sophisticated forms ofhigher-order polymorphism. In predicative higher-ranked settings, type annotations may guidethe type system to accept lambda functions of higher-ranked types.
In addition to OL’s type system, the bidirectional system proposed by DK [Dunfield and Krishnaswami 2013] accepts even better type annotations via bidirectional type checking, which also
allow higher-ranked function types to check against an unannotated lambda. Such annotations
also improve readability of the program, and are not much of a burden in practice. DK’s algorithm
is shown to be sound, complete and decidable in 70 pages of manual proofs. Though carefully
written, some of the proofs are incorrect (see discussion in Section 4.1.2 and 4.3.2), which creates
difficulties when formalizing them in a proof assistant. In their follow-up work Dunfield and Krishnaswami [2019] enrich the bidirectional higher-ranked system with existentials and indexed
types. With a more complex declarative system, they developed a proof of over 150 pages. It iseven more difficult to argue its correctness for every single detail within such a big development.
Unfortunately, we find that their Lemma 26 (Parallel Admissibility) appears to have the same issue as lemma 29 in [Dunfield and Krishnaswami 2013]: the conclusion is false. We also discuss
the issue in more detail in Section 4.1.2.
Peyton Jones et al. [2007] developed another higher-ranked predicative bidirectional type system. Their subtyping relation is enriched with deep skolemisation, which is more general than100

6 Related Workours and allows more valid relations. The concept is also known as the distributivity rule [Mitchell
1984]. For example,∀a. ∀b. a → b → b ≤ ∀a. a → (∀b. b → b)
this subtyping relation does not hold in OL’s subtyping relation, because the instantiation of bin the left-hand-side type happens strictly before the introduction of the variable b in the righthand-side type. Deep skolemisation can be achieved through a pre-processing that extracts all
the ∀’s in the return position of a function type to the top level. After such pre-processing, theright-hand-side type becomes ∀a. ∀b. a → b → b and the subtyping relation holds.
In terms of handling applications where type parameters are implicit, they do not use the application inference judgment as DK’s type system. Instead, they employ a complicated mechanism
for implicit instantiation taken care by the unification process for the algorithm. A manual proof
is given, showing that the algorithm is sound and complete with respect to their declarative specification.
In a more recent work, Xie and Oliveira [2018] proposed a variant of a bidirectional type inference system for a predicative system with higher-ranked types. Type information flows fromarguments to functions with an additional application mode. This variant allows more higherorder typed programs to be inferred without additional annotations. Following the new mode,
the let-generalization of the Hindley-Milner system is well supported as syntactic sugar. The
formalization includes some mechanized proofs for the declarative type system, but all proofs
regarding the algorithmic type system are manual.

6.1.2 Impredicative Algorithms
Impredicative System F allows instantiation with polymorphic types, but unfortunately its subtyping system is already undecidable [Chrząszcz 1998]. Works on partial impredicative typeinference algorithms navigate a variety of design tradeoffs for a decidable algorithm. Generally
speaking, such algorithms tend to be more complicated, and thus less adopted in real-world programming languages.
MLF [Le Botlan and Rémy 2003, 2009; Rémy and Yakobowski 2008] extends types of System
F with a form of bounded quantification and proposes an impredicative system. The type inference algorithm always infers principal types given proper type annotations. Through the technique called “monomorphic abstraction of polymorphic types”, polymorphic instantiations are
expressed by constraints on type variables of type schemes. An annotation is only needed when
an argument of a lambda function is used polymorphically. Moreover, their type system is robust
against a wide range of program transformations, including let-expansion, let-reduction and ηexpansion. However, the extended type structure of MLF introduces non-compatible types with
System F, and it complicates the metatheory and implementation of the type system.

101

6 Related Work

HMF [Leijen 2008] takes a slightly different approach by not extending types with bounds,
therefore programmers still work with plain System F types. The algorithm works similarly compared to MLF , except that it does not output richer types. Instead, when there are ambiguity
and no principal type can be inferred, being a conservative algorithm, HMF prefers predicative
instantiations to maintain backward the compatibility of HM. Soon after HMF, HML [Leijen
2009] is proposed as an extension of HMF with flexible types. The system eliminates rigid quantifications (α = σ) of MLF and only keeps the flexible quantifications (α ≥ σ). Furthermore, avariant “Rigid HML” is presented by restricting let-bindings to System F types only, so that type
annotations can still stay inside System F. Similar to HMF, they both require type annotations at
higher-ranked types or ambiguous implicit instantiations.
FPH [Vytiniotis et al. 2008] employ a box notion σ to encapsulate polymorphic instantiations
internally in the algorithm. A type inside a box indicates that the instantiation is impredicative.
Therefore an inferred type with a box type in it means that incomparable System F types may
be produced, and that is rejected before entering the environment. Although more annotations
might be required compared with other approaches, the algorithm of FPH is much simpler, thanks
to the simple syntax and subtyping relation of box types.
Guarded Impredicative Polymorphism [Serrano et al. 2018] was recently proposed as an improvement on GHC’s type inference algorithm with impredicative instantiation. They make useof local information in n-ary applications to infer polymorphic instantiations with a relatively
simple specification and unification algorithm. Although not all impredicative instantiations canbe handled well, their algorithm is already quite useful in practice.
A recent follow-up work, the Quick Look [Serrano et al. 2020], takes a more conservative approach. The algorithm will try its best to infer impredicative instantiations, and only use theinstantiation when it is the best one. In order to do so, the algorithm also needs to analyse all theargument types during a function call, and make use of the guardedness property to decide theprincipality of the inferred instantiation. When Quick Look cannot give the best instantiation,
it will instead try predicative inference as HM. This conservative approach makes sure that thealgorithm does not infer bad types and leads the subsequent type checking in wrong directions.
In the meantime, they treat the function arrow (→) as invariant like normal type constructors.
This change significantly restricts the subtyping relation and thus simplifies guesses for implicit
parameters. Manual η-expansions are required to regain the co- and contravariance of function
types.
FreezeML [Emrich et al. 2020] is another recent work that extends the ML type system withimpredicative instantiations. A special syntax of expression, the explicit freezing ⌈x⌉, is added
to guide the type system. Freezed variables are prevented to be instantiated by the type system,
therefore variables of polymorphic types may force the type inference algorithm to instantiate
impredicatively. In combination with the let-generalization rule, programmers may also encode102

6 Related Workexplicit generalization and explicit instantiation. This work provides a nice means for programmers to control how type inference algorithm deals with impredicative instantiations.

6.2 Type Inference Algorithms with Subtyping
Type systems in presence of subtyping usually encounter constraints that are not simply equalities as in HM. Therefore constraint solvers used in HM, where unifications are based on equality,cannot be easily extended to support subtyping. Instead, constraints are usually collected as subtyping relations and may delay resolving as the constraints accumulate. Eifrig et al. [1995a,c]
proposed systems that are based on constraint types, i.e. types expressed together with a set of
constraints τ | {τ1 ≤ τ2 }. Their type checking algorithm checks at each step whether each constraint in the closure of constraint set is consistent, which is a set of rules that prevent obvious
contradictions appear, such as Int ≤ Bool. Our attempt in Section 5.5.2 is similar to this idea,
where we exhaustively check if every subtyping relation derived from the bounds is valid. However, our algorithm tries to solve the bounds into concrete types, and it turns out that it neverterminates in some complex cases.
Constraint types improve the expressiveness of the type system, yet the type inference algorithm can be quite slow. The size of the constraint is linear in the program size, and the closure
can grow to cubic size. Pottier [1998] proposed three methods to simplify constraints in his Ph.D.
thesis, aiming at improving the efficiency of type inference algorithms and improving the readability of the resulting types. By canonization, constraints are converted to canonical forms with
the introduction of new meta-variables; garbage collection eliminates constraints that do not affectthe type; finally, minimization shares nodes within the constraint graph.
Inspired by the simplification strategies of Pottier’s, MLsub [Dolan and Mycroft 2017] suggest that the data flow on the constraint graph can reflect directly on types extended by a richer
type system, where lattices operations are used to represent constraints imposed on type variables. Polar types distinguish between input types and output types, and pose different restrictions on them. As a result, constraints can easily be transformed into canonical forms, and thebi-unification algorithm can solve them by simple substitutions. One can also view the MLsub
system as a different way to encode the constraint types: instead of a set of constraints that isstated along with the type, types themselves now contain subtyping constraints with the help oflattice operations. Similarly, the size of constraints may grow with the size of program and affectthe readability. Therefore, various simplification algorithms should be used in real applications.
A more recent work, the Simple-sub [Parreaux 2020], further simplifies the algorithm of MLsub
and is implemented in 500 lines of code. While being equivalent to MLsub, it is a more efficientvariant.

103

6 Related Work

6.3 Techniques Used in Type Inference Algorithms
6.3.1 Ordered Contexts in Type Inference
Gundry et al. [2010] revisit algorithm W and propose a new unification algorithm with the helpof ordered contexts. Similar to DK’s algorithm, information of meta-variables flows from input
contexts to output contexts. Not surprisingly, its information increase relation has a similar role
to DK’s context extension. Our algorithm, in contrast, eliminates output contexts and solution
records (bα = τ ), simplifying the information propagation process through immediate substitution by collecting all the judgments in a single worklist.

6.3.2 The Essence of ML Type Inference
Constraint-based type inference is adopted by Pottier and Rémy [2005] for ML type systems,
which do not employ higher-ranked polymorphism. An interesting feature of their algorithm isthat it keeps precise scoping of variables, similarly to our approach. Their algorithm is divided
into constraint generation and solving phases (which are typical of constraint-based algorithms).
Furthermore an intermediate language is used to describe constraints and their constraint solver
utilizes a stack to track the state of the solving process. In contrast, our algorithm has a single
phase, where the judgment chains themselves act as constraints, thus no separate constraint language is needed.

6.3.3 Lists of Judgments in Unification
Some work [Abel and Pientka 2011; Reed 2009] adopts a similar idea to this paper in work on
unification for dependently typed languages. Similarly to our work the algorithms need to be very
careful about scoping, since the order of variable declarations is fundamental in a dependently
typed setting. Their algorithms simplify a collection of unification constraints progressively ina single-step style. In comparison, our algorithm mixes variable declarations with judgments,
resulting in a simpler judgment form, while processing them in a similar way. One importantdifference is that contexts are duplicated in their unification judgments, which complicates theunification process, since the information of each local context needs to be synchronized. Instead
we make use of the nature of ordered context to control the scope of unification variables. While
their algorithms focus only on unification, our algorithm also deals with other types of judgments
like synthesis. A detailed discussion is given in Section 4.1.3.

104

6 Related Work

6.4 Mechanical Formalization of Polymorphic Type Systems
Since the publication of the POPLMark challenge [Aydemir et al. 2005], many theorem provers
and packages provide new methods for dealing with variable binding [Aydemir et al. 2008; Chlipala 2008; Urban 2008]. More and more type systems are formalized with these tools. However,mechanizing certain algorithmic aspects, like unification and constraint solving, has received very
little attention and is still challenging. Moreover, while most tools support local (input) contexts
in a neat way, many practical type-inference algorithms require more complex binding structureswith output contexts or various forms of constraint solving procedures.
Algorithm W, as one of the classic type inference algorithms for polymorphic type systems,
has been manually proven to be sound and complete with respect to the Hindley-Milner typesystem [Damas and Milner 1982; Hindley 1969; Milner 1978]. After around 15 years, the algorithm was formally verified by Naraschewski and Nipkow [1999] in Isabelle/HOL [Nipkow et al.
2002]. The treatment of new variables was tricky at that time, while the overall structure follows
the structure of Damas’s manual proof closely. Later on, other researchers [Dubois 2000; Dubois
and Menissier-Morain 1999] formalized algorithm W in Coq [The Coq development team 2017].
Nominal techniques [Urban 2008] in Isabelle/HOL have been developed to help programming
language formalizations, and are used for a similar verification [Urban and Nipkow 2008]. Moreover, Garrigue [Garrigue 2015] mechanized a type inference algorithm, with the help of locallynameless [Charguéraud 2012], for Core ML extended with structural polymorphism and recursion.

105

Part IV
Epilogue106

7 Conclusion and Future Work
7.1 Conclusion
In this thesis, we proposed new bidirectional type inference algorithms for predicative higherranked implicit parametric polymorphic systems. We showed how worklists ease the design ofalgorithms and also mechanical formalizations. By collecting all judgments in a single worklist,
the algorithm performs unification with a bird’s-eye view of all the judgments, therefore propagation between judgments is as simple as a global substitution. Compared with the classical HM
unification procedure, our algorithm does not need separated relations (or fixpoints) for unification. From the formalization point of view, eager substitutions are also easier to state and reason
in a proof assistant. Therefore, we obtained fully formalized properties for all our developments
relatively easily. Overall, we developed the following systems and/or type inference algorithms:• We developed a worklist algorithm for OL’s higher-ranked subtyping system. The algorithm operates on a worklist of subtyping judgments and a single context where a variabledeclaration is shared across the worklist. Compared with DK’s algorithm, our approach
avoids the use of output contexts, which complicates the scoping of variables and is hard
to formalize in a proof assistant. Eager substitutions that solve existential variables are
directly applied to the worklist, therefore passing the partial information to the rest judgments. We proved soundness, completeness and decidability of the algorithm in the Abella
theorem prover.
• We developed a worklist algorithm for DK’s higher-ranked bidirectional type system. In order to properly encode judgments that output types, such as the type inference judgment,
continuation-passing-style judgment chains are developed. Compared with the previous
work that uses a single context, we further unify the worklist with variable declarations.
Such unification results in a much more accurate track of variable scopings, and the algorithm will garbage-collect variables as soon as they are not referred to anymore. Unlike
using output contexts as DK’s algorithm, designing rules for worklist context is less likely
to contain bugs in terms of variable scoping. Once again, based on eager substitutions, thealgorithm is easy to formalize. We showed soundness, completeness and decidability in the
Abella theorem prover.

107

7 Conclusion and Future Work• We developed a backtracking-based algorithm for a higher-ranked bidirectional type system with object-oriented subtyping. With the introduction of the top and bottom types andrelevant subtyping relations, meta-variable instantiations are no longer deterministic likethe HM system. The backtracking-based algorithm preserves most characteristics of theprevious worklist context, and it “tries” obvious solutions in parallel with detailed analysis
as previous work. We proved that the algorithm is always sound, and subtyping is complete
under the rank-1 restriction.

7.2 Future WorkIn this section, we discuss several interesting possibilities to explore in the future.
Termination Theorem for Type Inference with Subtyping The algorithm we presented
and formalized in Chapter 5 enjoys several important machine-verified properties, including
soundness and completeness under a rank-1 restriction. However, we have not yet found a proper
termination measure for the algorithmic subtyping rules. What complicates the problem is that
common measures are not decreasing all the time. For example, subtyping between function
types may increase the number of judgments; and instantiation judgments that split existential
variables may increase the number of unsolved existential variables. We are mostly convincedby the fact that a large set of tests performed on randomly generated subtyping judgments do
terminate. And we hope that a clever termination argument may be proposed in the near future.
Practical Impredicative Type Inference Impredicative type inference algorithms are sometimes helpful when dealing with higher-ranked types. Simple forms of impredicativity can be
unambiguous and easy to understand by programmers, such ashead ids
where head :: ∀p. [p] → p and ids :: [∀a. a → a]. The application (head ids) should have type∀a. a → a, because p is instantiated to ∀a. a → a and that is the only choice we can make.
Moreover, even though there are programs that have incomparable System F types, impredicative system may offer means like type annotation to manually pick the right one. For example,
single id
where single :: ∀a. p → [p] and id :: ∀a. a → a. This term has two incomparable types[∀a. a → a] and ∀a. [a → a]. One might expect that a type annotation might help pick theright case, like ((single id) :: [∀a. a → a]), which requires a system that allows impredicative instantiation to do so. There are many impredicative systems developed out of various108

7 Conclusion and Future Worktechniques [Emrich et al. 2020; Le Botlan and Rémy 2003; Leijen 2008, 2009; Serrano et al. 2020,2018; Vytiniotis et al. 2008], and we leave the extension of impredicativity to our algorithms as
future work.
Optimization All the three type inference algorithms described in this thesis are based on eager global substitution on the worklists. The benefit is to reduce the difficulty for mechanical formalizations in theorem provers, especially in Abella. Additionally, eager substitutions represent
simple equivalent transformations on the state of worklist, alleviating the complication of variable scoping and reasoning for correctness. However, a naive implementation of our algorithm
will be very inefficient, since the worklist is iterated so often whenever an existential variable issolved or partially solved.
Compared with mature algorithms like the algorithm W [Milner 1978] and the OutsideIn(X) [Vytiniotis et al. 2011] type inference algorithm, which produces substitutions once all the constraints
are collected and reduced, our algorithms manipulate the judgments themselves on-the-fly. Efficient implementations will model meta-variables as mutable references and apply the results
if they are solved by the constraint solver. DK’s algorithm [Dunfield and Krishnaswami 2013]
requires output contexts, which are likely to be implemented in a state monad or other statefulapproaches. Solved existential variables encoded in their algorithmic context are different fromours. Instead of removing the declaration of the variable and propagate its solution to all the rest
judgments, they extend the entry in the context with its solution, αb = τ , and pass it to the output
context. Such entry is easy to implement with an efficient approach using mutable references.
We can also adopt such an idea and reformulate our eager substitution with lazy ones by keeping
track of solutions to existential variables, and only perform substitution when the judgment isjust about to be reduced.
Unfortunately, lazy substitution only solves part of the problem. By using ordered contexts,
the scoping of variables is precisely captured by the relative positions in which they are declaredin the context. Some algorithmic rules are designed to use the position information, where swapping positions might lead to unsound implementation. For example, the algorithmic system ofChapter 5 includes these rules:b ⊩ a ≤ βb −→16 {βb := a} Γ[a][β]bΓ[a][β]b ⊩ βb ≤ a −→17 {βb := a} Γ[a][β]bΓ[a][β]b is used to ensure that a is declared before β,b therefore it is fine for the
The hole notation Γ[a][β]monotype represented by βb to be a. In a naive implementation, frequent iteration is required tolook up the relative positions of variable declarations. We may address the problem for a more
efficient algorithm following the idea of Remy et al. [1992].

109

7 Conclusion and Future Work

Moreover, there are also reduction rules that remove and/or insert variables from(to) the middleof the ordered context, as in the following rules:
Γ[bα] ⊩ αb ≤ A → B −→14 {bα := αb1 → αb2 } (Γ[bα] ⊩ αb ≤ A → B)
when αb∈/ F V (A → B)
Γ[bα] ⊩ A → B ≤ αb −→15 {bα := αb1 → αb2 } (Γ[bα] ⊩ A → B ≤ αb)when αb∈/ F V (A → B)
To sum up, we plan to propose an implementation-friendly version of the algorithm that does
not require many eager substitutions, and we also hope that there will be suitable data structures or
algorithms which optimizes the complexity of those time-consuming operations on the ordered
context.
Class Hierarchy of Nominal Subtyping Nowadays, most mainstream object-oriented programming languages support nominal subtyping, which means that the subtyping relation is defined by the programmers explicitly through language constructs such as inheritance. For example, we may define a Pos class to represent positive integers, which inherits the Int class. The
subtyping relation Pos ≤ Int automatically holds. An algorithmic subtyping judgment αb ≤ Int
now might have several solutions: Int, Pos, or ⊥. In order to calculate a range of solutions insteadof just simple types, lazy algorithms that operate on bounds fit the task better. We plan to explore
extensions of the algorithm described in Section 5.5.2. The algorithm progressively collects upperand lower bounds of existential variables, and finally checks if valid solutions are satisfying all thebounds.
Nonetheless, we encounter termination problems when trying to adopt the lazy approach. Experiments indicate that loop dependency in combination with the instantiation rule (bα≤A→B) might cause infinite loops. As a practical compromise, we may impose restrictions on existential variables so that they are not instantiated to function types when they are likely to be aclass type. We also hope that better treatment on loop dependencies can be developed, especially
under assumptions of real-world programming tasks. For future work, we aim at a terminating
and sound algorithm for practical object-oriented type inference.
Type Inference with Recursive Types Among all the algorithms we proposed in this thesis,
we reject subtyping judgments likeαb ≤ A → B where αb ∈ FV(A) ∪ FV(B)1107 Conclusion and Future Workbecause no HM monotype satisfies a subtyping relation likeτ ≤ τ → Int
and unfolding such algorithmic judgment might cause an infinite loop. However, recursive types
may satisfy such judgment, for example,µx. x → Int ≤ (µx. x → Int) → Int
holds since the unfolding of µx. x → Int is (µx. x → Int) → Int. In other words, if we extend
our type system by including recursive types, we would accept such judgment with a principalrecursive type, instead of rejecting it because we cannot find such a type. The MLsub [Dolan
and Mycroft 2017] already accepts recursive types, and it deals with recursive constraints in theway we described above. It is an interesting question if adding recursive types may improve theexpressiveness of our system and remain complete at the same time.
Bounded Quantification and F-Bounded Quantification Bounded quantification[Cardelli and Wegner 1985] and F-bounded quantification [Canning et al. 1989] are techniques
commonly seen in object-oriented programming languages. Bounded quantification allows constraints imposed on universally quantified variables:∀(a ≤ Int). a → a → String
F-Bounded quantification further extends the constraints so that recursive references of the variables are also allowed. Although the subtyping is proven to be undecidable in presence of both
F-bounded quantification and variance on generics, Kennedy and Pierce [2007] proposed threeforms of restrictions that we can explore further. Combining bidirectional type checking withbounded quantifications may further improve the experience for object-oriented programmers.

111

Bibliography[Citing pages are listed after each reference.]

Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven
Schäfer, and Kathrin Stark. 2018. POPLMark Reloaded: Mechanizing Proofs by Logical Relations. Submitted to the Journal of functional programming (2018). [cited on page 9]Andreas Abel and Brigitte Pientka. 2011. Higher-order dynamic pattern unification for dependent types and records. In International Conference on Typed Lambda Calculi and Applications.
Springer, 10–26. [cited on pages 43, 50, and 104]
Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich.
2008. Engineering Formal Metatheory. In Proceedings of the 35th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL ’08). [cited on pages 9
and 105]
Brian E Aydemir, Aaron Bohannon, Matthew Fairbairn, J Nathan Foster, Benjamin C Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic.
2005. Mechanized metatheory for the masses: The POPLmark challenge. In The 18th International Conference on Theorem Proving in Higher Order Logics. [cited on pages 9 and 105]
Yves Bertot, Benjamin Grégoire, and Xavier Leroy. 2006. A Structured Approach to Proving
Compiler Optimizations Based on Dataflow Analysis. In Proceedings of the 2004 International
Conference on Types for Proofs and Programs (TYPES’04). [cited on page 9]Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John C. Mitchell. 1989. F-Bounded
Polymorphism for Object-Oriented Programming. In Proceedings of the Fourth International
Conference on Functional Programming Languages and Computer Architecture (Imperial College, London, United Kingdom) (FPCA ’89). Association for Computing Machinery, New
York, NY, USA, 273–280. https://doi.org/10.1145/99370.99392 [cited on page 111]
Luca Cardelli. 1988. A semantics of multiple inheritance. Information and Computation 76, 2(1988), 138–164. https://doi.org/10.1016/0890-5401(88)90007-7 [cited on page 8]112

Bibliography

Luca Cardelli and Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. ACM Comput. Surv. 17, 4 (Dec. 1985), 471–523. https://doi.org/10.1145/
6041.6042 [cited on page 111]
Bor-Yuh Evan Chang, Adam Chlipala, and George C. Necula. 2006. A Framework for Certified
Program Analysis and Its Applications to Mobile-code Safety. In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’06).
[cited on page 9]
Arthur Charguéraud. 2012. The Locally Nameless Representation. Journal of Automated Reasoning 49, 3 (01 Oct 2012), 363–408. [cited on page 105]Paul Chiusano and Runar Bjarnason. 2015. Unison. http://unisonweb.org [cited on page 7]
Adam Chlipala. 2008. Parametric Higher-order Abstract Syntax for Mechanized Semantics. In
Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming(ICFP ’08). [cited on page 105]
Jacek Chrząszcz. 1998. Polymorphic subtyping without distributivity. In Mathematical Foundations of Computer Science 1998, Luboš Brim, Jozef Gruska, and Jiří Zlatuška (Eds.). Springer
Berlin Heidelberg, Berlin, Heidelberg, 346–355. [cited on pages 19 and 101]
Alonzo Church. 1932. A Set of Postulates for the Foundation of Logic. Annals of Mathematics 33,
2 (1932), 346–366. http://www.jstor.org/stable/1968337 [cited on page 4]
Alonzo Church. 1941. The calculi of lambda-conversion. Number 6. Princeton University Press.
[cited on page 4]
Luis Damas and Robin Milner. 1982. Principal Type-schemes for Functional Programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’82). [cited on pages 5, 13, 29, and 105]
N.G de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automaticformula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75, 5 (1972), 381–392. https://doi.org/10.1016/1385-7258(72)90034-0 [cited on page 10]
Disciple Development Team. 2017. The Disciplined Disciple Compiler.

http://disciple.

ouroborus.net/ [cited on page 8]
Stephen Dolan and Alan Mycroft. 2017. Polymorphism, Subtyping, and Type Inference in MLsub.
In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

113

Bibliography(Paris, France) (POPL 2017). Association for Computing Machinery, New York, NY, USA,60–72. https://doi.org/10.1145/3009837.3009882 [cited on pages 23, 24, 78, 103,
and 111]Catherine Dubois. 2000. Proving ML type soundness within Coq. Theorem Proving in Higher
Order Logics (2000), 126–144. [cited on pages 9 and 105]
Catherine Dubois and Valerie Menissier-Morain. 1999. Certification of a type inference tool for
ML: Damas–Milner within Coq. Journal of Automated Reasoning 23, 3 (1999), 319–346. [cited
on pages 9 and 105]
Joshua Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13). [cited on pages 7, 9, 21, 27, 29, 31,
42, 43, 48, 64, 100, and 109]
Joshua Dunfield and Neelakantan R. Krishnaswami. 2019. Sound and Complete Bidirectional
Typechecking for Higher-rank Polymorphism with Existentials and Indexed Types. Proc. ACM
Program. Lang. 3, POPL, Article 9 (Jan. 2019), 28 pages. [cited on pages 48 and 100]
Jonathan Eifrig, Scott Smith, and Valery Trifonov. 1995a. Sound Polymorphic Type Inference for
Objects (OOPSLA ’95). Association for Computing Machinery, New York, NY, USA, 169–184.
https://doi.org/10.1145/217838.217858 [cited on page 103]
Jonathan Eifrig, Scott Smith, and Valery Trifonov. 1995b. Type Inference for Recursively Constrained Types and its Application to OOP. Electronic Notes in Theoretical Computer Science
1 (1995), 132 – 153. https://doi.org/10.1016/S1571-0661(04)80008-2 MFPS XI,Mathematical Foundations of Programming Semantics, Eleventh Annual Conference. [cited
on page 78]
Jonathan Eifrig, Scott Smith, and Valery Trifonov. 1995c. Type Inference for Recursively Constrained Types and its Application to OOP. Electronic Notes in Theoretical Computer Science
1 (1995), 132–153.

https://doi.org/10.1016/S1571-0661(04)80008-2 MFPS XI,Mathematical Foundations of Programming Semantics, Eleventh Annual Conference. [cited
on page 103]Frank Emrich, Sam Lindley, Jan Stolarek, James Cheney, and Jonathan Coates. 2020. FreezeML:
Complete and Easy Type Inference for First-Class Polymorphism. In Proceedings of the 41st
ACM SIGPLAN Conference on Programming Language Design and Implementation (London,UK) (PLDI 2020). Association for Computing Machinery, New York, NY, USA, 423–437.
https://doi.org/10.1145/3385412.3386003 [cited on pages 6, 102, and 109]

114

Bibliography

Phil Freeman. 2017. PureScript. http://www.purescript.org/ [cited on pages 7 and 8]
Andrew Gacek. 2008. The Abella Interactive Theorem Prover (System Description). In Proceedings of IJCAR 2008 (Lecture Notes in Artificial Intelligence). [cited on pages 10, 38, 42, 43, 60,
70, and 94]
Jacques Garrigue. 2015. A certified implementation of ML with structural polymorphism andrecursive types. Mathematical Structures in Computer Science 25, 4 (2015), 867–891. [cited on
pages 9 and 105]
Andrew Gill, John Launchbury, and Simon L. Peyton Jones. 1993. A Short Cut to Deforestation. In
Proceedings of the Conference on Functional Programming Languages and Computer Architecture(FPCA ’93). [cited on page 6]
Jean-Yves Girard. 1971. Une Extension De ĽInterpretation De Gödel a ĽAnalyse, Et Son Application a ĽElimination Des Coupures Dans ĽAnalyse Et La Theorie Des Types. In Proceedings of the Second Scandinavian Logic Symposium, J.E. Fenstad (Ed.). Studies in Logic andthe Foundations of Mathematics, Vol. 63. Elsevier, 63–92. https://doi.org/10.1016/
S0049-237X(08)70843-7 [cited on page 4]
Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures de l’arithmétiqued’ordre supérieur. Ph.D. Dissertation. Éditeur inconnu. [cited on page 4]
Adam Gundry, Conor McBride, and James McKinna. 2010. Type Inference in Context. In Proceedings of the Third ACM SIGPLAN Workshop on Mathematically Structured Functional Programming (MSFP ’10). [cited on pages 43 and 104]
Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Transactionsof the american mathematical society 146 (1969), 29–60. [cited on pages 5, 13, and 105]Mark P. Jones. 1995. Functional Programming with Overloading and Higher-Order Polymorphism. In Advanced Functional Programming (Lecture Notes in Computer Science 925). [cited
on page 6]
Andrew Kennedy and Benjamin C. Pierce. 2007. On Decidability of Nominal Subtyping with
Variance. In International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL/WOOD) (international workshop on foundations and developments of objectoriented languages (fool/wood) ed.). https://www.microsoft.com/en-us/research/
publication/on-decidability-of-nominal-subtyping-with-variance/ [cited on
page 111]

115

Bibliography

A. J. Kfoury and J. Tiuryn. 1992. Type Reconstruction in Finite Rank Fragments of the SecondOrder λ-Calculus. Inf. Comput. 98, 2 (June 1992), 228–257. https://doi.org/10.1016/
0890-5401(92)90020-G [cited on page 17]
Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew
Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. 2012.
Run Your Research: On the Effectiveness of Lightweight Mechanization. In Proceedings of the39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Philadelphia, PA, USA) (POPL ’12). 285–296. [cited on pages 9 and 42]
Ralf Lämmel and Simon Peyton Jones. 2003. Scrap Your Boilerplate: A Practical Design Pattern
for Generic Programming. In Proceedings of the 2003 ACM SIGPLAN International Workshop
on Types in Languages Design and Implementation (TLDI ’03). [cited on page 6]
John Launchbury and Simon L. Peyton Jones. 1994. Lazy Functional State Threads. In Proceedingsof the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation(Orlando, Florida, USA) (PLDI ’94). Association for Computing Machinery, New York, NY,
USA, 24–35. https://doi.org/10.1145/178243.178246 [cited on page 6]
John Launchbury and Simon L. Peyton Jones. 1995. State in Haskell. LISP and Symbolic Computation 8, 4 (1995), 293–341. [cited on page 6]
Didier Le Botlan and Didier Rémy. 2003. MLF: Raising ML to the Power of System F. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP’03). [cited on pages 6, 7, 101, and 109]
Didier Le Botlan and Didier Rémy. 2009. Recasting MLF. Information and Computation 207, 6(2009), 726–785. https://doi.org/10.1016/j.ic.2008.12.006 [cited on page 101]
Daan Leijen. 2008. HMF: Simple Type Inference for First-class Polymorphism. In Proceedingsof the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08).
[cited on pages 6, 7, 102, and 109]
Daan Leijen. 2009. Flexible Types: Robust Type Inference for First-Class Polymorphism. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Savannah, GA, USA) (POPL ’09). Association for Computing Machinery,
New York, NY, USA, 66–77. https://doi.org/10.1145/1480881.1480891 [cited on
pages 102 and 109]
Xavier Leroy et al. 2012. The CompCert verified compiler. Documentation and user’s manual.
INRIA Paris-Rocquencourt (2012). [cited on page 9]116

Bibliography

Alberto Martelli and Ugo Montanari. 1982. An Efficient Unification Algorithm. ACM Trans.
Program. Lang. Syst. 4, 2 (April 1982), 258–282. [cited on page 49]
Dale Miller. 1992. Unification under a mixed prefix. Journal of Symbolic Computation 14, 4 (1992),
321–358. https://doi.org/10.1016/0747-7171(92)90011-R [cited on page 28]
Dale Miller. 2000. Abstract Syntax for Variable Binders: An Overview. In CL 2000: Computational
Logic (Lecture Notes in Artificial Intelligence). [cited on pages 39 and 70]
Robin Milner. 1978. A theory of type polymorphism in programming. Journal of computer andsystem sciences 17, 3 (1978), 348–375. [cited on pages 4, 5, 13, 16, 49, 105, and 109]
John C. Mitchell. 1984. Coercion and Type Inference. In Proceedings of the 11th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages (Salt Lake City, Utah, USA)
(POPL ’84). Association for Computing Machinery, New York, NY, USA, 175–185. https://doi.org/10.1145/800017.800529 [cited on pages 8 and 101]
Wolfgang Naraschewski and Tobias Nipkow. 1999. Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning 23, 3 (1999), 299–318. [cited on pages 9, 16,
and 105]
Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle/HOL: a proof assistantfor higher-order logic. Vol. 2283. Springer Science & Business Media. [cited on page 105]
Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations to Work. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL ’96). [cited on pages 6, 7, 16, 18, 21, 27, 43, 81, and 100]
Lionel Parreaux. 2020. The Simple Essence of Algebraic Subtyping: Principal Type Inference with
Subtyping Made Easy (Functional Pearl). Proc. ACM Program. Lang. 4, ICFP, Article 124 (Aug.
2020), 28 pages. https://doi.org/10.1145/3409006 [cited on page 103]
Simon Peyton Jones and Mark Shields. 2004. Lexically-scoped type variables. (2004). http://research.microsoft.com/en-us/um/people/simonpj/papers/scoped-tyvars/
Draft. [cited on pages 73 and 75]
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical
type inference for arbitrary-rank types. Journal of functional programming 17, 1 (2007), 1–82.
[cited on pages 7, 19, and 100]
Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Trans. Program.
Lang. Syst. 22, 1 (Jan. 2000), 1–44. https://doi.org/10.1145/345099.345100 [cited on
page 7]117

Bibliography

Andrew M. Pitts. 2003. Nominal logic, a first order theory of names and binding. Information
and Computation 186, 2 (2003), 165–193. https://doi.org/10.1016/S0890-5401(03)00138-X Theoretical Aspects of Computer Software (TACS 2001). [cited on page 10]
François Pottier. 1998. Type inference in the presence of subtyping: from theory to practice. Ph.D.
Dissertation. INRIA. [cited on pages 78 and 103]
François Pottier and Didier Rémy. 2005. Advanced Topics in Types and Programming Languages.
The MIT Press, Chapter The Essence of ML Type Inference, 387–489.

[cited on pages 50

and 104]
Jason Reed. 2009. Higher-order Constraint Simplification in Dependent Type Theory. In Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory
and Practice (LFMTP ’09). [cited on pages 43, 50, and 104]
Didier Remy, E De Recherche, Et En Automatique, Domaine De Voluceau, and Calcul Symbolique Programmation. 1992. Extension of ML Type System with a Sorted Equational Theory on
Types. [cited on page 109]
Didier Rémy and Boris Yakobowski. 2008. From ML to MLF: Graphic Type Constraints with
Efficient Type Inference. SIGPLAN Not. 43, 9 (Sept. 2008), 63–74. https://doi.org/10.
1145/1411203.1411216 [cited on page 101]
John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium, B. Robinet (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 408–425. [cited on page 4]
John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In Proceedings of the
IFIP 9th World Computer Congress. [cited on page 74]
J C Reynolds. 1985. Three Approaches to Type Structure. In Proc. of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT) Berlin, March 25-29, 1985
on Mathematical Foundations of Software Development, Vol. 1: Colloquium on Trees in Algebra
and Programming (CAAP’85) (Berlin, Germany). Springer-Verlag, Berlin, Heidelberg, 97–138.
[cited on page 8]
Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. 2020. A Quick
Look at Impredicativity. Proc. ACM Program. Lang. 4, ICFP, Article 89 (Aug. 2020), 29 pages.
https://doi.org/10.1145/3408971 [cited on pages 6, 102, and 109]
Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. 2018. Guarded
Impredicative Polymorphism. In Proceedings of the 39th ACM SIGPLAN Conference on Pro-

118

Bibliography

gramming Language Design and Implementation (PLDI 2018).

[cited on pages 6, 7, 102,

and 109]
Zhendong Su, Alexander Aiken, Joachim Niehren, Tim Priesnitz, and Ralf Treinen. 2002. The
First-Order Theory of Subtyping Constraints. In Proceedings of the 29th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (Portland, Oregon) (POPL ’02).
Association for Computing Machinery, New York, NY, USA, 203–216. https://doi.org/
10.1145/503272.503292 [cited on page 80]
The Coq development team. 2017. The Coq proof assistant. https://coq.inria.fr/ [cited
on page 105]
Jerzy Tiuryn and Pawel Urzyczyn. 1996. The subtyping problem for second-order types is undecidable. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. [cited on
page 4]
Valery Trifonov and Scott Smith. 1996. Subtyping constrained types. In Static Analysis, Radhia
Cousot and David A. Schmidt (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 349–365.
[cited on page 78]
Christian Urban. 2008. Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning
40, 4 (2008), 327–356. [cited on page 105]
Christian Urban and Tobias Nipkow. 2008. Nominal verification of algorithm W. From Semantics
to Computer Science. Essays in Honour of Gilles Kahn (2008), 363–382.

[cited on pages 9

and 105]
Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. Outsidein(x) Modular Type Inference with Local Assumptions. J. Funct. Program. 21, 4–5 (Sept.
2011), 333–412. https://doi.org/10.1017/S0956796811000098 [cited on page 109]
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. 2008. FPH: First-class Polymorphism for Haskell. In Proceedings of the 13th ACM SIGPLAN International Conference on
Functional Programming (ICFP ’08). [cited on pages 6, 7, 102, and 109]
Joe B Wells. 1999. Typability and type checking in System F are equivalent and undecidable.
Annals of Pure and Applied Logic 98, 1-3 (1999), 111–156. [cited on pages 6, 15, 16, and 100]
Ningning Xie and Bruno C. d. S. Oliveira. 2018. Let Arguments Go First. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham, 272–299.
[cited on page 101]119

Bibliography

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018. Formalization of a Polymorphic
Subtyping Algorithm. In ITP (Lecture Notes in Computer Science, Vol. 10895). Springer, 604–
622. [cited on page 12]
Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. A Mechanical Formalization ofHigher-Ranked Polymorphic Type Inference. Proc. ACM Program. Lang. 3, ICFP, Article 112(July 2019), 29 pages. https://doi.org/10.1145/3341716 [cited on page 12]120