Types and Programming Languages

Description

A type system is a syntactic method for automatically checking the absence of certain erroneous behaviors by classifying program phrases according to the kinds of values they compute. The study of type systems--and of programming languages from a type-theoretic perspective -- -has important applications in software engineering, language design, high-performance compilers, and security.This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Each chapter is accompanied by numerous exercises and solutions, as well as a running implementation, available via the Web. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material.The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators. Extended case studies develop a variety of approaches to modeling the features of object-oriented languages. Cover......Page 1 Title Page......Page 5 Contents......Page 7 Preface......Page 15 1.1 Types in Computer Science......Page 25 1.2 What Type Systems Are Good For......Page 28 1.3 Type Systems and Language Design......Page 33 1.4 Capsule History......Page 34 1.5 Related Reading......Page 36 2.1 Sets, Relations, and Functions......Page 39 2.2 Ordered Sets......Page 40 2.3 Sequences......Page 42 2.4 Induction......Page 43 2.5 Background Reading......Page 44 Part I: Untyped Systems......Page 45 3.1 Introduction......Page 47 3.2 Syntax......Page 50 3.3 Induction on Terms......Page 53 3.4 Semantic Styles......Page 56 3.5 Evaluation......Page 58 3.6 Notes......Page 67 4 An ML Implementation of Arithmetic Expressions......Page 69 4.1 Syntax......Page 70 4.2 Evaluation......Page 71 4.3 The Rest of the Story......Page 73 5 The Untyped Lambda-Calculus......Page 75 5.1 Basics......Page 76 5.2 Programming in the Lambda-Calculus......Page 82 5.3 Formalities......Page 92 5.4 Notes......Page 97 6 Nameless Representation of Terms......Page 99 6.1 Terms and Contexts......Page 100 6.2 Shifting and Substitution......Page 102 6.3 Evaluation......Page 104 7.1 Terms and Contexts......Page 107 7.2 Shifting and Substitution......Page 109 7.3 Evaluation......Page 111 7.4 Notes......Page 112 Part II: Simple Types......Page 113 8.1 Types......Page 115 8.2 The Typing Relation......Page 116 8.3 Safety = Progress + Preservation......Page 119 9.1 Function Types......Page 123 9.2 The Typing Relation......Page 124 9.3 Properties of Typing......Page 128 9.4 The Curry-Howard Correspondence......Page 132 9.5 Erasure and Typability......Page 133 9.7 Notes......Page 135 10.1 Contexts......Page 137 10.3 Typechecking......Page 139 11.1 Base Types......Page 141 11.2 The Unit Type......Page 142 11.3 Derived Forms: Sequencing and Wildcards......Page 143 11.4 Ascription......Page 145 11.5 Let Bindings......Page 148 11.6 Pairs......Page 150 11.7 Tuples......Page 152 11.8 Records......Page 153 11.9 Sums......Page 156 11.10 Variants......Page 160 11.11 General Recursion......Page 166 11.12 Lists......Page 170 12.1 Normalization for Simple Types......Page 173 12.2 Notes......Page 176 13.1 Introduction......Page 177 13.3 Evaluation......Page 183 13.4 Store Typings......Page 186 13.5 Safety......Page 189 13.6 Notes......Page 194 14 Exceptions......Page 195 14.1 Raising Exceptions......Page 196 14.2 Handling Exceptions......Page 197 14.3 Exceptions Carrying Values......Page 199 Part III: Subtyping......Page 203 15.1 Subsumption......Page 205 15.2 The Subtype Relation......Page 206 15.3 Properties of Subtyping and Typing......Page 212 15.4 The Top and Bottom Types......Page 215 15.5 Subtyping and Other Features......Page 217 15.6 Coercion Semantics for Subtyping......Page 224 15.7 Intersection and Union Types......Page 230 15.8 Notes......Page 231 16 Metatheory of Subtyping......Page 233 16.1 Algorithmic Subtyping......Page 234 16.2 Algorithmic Typing......Page 237 16.3 Joins and Meets......Page 242 16.4 Algorithmic Typing and the Bottom Type......Page 244 17.2 Subtyping......Page 245 17.3 Typing......Page 246 18.1 What Is Object-Oriented Programming?......Page 249 18.2 Objects......Page 252 18.4 Subtyping......Page 253 18.5 Grouping Instance Variables......Page 254 18.6 Simple Classes......Page 255 18.7 Adding Instance Variables......Page 257 18.9 Classes with Self......Page 258 18.10 Open Recursion through Self......Page 259 18.11 Open Recursion and Evaluation Order......Page 261 18.12 A More Efficient Implementation......Page 265 18.13 Recap......Page 268 18.14 Notes......Page 269 19.1 Introduction......Page 271 19.2 Overview......Page 273 19.3 Nominal and Structural Type Systems......Page 275 19.4 Definitions......Page 278 19.5 Properties......Page 285 19.6 Encodings vs. Primitive Objects......Page 286 19.7 Notes......Page 287 Part IV: Recursive Types......Page 289 20 Recursive Types......Page 291 20.1 Examples......Page 292 20.2 Formalities......Page 299 20.4 Notes......Page 303 21 Metatheory of Recursive Types......Page 305 21.1 Induction and Coinduction......Page 306 21.2 Finite and Infinite Types......Page 308 21.3 Subtyping......Page 310 21.4 A Digression on Transitivity......Page 312 21.5 Membership Checking......Page 314 21.6 More Efficient Algorithms......Page 319 21.7 Regular Trees......Page 322 21.8 μ-Types......Page 323 21.9 Counting Subexpressions......Page 328 21.10 Digression: An Exponential Algorithm......Page 333 21.11 Subtyping Iso-Recursive Types......Page 335 21.12 Notes......Page 336 Part V: Polymorphism......Page 339 22.1 Type Variables and Substitutions......Page 341 22.2 Two Views of Type Variables......Page 343 22.3 Constraint-Based Typing......Page 345 22.4 Unification......Page 350 22.5 Principal Types......Page 353 22.6 Implicit Type Annotations......Page 354 22.7 Let-Polymorphism......Page 355 22.8 Notes......Page 360 23.1 Motivation......Page 363 23.2 Varieties of Polymorphism......Page 364 23.3 System F......Page 365 23.4 Examples......Page 368 23.5 Basic Properties......Page 377 23.6 Erasure, Typability, and Type Reconstruction......Page 378 23.7 Erasure and Evaluation Order......Page 381 23.8 Fragments of System F......Page 382 23.9 Parametricity......Page 383 23.10 Impredicativity......Page 384 23.11 Notes......Page 385 24.1 Motivation......Page 387 24.2 Data Abstraction with Existentials......Page 392 24.3 Encoding Existentials......Page 401 24.4 Notes......Page 403 25.1 Nameless Representation of Types......Page 405 25.2 Type Shifting and Substitution......Page 406 25.3 Terms......Page 407 25.4 Evaluation......Page 409 25.5 Typing......Page 410 26.1 Motivation......Page 413 26.2 Definitions......Page 415 26.3 Examples......Page 420 26.4 Safety......Page 424 26.5 Bounded Existential Types......Page 430 26.6 Notes......Page 432 27 Case Study: Imperative Objects, Redux......Page 435 28.1 Exposure......Page 441 28.2 Minimal Typing......Page 442 28.3 Subtyping in Kernel F_{