CIS6700-Spring2025/Homework 5.md

This lemma wasn't part of the exercises assigned but it's needed for the exercises and not proven in the book so I thought I'd sketch it out quickly.

Lemma 15.3.2 (Inversion of the subtype relation):

1. If S <: T₁ → T₂, then S = S₁ → S₂ such that T₁ <: S₁ and S₂ <: T₂.
2. If S <: {lᵢ : Tᵢ}, then S = {kⱼ : Sⱼ} such that {lᵢ} ⊆ {kⱼ} and Sⱼ <: Tᵢ when lᵢ = kⱼ. Proof:
3. By induction on the subtyping derivation. The applicable cases are S-Refl (holds directly), S-Trans (holds by induction hypothesis twice), and S-Arrow (holds directly).
4. By induction on the subtyping derivation. The applicable cases are S-Refl (holds directly), S-Trans (holds by induction hypothesis twice, using S-Trans and transitivity of subsets of labels), S-RcdWidth (holds directly using S-Refl and {l₁..lₙ} ⊆ {l₁..lₙ₊ₖ}), S-RcdDepth (holds directly), and S-RcdPerm (holds by induction hypothesis).

Here are the assigned exercises.

Lemma 15.3.6 (Canonical forms):

1. If v is a closed value of type T₁ → T₂, then v has the form λx: S₁. t₂.
2. If v is a closed value of type {lᵢ : Tᵢ}, then v has the form {kⱼ = vⱼ}, where {lᵢ} ⊆ {kⱼ}. Proof:
3. By induction on the typing derivation of Γ ⊢ v : T₁ → T₂. The only applicable cases are T-Abs and T-Sub; the first case holds directly. In the second case, we have Γ ⊢ v : S and S <: T₁ → T₂. By inversion on subtyping (Lemma 15.3.2), S = S₁ → S₂. Then v has the form of a function by the induction hypothesis.
4. By induction on the typing derivation of Γ ⊢ v : {lᵢ : Tᵢ}. We proceed similarly to the above, where the applicable cases are T-Rcd and T-Sub, the first case holds directly, and the second case holds using inversion (Lemma 15.3.2) and the induction hypothesis. The top-level lemmas hold by instantiating Γ = ∅.

Exercise 16.1.3: If we add Bool, we also need to add the subtyping rule Bool <: Bool so that the judgement remains reflexive.

Theorem 16.2.5: If Γ ⊢ t : T, then Γ ⊢> t : S and ⊢> S <: T. Proof: By induction on the typing derivation.

• Case T-Var: Holds by TA-Var.
• Case T-Abs: The premise is Γ, x: T₁ ⊢ t₂ : T₂, concluding with Γ ⊢ λx: T₁. t₂ : T₁ → T₂. By the induction hypothesis, we have Γ, x: T₁ ⊢> t₂ : S₂ and ⊢> S₂ <: T₂. By TA-Abs, we have Γ ⊢> λx: T₁. t₂ : T₁ → S₂, and by reflexivity and SA-Arrow we have ⊢> T₁ → S₂ <: T₁ → T₂.
• Case T-App: The premises are Γ ⊢ t₁ : T₁₁ → T₁₂ and Γ ⊢ t₂ : T₁₁, concluding with Γ ⊢ t₁ t₂ : T₁₂. By the induction hypothesis, we have Γ ⊢> t₁ : S₁, ⊢> S₁ <: T₁₁ → T₁₂ for the first premise and Γ ⊢> t₂ : S₂, ⊢> S₂ <: T₁₁ for the second. By inversion on subtyping, S₁ = S₁₁ → S₁₂ , ⊢> T₁₁ <: S₁₁, and ⊢> S₁₂ <: T₁₂. By transitivity, ⊢> S₂ <: T₁₁ <: S₁₁. Then we can use TA-App to build Γ ⊢> t₁ t₂ : S₁₂, with ⊢> S₁₂ <: T₁₂ as needed.
• Case T-Rcd: The premises are Γ ⊢ tᵢ : Tᵢ, concluding with Γ ⊢ {lᵢ = tᵢ} : {lᵢ : Tᵢ}. By the induction hypothesis, we have Γ ⊢> tᵢ : Sᵢ and ⊢> Sᵢ <: Tᵢ. By TA-Rcd, we have Γ ⊢> {lᵢ = tᵢ} : {lᵢ : Sᵢ}, and by SA-Rcd, we have ⊢> {lᵢ : Sᵢ} <: {lᵢ : Tᵢ}.
• Case T-Proj: The premise is Γ ⊢ t : {lᵢ : Tᵢ}, concluding with Γ ⊢ t.lⱼ : Tⱼ. By the induction hypothesis, we have Γ ⊢> t : S and ⊢> S <: {lᵢ : Tᵢ}. By inversion on subtyping, S = {kᵢ : Sᵢ}, where {lᵢ} ⊆ {kᵢ} and ⊢> Sᵢ <: Tⱼ when lⱼ = kᵢ. Letting lⱼ = kᵢ, we can use TA-Proj to build Γ ⊢> t.lⱼ : Sᵢ, with ⊢> Sᵢ <: Tⱼ.
• Case T-Sub: The premises are Γ ⊢ t : S and S <: T, concluding with Γ ⊢ t : T. By the induction hypothesis, we have Γ ⊢> t : U and ⊢> U <: S. By completeness (Proposition 16.1.5), we get ⊢> S <: T. Then by transitivity, we get ⊢> U <: S <: T as needed.

