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.
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.
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.
Here is a growing list of
researchers working on these topics, in many different
research sites:
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
Up to now, there is just one book devoted to this topic, but it covers both
theory and applications.
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)
Practically all of this material is discussed in the book referenced above.
Available source code
Source code for the library browser is available for the following systems:
The Isomorphisms of Types WWW Page
LIENSDMI
Roberto Di Cosmo
roberto@dicosmo.org