diff --git a/src/plfa/part2/Subtyping.lagda.md b/src/plfa/part2/Subtyping.lagda.md index d7095952..1266833a 100644 --- a/src/plfa/part2/Subtyping.lagda.md +++ b/src/plfa/part2/Subtyping.lagda.md @@ -10,6 +10,68 @@ next : /Bisimulation/ module plfa.part2.Subtyping where ``` +This chapter introduces *subtyping*, a concept that plays an important +role in object-oriented languages. Subtyping enables code to be more +reusable by allowing code work on objects of many different +types. Thus, subtyping provides a kind of polymorphism. In general, a +type `A` can be a subtype of another type `B`, written `A <: B`, when +an object of type `A` has all the capabilities expected of something +of type `B`. Or put another way, a type `A` can be a subtype of type +`B` when it is safe to substitute something of type `A` into code that +is expected something of type `B`. This is know as the *Liskov +Substitution Principle*. Given this semantic meaning of subtyping, a +subtype relation should always be reflexive and transitive. Given a +subtype relation `A <: B`, we refer to `B` as the supertype of `A`. + +To formulate a type system for a language with subtyping, one simply +adds the *subsumption rule*, which states that a term of type `A` +can also have type `B` if `A` is a subtype of `B`. + + ⊢<: : ∀{Γ M A B} + → Γ ⊢ M ⦂ A → A <: B + -------------------- + → Γ ⊢ M ⦂ B + +In this chapter we study subtyping in the relatively simple context of +records and record types. A *record* is a grouping of named values, +called *fields*. For example, one could represent a point on the +cartesian plane with the following record. + + { x = 4, y = 1 } + +A *record type* gives a type for each field. In the following, we +specify that the fields `x` and `y` both have type ``ℕ`. + + { x : `ℕ, y : `ℕ } + +One record type is a subtype of another if it has all of the fields of +the supertype and if the types of those fields are subtypes of the +corresponding fields in the supertype. So, for example, a point in +three dimensions is a subtype of a point in two dimensions. + + { x : `ℕ, y : `ℕ, z : `ℕ } <: { x : `ℕ, y : `ℕ } + +The elimination for for records is field access (aka. projection), +written `M # l`, and whose dynamic semantics is defined by the +following reduction rule, which says that accessing the field `lⱼ` +returns the value stored at that field. + + {l₁=v₁, ..., lⱼ=vⱼ, ..., lᵢ=vᵢ} # lⱼ —→ vⱼ + +In this chapter we add records and record types to the simply typed +lambda calculus (STLC) and prove type safety. The choice between +extrinsic and intrinsic typing is made more interesting by the +presense of subtyping. If we wish to include the subsumption rule, +then we cannot use intrinsicly typed terms, as intrinsic terms only +allow for syntax-directed rules, and subsumption is not syntax +directed. A standard alternative to the subsumption rule is to +instead use subtyping in the typing rules for the elimination forms, +an approach called algorithmic typing. Here we choose to include the +subsumption rule and use extrinsic typing, but we give an exercise at +the end for the reader to explore algorithmic typing with intrinsic +terms. + + ## Imports ``` @@ -27,16 +89,21 @@ open import Data.Vec.Membership.DecPropositional _≟_ using (_∈?_) open import Data.Vec.Membership.Propositional.Properties using (∈-lookup) open import Data.Vec.Relation.Unary.Any using (here; there) import Relation.Binary.PropositionalEquality as Eq -open Eq using (_≡_; _≢_; refl; sym; trans; cong) +open Eq using (_≡_; refl; sym; trans; cong) open import Relation.Nullary using (Dec; yes; no; ¬_) ``` ## Syntax +The syntax includes that of the STLC with a few additions regarding +records that we explain in the following sections. + ``` infix 4 _⊢_⦂_ +infix 4 _⊢*_⦂_ infix 4 _∋_⦂_ infixl 5 _,_ +infix 5 _[_] infixr 7 _⇒_ @@ -46,22 +113,47 @@ infixl 7 _·_ infix 8 `suc_ infix 9 `_ infixl 7 _#_ + +infix 4 _⊆_ +infix 5 ｛_⦂_｝ +infix 5 ｛_:=_｝ ``` +## Record Fields and their Properties -## Record Field Names, Functions and Properties - -We represent field identifiers (aka. names) as strings. +We represent field names as strings. ``` Name : Set Name = String ``` -The field identifiers of a record will be stored in a sequence, -specifically Agda's `Vec` type. We require that the field names of a -record be distinct, which we define as follows. +A record is traditionally written as follows + { l₁ = M₁, ..., lᵢ = Mᵢ } + +so a natural representation is a list of label-term pairs. +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: + + l₁, ..., lᵢ + M₁, ..., Mᵢ + +This representation has the advantage that the subscript notation `lᵢ` +corresponds to indexing into a vector. + +Likewise, a record type, traditionally written as + + { l₁ : A₁, ..., lᵢ : Aᵢ } + +will be represented as a pair of vectors, one vector of fields and one +vector of types. + + l₁, ..., lᵢ + A₁, ..., Aᵢ + +The field names of a record type must be distinct, which we define as +follows. ``` distinct : ∀{A : Set}{n} → Vec A n → Set distinct [] = ⊤ @@ -69,25 +161,24 @@ distinct (x ∷ xs) = ¬ (x ∈ xs) × distinct xs ``` For vectors of distinct elements, lookup is injective. - ``` distinct-lookup-inj : ∀ {n}{ls : Vec Name n}{i j : Fin n} → distinct ls → lookup ls i ≡ lookup ls j → i ≡ j -distinct-lookup-inj {.(suc _)} {x ∷ ls} {zero} {zero} ⟨ x∉ls , dls ⟩ lsij = refl -distinct-lookup-inj {.(suc _)} {x ∷ ls} {zero} {suc j} ⟨ x∉ls , dls ⟩ refl = +distinct-lookup-inj {ls = x ∷ ls} {zero} {zero} ⟨ x∉ls , dls ⟩ lsij = refl +distinct-lookup-inj {ls = x ∷ ls} {zero} {suc j} ⟨ x∉ls , dls ⟩ refl = ⊥-elim (x∉ls (∈-lookup j ls)) -distinct-lookup-inj {.(suc _)} {x ∷ ls} {suc i} {zero} ⟨ x∉ls , dls ⟩ refl = +distinct-lookup-inj {ls = x ∷ ls} {suc i} {zero} ⟨ x∉ls , dls ⟩ refl = ⊥-elim (x∉ls (∈-lookup i ls)) -distinct-lookup-inj {.(suc _)} {x ∷ ls} {suc i} {suc j} ⟨ x∉ls , dls ⟩ lsij = +distinct-lookup-inj {ls = x ∷ ls} {suc i} {suc j} ⟨ x∉ls , dls ⟩ lsij = cong suc (distinct-lookup-inj dls lsij) ``` We shall need to convert from an irrelevent proof of distinctness to a -relevant one. In general, this can be accomplished for any decidable -predicate. The following is a decision procedure for whether a vector +relevant one. In general, the laundering of irrelevant proofs into +relevant ones is easy to do when the predicate in question is +decidable. The following is a decision procedure for whether a vector is distinct. - ``` distinct? : ∀{n} → (xs : Vec Name n) → Dec (distinct xs) distinct? [] = yes tt @@ -100,9 +191,9 @@ distinct? (x ∷ xs) ... | no ¬dxs = no λ x₁ → ¬dxs (proj₂ x₁) ``` -With the decision procedure in hand, we can launder an irrelevant -proof into a relevant one. - +With this decision procedure in hand, the define the following +function for laundering irrelevant proofs of distinctness into +relevant ones. ``` distinct-relevant : ∀ {n}{fs : Vec Name n} .(d : distinct fs) → distinct fs distinct-relevant {n}{fs} d @@ -111,35 +202,25 @@ distinct-relevant {n}{fs} d ... | no ¬dfs = ⊥-elimi (¬dfs d) ``` -The fields of one record are a subset of the fields of another record -if every field of the first is also a field of the second. - +The fields of one record are a *subset* of the fields of another +record if every field of the first is also a field of the second. ``` _⊆_ : ∀{n m} → Vec Name n → Vec Name m → Set xs ⊆ ys = (x : Name) → x ∈ xs → x ∈ ys ``` -This subset relation is reflexive. - +This subset relation is reflexive and transitive. ``` ⊆-refl : ∀{n}{ls : Vec Name n} → ls ⊆ ls ⊆-refl {n}{ls} = λ x x∈ls → x∈ls -``` -It is also transitive. - -``` ⊆-trans : ∀{l n m}{ns : Vec Name n}{ms : Vec Name m}{ls : Vec Name l} - → ns ⊆ ms → ms ⊆ ls - → ns ⊆ ls + → ns ⊆ ms → ms ⊆ ls → ns ⊆ ls ⊆-trans {l}{n}{m}{ns}{ms}{ls} ns⊆ms ms⊆ls = λ x z → ms⊆ls x (ns⊆ms x z) ``` - - If `y` is an element of vector `xs`, then `y` is at some index `i` of the vector. - ``` lookup-∈ : ∀{ℓ}{A : Set ℓ}{n} {xs : Vec A n}{y} → y ∈ xs @@ -152,7 +233,6 @@ lookup-∈ {xs = x ∷ xs} (there y∈xs) If one vector `ns` is a subset of another `ms`, then for any element `lookup ns i`, there is an equal element in `ms` at some index. - ``` lookup-⊆ : ∀{n m : ℕ}{ns : Vec Name n}{ms : Vec Name m}{i : Fin n} → ns ⊆ ms @@ -168,17 +248,19 @@ lookup-⊆ {suc n} {m} {x ∷ ns} {ms} {suc i} x∷ns⊆ms = ## Types ``` -infix 5 ｛_⦂_｝ - data Type : Set where _⇒_ : Type → Type → Type `ℕ : Type ｛_⦂_｝ : {n : ℕ} (ls : Vec Name n) (As : Vec Type n) → .{d : distinct ls} → Type ``` -We do not want the details of the proof of distinctness to affect -whether two record types are equal, so we declare that parameter to be -irrelevant by placing a `.` in front of it. +In addition to function types `A ⇒ B` and natural numbers ``ℕ`, we +have the record type `｛ ls ⦂ As ｝`, where `ls` is a vector of field +names and `As` is a vector of types, as discussed above. We require +that the field names be distinct, but we do not want the details of +the proof of distinctness to affect whether two record types are +equal, so we declare that parameter to be irrelevant by placing a `.` +in front of it. ## Subtyping @@ -203,11 +285,26 @@ data _<:_ : Type → Type → Set where → ｛ ks ⦂ Ss ｝ {d1} <: ｛ ls ⦂ Ts ｝ {d2} ``` -The first premise of the record subtyping rule (`<:-rcd`) expresses -_width subtyping_ by requiring that all the labels in `ls` are also in -`ks`. So it allows the hiding of fields when going from a subtype to a -supertype. +The rule `<:-nat` simply states that ``ℕ` is a subtype of itself. +The rule `<:-fun` is the traditional rule for function types, which is +best understood with the following diagram. It answers the question, +when can a function of type `A ⇒ B` be used in place of a function of +type `C ⇒ D`. It shall be called with an argument of type `C`, so +we'll need to convert from `C` to `A`. We can then call the function +to get the result of type `B`. Finally, we need to convert from `B` to +`D`. + + C <: A + ⇓ ⇓ + D :> B + + +The record subtyping rule (`<:-rcd`) characterizes when a record of +one type can safely be used in place of another record type. The +first premise of the rule expresses _width subtyping_ by requiring +that all the field names in `ls` are also in `ks`. So it allows the +hiding of fields when going from a subtype to a supertype. The second premise of the record subtyping rule (`<:-rcd`) expresses _depth subtyping_, that is, it allows the types of the fields to change according to subtyping. The following is an abbreviation for @@ -221,11 +318,11 @@ _⦂_<:_⦂_ {m}{n} ks Ss ls Ts = (∀{i : Fin n}{j : Fin m} ## Subtyping is Reflexive -The proof that subtyping is reflexive does not go by induction on the -type because of the `<:-rcd` rule. We instead use induction on the -size of the type. So we first define size of a type, and the size of a +In this section we prove that subtyping is reflexive, that is, `A <: +A` for any type `A`. The proof does not go by induction on the type +`A` because of the `<:-rcd` rule. We instead use induction on the size +of the type. So we first define size of a type, and the size of a vector of types, as follows. - ``` ty-size : (A : Type) → ℕ vec-ty-size : ∀ {n : ℕ} → (As : Vec Type n) → ℕ @@ -239,7 +336,6 @@ vec-ty-size {n} (x ∷ xs) = ty-size x + vec-ty-size xs ``` The size of a type is always positive. - ``` ty-size-pos : ∀ {A} → 0 < ty-size A ty-size-pos {A ⇒ B} = s≤s z≤n @@ -249,7 +345,6 @@ ty-size-pos {｛ fs ⦂ As ｝ } = s≤s z≤n If a vector of types has a size smaller than `n`, then so is any type in the vector. - ``` lookup-vec-ty-size : ∀{n}{k} {As : Vec Type k} {j} → vec-ty-size As ≤ n @@ -260,7 +355,6 @@ lookup-vec-ty-size {n} {suc k} {A ∷ As} {suc j} As≤n = ``` Here is the proof of reflexivity, by induction on the size of the type. - ``` <:-refl-aux : ∀{n}{A}{m : ty-size A ≤ n} → A <: A <:-refl-aux {0}{A}{m} @@ -270,17 +364,37 @@ Here is the proof of reflexivity, by induction on the size of the type. ... | () <:-refl-aux {suc n}{`ℕ}{m} = <:-nat <:-refl-aux {suc n}{A ⇒ B}{m} = - let a = ≤-pred m in - <:-fun (<:-refl-aux{n}{A}{m+n≤o⇒m≤o (ty-size A) a }) - (<:-refl-aux{n}{B}{m+n≤o⇒n≤o (ty-size A) a}) -<:-refl-aux {suc n}{｛ fs ⦂ As ｝ {d} }{m} = <:-rcd {d1 = d}{d2 = d} ⊆-refl G + let A<:A = <:-refl-aux {n}{A}{m+n≤o⇒m≤o _ (≤-pred m) } in + let B<:B = <:-refl-aux {n}{B}{m+n≤o⇒n≤o _ (≤-pred m) } in + <:-fun A<:A B<:B +<:-refl-aux {suc n}{｛ ls ⦂ As ｝ {d} }{m} = <:-rcd {d1 = d}{d2 = d} ⊆-refl G where - G : fs ⦂ As <: fs ⦂ As + G : ls ⦂ As <: ls ⦂ As G {i}{j} lij rewrite distinct-lookup-inj (distinct-relevant d) lij = let As[i]≤n = lookup-vec-ty-size {As = As}{i} (≤-pred m) in <:-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` +and proceeds by induction on `n`. +* If it is `0`, then we have a contradiction because the size of a type is always positive. + +* If it is `suc n`, we proceed by cases on the type `A`. + + * If it is ``ℕ`, then we have ``ℕ <: `ℕ` by rule `<:-nat`. + * If it is `A ⇒ B`, then by induction we have `A <: A` and `B <: B`. + We conclude that `A ⇒ B <: A ⇒ B` by rule `<:-fun`. + * If it is `｛ ls ⦂ As ｝`, then it suffices to prove that + `ls ⊆ ls` and `ls ⦂ As <: ls ⦂ As`. The former is proved by `⊆-refl`. + 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`. + Because `lookup` is injective on distinct vectors, we have `i ≡ j`. + We then use the induction hypothesis to show that + `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 + is one smaller than the size of `｛ ls ⦂ As ｝`. + +The following corollary packages up reflexivity for ease of use. ``` <:-refl : ∀{A} → A <: A <:-refl {A} = <:-refl-aux {ty-size A}{A}{≤-refl} @@ -302,10 +416,10 @@ already proved the two lemmas needed in the case for `<:-rcd`: <:-trans {.`ℕ} {`ℕ} {.`ℕ} <:-nat <:-nat = <:-nat <:-trans {｛ ls ⦂ As ｝{d1} } {｛ ms ⦂ Bs ｝ {d2} } {｛ ns ⦂ Cs ｝ {d3} } (<:-rcd ms⊆ls As<:Bs) (<:-rcd ns⊆ms Bs<:Cs) = - <:-rcd (⊆-trans ns⊆ms ms⊆ls) G + <:-rcd (⊆-trans ns⊆ms ms⊆ls) As<:Cs where - G : ls ⦂ As <: ns ⦂ Cs - G {i}{j} lij + As<:Cs : ls ⦂ As <: ns ⦂ Cs + As<:Cs {i}{j} lij with lookup-⊆ {i = i} ns⊆ms ... | ⟨ k , lik ⟩ with lookup-⊆ {i = k} ms⊆ls @@ -338,14 +452,14 @@ data _∋_⦂_ : Context → ℕ → Type → Set where → Γ , B ∋ (suc x) ⦂ A ``` - - ## Terms and the typing judgment ``` Id : Set Id = ℕ +``` +``` data Term : Set where `_ : Id → Term ƛ_ : Term → Term @@ -686,13 +800,13 @@ progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L ... | C-zero = step β-zero ... | C-suc CL = step (β-suc (value CL)) progress (⊢μ ⊢M) = step β-μ -progress (⊢# {Γ}{A}{M}{n}{fs}{As}{d}{i}{f} ⊢R lif liA) +progress (⊢# {Γ}{A}{M}{n}{ls}{As}{d}{i}{f} ⊢R lif liA) with progress ⊢R ... | step R—→R′ = step (ξ-# R—→R′) ... | done VR with canonical ⊢R VR -... | C-rcd ⊢Ms dks (<:-rcd fs⊆fs' _) - with lookup-⊆ {i = i} fs⊆fs' +... | C-rcd ⊢Ms dks (<:-rcd ls⊆ls' _) + with lookup-⊆ {i = i} ls⊆ls' ... | ⟨ k , eq ⟩ rewrite eq = step (β-# {j = k} lif) progress (⊢rcd x d) = done V-rcd progress (⊢<: {A = A}{B} ⊢M A<:B) = progress ⊢M @@ -732,7 +846,7 @@ rename-pres ρ⦂ (⊢` ∋w) = ⊢` (ρ⦂ ∋w) rename-pres {ρ = ρ} ρ⦂ (⊢ƛ ⊢N) = ⊢ƛ (rename-pres {ρ = ext ρ} (ext-pres {ρ = ρ} ρ⦂) ⊢N) rename-pres {ρ = ρ} ρ⦂ (⊢· ⊢L ⊢M)= ⊢· (rename-pres {ρ = ρ} ρ⦂ ⊢L) (rename-pres {ρ = ρ} ρ⦂ ⊢M) rename-pres {ρ = ρ} ρ⦂ (⊢μ ⊢M) = ⊢μ (rename-pres {ρ = ext ρ} (ext-pres {ρ = ρ} ρ⦂) ⊢M) -rename-pres ρ⦂ (⊢rcd ⊢Ms dfs) = ⊢rcd (ren-vec-pres ρ⦂ ⊢Ms ) dfs +rename-pres ρ⦂ (⊢rcd ⊢Ms dls) = ⊢rcd (ren-vec-pres ρ⦂ ⊢Ms ) dls rename-pres {ρ = ρ} ρ⦂ (⊢# {d = d} ⊢R lif liA) = ⊢# {d = d}(rename-pres {ρ = ρ} ρ⦂ ⊢R) lif liA rename-pres {ρ = ρ} ρ⦂ (⊢<: ⊢M lt) = ⊢<: (rename-pres {ρ = ρ} ρ⦂ ⊢M) lt rename-pres ρ⦂ ⊢zero = ⊢zero @@ -777,7 +891,7 @@ subst-pres σ⦂ (⊢` eq) = σ⦂ eq subst-pres {σ = σ} σ⦂ (⊢ƛ ⊢N) = ⊢ƛ (subst-pres{σ = exts σ}(exts-pres {σ = σ} σ⦂) ⊢N) subst-pres {σ = σ} σ⦂ (⊢· ⊢L ⊢M) = ⊢· (subst-pres{σ = σ} σ⦂ ⊢L) (subst-pres{σ = σ} σ⦂ ⊢M) subst-pres {σ = σ} σ⦂ (⊢μ ⊢M) = ⊢μ (subst-pres{σ = exts σ} (exts-pres{σ = σ} σ⦂) ⊢M) -subst-pres σ⦂ (⊢rcd ⊢Ms dfs) = ⊢rcd (subst-vec-pres σ⦂ ⊢Ms ) dfs +subst-pres σ⦂ (⊢rcd ⊢Ms dls) = ⊢rcd (subst-vec-pres σ⦂ ⊢Ms ) dls subst-pres {σ = σ} σ⦂ (⊢# {d = d} ⊢R lif liA) = ⊢# {d = d} (subst-pres {σ = σ} σ⦂ ⊢R) lif liA subst-pres {σ = σ} σ⦂ (⊢<: ⊢N lt) = ⊢<: (subst-pres {σ = σ} σ⦂ ⊢N) lt @@ -848,3 +962,115 @@ preserve (⊢# {ls = ls′}{i = i} ⊢M refl refl) (β-# {ls = ks}{Ms}{j = j} ks ⊢<: ⊢Ms[k] (As<:Bs (sym ls′[i]=ks[k])) preserve (⊢<: ⊢M A<:B) M—→N = ⊢<: (preserve ⊢M M—→N) A<:B ``` + +#### Exercise `intrinsic-records` (stretch) + +Formulate the language of this chapter, STLC with records, using +intrinsicaly typed terms. This requires taking an algorithmic approach +to the type system, which means that there is no subsumption rule and +instead subtyping is used in the elimination rules. For example, +the rule for function application would be: + + _·_ : ∀ {Γ A B C} + → Γ ⊢ A ⇒ B + → Γ ⊢ C + → C <: A + ------- + → Γ ⊢ B + +#### Exercise `type-check-records` (practice) + +Write a recursive function whose input is a `Term` and whose output +is a typing derivation for that term, if one exists. + + type-check : (M : Term) → (Γ : Context) → Maybe (Σ[ A ∈ Type ] Γ ⊢ M ⦂ A) + +### Exercise `variants` (recommended) + +Add variants to the language of this Chapter and update the proofs of +progress and preservation. The variant type is a generalization of a +sum type, similar to the way the record type is a generalization of +product. The following summarizes the treatement of variants in the +book Types and Programming Languages. A variant type is traditionally +written: + + 〈l₁:A₁, ..., lᵤ:Aᵤ〉 + +The term for introducing a variant is + + 〈l=t〉 + +and the term for eliminating a variant is + + case L of 〈l₁=x₁〉 ⇒ M₁ | ... | 〈lᵤ=xᵤ〉 ⇒ Mᵤ + +The typing rules for these terms are + + (T-Variant) + Γ ⊢ Mⱼ : Aⱼ + --------------------------------- + Γ ⊢ 〈lⱼ=Mⱼ〉 : 〈l₁=A₁, ... , lᵤ=Aᵤ〉 + + + (T-Case) + Γ ⊢ L : 〈l₁=A₁, ... , lᵤ=Aᵤ〉 + ∀ i ∈ 1..u, Γ,xᵢ:Aᵢ ⊢ Mᵢ : B + --------------------------------------------------- + Γ ⊢ case L of 〈l₁=x₁〉 ⇒ M₁ | ... | 〈lᵤ=xᵤ〉 ⇒ Mᵤ : B + +The non-algorithmic subtyping rules for variants are + + (S-VariantWidth) + ------------------------------------------------------------ + 〈l₁=A₁, ..., lᵤ=Aᵤ〉 <: 〈l₁=A₁, ..., lᵤ=Aᵤ, ..., lᵤ₊ₓ=Aᵤ₊ₓ〉 + + (S-VariantDepth) + ∀ i ∈ 1..u, Aᵢ <: Bᵢ + --------------------------------------------- + 〈l₁=A₁, ..., lᵤ=Aᵤ〉 <: 〈l₁=B₁, ..., lᵤ=Bᵤ〉 + + (S-VariantPerm) + ∀i∈1..u, ∃j∈1..u, kⱼ = lᵢ and Aⱼ = Bᵢ + ---------------------------------------------- + 〈k₁=A₁, ..., kᵤ=Aᵤ〉 <: 〈l₁=B₁, ..., lᵤ=Bᵤ〉 + +Come up with an algorithmic subtyping rule for variant types. + +### Exercise `<:-alternative` (stretch) + +Revise this formalization of records with subtyping (including proofs +of progress and preservation) to use the non-algorithmic subtyping +rules for Chapter 15 of TAPL, which we list here: + + (S-RcdWidth) + -------------------------------------------------------------- + { l₁:A₁, ..., lᵤ:Aᵤ, ..., lᵤ₊ₓ:Aᵤ₊ₓ } <: { l₁:A₁, ..., lᵤ:Aᵤ } + + (S-RcdDepth) + ∀i∈1..u, Aᵢ <: Bᵢ + ---------------------------------------------- + { l₁:A₁, ..., lᵤ:Aᵤ } <: { l₁:B₁, ..., lᵤ:Bᵤ } + + (S-RcdPerm) + ∀i∈1..u, ∃j∈1..u, kⱼ = lᵢ and Aⱼ = Bᵢ + ---------------------------------------------- + { k₁:A₁, ..., kᵤ:Aᵤ } <: { l₁:B₁, ..., lᵤ:Bᵤ } + +You will most likely need to prove inversion lemmas for the subtype relation +of the form: + + If S <: T₁ ⇒ T₂, then S ≡ S₁ ⇒ S₂, T₁ <: S₁, and S₂ <: T₂, for some S₁, S₂. + + If S <: { lᵢ : Tᵢ | i ∈ 1..n }, then S ≡ { kⱼ : Sⱼ | j ∈ 1..m } + and { lᵢ | i ∈ 1..n } ⊆ { kⱼ | j ∈ 1..m } + and Sⱼ <: Tᵢ for every i and j such that lᵢ = kⱼ. + +## References + +* Reynolds 1980 + +* Cardelli 1984 + +* Liskov + +* Types and Programming Languages. Benjamin C. Pierce. The MIT Press. 2002.