Practical Foundations for Programming Languages SECOND EDITION Robert Harper PRE Carnegie Mellon University
PREVIEW Practical Foundations for Programming Languages SECOND EDITION Robert Harper Carnegie Mellon University
Preface to the Second Edition Writing the second edition to a text book incurs the same risk as building the second version of a software system.It is difficult to make substantive improvements,while avoiding the temptation to overburden and undermine the foundation on which one is building.With the hope of avoiding the second system effect,I have sought to make corrections,revisions,expansions,and deletions that improve the coherence of the development,remove some topics that distract from the main themes,add new topics that were omitted from the first edition,and include exercises for almost every chapter. The revision removes a number of typographical errors,corrects a few material errors(espe- cially the formulation of the parallel abstract machine and of concurrency in Algol),and improves the writing throughout.Some chapters have been deleted(general pattern matching and polar- ization,restricted forms of polymorphism),some have been completely rewritten(the chapter on higher kinds),some have been substantially revised (general and parametric inductive defi- nitions,concurrent and distributed Algol),several have been reorganized(to better distinguish partial from total type theories),and a new chapter has been added(on type refinements).Titular attributions on several chapters have been removed,not to diminish credit,but to avoid confusion between the present and the original formulations of several topics.A new system of(pronounce- able!)language names has been introduced throughout.The exercises generally seek to expand on the ideas in the main text,and their solutions often involve significant technical ideas that merit study.Routine exercises of the kind one might include in a homework assignment are deliberately few. My purpose in writing this book is to establish a comprehensive framework for formulating and analyzing a broad range of ideas in programming languages.If language design and pro- gramming methodology are to advance from a trade-craft to a rigorous discipline,it is essential that we first get the definitions right.Then,and only then,can there be meaningful analysis and consolidation of ideas.My hope is that I have helped to build such a foundation. I am grateful to Stephen Brookes,Evan Cavallo,Karl Crary,Jon Sterling,James R.Wilcox,and Todd Wilson for their help in critiquing drafts of this edition and for their suggestions for revision. I thank my department head,Frank Pfenning,for his support of my work on the completion of this edition.Thanks also to my editors,Ada Brunstein and Lauren Cowles,for their guidance and assistance.And thanks to Evan Cavallo and Andrew Shulaev for corrections to the draft. Neither the author nor the publisher make any warranty,express or implied,that the defi- nitions,theorems,and proofs contained in this volume are free of error,or are consistent with
PREVIEW Preface to the Second Edition Writing the second edition to a text book incurs the same risk as building the second version of a software system. It is difficult to make substantive improvements, while avoiding the temptation to overburden and undermine the foundation on which one is building. With the hope of avoiding the second system effect, I have sought to make corrections, revisions, expansions, and deletions that improve the coherence of the development, remove some topics that distract from the main themes, add new topics that were omitted from the first edition, and include exercises for almost every chapter. The revision removes a number of typographical errors, corrects a few material errors (especially the formulation of the parallel abstract machine and of concurrency in Algol), and improves the writing throughout. Some chapters have been deleted (general pattern matching and polarization, restricted forms of polymorphism), some have been completely rewritten (the chapter on higher kinds), some have been substantially revised (general and parametric inductive definitions, concurrent and distributed Algol), several have been reorganized (to better distinguish partial from total type theories), and a new chapter has been added (on type refinements). Titular attributions on several chapters have been removed, not to diminish credit, but to avoid confusion between the present and the original formulations of several topics. A new system of (pronounceable!) language names has been introduced throughout. The exercises generally seek to expand on the ideas in the main text, and their solutions often involve significant technical ideas that merit study. Routine exercises of the kind one might include in a homework assignment are deliberately few. My purpose in writing this book is to establish a comprehensive framework for formulating and analyzing a broad range of ideas in programming languages. If language design and programming methodology are to advance from a trade-craft to a rigorous discipline, it is essential that we first get the definitions right. Then, and only then, can there be meaningful analysis and consolidation of ideas. My hope is that I have helped to build such a foundation. I am grateful to Stephen Brookes, Evan Cavallo, Karl Crary, Jon Sterling, James R. Wilcox, and Todd Wilson for their help in critiquing drafts of this edition and for their suggestions for revision. I thank my department head, Frank Pfenning, for his support of my work on the completion of this edition. Thanks also to my editors, Ada Brunstein and Lauren Cowles, for their guidance and assistance. And thanks to Evan Cavallo and Andrew Shulaev for corrections to the draft. Neither the author nor the publisher make any warranty, express or implied, that the definitions, theorems, and proofs contained in this volume are free of error, or are consistent with
any particular standard of merchantability,or that they will meet requirements for any particular application.They should not be relied on for solving a problem whose incorrect solution could result in injury to a person or loss of property.If you do use this material in such a manner,it is at your own risk.The author and publisher disclaim all liability for direct or consequential damage resulting from its use. Pittsburgh July,2015 PREVIE
PREVIEW any particular standard of merchantability, or that they will meet requirements for any particular application. They should not be relied on for solving a problem whose incorrect solution could result in injury to a person or loss of property. If you do use this material in such a manner, it is at your own risk. The author and publisher disclaim all liability for direct or consequential damage resulting from its use. Pittsburgh July, 2015
Preface to the first edition Types are the central organizing principle of the theory of programming languages.Language fea- tures are manifestations of type structure.The syntax of a language is governed by the constructs that define its types,and its semantics is determined by the interactions among those constructs. The soundness of a language design-the absence of ill-defined programs-follows naturally. The purpose of this book is to explain this remark.A variety of programming language features are analyzed in the unifying framework of type theory.A language feature is defined by its statics, the rules governing the use of the feature in a program,and its dynamics,the rules defining how programs using this feature are to be executed.The concept of safety emerges as the coherence of the statics and the dynamics of a language. In this way we establish a foundation for the study of programming languages.But why these particular methods?The main justification is provided by the book itself.The methods we use are both precise and intuitive,providing a uniform framework for explaining programming language concepts.Importantly,these methods scale to a wide range of programming language concepts, supporting rigorous analysis of their properties.Although it would require another book in itself to justify this assertion,these methods are also practical in that they are directly applicable to imple- mentation and uniquely effective as a basis for mechanized reasoning.No other framework offers as much Being a consolidation and distillation of decades of research,this book does not provide an exhaustive account of the history of the ideas that inform it.Suffice it to say that much of the de- velopment is not original,but rather is largely a reformulation of what has gone before.The notes at the end of each chapter signpost the major developments,but are not intended as a complete guide to the literature.For further information and alternative perspectives,the reader is referred to such excellent sources as Constable (1986),Constable(1998),Girard(1989),Martin-Lof(1984), Mitchell(1996),Pierce(2002,2004),and Reynolds(1998). The book is divided into parts that are,in the main,independent of one another.Parts I and II, however,provide the foundation for the rest of the book,and must therefore be considered prior to all other parts.On first reading it may be best to skim Part I,and begin in earnest with Part II, returning to Part I for clarification of the logical framework in which the rest of the book is cast. Numerous people have read and commented on earlier editions of this book,and have sug- gested corrections and improvements to it.I am particularly grateful to Umut Acar,Jesper Louis Andersen,Carlo Angiuli,Andrew Appel,Stephanie Balzer,Eric Bergstrom,Guy E.Blelloch,Il- iano Cervesato,Lin Chase,Karl Crary,Rowan Davies,Derek Dreyer,Dan Licata,Zhong Shao
PREVIEW Preface to the First Edition Types are the central organizing principle of the theory of programming languages. Language features are manifestations of type structure. The syntax of a language is governed by the constructs that define its types, and its semantics is determined by the interactions among those constructs. The soundness of a language design—the absence of ill-defined programs—follows naturally. The purpose of this book is to explain this remark. A variety of programming language features are analyzed in the unifying framework of type theory. A language feature is defined by its statics, the rules governing the use of the feature in a program, and its dynamics, the rules defining how programs using this feature are to be executed. The concept of safety emerges as the coherence of the statics and the dynamics of a language. In this way we establish a foundation for the study of programming languages. But why these particular methods? The main justification is provided by the book itself. The methods we use are both precise and intuitive, providing a uniform framework for explaining programming language concepts. Importantly, these methods scale to a wide range of programming language concepts, supporting rigorous analysis of their properties. Although it would require another book in itself to justify this assertion, these methods are also practical in that they are directly applicable to implementation and uniquely effective as a basis for mechanized reasoning. No other framework offers as much. Being a consolidation and distillation of decades of research, this book does not provide an exhaustive account of the history of the ideas that inform it. Suffice it to say that much of the development is not original, but rather is largely a reformulation of what has gone before. The notes at the end of each chapter signpost the major developments, but are not intended as a complete guide to the literature. For further information and alternative perspectives, the reader is referred to such excellent sources as Constable (1986), Constable (1998), Girard (1989), Martin-Lof¨ (1984), Mitchell (1996), Pierce (2002, 2004), and Reynolds (1998). The book is divided into parts that are, in the main, independent of one another. Parts I and II, however, provide the foundation for the rest of the book, and must therefore be considered prior to all other parts. On first reading it may be best to skim Part I, and begin in earnest with Part II, returning to Part I for clarification of the logical framework in which the rest of the book is cast. Numerous people have read and commented on earlier editions of this book, and have suggested corrections and improvements to it. I am particularly grateful to Umut Acar, Jesper Louis Andersen, Carlo Angiuli, Andrew Appel, Stephanie Balzer, Eric Bergstrom, Guy E. Blelloch, Iliano Cervesato, Lin Chase, Karl Crary, Rowan Davies, Derek Dreyer, Dan Licata, Zhong Shao
Rob Simmons,and Todd Wilson for their extensive efforts in reading and criticizing the book.I also thank the following people for their suggestions:Joseph Abrahamson,Arbob Ahmad,Zena Ariola,Eric Bergstrome,William Byrd,Alejandro Cabrera,Luis Caires,Luca Cardelli,Manuel Chakravarty,Richard C.Cobbe,James Cooper,Yi Dai,Daniel Dantas,Anupam Datta,Jake Don- ham,Bill Duff,Matthias Felleisen,Kathleen Fisher,Dan Friedman,Peter Gammie,Maia Gins- burg,Byron Hawkins,Kevin Hely,Kuen-Bang Hou(Favonia),Justin Hsu,Wojciech Jedynak,Cao Jing,Salil Joshi,Gabriele Keller,Scott Kilpatrick,Danielle Kramer,Dan Kreysa,Akiva Leffert, Ruy Ley-Wild,Karen Liu,Dave MacQueen,Chris Martens,Greg Morrisett,Stefan Muller,Tom Murphy,Aleksandar Nanevski,Georg Neis,David Neville,Adrian Trejo Nunez,Cyrus Omar, Doug Perkins,Frank Pfenning,Jean Pichon,Benjamin Pierce,Andrew M.Pitts,Gordon Plotkin, David Renshaw,John Reynolds,Andreas Rossberg,Carter Schonwald,Dale Schumacher,Dana Scott,Shayak Sen,Pawel Sobocinski,Kristina Sojakova,Daniel Spoonhower,Paulo Tanimoto,Joe Tassarotti,Peter Thiemann,Bernardo Toninho,Michael Tschantz,Kami Vaniea,Carsten Varming, David Walker,Dan Wang,Jack Wileden,Sergei Winitzki,Roger Wolff,Omer Zach,Luke Zarko, and Yu Zhang.I am very grateful to the students of 15-312 and 15-814 at Carnegie Mellon who have provided the impetus for the preparation of this book and who have endured the many revisions to it over the last ten years. I thank the Max Planck Institute for Software Systems for its hospitality and support.I also thank Espresso a Mano in Pittsburgh,CB2 Cafe in Cambridge,and Thonet Cafe in Saarbrucken for providing a steady supply of coffee and a conducive atmosphere for writing. This material is,in part,based on work supported by the National Science Foundation under Grant Nos.0702381 and 0716469.Any opinions,findings,and conclusions or recommendations expressed in this material are those of the author(s)and do not necessarily reflect the views of the National Science Foundation. Robert Harper Pittsburgh PRE March,2012
PREVIEW Rob Simmons, and Todd Wilson for their extensive efforts in reading and criticizing the book. I also thank the following people for their suggestions: Joseph Abrahamson, Arbob Ahmad, Zena Ariola, Eric Bergstrome, William Byrd, Alejandro Cabrera, Luis Caires, Luca Cardelli, Manuel Chakravarty, Richard C. Cobbe, James Cooper, Yi Dai, Daniel Dantas, Anupam Datta, Jake Donham, Bill Duff, Matthias Felleisen, Kathleen Fisher, Dan Friedman, Peter Gammie, Maia Ginsburg, Byron Hawkins, Kevin Hely, Kuen-Bang Hou (Favonia), Justin Hsu, Wojciech Jedynak, Cao Jing, Salil Joshi, Gabriele Keller, Scott Kilpatrick, Danielle Kramer, Dan Kreysa, Akiva Leffert, Ruy Ley-Wild, Karen Liu, Dave MacQueen, Chris Martens, Greg Morrisett, Stefan Muller, Tom Murphy, Aleksandar Nanevski, Georg Neis, David Neville, Adrian Trejo Nunez, Cyrus Omar, ˜ Doug Perkins, Frank Pfenning, Jean Pichon, Benjamin Pierce, Andrew M. Pitts, Gordon Plotkin, David Renshaw, John Reynolds, Andreas Rossberg, Carter Schonwald, Dale Schumacher, Dana Scott, Shayak Sen, Pawel Sobocinski, Kristina Sojakova, Daniel Spoonhower, Paulo Tanimoto, Joe Tassarotti, Peter Thiemann, Bernardo Toninho, Michael Tschantz, Kami Vaniea, Carsten Varming, David Walker, Dan Wang, Jack Wileden, Sergei Winitzki, Roger Wolff, Omer Zach, Luke Zarko, and Yu Zhang. I am very grateful to the students of 15–312 and 15–814 at Carnegie Mellon who have provided the impetus for the preparation of this book and who have endured the many revisions to it over the last ten years. I thank the Max Planck Institute for Software Systems for its hospitality and support. I also thank Espresso a Mano in Pittsburgh, CB2 Cafe in Cambridge, and Thonet Cafe in Saarbrucken ¨ for providing a steady supply of coffee and a conducive atmosphere for writing. This material is, in part, based on work supported by the National Science Foundation under Grant Nos. 0702381 and 0716469. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation. Robert Harper Pittsburgh March, 2012
Contents Preface to the Second Edition Preface to the First Edition I Judgments and Rules IEW 1 Abstract Syntax 3 1.1 Abstract Syntax Trees..... 4 1.2 Abstract Binding Trees 6 1.3 Notes.·.·.···· 10 2 Inductive Definitions 13 2.1 Judgments 13 2.2 Inference Rules 44444 14 2.3 Derivations....·.·. 15 2.4 Rule Induction..。.·...···· 16 2.5 Iterated and Simultaneous Inductive Definitions... 18 2.6 Defining Functions by Rules..,. 19 2.7 Notes.········ 20 3 Hypothetical and General Judgments 23 3.1 Hypothetical Judgments 23 3.1.1 Derivability ....... 23 3.1.2 Admissibility··..·...· 25 3.2 Hypothetical Inductive Definitions ... 26 3.3 General Judgments...············ 3.4 Generic Inductive Definitions 29 3.5 Notes...··············· 30
PREVIEW Contents Preface to the Second Edition iii Preface to the First Edition v I Judgments and Rules 1 1 Abstract Syntax 3 1.1 Abstract Syntax Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 Abstract Binding Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2 Inductive Definitions 13 2.1 Judgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 Inference Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.3 Derivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.4 Rule Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.5 Iterated and Simultaneous Inductive Definitions . . . . . . . . . . . . . . . . . . . . . 18 2.6 Defining Functions by Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.7 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3 Hypothetical and General Judgments 23 3.1 Hypothetical Judgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.1.1 Derivability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.1.2 Admissibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.2 Hypothetical Inductive Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.3 General Judgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3.4 Generic Inductive Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
viii CONTENTS ⅡStatics and Dynamics 33 4 Statics 4.1 Syntax 36 4.2 Type System................. 4.3 Structural Properties.··········· 37 4.4 39 5 Dynamics 41 5.1 Transition Systems·.·.······· 41 5.2 Structural Dynamics 42 5.3 Contextual Dynamics....... 5.4 Equational Dynamics.·.·.·. % 5.5 Notes..········ 6 Type Safety 51 6.1 Preservation............ 52 6.2 Progress 6.3 Run-Time Errors....... 53 6.4 Notes......... 7 Evaluation Dynamics 57 7.1 Evaluation Dynamics.·.··· 7.2 Relating Structural and Evaluation Dynamics 58 7.3 Type Safety,Revisited............. 7.4 Cost Dynamics 7.5 Notes 61 III Total Functions 63 8 Function Definitions and Values 8.1 First-Order Functions. 65 8.2 Higher-Order Functions 8.3 Evaluation Dynamics and Definitional Equality 8.4 Dynamic Scope 0 8.5 Notes···············“ 71 9 System T of Higher-Order Recursion 7 9.1 Statics..··········· 73 9.2 Dynamics 9.3 Definability 9.4 Undefinability 77 9.5 Notes.······
PREVIEW viii CONTENTS II Statics and Dynamics 33 4 Statics 35 4.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 4.2 Type System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 4.3 Structural Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 4.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 5 Dynamics 41 5.1 Transition Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 5.2 Structural Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 5.3 Contextual Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 5.4 Equational Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 5.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 6 Type Safety 51 6.1 Preservation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 6.2 Progress . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 6.3 Run-Time Errors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 6.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 7 Evaluation Dynamics 57 7.1 Evaluation Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 7.2 Relating Structural and Evaluation Dynamics . . . . . . . . . . . . . . . . . . . . . . . 58 7.3 Type Safety, Revisited . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 7.4 Cost Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 7.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 III Total Functions 63 8 Function Definitions and Values 65 8.1 First-Order Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 8.2 Higher-Order Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 8.3 Evaluation Dynamics and Definitional Equality . . . . . . . . . . . . . . . . . . . . . 69 8.4 Dynamic Scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 8.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 9 System T of Higher-Order Recursion 73 9.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 9.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 9.3 Definability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 9.4 Undefinability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 9.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
CONTENTS 4 IV Finite Data Types 81 10 Product Types 83 10.1 Nullary and Binary Products 10.2 Finite Products 8 l0.3 Primitive Mutual Recursion·.,.....·····, 6 10.4 Notes...··················· 11 Sum Types 11.1 Nullary and Binary Sums 11.2 Finite Sums...··········· 11.3 Applications of Sum Types... 11.3.1 Void and Unit .. 11.3.2 Booleans....... 11.3.3 Enumerations .. 899922294 11.3.4 Options 11.4 Notes......... 95 V Types and Propositions 97 12 Constructive Logic 99 12.1 Constructive Semantics ····.100 12.2 Constructive Logic 100 12.2.1 Provability 101 12.2.2 Proof Terms 103 12.3 Proof Dynamics·. 104 12.4 Propositions as Types.·· 105 12.5 Notes...,. 105 13 Classical Logic 109 13.1 Classical Logic.··.· ··..110 13.1.1 Provability and Refutability ···.110 13.1.2 Proofs and Refutations 112 13.2 Deriving Elimination Forms 114 13.3 Proof Dynamics..···,. ..115 13.4 Law of the Excluded Middle 117 13.5 The Double-Negation Translation.. 118 13.6 Notes.........· 119 VI Infinite Data Types 121 14 Generic Programming 123 14.1 Introduction..... 123
PREVIEW CONTENTS ix IV Finite Data Types 81 10 Product Types 83 10.1 Nullary and Binary Products . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 10.2 Finite Products . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 10.3 Primitive Mutual Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 10.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 11 Sum Types 89 11.1 Nullary and Binary Sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 11.2 Finite Sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 11.3 Applications of Sum Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 11.3.1 Void and Unit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 11.3.2 Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 11.3.3 Enumerations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 11.3.4 Options . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 11.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 V Types and Propositions 97 12 Constructive Logic 99 12.1 Constructive Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 12.2 Constructive Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 12.2.1 Provability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 12.2.2 Proof Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 12.3 Proof Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 12.4 Propositions as Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 12.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 13 Classical Logic 109 13.1 Classical Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 13.1.1 Provability and Refutability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 13.1.2 Proofs and Refutations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 13.2 Deriving Elimination Forms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 13.3 Proof Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 13.4 Law of the Excluded Middle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 13.5 The Double-Negation Translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 13.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 VI Infinite Data Types 121 14 Generic Programming 123 14.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
CONTENTS 14.2 Polynomial Type Operators...··············· 123 l4.3 Positive Type Operators...··········.······ 126 127 15 Inductive and Coinductive Types 129 15.1 Motivating Examples.....·.·.···.··· 4 ·...129 15.2 Statics..............·········· 132 1521 Types..·················· 133 152.2 Expressions·············· 133 15.3 Dynamics.....············ 134 15.4 Solving Type Equations 135 15.5 Notes···················· 136 vII Variable Types 139 16 System F of Polymorphic Types 141 16.1 Polymorphic Abstraction... 142 16.2 Polymorphic Definability 145 16.2.1 Products and Sums 145 16.2.2 Natural Numbers. 146 16.3 Parametricity Overview 147 16.4 Notes....... 148 17 Abstract Types 151 17.1 Existential Types 151 17.1.1 Statics.. 152 17.1.2 Dynamics 152 17.13 Safety..· 153 17.2 Data Abstraction...... 153 17.3 Definability of Existential Types 155 17.4 Representation Independence 155 17.5 Notes....... 157 18 Higher Kinds 159 18.1 Constructors and Kinds 。。。 160 18.2 Constructor Equality 161 18.3 Expressions and Types 162 18.4 Notes◆.·········· 163 VIII Partiality and Recursive Types 165 19 System PCF of Recursive Functions 167 19.1 Statics....············· 169
PREVIEW x CONTENTS 14.2 Polynomial Type Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 14.3 Positive Type Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 14.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 15 Inductive and Coinductive Types 129 15.1 Motivating Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129 15.2 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 15.2.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 15.2.2 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 15.3 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 15.4 Solving Type Equations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135 15.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 VII Variable Types 139 16 System F of Polymorphic Types 141 16.1 Polymorphic Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142 16.2 Polymorphic Definability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 16.2.1 Products and Sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 16.2.2 Natural Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146 16.3 Parametricity Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 16.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148 17 Abstract Types 151 17.1 Existential Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151 17.1.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 17.1.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 17.1.3 Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 17.2 Data Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 17.3 Definability of Existential Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 17.4 Representation Independence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 17.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157 18 Higher Kinds 159 18.1 Constructors and Kinds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160 18.2 Constructor Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161 18.3 Expressions and Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162 18.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163 VIII Partiality and Recursive Types 165 19 System PCF of Recursive Functions 167 19.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
CONTENTS 女 19.2 Dynamics 170 l9.3 Definability.···.·········· 171 19.4 Finite and Infinite Data Structures 。。 173 19.5 Totality and Partiality.......... 174 19.6 Notes...·········· 175 20 System FPC of Recursive Types 177 20.1 Solving Type Equations 178 20.2 Inductive and Coinductive Types.···.··· 179 20.3Self-Reference................. 180 20.4 The Origin of State.·.·.·...···.··· 182 20.5 Notes..············· 183 IX Dynamic Types 185 21 The Untyped A-Calculus 187 21.1Theλ-Calculus 187 21.2 Definability ·····188 21.3 Scott's Theorem.·.·.· ····190 21.4 Untyped Means Uni-Typed 192 21.5 Notes.·········· 193 22 Dynamic Typing 195 22.1 Dynamically Typed PCF 196 22.2 Variations and Extensions. 199 22.3 Critique of Dynamic Typing.. 201 22.4 Notes..··... 44444 202 23 Hybrid Typing 205 23.1 A Hybrid Language.. .......205 23.2 Dynamic as Static Typing·..··· 207 23.3 Optimization of Dynamic Typing 208 23.4 Static Versus Dynamic Typing. 210 23.5 Notes . 211 X Subtyping 213 24 Structural Subtyping 215 24.1 Subsumption.. ..215 24.2 Varieties of Subtyping ....216 24.3 Variance 218 24.4 Dynamics and Safety 223 24.5 Notes...······ 224
PREVIEW CONTENTS xi 19.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170 19.3 Definability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171 19.4 Finite and Infinite Data Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173 19.5 Totality and Partiality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174 19.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175 20 System FPC of Recursive Types 177 20.1 Solving Type Equations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178 20.2 Inductive and Coinductive Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179 20.3 Self-Reference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 180 20.4 The Origin of State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182 20.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183 IX Dynamic Types 185 21 The Untyped λ-Calculus 187 21.1 The λ-Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 21.2 Definability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188 21.3 Scott’s Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 190 21.4 Untyped Means Uni-Typed . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192 21.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193 22 Dynamic Typing 195 22.1 Dynamically Typed PCF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196 22.2 Variations and Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199 22.3 Critique of Dynamic Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201 22.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202 23 Hybrid Typing 205 23.1 A Hybrid Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205 23.2 Dynamic as Static Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207 23.3 Optimization of Dynamic Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208 23.4 Static Versus Dynamic Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 210 23.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211 X Subtyping 213 24 Structural Subtyping 215 24.1 Subsumption . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215 24.2 Varieties of Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216 24.3 Variance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 218 24.4 Dynamics and Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 223 24.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224