Exercise 16.2.6: I think the system without S-Arrow would still have the minimal typing property. The proof would proceed exactly as in Theorem 16.2.5. Completeness (S <: T implies ⊢> S <: T) still holds, since the induction would just be missing one case.

Lemma (existence of a subtype): For every S, T, either there exists some N such that N <: S or N <: T, or no such N is possible. Proof: By induction on the structure of S and T. If one of the types is Top, then the other type is a subtype of both by reflexivity and S-Top. If the types have different shapes (i.e. one is a function type, the other a record type), supposing we have a subtype N, by inversion on the subtyping derivations, N would have to be both a function type and a record type, which is a contradiction, so no such N exists. That leaves the cases where both types are function types or record types.

• Case S₁ → S₂, T₁ → T₂. By the induction hypothesis, either S₂ and T₂ have a subtype N₂, or no such subtype exists. If it exists, then Top → N₂ is a subtype, since S₁ <: Top, T₁ <: Top, N₂ <: S₂, and N₂ <: T₂, and we construct Top → N₂ <: S₁ → S₂ and Top → N₂ <: T₁ → T₂ by S-Arrow. If it does not exist, then supposing we had a subtype N₁ → N₂ of both S₁ → S₂ and T₁ → T₂, by inversion, we have N₂ <: S₂ and N₂ <: T₂, which is a contradiction, so there must be no such subtype.
• Case {kᵢ : Sᵢ}, {lⱼ : Tⱼ}. By the induction hypothesis, each pair Sᵢ, Tᵢ either have a subtype Nᵢⱼ, or no such subtype exists. Let {klᵢⱼ} = {kᵢ} ∪ {lⱼ}.
  • If all Sᵢ and Tⱼ for which kᵢ = lⱼ have a subtype, then we claim the subtype is {klᵢⱼ : Uᵢⱼ} such that Uᵢⱼ = Nᵢⱼ if klᵢⱼ = kᵢ = lⱼ, Uᵢⱼ = Sᵢ if klᵢⱼ = kᵢ only, or Uᵢⱼ = Tⱼ if klᵢⱼ = lⱼ only. We can construct {klᵢⱼ : Uᵢⱼ} <: {kᵢ : Sᵢ} by S-Rcd since {kᵢ} ⊆ {klᵢⱼ}, and kᵢ = kₗᵢⱼ implies Sᵢ <: Uᵢⱼ, where Uᵢⱼ = Sᵢ or Uᵢⱼ = Nᵢⱼ. Similarly, we can construct {klᵢⱼ : Uᵢⱼ} <: {lⱼ : Tⱼ} by S-Rcd.
  • If there exists some klᵢⱼ such that klᵢⱼ = kᵢ = lⱼ but Sᵢ and Tⱼ have no subtype, then we claim there is no subtype. Supposing there were a subtype N, by inversion we must have that N = {nₘ : Nₘ} where kᵢ = nₘ implies Nₘ <: Sᵢ and lⱼ = nₘ implies Nₘ <: Tⱼ. In the case where nₘ = klᵢⱼ, this gives us a subtype of Sᵢ and Tⱼ, which is a contradiction.

Proposition 16.3.2:

