Efficient and Flexible Matching of Recursive Types

AbstractEquality and subtyping of recursive types were studied in the 1990s by Amadio and Cardelli; Kozen, Palsberg, and Schwartzbach; Brandt and Henglein; and others. Potential applications include automatic generation of bridge code for multilanguage systems and type-based retrieval of software modules from libraries. In this paper, 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. Advocated by Auerbach, Barton, and Raghavachari, these properties enable flexible matching of types. For two types of size at most n, our algorithm takes O(n) iterations each of which takes O(n) time, for a total of O(n2) time