21.11 Subtyping Iso-Recursive Types

< Free Open Study >

We remarked in §20.2 that some treatments of recursive types adopt an iso-recursive presentation, where the folding and unfolding of recursive types is witnessed explicitly by the term constructors fold and unfold. In such languages, the μ type constructor is "rigid," in the sense that its position in a type affects how terms belonging to this type can be used.

If we add subtyping to a language with iso-recursive types, the rigidity of the μ constructor also affects the subtype relation. Instead of intuitively "unrolling to the limit, then subtyping," as we have done in most of this chapter, we must define subtyping rules involving recursive types directly.

The most common definition of iso-recursive subtyping is the Amber rule— so-called because it was popularized by Cardelli's Amber language (1986):

Intuitively, this rule can be read, "To show that μX.S is a subtype of μY.T under some set of assumptions Σ, it suffices to show S <: T under the additional assumption that X <: Y. ^[5] Σ here is just a set of pairs of recursion variables, recording the pairs of recursive types that have already been considered. These assumptions are used by another subtyping rule

that allows us to conclude X <: Y if we are currently assuming it.

In effect, adding these two rules to the usual subtyping algorithm from Chapter 16 (and extending the other rules so that they pass Σ through from premises to conclusion) yields an algorithm that behaves somewhat like the subtype^ac algorithm in Figure 21-5, with Σ playing the role of A. The differences are that (1) we "unfold" recursive types only when they appear on both sides of the <: at once, and (2) we do not substitute the recursive types into their bodies (we just leave them as variables), which makes it easy to see that the algorithm terminates.

The subtyping rules found in nominal type systems (such as Featherweight Java, Chapter 19) are closely related to the Amber rule.

21.11.1 Exercise [Recommended, ⋆⋆]

Find recursive types S and T such that S <: T using the equi-recursive definition, but not using the Amber rule.

^[5]Note that this rule, unlike most rules involving binding constructs on both sides, such as S-All in Figure 26-1, demands that the bound variables X and Y be renamed to be distinct before the rule is applied.

< Free Open Study >