1. For every S, T, there exists some J = S ∨ T.
2. For every S, T, N such that N <: S and N <: T, there exists some M = S ∧ T. Proof: By induction on the structure of S and T, proving both simultaneously, although I will write them separately, even though I use the induction hypotheses jointly.
3. Goal S ∨ T. If one of the types is Top, then the join is Top. If the types have different shapes, then the join must be Top, since a function type cannot be the supertype of a record type and vice versa by inversion. That leaves the cases where both types are function types or record types.
   • Case S₁ → S₂, T₁ → T₂. By the induction hypothesis, we know thatJ₂ = S₂ ∨ T₂ exists. There are two possible subcases to consider, using the above lemma (existence of a subtype).
     • If S₁ and T₁ have a subtype, then by the induction hypothesis, we know that M₁ = S₁ ∧ T₁ exists. We claim that M₁ → J₂ is the join; we know it is a supertype by S-Arrow. It remains to show that it is minimal, i.e. for every U such that S₁ → S₂ <: U and T₁ → T₂ <: U, we have M₁ → J₂ <: U. If U is Top, then we are done. Otherwise, it must be that U = U₁ → U₂, and by inversion, U₁ <: S₁, U₁ <: T₁, S₂ <: U₂, and T₂ <: U₂. It suffices to show that U₁ <: M₁ and J₂ <: U₂. The former holds by maximality of the meet M₁ = S₁ ∨ T₁, while the latter holds by minimality of the join J₂ = S₂ ∨ T₂.
     • If S₁ and T₁ do not have a subtype, then we claim that Top is the join. We must show it to be minimal: for every U such that S₁ → S₂ <: U and T₁ → T₂ <: U, we have Top <: U. If U is Top, then we are done. Otherwise, it must be that U = U₁ → U₂, and by inversion, U₁ <: S₁, U₁ <: T₁, S₂ <: U₂, and T₂ <: U₂. However, this makes U₁ a subtype of S₁ and T₁, which is a contradiction.
   • Case {kᵢ : Sᵢ}, {lⱼ : Tⱼ}. By the induction hypothesis, we know that every Sᵢ, Tⱼ have a join. Let {klᵢⱼ | klᵢⱼ = kᵢ = lⱼ} be the common labels, i.e. {kᵢ} ∩ {lⱼ}, and let Jᵢⱼ = Sᵢ ∨ Tⱼ. We claim that {klᵢⱼ : Jᵢⱼ} is the join; we know it is a supertype by S-Rcd. It remains to show that it is minimal, i.e. for every U such that {kᵢ : Sᵢ} <: U and {lⱼ : Tⱼ} <: U, we have {klᵢⱼ : Jᵢⱼ} <: U. If U is Top, then we are done. Otherwise, it must be that U = {uₙ : Uₙ}, and by inversion, {uₙ} ⊆ {kᵢ}, {uₙ} ⊆ {lⱼ}, kᵢ = uₙ implies Sᵢ <: Uₙ, and lⱼ = uₙ implies Tⱼ <: Uₙ. Then we know {uₙ} ⊆ {kᵢ} ∩ {lⱼ} = {klᵢⱼ}, and if kᵢⱼ = uₙ, then Sᵢ <: Uₙ and Tᵢ <: Uₙ. By minimality of the join Jᵢⱼ, we have Jᵢⱼ <: Uₙ. Then we can use S-Rcd to build {klᵢⱼ : Jᵢⱼ} <: U.
4. Goal S ∧ T. If one of the types is Top, then the meet is the other type. If the types have different shapes, then N being a subtype of both is a contradiction by inversion. That leaves the cases where both types are function types or record types.
   • Case S₁ → S₂, T₁ → T₂. By inversion, N = N₁ → N₂ where S₁ <: N₁, T₁ <: N₁, N₂ <: S₂, N₂ <: T₂. By the induction hypothesis, we know that M₂ = S₂ ∨ T₂ and J₁ = S₁ ∧ T₁ exist. We claim that J₁ → M₂ is the meet; we know it is a subtype by S-Arrow. It remains to show that it is maximal, i.e. for every U such that U <: S₁ → S₂ and U <: T₁ → T₂, we have U <: J₁ → M₂. By inversion, U = U₁ → U₂ such that S₁ <: U₁, T₁ <: U₁, U₂ <: S₂, and U₂ <: T₂. It suffices to show that J₁ <: U₁ and U₂ <: M₂. The former holds by minimality of the join J₁ = S₁ ∧ T₁, while the latter holds by maximality of the meet M₂ = S₂ ∨ T₂.
   • Case {kᵢ : Sᵢ}, {lⱼ : Tⱼ}. By inversion, N = {nₘ : Nₘ} where {nₘ} ⊆ {kᵢ}, {nₘ} ⊆ {lⱼ}, kᵢ = nₘ implies Nₘ <: Sᵢ, and lⱼ = nₘ implies Nₘ <: Tⱼ. By the induction hypothesis, we know that every Sᵢ, Tⱼ have a meet. Let {klᵢⱼ} = {kᵢ} ∪ {lⱼ} be the union of all labels, and for every klᵢⱼ, let Mᵢⱼ = Sᵢ ∧ Tᵢ if klᵢⱼ ∈ {kᵢ} ∩ {lⱼ}, Mᵢⱼ = Sᵢ if klᵢⱼ ∈ {kᵢ} only, and Mᵢⱼ = Tᵢ if klᵢⱼ ∈ {lⱼ} only. We claim that {klᵢⱼ : Mᵢⱼ} is the meet; we know it is a subtype by S-Rcd. It remains to show that it is maximal, ie. for every U such that U <: {kᵢ : Sᵢ} and U <: {lⱼ : Tⱼ}, we have U <: {Mᵢⱼ : Jᵢⱼ}. By inversion, U = {uₙ : Uₙ} where {kᵢ} ⊆ {uₙ}, {lⱼ} ⊆ {uₙ}, kᵢ = uₙ implies Uₙ <: Sᵢ, and lⱼ = uₙ implies Uₙ <: Tⱼ. Then we know {kᵢⱼ} = {kᵢ} ∪ {lⱼ} ⊆ {uₙ}. Supposing kᵢⱼ = uₙ, either uₙ = kᵢ = lⱼ, in which case Uₙ <: Sᵢ ∧ Tⱼ by maximality of the meet, or uₙ = kᵢ only, in which case Uₙ <: Sᵢ, or uₙ = lⱼ only, in which case Uₙ <: Tⱼ, so together we have Uₙ <: Mᵢⱼ. Then we can use S-Rcd to build U <: {klᵢⱼ : Mᵢⱼ}.