Efficient and flexible matching of recursive types

Equality and subtyping of recursive types have been studied in the 1990s by: R.M. Amadaio and L. Cardelli (1993); D. Kozen et al. (1993); M. Brandt and F. Henglein (1997) and others. Potential applications include automatic generation of bridge code for multi-language systems and type-based retrieval of software modules from libraries. J. Auerbach et al. (1998) advocate a highly flexible combination of matching rules for which there, until now, are no efficient algorithmic techniques. We present an efficient decision procedure for a notion of type equality that includes unfolding of recursive types, and associativity and commutativity of product types, as advocated by Auerbach et al. For two types of size at most n, our algorithm decides equality in O(n² ) time. The algorithm iteratively prunes a set of type pairs, and eventually it produces a set of pairs of equal types. In each iteration, the algorithm exploits a so-called coherence property of the set of type pairs produced in the preceding iteration. The algorithm takes O(n) iterations, each of which takes O(n) time, for a total of O(n²) time