[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