Completely Subtyping Iso-recursive Types
Jeremy Blackburn, Ivory Hernandez, Jay Ligatti, Michael Nachtigal · 2012
Well-known techniques exist for proving the soundness of subtyping relations with respect to type safety. However, completeness has not been treated with widely applicable techniques, as far as we are aware. This paper develops some techniques for stating and proving that a subtyping relation is complete with respect to type safety and applies the techniques to the study of iso-recursive subtyping. The common subtyping rules for iso-recursive types—the “Amber rules”—are shown to be incomplete with respect to type safety. That is, there exist iso-recursive types τ1 and τ2 such that τ1 can safely be considered a subtype of τ2, but τ1≤τ2 is not derivable with the Amber rules. This paper defines new, algorithmic rules for subtyping isorecursive types and proves that the rules are sound and complete with respect to type safety.