Formalized Higher-Ranked Polymorphic Type Inference Algorithms
by
( )
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"
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.
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.
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
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
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
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
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
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
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
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
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
However, the type parameter seems a bit redundant: given the type of arr is Double [], the generic variable
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" +
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
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
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:
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
The fact that implicit parametric algorithm for full System
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,
For example, the following function
can be assigned to types Int
function as the types mentioned above, a more-general-than relation
function as the types mentioned above, a more-general-than relation
Predicativity In the HM system,
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
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
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
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
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
function application
function application
The use of application inference judgment avoids implicit instantiations of types like HM, instead, when the 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
is encoded as
check E(all A) := nablaa, check
in Abella, where the
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:
2
BACKGROUND
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
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
Expressions
Type variables
Figure 2.1: HM Syntax
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
For example,
is obtained by the substitution
substitutes
2 Background
TypIng The typing relation
Rule HM-Let is also referred to as let-polymorphism. In (untyped) lambda calculus, let
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
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
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
-
-
.
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
For example, consider the following function definition
This is not typeable in HM, because the argument of the lambda abstraction,
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
and infers type
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
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
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
Subtyping rules OL-SUB-Var, OL-SUB-Unit handle simple cases that do not involve universal quantifiers. Rule OL-SUB-
The most interesting rule is OL-SUB-
2 Background
Figure 2.5: Subtyping of the Odersky-Läufer System
Figure 2.6: Typing of the Odersky-Läufer System
but the algorithmic system does not guess and defers the instantiation until it can determine the monotype deterministically. The fact that
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-
TypIng The type system of Odersky-Läufer, shown in Figure 2.6, extends HM’s type system in the following aspects.
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 and let-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
The 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, and let-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,
2 Background
| Type variables |
|
||
| Types |
|
|
|
| Monotypes |
|
|
|
| Expressions |
|
|
|
| Contexts |
|
|
|
Figure 2.7: Syntax of Declarative System
is typeable in higher-ranked bidirectional systems, as the outer type annotation may act as if both the argument type and return type of the lambda is given. The Dunfield-Krishnaswami type system [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 and leave 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 shown in Figure 2.7. A declarative type
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
Declarative Typing The bidirectional type system, shown in Figure 2.9, has three judgments. The checking judgment
Many rules are standard. Rule DeclVar looks up term variables in the context. Rules Decl1I and Decl1I
2 Background
Figure 2.8: Declarative Well-formedness and Subtyping
expression
Application
2 Background
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 an algorithm. 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
2 Background
| Types |
|
|
|
| Positive Types |
|
|
|
| Negative Types |
|
|
|
Figure 2.10: Types of MLsub
distributive lattice can be defined via a set of equivalence classes of
The partial order
Type schemes are not defined as the usual
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
An important consequence is that all the constraints are of the form
2 Background
Interestingly, the polar subtyping judgments avoids difficult judgments like
2.4.2 BIUNIFICATION
Type inference for MLsub, similar to that for ML, is mainly a unification algorithm. However, in presence of subtyping, equality-based unification loses information about subtyping constraints.
For the atomic constraint
Luckily, lattices in MLsub helps express subtyping constraints on types directly. The constraint
In presence of polar types, the biunification algorithm of MLsub produces a bisubstitution
For example, the choose function is typed
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 the size 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.
PART II
Higher-Ranked Type Inference Algorithms
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 in formalization, 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 work is 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 our approach 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
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, represented
3 Higher-Ranked Polymorphism Subtyping Algorithm
Type variables
| Types |
|
|
|
| Monotypes |
|
|
|
| Contexts |
|
|
|
Figure 3.1: Syntax of Declarative System
Figure 3.2: Well-formedness of Declarative Types and Declarative Subtyping
by
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
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 another simpler algorithm by DK and present ours afterwards.
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 notable difference to the declarative judgment is the presence of a so-called output context
Output contexts are useful to transfer information across judgments in Dunfield and Krishnaswami's approach. For example, the algorithmic rule corresponding to
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
Dunfield and Krishnaswami introduce an existential variable-denoted with
The first step applies Rule
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 becomes a base case, and Rule
Dunfield and Krishnaswami's algorithmic specification is elegant and contains several useful ideas for a mechanical formalization of polymorphic subtyping. For example, ordered contexts and existential variables enable a purely inductive formulation of polymorphic subtyping. However, the binding/scoping structure of their algorithmic judgment is still fairly complicated and poses 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 the idea of solving those variables, but drop output contexts. Instead, our algorithmic rule has the form:
where
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:
The derivation of the previous example with the worklist approach is:
3 Higher-Ranked Polymorphism Subtyping Algorithm
To derive
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 and algorithmic systems.
3.2 A Worklist Algorithm for Polymorphic Subtyping
This section presents our algorithm for polymorphic subtyping. A novel aspect of our algorithm is the 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
WORKLIST JUDGMENTS The form of our algorithmic judgments is non-standard. Our algorithm keeps track of an explicit list of outstanding work: the list
Hole Notation To facilitate context manipulation, we use the syntax
3 Higher-Ranked Polymorphism Subtyping Algorithm
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
Firstly, we have five rules that are similar to those in the declarative system, mostly just adapted to the worklist style. For instance, Rule
Secondly, Rules
Figure 3.4: Algorithmic Subtyping
choose to instantiate
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 by strengthening and weakening lemmas of both systems, where most of them are straightforward to prove, except for the strengthening lemma of the declarative system, which is a little trickier.
Figure 3.5: A Success Derivation for the Algorithmic Subtyping Relation
Figure 3.6: A Failing Derivation for the Algorithmic Subtyping Relation
EXAmple We illustrate the subtyping rules through a sample derivation in Figure 3.5, which shows that that
In step 1, we have only one judgment, and that one has a top-level
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
A Failing Derivation We illustrate the role of ordered contexts through another example:
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 of contexts
The following two lemmas generalize Rule
Lemma 3.1 (Insert). If
Lemma 3.2 (Extract). If
3 Higher-Ranked Polymorphism Subtyping Algorithm
Figure 3.7: Transfer Rules
In order to match the shape of algorithmic subtyping relation for the following proofs, we define a relation
Definition 1 (Declarative Subtyping Worklist).
3.3.2 SOUNDNESS
Our algorithm is sound with respect to the declarative specification. For any derivation of a list of algorithmic judgments
Theorem 3.3 (Soundness). If
The proof proceeds by induction on the derivation of
3.3.3 Completeness
Completeness of the algorithm means that any declarative derivation has an algorithmic counterpart.
Theorem 3.4 (Completeness). If
3 Higher-Ranked Polymorphism Subtyping Algorithm
The proof proceeds by induction on the derivation of
Lemma 3.5 (Prune Transfer for Instantiation). If
A similar lemma holds for the symmetric case
3.3.4 Decidability
The third key result for our algorithm is decidability.
Theorem 3.6 (Decidability). Given any well-formed judgment list
We have proven this theorem by means of a lexicographic group of induction measurements
Definition 2 (Worklist Measures).
3 Higher-Ranked Polymorphism Subtyping Algorithm
The context measure
Definition 3 (Context Measure).
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
Definition
These instantiation judgments are these ones consumed and produced by Rules
Lemma 3.7 (Instantiation Decidability). For any context
-
, s.t. , it is decidable whether . -
, s.t. and , it is decidable whether .
In other words, for any instantiation judgment prefix
In summary, the decidability theorem can be shown through a lexicographic group of induction measurements
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 expressed
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
Encoding of the Declarative System As a concrete example, our declarative context (wellformedness relation) and well-formedness rules are encoded as follows.
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 (::) :
Note that in Abella, the symbol (:=) used in definitions is similar to the (:-) symbol in Pro
3 Higher-Ranked Polymorphism Subtyping Algorithm
| File(s) | SLOC | # of Theorems | Description |
| olist.thm, nat.thm | 303 | 55 | Basic data structures |
| higher.thm, order.thm | 164 | 15 | Declarative system |
| higher_alg.thm | 618 | 44 | Algorithmic system |
| trans.thm | 411 | 46 | Transfer |
| sound.thm | 166 | 2 | Soundness theorem |
| depth.thm | 143 | 12 | Definition of depth |
| complete.thm | 626 | 28 | Lemmas and Completeness theorem |
| decidable.thm | 1077 | 53 | Lemmas and Decidability theorem |
| Total | 3627 | 267 | (33 definitions in total) |
Figure 3.8: Statistics for the proof scripts
member (bound
Encoding of the Algorithmic System In terms of the algorithmic system, notably, Abella handles the
In this piece of code, we use Exp to denote the worklist
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 tactics
4
A Type-Inference Algorithm for Higher-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 is adopted in practice by a few real implementations of functional languages, including PureScript and Unison. The DK type system has two variants: a declarative and an algorithmic one. The two variants 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 system using 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 and lemmas 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 not invalidate 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 our own work. We expect that for most non-trivial manual proofs similar problems exist, so this should not be understood as a sign of sloppiness on their part. Instead, it should be an indicator that reinforces the arguments for mechanical formalizations: manual formalizations are errorprone due to the multiple tedious details involved in them. There are several other examples of manual formalizations that were found to have similar problems. For example, Klein et al.
4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
[2012] mechanized formalizations in Redex for nine ICFP 2009 papers and all were found to have 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 the complex 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 a theorem 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 for polymorphic 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 type system. 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 to enable the transfer of inferred information across judgments. A further refinement to the idea of 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 in judgments. Furthermore it avoids the duplication of context information across judgments in worklists that occurs in other techniques [Abel and Pientka 2011; Reed 2009]. Despite the use of 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 judgment that unifies ordered contexts and the worklists themselves.
4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
| Type variables |
|
||
| Types |
|
|
|
| Monotypes |
|
|
|
| Expressions |
|
|
|
| Contexts |
|
|
|
Figure 4.1: Syntax of Declarative System (Extends Figure 3.1)
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 the rules 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
|
|
|
|
|
|
Figure 4.3: Declarative Typing
that more specific rules are always the best choices, i.e. DecI
For example,
but fails when applied to DeclSub:
Rule Decl
4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
judgments. For example,
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.
In addition to the regular (universally quantified) type variables
All algorithmic judgments thread an algorithmic context. They have the form
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:
The inference task yields an output context
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 existential
4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
variables. For this reason the DK algorithm uses scope markers
To indicate that the scope of
One may suggest that the marker
the algorithm introduces new existential variables right before
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 found several 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 to these lemmas.
More seriously, we have also found a lemma that simply does not hold: Lemma 29 (Parallel Admissibility
In what follows, we briefly discuss the problem through counterexamples. False lemmas are found 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
-
-
If
then . -
If
and and , then
We give a counter-example to this lemma:
Pick
- 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
-
-
If
then . -
If
and types and , then .
A similar counter-example is given:
Pick
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 is more 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 these accounts, in particular compared to traditional constraint-based type-inference algorithms like Algorithm
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, the instantiations 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 have mentioned above, the stack discipline of the ordered contexts does not mesh well with the use of 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 we give 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 find inspiration 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
Because the whole set is explicitly available, the variable
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 are
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
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 some problems in DK's algorithmic formulation by using a worklist-based judgment of the form
where
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
No Inference Judgments Secondly, and more importantly, the approach only deals with a judgment for checking whether one type is the subtype of another. While this may not be so difficult to adapt to the checking mode of term typing
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
For example, suppose that the top judgment of the following worklist checks the identity function against
To proceed, two auxiliary variables
which will be satisfied after several steps, and the worklist becomes
Since the variable declarations
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 variable scoping 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
4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
placeholder type variable
Take the following worklist as an example
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,
The algorithm first analyses the two subtyping judgments and will find the best solutions
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
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 is achieved 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 that arise 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 from the declarative system. It only introduces one additional feature. In order to find unknown types
Existential variables
Algorithmic types
Algorithmic judgment chain
Algorithmic worklist
wf
Figure 4.4: Extended Syntax and Well-Formedness for the Algorithmic System
4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
Judgment Chains Judgment chains
WorkList Judgments Our algorithm has a non-standard form. We combine traditional contexts and judgment(s) into a single sort, the worklist
Hole Notation We use the syntax
4.2.2 Algorithmic System
The algorithmic typing reduction rules, defined in Figure 4.5, have the form
when
when
Figure 4.5: Algorithmic Typing
In the case that
Please note that when a new variable is introduced in the right-hand side worklist
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.
- Algorithmic subtyping We have six subtyping rules (Rules 4-9) that are similar to their declarative counterparts. For instance, Rule 7 consumes a subtyping judgment and pushes two back to the worklist. Rule 8 differs from declarative Rule
L by introducing an existential variable instead of guessing the monotype instantiation. Each existential variable is later solved to a monotype with the same context, so the final solution of 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
Example Consider the derivation of the subtyping judgment
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
Now the existential variable
-
Existential decomposition. Rules 10 and 11 are algorithmic versions of Rule
; they both partially instantiate to function types. The domain and range of the new function type are not determined: they are fresh existential variables with the same scope as . We replace in the worklist with . To propagate the instantiation to the rest of the worklist and maintain wellformedness, every reference to is replaced by . The occurs-check condition prevents divergence as usual. For example, without it would diverge. -
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
can be solved with another existential variable only if occurs after .
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.
- Checking judgments. Rules
deal with checking judgments. Rule 18 is similar to DeclSub, but rewritten in the continuation-passing-style. The side conditions and prevent overlap with Rules 19, 20 and 21 ; this is further discussed at the end of this section. 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 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.
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 the metatheory 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
In comparison, DK's algorithmic subsumption rule has no restriction on the expression
- Inference judgments. Inference judgments behave differently compared with subtyping and checking 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
that affect the remaining judgment chain. This rule is carefully designed so that the output variables are bound by 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. When an inference judgment succeeds with type
Rule 25 infers the type of a lambda expression by introducing
4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
- 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 to the function type , just like Rules 10,11 and 21 .
ExAmple Figure 4.6 shows a sample derivation of the algorithm. It checks the application
After that, Rule 28 changes the application inference judgment to a check of the argument against the input type
In summary, our type checking algorithm accepts
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
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
These restrictions have not been imposed arbitrarily: we formally prove that the restricted algorithm 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.
Figure 4.6: A Sample Derivation for Algorithmic Typing
Declarative worklist
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
Figure 4.8: Declarative Transfer
Worklist instantiation. The relation
Observe that the instantiation
Lemmas 4.3 and 4.4 generalize Rule
Lemma 4.3 (Insert). If
Lemma 4.4 (Extract). If
Declarative transfer. Figure 4.8 defines a relation
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
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:
- Restrict the shape of
in the rule subtyping rule:
- Drop the redundant rule Decl1I, which can be easily derived by a combination of DeclSub, Decl1I
and Unit:
- Restrict the shapes of
and in the subsumption rule 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 with respect 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.
Figure 4.9: Context Subtyping
Modifications (1) and (3) require inversion lemmas for the rules that overlap. Firstly, Rule
Lemma 4.5 (Invertibility of
The lemma implies that preferring Rule
Secondly, Rule DeclSub overlaps with both Dec
Lemma 4.6 (Invertibility of DecI
Lemma 4.7 (Invertibility of Decl
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
Lemma 4.8 (Subsumption). Given
-
If
and then ; -
If
then there exists s.t. and ; -
If
and , then there exists s.t. and .
4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
This lemma expresses that any derivation in a context
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 description of 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 applications of 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
Proof. The proof is by a nested mutual induction on the lexicographical order of the measures
where the second measure simple give an natural number for each type of judgment: (1) checking judgments (
All but two cases can be finished easily following the declarative typing derivation, and the proof shares a similar structure to DK's. One tricky case related to Rule Decl
Another tricky case is Decl
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.
4 A Type-Inference Algorithm for Higher-Ranked Polymorphism
Three-Way Soundness and Completeness Theorems We now have three systems that can be related: DK's overlapping declarative system, our non-overlapping declarative system, and our algorithmic 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 completeness of 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
Theorem 4.9 (Soundness). If
The proof proceeds by induction on the derivation of
Corollary 4.10 (Soundness, single judgment form). Given wf
-
If
. then there exist s.t. and ; -
If
. then there exist