52 lines
12 KiB
Markdown
52 lines
12 KiB
Markdown
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**:
|
||
1. 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).
|
||
2. 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**:
|
||
1. 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.
|
||
2. 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.
|
||
1. 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 that`J₂ = 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`.
|
||
2. 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ᵢⱼ}`. |