michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix #495.

Browse source
This commit is contained in:
Wen Kokke 2020-07-19 13:56:36 +01:00
parent 4423c37089
commit 935362efc4
1 changed files with 30 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
src/plfa/part2/Subtyping.lagda.md
View file

@ -1,5 +1,5 @@
--- ---
title : "Subtyping: records" title : "Subtyping: Records"
layout : page layout : page
prev : /More/ prev : /More/
permalink : /Subtyping/ permalink : /Subtyping/
@ -30,7 +30,7 @@ can also have type `B` if `A` is a subtype of `B`.
⊢<: : ∀{Γ M A B} ⊢<: : ∀{Γ M A B}
→ Γ ⊢ M ⦂ A → Γ ⊢ M ⦂ A
→ A <: B → A <: B
----------- -----------
→ Γ ⊢ M ⦂ B → Γ ⊢ M ⦂ B
@ -58,7 +58,7 @@ written `M # l`, and whose dynamic semantics is defined by the
following reduction rule, which says that accessing the field `lⱼ` following reduction rule, which says that accessing the field `lⱼ`
returns the value stored at that field. returns the value stored at that field.
{l₁=v₁, ..., lⱼ=vⱼ, ..., lᵢ=vᵢ} # lⱼ —→ vⱼ {l₁=v₁, ..., lⱼ=vⱼ, ..., lᵢ=vᵢ} # lⱼ —→ vⱼ
In this chapter we add records and record types to the simply typed In this chapter we add records and record types to the simply typed
lambda calculus (STLC) and prove type safety. It is instructive to see lambda calculus (STLC) and prove type safety. It is instructive to see
@ -138,14 +138,14 @@ Name = String
A record is traditionally written as follows A record is traditionally written as follows
{ l₁ = M₁, ..., lᵢ = Mᵢ } { l₁ = M₁, ..., lᵢ = Mᵢ }
so a natural representation is a list of label-term pairs. so a natural representation is a list of label-term pairs.
However, we find it more convenient to represent records as a pair of However, we find it more convenient to represent records as a pair of
vectors (Agda's `Vec` type), one vector of fields and one vector of terms: vectors (Agda's `Vec` type), one vector of fields and one vector of terms:
l₁, ..., lᵢ l₁, ..., lᵢ
M₁, ..., Mᵢ M₁, ..., Mᵢ
This representation has the advantage that the traditional subscript This representation has the advantage that the traditional subscript
notation `lᵢ` corresponds to indexing into a vector. notation `lᵢ` corresponds to indexing into a vector.
@ -244,9 +244,9 @@ If one vector `ns` is a subset of another `ms`, then for any element
lookup-⊆ : ∀{n m : ℕ}{ns : Vec Name n}{ms : Vec Name m}{i : Fin n} lookup-⊆ : ∀{n m : ℕ}{ns : Vec Name n}{ms : Vec Name m}{i : Fin n}
→ ns ⊆ ms → ns ⊆ ms
→ Σ[ k ∈ Fin m ] lookup ns i ≡ lookup ms k → Σ[ k ∈ Fin m ] lookup ns i ≡ lookup ms k
lookup-⊆ {suc n} {m} {x ∷ ns} {ms} {zero} ns⊆ms lookup-⊆ {suc n} {m} {x ∷ ns} {ms} {zero} ns⊆ms
with lookup-∈ (ns⊆ms x (here refl)) with lookup-∈ (ns⊆ms x (here refl))
... | ⟨ k , ms[k]=x ⟩ = ... | ⟨ k , ms[k]=x ⟩ =
⟨ k , (sym ms[k]=x) ⟩ ⟨ k , (sym ms[k]=x) ⟩
lookup-⊆ {suc n} {m} {x ∷ ns} {ms} {suc i} x∷ns⊆ms = lookup-⊆ {suc n} {m} {x ∷ ns} {ms} {suc i} x∷ns⊆ms =
lookup-⊆ {n} {m} {ns} {ms} {i} (λ x z → x∷ns⊆ms x (there z)) lookup-⊆ {n} {m} {ns} {ms} {i} (λ x z → x∷ns⊆ms x (there z))
@ -258,7 +258,7 @@ lookup-⊆ {suc n} {m} {x ∷ ns} {ms} {suc i} x∷ns⊆ms =
data Type : Set where data Type : Set where
_⇒_ : Type → Type → Type _⇒_ : Type → Type → Type
`ℕ : Type `ℕ : Type
｛_⦂_｝ : {n : ℕ} (ls : Vec Name n) (As : Vec Type n) → .{d : distinct ls} → Type ｛_⦂_｝ : {n : ℕ} (ls : Vec Name n) (As : Vec Type n) → .{d : distinct ls} → Type
``` ```
In addition to function types `A ⇒ B` and natural numbers `ℕ`, we In addition to function types `A ⇒ B` and natural numbers `ℕ`, we
@ -366,7 +366,7 @@ Here is the proof of reflexivity, by induction on the size of the type.
with ty-size-pos {A} with ty-size-pos {A}
... | pos rewrite n≤0⇒n≡0 m ... | pos rewrite n≤0⇒n≡0 m
with pos with pos
... | () ... | ()
<:-refl-aux {suc n}{`ℕ}{m} = <:-nat <:-refl-aux {suc n}{`ℕ}{m} = <:-nat
<:-refl-aux {suc n}{A ⇒ B}{m} = <:-refl-aux {suc n}{A ⇒ B}{m} =
let A<:A = <:-refl-aux {n}{A}{m+n≤o⇒m≤o _ (≤-pred m) } in let A<:A = <:-refl-aux {n}{A}{m+n≤o⇒m≤o _ (≤-pred m) } in
@ -376,7 +376,7 @@ Here is the proof of reflexivity, by induction on the size of the type.
where where
G : ls ⦂ As <: ls ⦂ As G : ls ⦂ As <: ls ⦂ As
G {i}{j} lij rewrite distinct-lookup-inj (distinct-relevant d) lij = G {i}{j} lij rewrite distinct-lookup-inj (distinct-relevant d) lij =
let As[i]≤n = ≤-trans (lookup-vec-ty-size {As = As}{i}) (≤-pred m) in let As[i]≤n = ≤-trans (lookup-vec-ty-size {As = As}{i}) (≤-pred m) in
<:-refl-aux {n}{lookup As i}{As[i]≤n} <:-refl-aux {n}{lookup As i}{As[i]≤n}
``` ```
The theorem statement uses `n` as an upper bound on the size of the type `A` The theorem statement uses `n` as an upper bound on the size of the type `A`
@ -394,7 +394,7 @@ and proceeds by induction on `n`.
Regarding the latter, we need to show that for any `i` and `j`, Regarding the latter, we need to show that for any `i` and `j`,
`lookup ls j ≡ lookup ls i` implies `lookup As j <: lookup As i`. `lookup ls j ≡ lookup ls i` implies `lookup As j <: lookup As i`.
Because `lookup` is injective on distinct vectors, we have `i ≡ j`. Because `lookup` is injective on distinct vectors, we have `i ≡ j`.
We then use the induction hypothesis to show that We then use the induction hypothesis to show that
`lookup As i <: lookup As i`, noting that the size of `lookup As i <: lookup As i`, noting that the size of
`lookup As i` is less-than-or-equal to the size of `As`, which `lookup As i` is less-than-or-equal to the size of `As`, which
is one smaller than the size of `｛ ls ⦂ As ｝`. is one smaller than the size of `｛ ls ⦂ As ｝`.
@ -421,7 +421,7 @@ The following corollary packages up reflexivity for ease of use.
where where
As<:Cs : ls ⦂ As <: ns ⦂ Cs As<:Cs : ls ⦂ As <: ns ⦂ Cs
As<:Cs {i}{j} ls[j]=ns[i] As<:Cs {i}{j} ls[j]=ns[i]
with lookup-⊆ {i = i} ns⊆ms with lookup-⊆ {i = i} ns⊆ms
... | ⟨ k , ns[i]=ms[k] ⟩ = ... | ⟨ k , ns[i]=ms[k] ⟩ =
let As[j]<:Bs[k] = As<:Bs {k}{j} (trans ls[j]=ns[i] ns[i]=ms[k]) in let As[j]<:Bs[k] = As<:Bs {k}{j} (trans ls[j]=ns[i] ns[i]=ms[k]) in
let Bs[k]<:Cs[i] = Bs<:Cs {i}{k} (sym ns[i]=ms[k]) in let Bs[k]<:Cs[i] = Bs<:Cs {i}{k} (sym ns[i]=ms[k]) in
@ -450,7 +450,7 @@ The proof is by induction on the derivations of `A <: B` and `B <: C`.
if we can prove that `lookup ls j ≡ lookup ms k`. if we can prove that `lookup ls j ≡ lookup ms k`.
We already have `lookup ls j ≡ lookup ns i` and we We already have `lookup ls j ≡ lookup ns i` and we
obtain `lookup ns i ≡ lookup ms k` by use of the lemma `lookup-⊆`, obtain `lookup ns i ≡ lookup ms k` by use of the lemma `lookup-⊆`,
noting that `ns ⊆ ms`. noting that `ns ⊆ ms`.
We can obtain the later, that `lookup Bs k <: lookup Cs i`, We can obtain the later, that `lookup Bs k <: lookup Cs i`,
from `｛ ms ⦂ Bs ｝ <: ｛ ns ⦂ Cs ｝`. from `｛ ms ⦂ Bs ｝ <: ｛ ns ⦂ Cs ｝`.
It suffices to show that `lookup ms k ≡ lookup ns i`, It suffices to show that `lookup ms k ≡ lookup ns i`,
@ -527,7 +527,7 @@ The typing judgment takes the form `Γ ⊢ M ⦂ A` and relies on an
auxiliary judgment `Γ ⊢* Ms ⦂ As` for typing a vector of terms. auxiliary judgment `Γ ⊢* Ms ⦂ As` for typing a vector of terms.
``` ```
data _⊢*_⦂_ : Context → ∀ {n} → Vec Term n → Vec Type n → Set data _⊢*_⦂_ : Context → ∀ {n} → Vec Term n → Vec Type n → Set
data _⊢_⦂_ : Context → Term → Type → Set where data _⊢_⦂_ : Context → Term → Type → Set where
@ -607,7 +607,7 @@ chapter. Here we discuss the three new rules.
* Rule `⊢<:`: (Subsumption) If a term `M` has type `A`, and `A <: B`, * Rule `⊢<:`: (Subsumption) If a term `M` has type `A`, and `A <: B`,
then term `M` also has type `B`. then term `M` also has type `B`.
## Renaming and Substitution ## Renaming and Substitution
@ -712,7 +712,7 @@ data Value : Term → Set where
→ Value (`suc V) → Value (`suc V)
V-rcd : ∀{n}{ls : Vec Name n}{Ms : Vec Term n} V-rcd : ∀{n}{ls : Vec Name n}{Ms : Vec Term n}
→ Value ｛ ls := Ms ｝ → Value ｛ ls := Ms ｝
``` ```
## Reduction ## Reduction
@ -827,10 +827,10 @@ canonical ⊢zero V-zero = C-zero
canonical (⊢suc ⊢V) (V-suc VV) = C-suc (canonical ⊢V VV) canonical (⊢suc ⊢V) (V-suc VV) = C-suc (canonical ⊢V VV)
canonical (⊢case ⊢L ⊢M ⊢N) () canonical (⊢case ⊢L ⊢M ⊢N) ()
canonical (⊢μ ⊢M) () canonical (⊢μ ⊢M) ()
canonical (⊢rcd ⊢Ms d) VV = C-rcd {dls = d} ⊢Ms d <:-refl canonical (⊢rcd ⊢Ms d) VV = C-rcd {dls = d} ⊢Ms d <:-refl
canonical (⊢<: ⊢V <:-nat) VV = canonical ⊢V VV canonical (⊢<: ⊢V <:-nat) VV = canonical ⊢V VV
canonical (⊢<: ⊢V (<:-fun {A}{B}{C}{D} C<:A B<:D)) VV canonical (⊢<: ⊢V (<:-fun {A}{B}{C}{D} C<:A B<:D)) VV
with canonical ⊢V VV with canonical ⊢V VV
... | C-ƛ {N}{A′}{B′}{A}{B} ⊢N AB′<:AB = C-ƛ ⊢N (<:-trans AB′<:AB (<:-fun C<:A B<:D)) ... | C-ƛ {N}{A′}{B′}{A}{B} ⊢N AB′<:AB = C-ƛ ⊢N (<:-trans AB′<:AB (<:-fun C<:A B<:D))
canonical (⊢<: ⊢V (<:-rcd {ks = ks}{ls = ls}{d2 = dls} ls⊆ks ls⦂Ss<:ks⦂Ts)) VV canonical (⊢<: ⊢V (<:-rcd {ks = ks}{ls = ls}{d2 = dls} ls⊆ks ls⦂Ss<:ks⦂Ts)) VV
with canonical ⊢V VV with canonical ⊢V VV
@ -915,8 +915,8 @@ progress (⊢· ⊢L ⊢M)
... | done VL ... | done VL
with progress ⊢M with progress ⊢M
... | step M—→M′ = step (ξ-·₂ VL M—→M′) ... | step M—→M′ = step (ξ-·₂ VL M—→M′)
... | done VM ... | done VM
with canonical ⊢L VL with canonical ⊢L VL
... | C-ƛ ⊢N _ = step (β-ƛ VM) ... | C-ƛ ⊢N _ = step (β-ƛ VM)
progress ⊢zero = done V-zero progress ⊢zero = done V-zero
progress (⊢suc ⊢M) with progress ⊢M progress (⊢suc ⊢M) with progress ⊢M
@ -950,7 +950,7 @@ progress (⊢<: {A = A}{B} ⊢M A<:B) = progress ⊢M
* Case `⊢rcd`: we immediately characterize the record as a value. * Case `⊢rcd`: we immediately characterize the record as a value.
* Case `⊢<:`: we invoke the induction hypothesis on sub-derivation of `Γ ⊢ M ⦂ A`. * Case `⊢<:`: we invoke the induction hypothesis on sub-derivation of `Γ ⊢ M ⦂ A`.
## Preservation <a name="subtyping-preservation"></a> ## Preservation <a name="subtyping-preservation"></a>
@ -1047,9 +1047,9 @@ subst-pres : ∀ {Γ Δ σ N A}
----------------- -----------------
→ Δ ⊢ subst σ N ⦂ A → Δ ⊢ subst σ N ⦂ A
subst-pres σ⦂ (⊢` eq) = σ⦂ eq subst-pres σ⦂ (⊢` eq) = σ⦂ eq
subst-pres {σ = σ} σ⦂ (⊢ƛ ⊢N) = ⊢ƛ (subst-pres{σ = exts σ}(exts-pres {σ = σ} σ⦂) ⊢N) subst-pres {σ = σ} σ⦂ (⊢ƛ ⊢N) = ⊢ƛ (subst-pres{σ = exts σ}(exts-pres {σ = σ} σ⦂) ⊢N)
subst-pres {σ = σ} σ⦂ (⊢· ⊢L ⊢M) = ⊢· (subst-pres{σ = σ} σ⦂ ⊢L) (subst-pres{σ = σ} σ⦂ ⊢M) subst-pres {σ = σ} σ⦂ (⊢· ⊢L ⊢M) = ⊢· (subst-pres{σ = σ} σ⦂ ⊢L) (subst-pres{σ = σ} σ⦂ ⊢M)
subst-pres {σ = σ} σ⦂ (⊢μ ⊢M) = ⊢μ (subst-pres{σ = exts σ} (exts-pres{σ = σ} σ⦂) ⊢M) subst-pres {σ = σ} σ⦂ (⊢μ ⊢M) = ⊢μ (subst-pres{σ = exts σ} (exts-pres{σ = σ} σ⦂) ⊢M)
subst-pres σ⦂ (⊢rcd ⊢Ms dls) = ⊢rcd (subst-vec-pres σ⦂ ⊢Ms ) dls subst-pres σ⦂ (⊢rcd ⊢Ms dls) = ⊢rcd (subst-vec-pres σ⦂ ⊢Ms ) dls
subst-pres {σ = σ} σ⦂ (⊢# {d = d} ⊢M lif liA) = subst-pres {σ = σ} σ⦂ (⊢# {d = d} ⊢M lif liA) =
⊢# {d = d} (subst-pres {σ = σ} σ⦂ ⊢M) lif liA ⊢# {d = d} (subst-pres {σ = σ} σ⦂ ⊢M) lif liA
@ -1097,7 +1097,7 @@ The proof is by induction on the typing derivation.
* Case `⊢-*-∷`: So we have `∅ ⊢ M ⦂ B` and `∅ ⊢* Ms ⦂ As`. We proceed by cases on `i`. * Case `⊢-*-∷`: So we have `∅ ⊢ M ⦂ B` and `∅ ⊢* Ms ⦂ As`. We proceed by cases on `i`.
* If it is `0`, then lookup yields term `M` and `A ≡ B`, so we conclude that `∅ ⊢ M ⦂ A`. * If it is `0`, then lookup yields term `M` and `A ≡ B`, so we conclude that `∅ ⊢ M ⦂ A`.
* If it is `suc i`, then we conclude by the induction hypothesis. * If it is `suc i`, then we conclude by the induction hypothesis.
@ -1144,7 +1144,7 @@ with cases on `M —→ N`.
* Case `⊢#` and `ξ-#`: So `∅ ⊢ M ⦂ ｛ ls ⦂ As ｝`, `lookup ls i ≡ l`, `lookup As i ≡ A`, * Case `⊢#` and `ξ-#`: So `∅ ⊢ M ⦂ ｛ ls ⦂ As ｝`, `lookup ls i ≡ l`, `lookup As i ≡ A`,
and `M —→ M′`. We apply the induction hypothesis to obtain `∅ ⊢ M′ ⦂ ｛ ls ⦂ As ｝` and `M —→ M′`. We apply the induction hypothesis to obtain `∅ ⊢ M′ ⦂ ｛ ls ⦂ As ｝`
and then conclude by rule `⊢#`. and then conclude by rule `⊢#`.
* Case `⊢#` and `β-#`. We have `∅ ⊢ ｛ ks := Ms ｝ ⦂ ｛ ls ⦂ As ｝`, `lookup ls i ≡ l`, * Case `⊢#` and `β-#`. We have `∅ ⊢ ｛ ks := Ms ｝ ⦂ ｛ ls ⦂ As ｝`, `lookup ls i ≡ l`,
`lookup As i ≡ A`, `lookup ks j ≡ l`, and `｛ ks := Ms ｝ # l —→ lookup Ms j`. `lookup As i ≡ A`, `lookup ks j ≡ l`, and `｛ ks := Ms ｝ # l —→ lookup Ms j`.
By the canonical forms lemma, we have `∅ ⊢* Ms ⦂ Bs`, `ls ⊆ ks` and `ks ⦂ Bs <: ls ⦂ As`. By the canonical forms lemma, we have `∅ ⊢* Ms ⦂ Bs`, `ls ⊆ ks` and `ks ⦂ Bs <: ls ⦂ As`.
@ -1230,7 +1230,7 @@ The non-algorithmic subtyping rules for variants are
∀i∈1..u, ∃j∈1..u, kⱼ = lᵢ and Aⱼ = Bᵢ ∀i∈1..u, ∃j∈1..u, kⱼ = lᵢ and Aⱼ = Bᵢ
---------------------------------------------- ----------------------------------------------
〈k₁=A₁, ..., kᵤ=Aᵤ〉 <: 〈l₁=B₁, ..., lᵤ=Bᵤ〉 〈k₁=A₁, ..., kᵤ=Aᵤ〉 <: 〈l₁=B₁, ..., lᵤ=Bᵤ〉
Come up with an algorithmic subtyping rule for variant types. Come up with an algorithmic subtyping rule for variant types.
#### Exercise `<:-alternative` (stretch) #### Exercise `<:-alternative` (stretch)
@ -1260,7 +1260,7 @@ of the form:
If S <: { lᵢ : Tᵢ | i ∈ 1..n }, then S ≡ { kⱼ : Sⱼ | j ∈ 1..m } If S <: { lᵢ : Tᵢ | i ∈ 1..n }, then S ≡ { kⱼ : Sⱼ | j ∈ 1..m }
and { lᵢ | i ∈ 1..n } ⊆ { kⱼ | j ∈ 1..m } and { lᵢ | i ∈ 1..n } ⊆ { kⱼ | j ∈ 1..m }
and Sⱼ <: Tᵢ for every i and j such that lᵢ = kⱼ. and Sⱼ <: Tᵢ for every i and j such that lᵢ = kⱼ.
## References ## References
@ -1274,6 +1274,5 @@ of the form:
* Barbara H. Liskov and Jeannette M. Wing. A Behavioral Notion of * Barbara H. Liskov and Jeannette M. Wing. A Behavioral Notion of
Subtyping. In ACM Trans. Program. Lang. Syst. Volume 16, 1994. Subtyping. In ACM Trans. Program. Lang. Syst. Volume 16, 1994.
* Types and Programming Languages. Benjamin C. Pierce. The MIT Press. 2002.
* Types and Programming Languages. Benjamin C. Pierce. The MIT Press. 2002.