  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.
