The following newly published book may be of interest to TYPES subscribers. It is a study of the notion of type-isomorphisms in functional languages, both from a theoretical and a practical point of view. It is based on my PhD dissertation, but has been extensively revised, updated and provided with a completely new introduction to the topic, that makes it accessible to a wide spectrum of readers. It tries hard to provide a complete reference and discussion of all research done in this area, from the definition of confluent rewriting systems for typed lambda calculi equipped with various extensionality rules, to the characterization of isomorphisms of types in different typed calculi, to the applications to extensions of ML-style type-inference algorithms and the design of library search tools based on types. I enclose a summary of the book, also available at URL http://www.ens.fr/users/dicosmo/Publications/ISObook.html --Roberto Di Cosmo LIENS Ecole Normale Superieure 45, Rue d'Ulm 75005 Paris FRANCE ------------------------------------------------------------------------- Isomorphisms of Types: from lambda calculus to information retrieval and language design. Roberto Di Cosmo Progress in Theoretical Computer Science. Birkhauser. 1995. ISBN 0-8176-3763-X. ------------------------------------------------------------------------- Table of Contents 1 Introduction 11 1.1 What is a type?. . . . . . . . . . . . . . . . . . . . . . . : 12 1.2 Types in mathematical logic. . . . . . . . . . . . . . . . . . 13 1.3 Types for programming . . . . . . . . . . . . . . . . . . . . 14 1.3.1 Imperative languages . . . . . . . . . . . . . . . . . . 15 1.3.2 Limits of static type-checking . . . . . . . . . . . . : 19 1.3.3 Functional languages . . . . . . . . . . . . . . . . . . 20 1.3.4 The lambda calculus . . . . . . . . . . . . . . . . . . 21 1.4 Exploring typed lambda-calculi . . . . . . . . . . . . . . . : 23 1.4.1 Church-style types . . . . . . . . . . . . . . . . . . : 23 1.4.2 Curry-style types . . . . . . . . . . . . . . . . . . . 24 1.4.3 Explicit polymorphic types . . . . . . . . . . . . . . . 24 1.4.4 Implicit polymorphic types . . . . . . . . . . . . . . . 25 1.5 The typed lambda-calculi used in this work . . . . . . . . . : 27 1.5.1 The calculus lambda-2-pi-* . . . . . . . . . . . . . . . 27 1.5.2 General notations for terms and substitutions . . . . . 28 1.6 The Curry-Howard Isomorphism . . . . . . . . . . . . . . : 30 1.7 Using types to classify and retrieve software . . . . . . . : 34 1.7.1 Object-oriented languages . . . . . . . . . . . . . . : 35 1.7.2 Functional languages . . . . . . . . . . . . . . . . . . 36 1.8 When are two types equal? . . . . . . . . . . . . . . . . . . 37 1.8.1 Isomorphic types . . . . . . . . . . . . . . . . . . . . 38 1.8.2 Isomorphisms in category theory . . . . . . . . . . . : 41 1.8.3 Digression: Tarski's High School Algebra Problem : 43 1.8.4 Isomorphisms in logic . . . . . . . . . . . . . . . . : 45 1.9 Isomorphisms and the lambda calculus . . . . . . . . . . . . . 46 1.9.1 Isomorphisms and invertibility . . . . . . . . . . . . . 46 1.9.2 The theories of isomorphisms for typed ~-calculi . . . . 49 1.9.3 Soundness . . . . . . . . . . . . . . . . . . . . . . . 50 2 Confluence Results 57 2.1 Introduction. . . . . . . . . . . . . . . . . . . . . . . . . : 58 2.2 Extensionality. . . . . . . . . . . . . . . . . . . . . . . . . 61 2.2.1 Survey. . . . . . . . . . . . . . . . . . . . . . . . . . 62 2.3 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 2.3.1 Weakly confluent reduction . . . . . . . . . . . . . . . 67 2.3.2 Investigating strong normalization . . . . . . . . . . . 71 2.3.3 A general criterion for confluence . . . . . . . . . . : 72 2.4 Confluence . . . . . . . . . . . . . . . . . . . . . . . . . : 74 2.5 Weak normalization . . . . . . . . . . . . . . . . . . . . . . 79 2.6 Decidability and conservative extension results . . . . . . . : 81 2.7 Other related works . . . . . . . . . . . . . . . . . . . . . . 81 3 Strong normalization results 85 3.1 Normalization without Beta2 on gentop n.f.'s . . . . . . . . . . 86 3.1.1 Reducibility with parameters . . . . . . . . . . . . . . : 89 3.2 Normalization without jtopand SPtop. . . . . . . . . . . . . . . 96 4 First-Order Isomorphic Types 101 4.1 Rewriting types . . . . . . . . . . . . . . . . . . . . . . . : 103 4.2 From lambda1-pi-* to the classical lambda-beta-eta . . . . . . 105 4.3 Using finite hereditary permutations . . . . . . . . . . . . : 112 4.4 The complete theories of lambda1-pi and lambda1-* . . . . . . : 116 5 Second-Order Isomorphic Types 119 5.1 Towards completeness . . . . . . . . . . . . . . . . . . . . : 120 5.1.1 Outline of the section . . . . . . . . . . . . . . . . : 120 5.1.2 Reduction to a subclass of types . . . . . . . . . . . : 121 5.1.3 Reduction to a subclass of terms . . . . . . . . . . . : 123 5.2 Characterizing canonical terms . . . . . . . . . . . . . . . . 124 5.2.1 Outline of the section . . . . . . . . . . . . . . . . : 124 5.2.2 Projection of invertibility over coordinates. . . . . . . 125 5.2.3 Reduction of coordinates to lambda2 . . . . . . . . . . : 130 5.2.4 Syntactic characterization of canonical bijections . . . 137 5.3 Completeness for isomorphisms . . . . . . . . . . . . . . . . . 139 5.3.1 Uniform isomorphisms . . . . . . . . . . . . . . . . . : 143 5.4 Decidability of the equational theory . . . . . . . . . . . . : 143 5.5 The complete theories of lambda2-pi and lambda2-* . . . . . . : 145 5.6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . : 146 A Properties of n-tuples . . . . . . . . . . . . . . . . . . . : 147 B Technical lemmas. . . . . . . . . . . . . . . . . . . . . . . . 151 C Miscellanea . . . . . . . . . . . . . . . . . . . . . . . . . : 161 6 Isomorphisms for ML 165 6.1 Introduction. . . . . . . . . . . . . . . . . . . . . . . . . : 166 6.2 Isomorphisms of types in ML-style languages . . . . . . . . . . 167 6.2.1 A formal setting for valid isomorphisms in ML-like languages . . . . . . . . . . . . . . . . . . . . . . . . 168 6.3 Completeness and conservativity results . . . . . . . . . . . : 172 6.3.1 Completeness . . . . . . . . . . . . . . . . . . . . . . 174 6.3.2 Relating Th2-pi-T and ThML . . . . . . . . . . . . . . : 174 6.4 Deciding ML isomorphism . . . . . . . . . . . . . . . . . . . : 175 6.4.1 An improved decision procedure . . . . . . . . . . . . : 177 6.4.2 Equality as unification with variable renamings . . . . : 179 6.4.3 Dynamic programming . . . . . . . . . . . . . . . . . . : 180 6.4.4 Experimental results . . . . . . . . . . . . . . . . . . 185 6.5 Adding isomorphisms to the ML type-checker . . . . . . . . . . 188 6.5.1 Type-inference with just (Split) . . . . . . . . . . . : 191 6.5.2 What is special in (Split) . . . . . . . . . . . . . . : 191 6.5.3 Choosing the right isomorphisms . . . . . . . . . . . . : 193 6.5.4 Right isomorphisms in impure context . . . . . . . . . . 195 6.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . : 195 6.7 Some technical Lemmas . . . . . . . . . . . . . . . . . . . . . 196 6.8 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . 196 6.9 Conservativity . . . . . . . . . . . . . . . . . . . . . . . : 200 7 Related Works, Future Perspectives 205 7.1 Equational matching of types . . . . . . . . . . . . . . . . : 206 7.1.1 Decomposing the matching problem . . . . . . . . . . . : 207 7.2 Using equational unification . . . . . . . . . . . . . . . . . 210 7.3 Extending the paradigm . . . . . . . . . . . . . . . . . . . . 210 7.3.1 Searching through type classes . . . . . . . . . . . . . 210 7.3.2 Searching with more powerful specifications . . . . . . : 211 7.3.3 Recursive terms and types . . . . . . . . . . . . . . . : 211 7.3.4 Other applications of type isomorphisms . . . . . . . . : 212 7.4 Future work and perspectives . . . . . . . . . . . . . . . . : 212 7.4.1 Design of type systems for functional languages . . . . : 212 7.4.2 Object retrieval in object-oriented libraries . . . . . : 213 7.4.3 Dynamic composition of software components . . . . . . . 213 7.4.4 Representation optimization . . . . . . . . . . . . . . . 213 Notation Index . . . . . . . . . . . . . . . . . . . . . . . . . . . 215 Subject Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219 Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . 225 Citation Index . . . . . . . . . . . . . . . . . . . . . . . . . . . 237 =========================================================================== >From the publisher's hype ... ----------------------------- Isomorphisms of types is a research topic that has its roots both in the common use of types in programming languages and in important branches of mathematical logic like the theory of types and the lambda-calculus. The study of isomorphic types started from very theoretical motivations in category theory and the theory of lamda-calculus and turned out to provide a basis for both the design of new type systems for programming languages and the development of natural tools for information retrieval in software libraries. The author begins his investigations with the origin of the concept in mathematical logic and then focuses on its modern use in programming languages and type theory, showing how the typed lamda-calculus can be of great help in understanding many key features of the type systems available in modern programming language. He then demonstrates why types are good candidates to classify software components and how they can be used as retrieval tools, with motivations and examples coming from ML, Objective C, and Smalltalk. The reader will find here a fascinating exposition of a fundamental topic in computer science. The notion of type is now an essential tool in the design of usable programming langues, to prove properties of programs, to ensure data encapsulation and hiding, and to retrieve software components, and many more applications for the computer science researcher. For Orders and Information Contact: In North America: Birkhauser 675 Massachusetts Ave. Cambridge, MA 02139 Ph. 1 800 777-4643 Fax. 1 617 876-1272 Outside N. America: Birkhauser Verlag AG P.O. Box 133 Klosterberg 23 CH-1040 Basel Switzerland Fax 41 61 271 7666