This is a book about isomorphisms 0/ types, arecent difficult research topic in type theory that turned out to be able to have valuable practical applications both for programming language design and far more human- centered information retrieval in software libraries. By means of a deep study of the syntax of the now widely known typed A-ca1culus, it is possible to identify some simple equations between types that on one hand allow to improve the design of the ML language, and on the other hand provide the basis for building radically new information retrieval systems for functional software...