Under consideration for publication in J. Functional Programming 1 Equational Theories with Recursive Types

Studies of equivalence for recursive types often consider impoverished type systems, where the equational theory is generated only by the fold/unfold rule µX. T (X) ≡ T (µX. T (X)). Recursive types have been applied in much richer contexts, including systems with β and η-equivalence, but without any guarantee that the implementations are correct. Though there are plausible ways to adapt standard recursive-type algorithms to richer equational theories, Colazzo and Ghelli observed that two “obvious ” ways of extending the algorithm in a different direction (adding universally-quantified types) both fail. Extended systems may not even be formally specified; combining βη-equivalence with coinductive equivalence of recursive types requires care to avoid inconsistency. In this paper we both define and analyze coinductive equivalence for recursive types combined with other common equational principles. We start by adding pairing and projection, allowing even pairs to be recursively defined. (This permits direct definitions for collections of mutually-recursive types.) We show that our definition yields a decidable theory with all the expected equational properties