Formalized Higher-Ranked Polymorphic Type Inference Algorithms
by
Jinxu Zhao
( )
A thesis submitted in partial fulfillment of the requirements for the 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 byJinxu Zhaofor the degree of Doctor of Philosophyat The University of Hong Kongin July 2021
Modern functional programming languages, such as Haskell or OCaml, use sophisticated forms of type inference. In the meantime, more and more object-oriented programming languages implement advanced type inference algorithms, which greatly reduces the number of redundant and uninteresting 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 reuse and 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 a novel 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 2021
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 projects of 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 feel
desperate, the time spent with you is always delightful and encouraging. Life would be much harder without you.
Contents
Declaration
ACKNOWLEDgMENTS ..... II
List of Figures ..... VIII
LIST OF TABLES
I Prologue
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. . ..... 10
2 BaCKground ..... 13
2.1 Hindley-Milner Type System ..... 13
2.1.1 Declarative System ..... 13
2.1.2 Algorithmic System and Principality ..... 15
2.2 Odersky-Läufer Type System ..... 16
2.2.1 Higher-Ranked Types ..... 17
2.2.2 Declarative System ..... 17
2.2.3 Relating to ..... 20
2.3 Dunfield-Krishnaswami Bidirectional Type System ..... 20
2.3.1 Declarative System ..... 21
2.4 MLsub ..... 23
2.4.1 Types and Polar Types ..... 23
2.4.2 Biunification ..... 25
II Higher-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
3.2 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
3.3 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
3.4 The Choice of Abella ..... 38
3.4.1 Statistics and Discussion ..... 41
4 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
4.2 Algorithmic System ..... 52
4.2.1 Syntax and Well-Formedness ..... 52
4.2.2 Algorithmic System ..... 54
4.3 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.3.5 Decidability ..... 67
4.3.6 Abella and Proof Statistics ..... 70
4.4 Discussion ..... 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
5 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
5.4 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
5.5 Discussion ..... 95
5.5.1 A Complete Algorithm Under Monotype Guessing Restrictions ..... 95
5.5.2 Lazy Substitution and Non-terminating Loops . ..... 96
III Related Work ..... 99
6 Related Work ..... 100
6.1 Higher-Ranked Polymorphic Type Inference Algorithms ..... 100
6.1.1 Predicative Algorithms ..... 100
6.1.2 Impredicative Algorithms ..... 101
6.2 Type Inference Algorithms with Subtyping ..... 103
6.3 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
6.4 Mechanical Formalization of Polymorphic Type Systems ..... 105
IV Epilogue ..... 106
7 Conclusion and Future Work ..... 107
7.1 Conclusion ..... 107
7.2 Future Work ..... 108
BIBLIOGRAPHY ..... 112
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
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
PARt I
Prologue
1 krrowecrox
1.1 Type Systems and Type Inference Algorithms
Statically typed programming languages are widely used nowadays. Programs are categorized by various types before they are compiled and executed. Type errors caught before execution usually indicate 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 is
Similarly, the swap function for a float array can be defined as
which mostly shares the same body with the above definition for integer array, except that the type of element in the array changes from int to float. If such functionality is a commonly used 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:
where denotes a generic type that programmers may arbitrarily pick. The swap2_generic function 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)
However, the type parameter seems a bit redundant: given the type of arr is Double [], the generic variable 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 write by mistake, like "3" / 3; or even well-typed programs with ambiguous/unexpected meaning like "3" + (for someone who is not familiar with the conventions, she might think this evaluates to " 39 "). Or even more commonly seen in practice, an accidentally misspelled variable name does not cause a runtime error until the line of code is actually executed. Type systems are designed to prevent such problems from happening, therefore statically-typed languages ensure type-safety, or "well-typed programs cannot go wrong". Type inference algorithms that come along with modern type systems help eliminate trivial or redundant parts of programs to improve the conciseness.
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, the system 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 [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 can be encoded in System F:
To enjoy the polymorphism of such a function, one needs to first supply a type argument like id @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 compared with 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 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,
And we typically use the function without specifying the type parameters, because the type system already supports implicit parametric polymorphism:
int ;
String ;
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
and Urzyczyn 1996]. For example, the following expression is ambiguous when the implicit type argument is not given:
It is unclear how the type variable is instantiated during the polymorphic application: one possibility is that is chosen to be the type of id, or , resulting in the type (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 restricted version of System F). However, another valid type is , which is obtained by first instantiating id with a fresh type variable , and generalizing the type after calculating the type 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 is impossible motivates people to discover restrictions on the type system under which type inference algorithms are capable of guessing 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, where polymorphic types can only have universal quantifiers in the top level. For example, is allowed, but not . The type system of many programming languages like Java adopts the idea from , where generics is a syntax to express polymorphic types in HM: all the generic variables must be declared at the top level before the function 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 function
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 . In order to use the
function as the types mentioned above, a more-general-than relation is used to describe that the polymorphic type can be instantiated to more concrete types:
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 as predicative. 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 type systems 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 to type 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:
The type is rank-2 because of the inner quantifier in the argument position of the type. Such a type 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 by allowing higher-ranked types, but instantiations are still limited to monotypes, thus the system remains predicative.
1 Introduction
1.1.4 Bidirectional Typing
In order to improve the expressiveness for higher-ranked systems, some type annotations are necessary 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,
the type of hpoly is (Int, Char), which is a rank-2 type and is not typeable in HM. Notably (and unlike Hindley-Milner) the lambda argument 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 used in the first argument of the function.
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: type checking, 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 both and are inputs: i.e. we check whether expression has some type . In the synthesis mode only is an input: we need to calculate the output type from the input expression . 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 for the 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 , where the function type and argument expression are input, and type is the output representing the result type of the
function application . Note that does not appear in this relation, and one can tell the procedure for type checking application expressions from the shape of the judgment - firstly, the type of the function is inferred to ; then the application inference judgment is reduced to a checking judgment to verify if the argument checks against the argument part of ; finally, output the return part of . Formally, the rules implement the procedure we described above:
The use of application inference judgment avoids implicit instantiations of types like HM, instead, when the function type is a polymorphic type, it is explicitly instantiated by the application inference until it becomes a function type:
As 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 the degree 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 the minimal support for subtyping.
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 in theorem provers. The remarkable exception is work done on the formalization of certain parts of 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 no formalization 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 their correctness 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 logical relations [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, and error-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 found problems 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, a natural solution for these problems. Theorem provers can automatically check and validate the proofs, 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 is often quite delicate. Studying the meta-theory for such extensions would be greatly aided by the existence of a mechanical formalization of the base language, which could then be reused and extended 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 that are invalidated after extensions.
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 to deal with these complex forms of binding in theorem provers. We believe that this is the primary reason 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 the nominal 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 type checking rule
is encoded as
check E(all A) := nablaa, check a)
in Abella, where the quantifier introduces a fresh type variable and later use it to "open" the body of . .
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 the first to formalize the meta-theoretical results of a polymorphic higher-ranked subtyping algorithm.
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 a single 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 and judgments. This enables precise scope tracking of variables in judgments and avoids the duplication of context information across judgments in worklists. Similar to the previous algorithm, partial solutions are propagated across judgments in a single list consist of both variable bindings and judgments. Nevertheless, the unification of worklists and contexts exploits the fact that judgments are usually sharing a large part of common information. And one can easily tell when a variable is no longer referred to.
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 and mechanically proven.
A new backtracking-based worklist algorithm is presented and proven to be sound with 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 for the non-deterministic trial without missing any of them.
We also formalize the rank-1 restriction of subtyping relation, and proved that our algorithmic 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:
In this chapter, we introduce some highly related type systems. They are basic concepts and should 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 system that 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 that further 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 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 , or a function type .
Expressions includes variables , literals (), lambda abstractions . , applications and the let expression let in . A context is a collection of type bindings for variables.
Type variables
Figure 2.1: HM Syntax
HM Type Instantiation
HM Typing
Figure 2.2: HM Type System
Type Instantiation The relations between types are described via type instantiations. The rule shown to the top of Figure 2.2 checks if . is a generic instance of . . This relation is valid when for a series of mono-types and each variable in is not free in .
For example,
is obtained by the substitution , and
substitutes by , and generalizes after the substitution.
2 Background
TypIng The typing relation synthesizes a type for an expression under the context . Rule HM-Var looks up the binding of a variable in the context. Rule HM-Unit always gives the unit type 1 to the unit expression (). For a lambda abstraction , Rule HM-Abs guesses its input type and computes the type of its body as the return type. Rule HM-App eliminates a function type by an application , where the argument type must be the same as the input type of the function, and the type of the whole application is .
Rule HM-Let is also referred to as let-polymorphism. In (untyped) lambda calculus, let in behaves the same as . However, the HM let rule derives the type of first, and binds the polymorphic type into the context before . 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 . 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 that any expression (function) that has a polymorphic type can be automatically instantiated with a proper 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 this thesis, 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 can be obtained by replacing Rules HM-Var and HM-Let by the following rules:
A generalization on , the synthesized type of , 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 . The following property shows that the new system is (almost) equivalent to the original declarative system.
2 Background
Theorem 2.1 (Equivalence of Syntax-Directed System).
If then
If then , and . , where .
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 , then computes principal type scheme , i.e.
.
Note that both the above theorems are not formalized by the author. The reader may refer to an 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 of rank-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 check and 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
This is not typeable in HM, because the argument of the lambda abstraction, , is applied to both 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,
2 Background
The solution is also natural: if the programmer may pick the type of argument she wants, the type system can figure out the rest. By adding type annotation on , OL now accepts the definition
and infers type (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,
The following example illustrates what rank a type belongs to:
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 and (argument) annotated lambda functions . Annotations on expressions help guide the type system properly, acting as a machine-
2 Background
Figure 2.3: Syntax of Odersky-Läufer System
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 a polymorphic 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 can always be instantiated to match any instantiation of , then is "at least as polymorphic as" . We also say that is "more polymorphic than" and write . 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 is a subtype of in the context , where is fresh in , then . Intuitively, if is more general than (where the universal quantifier already indicates that . is a general type), then must instantiate to for every .
The most interesting rule is OL-SUB- . If some instantiation of , is a subtype of , then . . The monotype we used to instantiate is guessed in this declarative rule,
2 Background
Figure 2.5: Subtyping of the Odersky-Läufer System