Qualified Types: Theory and Practice (Distinguished Dissertations in Computer Science (No. 9))

✍ Scribed by Mark P. Jones

• Publisher: Cambridge University Press
• Year: 2003
• Tongue: English
• Leaves: 170
• Series: Distinguished Dissertations in Computer Science (No. 9)
• Category: Library

✦ Synopsis

This book describes the use of qualified types to provide a general framework for the combination of polymorphism and overloading. For example, qualified types can be viewed as a generalization of type classes in the functional language Haskell and the theorem prover Isabelle. These in turn are extensions of equality types in Standard ML. Other applications of qualified types include extensible records and subtyping. Using a general formulation of qualified types, the author extends the Damas/Milner type inference algorithm to support qualified types, which in turn specifies the set of all possible types for any term. In addition, he describes a new technique for establishing suitable coherence conditions that guarantee the same semantics for all possible translations of a given term. Practical issues that arise in concrete implementations are also discussed, concentrating in particular on the implementation of overloading in Haskell and Gofer, a small functional programming system developed by the author.

✦ Table of Contents

Cover......Page 1
Frontmatter......Page 2
Contents......Page 6
Summary of notation......Page 10
Acknowledgements......Page 13
1.1 Type systems for programming languages......Page 14
1.2 Type inference and polymorphism......Page 15
1.3 The choice between all' andone'......Page 16
1.5 Outline of thesis......Page 17
2.1 Basic definitions......Page 19
2.2 Type classes......Page 21
2.3 Subtyping......Page 24
2.4 Extensible records......Page 26
3 - Type inference for qualified types......Page 29
3.1 An extension of ML with qualified types......Page 30
3.2 Understanding type schemes......Page 31
3.3 A syntax-directed approach......Page 36
3.4 Type inference......Page 38
3.5 Related work......Page 42
4 - Evidence......Page 44
4.1 Simple implementations of overloading......Page 45
4.2 Overloading made explicit......Page 46
4.3 Predicate entailment with evidence......Page 48
4.4 Evidence, predicates and implementations......Page 49
4.5 Type classes and dictionaries......Page 50
4.6 Subtyping and coercion......Page 52
4.7 Implementation of extensible records......Page 53
5 - Semantics and coherence......Page 56
5.1 A version of polymorphic [GREEK SMALL LETTER LAMDA]-calculus with qualified types......Page 57
5.2 Translation from OML to OP......Page 59
5.3 The coherence problem......Page 61
5.4 A definition of equality for OP terms......Page 62
5.5 Ordering and conversion functions......Page 66
5.6 Syntax-directed translation......Page 71
5.7 Type inference and translation......Page 73
5.8 Coherence results......Page 75
5.9 Comparison with related work......Page 78
6.1 Evidence parameters considered harmful......Page 80
6.2 Satisfiability......Page 86
6.3 Incorporating the rule of subsumption......Page 89
7 - Type classes in Haskell......Page 91
7.1 Context reduction......Page 92
7.2 Implementation of type classes in HTC......Page 95
7.3 The problem of repeated construction......Page 97
7.4 Repeated construction caused by recursion......Page 98
7.5 Other opportunities for shared dictionaries......Page 105
7.6 Alternative implementations of dictionary construction......Page 112
8.1 The basic principles of GTC......Page 114
8.2 The Gofer implementation of dictionaries......Page 117
8.3 A concrete implementation......Page 121
9 - Summary and future work......Page 127
9.1 Towards a categorical semantics......Page 128
9.2 Constructor classes......Page 129
9.3 Reasoning in the presence of overloading......Page 131
10.1 Constructor classes......Page 134
10.2 Template based implementations......Page 135
10.3 Making use of satisfiability......Page 136
10.5 The use of subsumption......Page 137
Appendix A - Proofs......Page 139
References......Page 161
Index......Page 168