Full Iso-recursive Types

TL;DR

The paper tackles the equivalence between iso-recursive and equi-recursive types and the runtime overhead from coercions by introducing full iso-recursive types that use computationally irrelevant casts. It presents the calculus $λ^{0μ}_{Fi}$, extending the simply-typed lambda calculus with full iso-recursive types, and proves type soundness along with equivalence to equi-recursive types via a type-directed elaboration and an erasure process that preserves termination/divergence. It further extends the results to subtyping, showing equi-recursive subtyping can be expressed via iso-recursive subtyping with cast operators, and provides a Coq formalization of the metatheory (except for one decomposition lemma adapted from prior work). These contributions yield a unified, overhead-free pathway to model recursive types and have practical implications for compiler design, enabling source languages with equi-recursive types to elaboratively target languages with full iso-recursive types. Overall, the work simplifies reasoning about recursive-type equivalence, supports subtyping extensions, and offers a viable architectural model akin to GHC-style pipelines where casts are erased at runtime.

Abstract

There are two well-known formulations of recursive types: iso-recursive and equi-recursive types. Abadi and Fiore [1996] have shown that iso- and equi-recursive types have the same expressive power. However, their encoding of equi-recursive types in terms of iso-recursive types requires explicit coercions. These coercions come with significant additional computational overhead, and complicate reasoning about the equivalence of the two formulations of recursive types. This paper proposes a generalization of iso-recursive types called full iso-recursive types. Full iso-recursive types allow encoding all programs with equi-recursive types without computational overhead. Instead of explicit term coercions, all type transformations are captured by computationally irrelevant casts, which can be erased at runtime without affecting the semantics of the program. Consequently, reasoning about the equivalence between the two approaches can be greatly simplified. We present a calculus called $λ^μ_{Fi}$, which extends the simply typed lambda calculus (STLC) with full iso-recursive types. The $λ^μ_{Fi}$ calculus is proved to be type sound, and shown to have the same expressive power as a calculus with equi-recursive types. We also extend our results to subtyping, and show that equi-recursive subtyping can be expressed in terms of iso-recursive subtyping with cast operators.