Logic in Computer Science (LICS 2000)

Paper: Efficient and Flexible Matching of Recursive Types (at LICS 2000)

Authors: Jens Palsberg Tian Zhao

Abstract

Equality and subtyping of recursive types have been 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 multi-language systems and type-based retrieval of software modules from libraries. Auerbach, Barton, and Raghavachari advocate a highly flexible combination of matching rules for which there, until now, are no efficient algorithmic techniques. 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, as advocated by Auerbach et al. For two types of size at most n, our algorithm decides equality in O(n2) 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(n2) time.

BibTeX

  @InProceedings{PalsbergZhao-EfficientandFlexibl,
    author = 	 {Jens Palsberg and Tian Zhao},
    title = 	 {Efficient and Flexible Matching of Recursive Types},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {388--398},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }