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 $\lambda^{\mu}_{Fi}$, which extends the simply typed lambda calculus (STLC) with full iso-recursive types. The $\lambda^{\mu}_{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.

翻译：递归类型存在两种众所周知的表述方式：同构递归类型与等价递归类型。Abadi与Fiore[1996]已证明同构递归类型与等价递归类型具有相同的表达能力。然而，他们提出的基于同构递归类型对等价递归类型的编码方案需要显式的强制转换操作。这些强制转换会带来显著的计算开销，并使关于两种递归类型表述方式等价性的推理变得复杂。本文提出了一种称为"完全同构递归类型"的同构递归类型泛化形式。完全同构递归类型能够无计算开销地编码所有使用等价递归类型的程序。所有类型转换均通过计算无关的强制操作实现，而非显式的项强制转换，这些强制操作可在运行时被擦除而不影响程序语义。因此，关于两种方法等价性的推理得以大幅简化。我们提出了一种称为$\lambda^{\mu}_{Fi}$的演算系统，该系统通过完全同构递归类型扩展了简单类型λ演算（STLC）。我们证明了$\lambda^{\mu}_{Fi}$演算具有类型可靠性，并展示了其与等价递归类型演算具有相同的表达能力。我们还将研究结果扩展至子类型系统，证明了等价递归子类型可通过带强制操作符的同构递归子类型进行表达。