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 fall-out: 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:

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 type-inference 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). 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
LIENS-DMI
Roberto Di Cosmo
roberto@dicosmo.org