Full Iso-recursive Types
Litao Zhou, Qianyong Wan, Bruno C. d. S. Oliveira

TL;DR
This paper introduces full iso-recursive types, a generalization that encodes equi-recursive types efficiently using irrelevant casts, simplifying reasoning and eliminating runtime overhead.
Contribution
It proposes full iso-recursive types allowing encoding of equi-recursive types without overhead, and extends lambda calculus with type soundness and expressiveness equivalence.
Findings
Full iso-recursive types can encode equi-recursive types efficiently.
Type casts are computationally irrelevant and erased at runtime.
Equi-recursive subtyping can be expressed with cast operators.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems
