Coercive type isomorphism

Abstract

There is a variety of situations in programming in which it is useful to think of two distinct types as representations of the same abstract structure. However, language features which allow such relations to be effectively expressed at an abstract level are lacking. We propose a generalization of ML-style type inference to deal effectively with this problem. Under the generalization, the (normally free) algebra of type expressions is subjected to an equational theory generated by a finite set of user-specified equations that express interconvertibility relations between objects of “equivalent” types. Each type equation is accompanied by a pair of conversion functions that are (at least partial) inverses. We show that so long as the equational theory satisfies a reasonably permissive syntactic constraint, the resulting type system admits a complete type inference algorithm that produces unique principal types. The main innovation required in type inference is the replacement of ordinary free unification by unification in the userspecified equational theory. The syntactic constraint ensures that the latter is unitary, i.e., yields unique most general unifiers. The proposed constraint is of independent interest as the first known syntactic characterization for a class of unitary theories. Some of the applications of the system are similar to those of Wadler's views . However, our system is considerably more general, and more orthogonal to the underlying language.