TypesandProgrammingLanguages

Types and Programming LanguagesTypes and programming LanguagesBenjamin C. pierceThe Mit PressCambridge, massachusettsLondon, englandC2002 Benjamin C. PierceAll rights reserved. No part of this book may be reproduced in any form byany electronic of mechanical means (including photocopying, recording, orinformation storage and retrieval)without permission in writing from thepublisherThis book was set in Lucida bright by the author using the LATEX documentpreparation systemPrinted and bound in the united states of americaLibrary of Congress Cataloging-in-Publication DataPierce, benjamin cTypes and programming languages/Benjamin C. Piercep. CmIncludes bibliographical references and indexisBn 0-262-16209-1(hC: alk. paper1. Programming languages(Electronic computers). I. TitleQA76.7P542002005.13-dc212001044428ContentsPreface1 Introductie1. 1 Types in Computer science1. 2 What Type systems Are Good For 43 Type Systems and language design1. 4 Capsule histo101.5 Related Reading2 Mathematical preliminaries152.1 Sets, Relations, and functions 152.2 Ordered sets 162.3 Sequences 182.4 Induction 192.5 Background reading 20Untyped Systems 213 Untyped Arithmetic Expressions 233.1 Introduction 233.2 Syntax 263.3 Induction on terms 293.4 Semantic Styles 323.5 Evaluation 343.6 Notes 43Contents4 An ML Implementation of Arithmetic Expressions 454.1 Syntax 464.2 Evaluation 474.3 The rest of the Story 495 The Untyped lambda-Calculus515.1 Basics525.2 Programming in the Lambda-Calculus 585.3 Formalities 685. 4 Notes 736 Nameless Representation of Terms 756.1 Terms and Contexts 766.2 Shifting and Substitution6.3 Evaluation 807 An ML Implementation of the Lambda-Calculus 837.1 Terms and contexts 837. 2 Shifting and substitution 857.3 Evaluatio877. 4 Note88Simple Types 898 Typed Arithmetic Expressions 918.1 Types 98.2 The Typing relation 928.3 Safety= Progress Preservation 959 Simply Typed lambda-Calculus 999.1 Function Types9.2 The Typing Relation 1009.3 Properties of Typing 1049. 4 The curry-Howard Correspondence 1089.5 Erasure and Typability 1099.6 Curry-Style vs Church-Style 1119.7 Notes 11110 An ML Implementation of Simple Types 11310.1CO10.2 Terms and Types 11510.3 Typechecking 115Contents11 Simple extensions 117IlI Base Types 1111.2 The Unit Type 11811.3 Derived Forms: Sequencing and wildcards 11911.4 Ascription 12111.5 Let Bindings 12411.6Pais12611.7 Tuples 12811. 8 Records 12911.9Sums13211.10 Variants 13611.11 General recursion 14211.12 Lists14612 Normalization 14912.1 Normalization for Simple types 14912.2 Notes 15213 References 15313.1 Introduction 15313.2 Typing 15913.3 Evaluation 15913.4 Store Typings 16213.5 Safet16513.6 Notes 17014 Exceptions17114.1 Raising Exceptions 17214.2 Handling Exceptions 17314.3 Exceptions Carrying Values 175IlI Subtyping 1795 Subtyping 18115.1 Subsumption 18115.2 The Subtype relatio18215.3 Properties of Subtyping and Typing 18815.4 The Top and bottom Types 19115.5 Subtyping and other Features 19315.6 Coercion Semantics for Subtyping 20015.7 Intersection and Union Types 20615. 8 Notes 207Contents16 Metatheory of subtyping 20916.1 Algorithmic Subtyping 21016.2 Algorithmic Typing 21316.3 Joins and meets 21816.4 Algorithmic Typing and the bottom Type 22017 An ML Implementation of Subtyping 22117.1 Syntax 22117.2 Subtyping 22117.3 Typing 22218 Case Study: Imperative Objects 22518.1 What Is object-Oriented Programming? 22518.2 Objects 22 818.3 Object Generators 22918.4 Subtyping 22918.5 Grouping Instance variables 23018.6 Simple classes 23118.7 Adding instance Variables 23318.8 Calling Superclass Methods 23418.9 Classes with Self 23418.10 Open Recursion through Self 23518.11 Open Recursion and Evaluation Order 23718.12 A More Efficient Implementation 24118.13R24418.14 Notes24519 Case Study: Featherweight Java 24719.1 Introduct24719.2 Overview 24919.3 Nominal and Structural Type systems 25119.4 Definitions 25419.5 Properties 26119.6 Encodings vS Primitive objects 26219.7 Notes 263ContentsN Recursive Types 26520 Recursive types26720.1 Examples 26820.2 Formali27520.3 Subtyping27920.4 Notes 27921 Metatheory of Recursive Types 28121.1 Induction and coinduction 28221.2 Finite and Infinite Types 28421.3 Subtyping 28621.4 A Digression on Transitivity 28821.5 Membership Checking 29021.6 More Efficient Algorithms 29521.7 Regular trees 298218μ- Types29921.9 Counting Subexpressions 30421.10 Digression: An Exponential Algorithm 30921.11 Subtyping Iso-Recursive Types 31121.12 Notes312v Polymorphism 31522 Type Reconstruction 31722.1 Type Variables and Substitutions 31722.2 Two Views of Type variables 31922.3 Constraint-Based Typing 32122.4 Unification 32622.5 Principal Types 32922.6 Implicit Type Annotations 33022.7 Let-Polymorphism33122. 8 Notes 33623 Universal Types 33923.1 Motivation 33923.2 Varieties of polymorphism 34023.3 System F 34123.4 Examples 34423.5 Basic Properties 35323.6 Erasure, Typability, and Type reconstruction 354Contents23.7 Erasure and Evaluation Order 35723.8 Fragments of System F 35823.9 Parametricity 3523.10 Impredicativity 36023.11 Notes36124 Existential Types36324.1 Motivation 36324.2 Data abstraction with existentials 36824.3 Encoding Existentials 37724.4 Not37925 An ML Implementation of System F 38125.1 Nameless representation of Types 38125.2 Type Shifting and Substitution 38225.3 Terms 38325.4 Evaluation 38525.5 Typing 38626 Bounded Quantification 38926.1 Motivation 38926.2 Definitions 39126.3 Examples 39626.4 Safe26.5 Bounded Existential Types 40626.6 Notes40827 Case Study: Imperative Objects, Redux 41128 Metatheory of bounded Quantification 41728.1 Exposure 41728.2 Minimal Typing 41828.3 Subtyping in Kernel F<: 42128.4 Subtyping in Full Fs: 42428.5 Undecidability of Full F42728.6 Joins and meets 43228.7 Bounded existentials 43528.8 Bounded Quantification and the Bottom Type 436