Type Isomorphisms
The WWW Home Page
In this page you will find relevant information and up to date references on the research on isomorphisms of types, both in its theoretical aspects and in its applications.
Introduction and Overview
In modern programming languages the notion of type has become so natural and widespread, that it is easy to forget about its origins and its theoretical relevance. A type is simply seen as a useful means of classification of the objects that a program manipulates: types help to understand better what a program does, and also provide a valuable firewall against many common programming errors.But the theory of types is also a well established and very active field of research in mathematical logic and theoretical computer science, that can often generate interesting practical fallout. This document is a simple starting point for the exploration of one such successful story of nice theory that produced valuable practical fallout: the study of isomorphic types, originally started from very theoretical motivations in category theory and in the theory of lambda calculus, turned out to provide a firm basis both for the design of new programming languages and for the development of natural tools for information retrieval in software libraries.
Isomorphic types
Two types A and B are isomorphic it there are two conversion functions f of type A>B and g of type B>A, such that g(f(x))=x for any x of type A and f(g(y))=y for any y of type B.This definition is very simple and carries the idea that isomorphic types provide essentially the same information.
Once the definition is given, one can study such isomorphisms in different languages, find a set of axioms that can be used to describe them, and design an algorithm to decide equality, matching or unification modulo such set of axioms.
Current Research
Many people have worked on the theoretical or applied aspects of isomorphic types, in many reasearch centers. Here we try to keep an up to date description of the ongoing work: if you happen to notice that you should be cited and you are not, please mail a message to the maintainer of this page.
Theory
Here is a growing list of researchers working on these topics, in many different research sites:
 Kim BRUCE kim@cs.williams.edu WILLIAMS COLLEGE
 Roberto DI COSMO roberto@dicosmo.org LIENSDMI
 Giuseppe LONGO longo@di.ens.fr LIENSDMI
 Brian MATTHEWS bmm@inf.rl.ac.uk RUTHERFORD APPLETON LABORATORY
 Mikael RITTRI rittri@cs.chalmers.se CHALMERS
 Sergei SOLOVIEV Sergei.Soloviev@durham.ac.uk DURHAM
 Jeanette WING wing@cs.cmu.edu CMU
 Amy MOORMANN ZAREMSKY amy+@cs.cmu.edu CMU
