[Prev][Next][Index][Thread]
[New Book]: Isomorphisms of Types
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 <dicosmo@dmi.ens.fr>
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