Applications
The equivalence of types induced by the notion of isomorphisms can be used to help a user locate a function starting from the type he would give to that function. As well argued in Mikael Rittri's and Runciman and Toyn's seminal papers, the type the user will come up with is not necessarily the one chosen by the library implementors, but it is very likely that it is isomorphic to it.Using the theories of isomorphisms, we can implement library browser that will retrieve functions whose type is isomorphic to the user supplied type, like the one provided with CamlLight 0.7, which you can test directly from this page (here in english et ici en français). Also, isomorphic types can help in designing better typeinference systems, like the one described in Journal of Functional Programming, Oct. 1993
Books
Up to now, there is just one book devoted to this topic, but it covers both theory and applications.Selected papers
There have been many published papers and unpublished reports on this and related subjects: here follows a list of them (a dvi or ps version of the paper or an associated technical report is just a click away from you). Mikael Rittri.
{Retrieving library identifiers by equational matching of types} in {10th Int.\
Conf.\ on Automated Deduction}.
Lecture Notes in Computer Science, 449, July 1990.
 Mikael Rittri.
{Searching program libraries by type and proving compiler correctness by
bisimulation}.
PhD thesis, {University of G\"oteborg}, G\"oteborg, Sweden, 1990.
 Mikael Rittri.
Using types as search keys in function libraries.
Journal of Functional Programming, 1(1):7189, 1991.
 Mikael Rittri.
Retrieving library functions by unifying types modulo linear isomorphisms.
Technical Report~66, Chalmers University of Technology and University of
G\"oteborg, 1992.
Programming Methodology Group.
 Mikael Rittri.
Retrieving library functions by unifying types modulo linear isomorphism.
RAIRO Theoretical Informatics and Applications, 27(6):523540,
1993.

Roberto Di Cosmo.
Isomorphisms of types.
Tesi di dottorato, Dipartimento di Informatica, Universitá
di Pisa, 40, Corso Italia  56100 Pisa  Italy, January 1993.

Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo.
Provable isomorphisms of types.
Mathematical Structures in Computer Science,
2(2):231247, 1992.
Proc. of Symposium on Symbolic Computation, ETH, Zurich,
March 1990.
(DVI)
(ABSTRACT)

Roberto Di Cosmo and Giuseppe Longo.
Constuctively equivalent propositions and
isomorphisms of objects (or terms as natural transformations).
In Moschovakis, editor, Logic from Computer Science,
volume 21 of Mathematical Sciences Research Institute Publications,
pages 7394. Springer Verlag, Berkeley, 1991.
Proceedings of a workshop held November 1317, 1989.
 Roberto Di Cosmo.
Second order isomorphic types. A proof theoretic
study on second order lambdacalculus with surjective pairing and terminal
object.
Information and Computation, pages 176201, June
1995.
(ABSTRACT)

Roberto Di Cosmo.
Type isomorphisms in a type assignment
framework.
In 19th Ann. ACM Symp. on Principles of Programming
Languages (POPL), pages 200210. ACM, 1992.
(DVI)
(ABSTRACT)

Roberto Di Cosmo.
Deciding type isomorphisms in a type assignment
framework.
Journal of Functional Programming, 3(3):485525,
1993.
Special Issue on ML.
(DVI)
(ABSTRACT)
 Brian Matthews.
Reusing functional code using type classes for library search.
Systems Engineering, Rutherford Appleton Laboratory, Didcot, OXO N, OX11 0QX,
U.K., email: bmm@inf.rl.ac.uk.
 Eugene~R. Rollins and Jeannette~M. Wing.
Specifications as search keys for software libraries.
In K.~Furukawa, editor, Eighth International Conference on Logic
Programming, pages 173187. MIT Press, 91.
 Colin Runciman and Ian Toyn.
Retrieving reusable software components by polymorphic type.
Journal of Functional Programming, 1(2):191211, 1991.
 Sergei~V. Soloviev.
A complete axiom system for isomorphism of types in closed categories.
In A.~Voronkov, editor, Logic Programming and Automated Reasoning, 4th
International Conference, volume 698 of Lecture Notes in
Artificial Intelligence (subseries of LNCS), pages 360371, St.
Petersburg, Russia, 1993. SpringerVerlag.
 Sergei~V. Soloviev and Alexander E.Andreev.
Linear isomorphism of types: a low upper bound for complexity.
Technical report, BRICS reports in Computer Science, 1994.
 Jeannette~M. Wing, Eugene Rollins, and
Amy~Moormann Zaremski.
Thoughts on a {Larch/ML} and a new application for {LP}.
In First International Workshop on Larch, Dedham, MA, July 1992.
Also available as CMUCS92135, July 1992.
 Amy~Moormann Zaremsky and Jeannette~M. Wing.
Signature matching: a key to reuse.
In SIGSOFT, December 1993.
Also available as CMUCS93151, May 1993.
 Roberto Di Cosmo.
Isomorphisms of types: from lambdacalculus to
information retrieval and language design.
Birkhauser, 1995.
ISBN081763763X.
(ABSTRACT)
Available source code
Source code for the library browser is available for the following systems:
 CAML 3.1 directory user_lib/FIND_IN_LIB in common.tar.Z
 CamlLight 0.6 directory contrib/search_isos in cl6unix.tar.Z
 CamlLight 0.7 directory contrib/camlsearch in cl7beta1unix.tar.gz
 Haskell ask Brian Matthews
 LML ask Mikael Rittri
 SML ask Jeanette Wing
The Isomorphisms of Types WWW Page LIENSDMI Roberto Di Cosmo roberto@dicosmo.org