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

text through <:-refl

Browse source
This commit is contained in:
Jeremy Siek 2020-07-16 14:55:03 -04:00
parent b6b128c337
commit a8682af3d4
1 changed files with 290 additions and 64 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -10,6 +10,68 @@ next : /Bisimulation/
module plfa.part2.Subtyping where 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 ## 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.Membership.Propositional.Properties using (∈-lookup)
open import Data.Vec.Relation.Unary.Any using (here; there) open import Data.Vec.Relation.Unary.Any using (here; there)
import Relation.Binary.PropositionalEquality as Eq 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; ¬_) open import Relation.Nullary using (Dec; yes; no; ¬_)
``` ```
## Syntax ## 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 _⊢*_⦂_
infix 4 _∋_⦂_ infix 4 _∋_⦂_
infixl 5 _,_ infixl 5 _,_
infix 5 _[_]
infixr 7 _⇒_ infixr 7 _⇒_
@ -46,22 +113,47 @@ infixl 7 _·_
infix 8 `suc_ infix 8 `suc_
infix 9 `_ infix 9 `_
infixl 7 _#_ infixl 7 _#_
infix 4 _⊆_
infix 5 ｛_⦂_｝
infix 5 ｛_:=_｝
``` ```
## Record Fields and their Properties
## Record Field Names, Functions and Properties We represent field names as strings.
We represent field identifiers (aka. names) as strings.
``` ```
Name : Set Name : Set
Name = String Name = String
``` ```
The field identifiers of a record will be stored in a sequence, A record is traditionally written as follows
specifically Agda's `Vec` type. We require that the field names of a
record be distinct, which we define 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 : ∀{A : Set}{n} → Vec A n → Set
distinct [] = ⊤ distinct [] = ⊤
@ -69,25 +161,24 @@ distinct (x ∷ xs) = ¬ (x ∈ xs) × distinct xs
``` ```
For vectors of distinct elements, lookup is injective. For vectors of distinct elements, lookup is injective.
``` ```
distinct-lookup-inj : ∀ {n}{ls : Vec Name n}{i j : Fin n} distinct-lookup-inj : ∀ {n}{ls : Vec Name n}{i j : Fin n}
→ distinct ls → lookup ls i ≡ lookup ls j → distinct ls → lookup ls i ≡ lookup ls j
→ i ≡ j → i ≡ j
distinct-lookup-inj {.(suc _)} {x ∷ ls} {zero} {zero} ⟨ x∉ls , dls ⟩ lsij = refl distinct-lookup-inj {ls = 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} {suc j} ⟨ x∉ls , dls ⟩ refl =
⊥-elim (x∉ls (∈-lookup j ls)) ⊥-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)) ⊥-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) cong suc (distinct-lookup-inj dls lsij)
``` ```
We shall need to convert from an irrelevent proof of distinctness to a We shall need to convert from an irrelevent proof of distinctness to a
relevant one. In general, this can be accomplished for any decidable relevant one. In general, the laundering of irrelevant proofs into
predicate. The following is a decision procedure for whether a vector 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. is distinct.
``` ```
distinct? : ∀{n} → (xs : Vec Name n) → Dec (distinct xs) distinct? : ∀{n} → (xs : Vec Name n) → Dec (distinct xs)
distinct? [] = yes tt distinct? [] = yes tt
@ -100,9 +191,9 @@ distinct? (x ∷ xs)
... | no ¬dxs = no λ x₁ → ¬dxs (proj₂ x₁) ... | no ¬dxs = no λ x₁ → ¬dxs (proj₂ x₁)
``` ```
With the decision procedure in hand, we can launder an irrelevant With this decision procedure in hand, the define the following
proof into a relevant one. 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 : Vec Name n} .(d : distinct fs) → distinct fs
distinct-relevant {n}{fs} d distinct-relevant {n}{fs} d
@ -111,35 +202,25 @@ distinct-relevant {n}{fs} d
... | no ¬dfs = ⊥-elimi (¬dfs d) ... | no ¬dfs = ⊥-elimi (¬dfs d)
``` ```
The fields of one record are a subset of the fields of another record The fields of one record are a *subset* of the fields of another
if every field of the first is also a field of the second. record if every field of the first is also a field of the second.
``` ```
_⊆_ : ∀{n m} → Vec Name n → Vec Name m → Set _⊆_ : ∀{n m} → Vec Name n → Vec Name m → Set
xs ⊆ ys = (x : Name) → x ∈ xs → x ∈ ys 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 : Vec Name n} → ls ⊆ ls
⊆-refl {n}{ls} = λ x x∈ls → x∈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} ⊆-trans : ∀{l n m}{ns : Vec Name n}{ms : Vec Name m}{ls : Vec Name l}
→ ns ⊆ ms → ms ⊆ ls → ns ⊆ ms → ms ⊆ ls → ns ⊆ ls
→ ns ⊆ ls
⊆-trans {l}{n}{m}{ns}{ms}{ls} ns⊆ms ms⊆ls = λ x z → ms⊆ls x (ns⊆ms x z) ⊆-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 If `y` is an element of vector `xs`, then `y` is at some index `i` of
the vector. the vector.
``` ```
lookup-∈ : ∀{ℓ}{A : Set ℓ}{n} {xs : Vec A n}{y} lookup-∈ : ∀{ℓ}{A : Set ℓ}{n} {xs : Vec A n}{y}
→ y ∈ xs → 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 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 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} lookup-⊆ : ∀{n m : ℕ}{ns : Vec Name n}{ms : Vec Name m}{i : Fin n}
→ ns ⊆ ms → ns ⊆ ms
@ -168,17 +248,19 @@ lookup-⊆ {suc n} {m} {x ∷ ns} {ms} {suc i} x∷ns⊆ms =
## Types ## Types
``` ```
infix 5 ｛_⦂_｝
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
``` ```
We do not want the details of the proof of distinctness to affect In addition to function types `A ⇒ B` and natural numbers ``ℕ`, we
whether two record types are equal, so we declare that parameter to be have the record type `｛ ls ⦂ As ｝`, where `ls` is a vector of field
irrelevant by placing a `.` in front of it. 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 ## Subtyping
@ -203,11 +285,26 @@ data _<:_ : Type → Type → Set where
→ ｛ ks ⦂ Ss ｝ {d1} <: ｛ ls ⦂ Ts ｝ {d2} → ｛ ks ⦂ Ss ｝ {d1} <: ｛ ls ⦂ Ts ｝ {d2}
``` ```
The first premise of the record subtyping rule (`<:-rcd`) expresses The rule `<:-nat` simply states that ``ℕ` is a subtype of itself.
_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 `<:-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 The second premise of the record subtyping rule (`<:-rcd`) expresses
_depth subtyping_, that is, it allows the types of the fields to _depth subtyping_, that is, it allows the types of the fields to
change according to subtyping. The following is an abbreviation for 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 ## Subtyping is Reflexive
The proof that subtyping is reflexive does not go by induction on the In this section we prove that subtyping is reflexive, that is, `A <:
type because of the `<:-rcd` rule. We instead use induction on the A` for any type `A`. The proof does not go by induction on the type
size of the type. So we first define size of a type, and the size of a `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. vector of types, as follows.
``` ```
ty-size : (A : Type) → ℕ ty-size : (A : Type) → ℕ
vec-ty-size : ∀ {n : ℕ} → (As : Vec Type n) → ℕ 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. The size of a type is always positive.
``` ```
ty-size-pos : ∀ {A} → 0 < ty-size A ty-size-pos : ∀ {A} → 0 < ty-size A
ty-size-pos {A ⇒ B} = s≤s z≤n 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 If a vector of types has a size smaller than `n`, then so is any type
in the vector. in the vector.
``` ```
lookup-vec-ty-size : ∀{n}{k} {As : Vec Type k} {j} lookup-vec-ty-size : ∀{n}{k} {As : Vec Type k} {j}
→ vec-ty-size As ≤ n → 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. 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 : ∀{n}{A}{m : ty-size A ≤ n} → A <: A
<:-refl-aux {0}{A}{m} <:-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}{`ℕ}{m} = <:-nat
<:-refl-aux {suc n}{A ⇒ B}{m} = <:-refl-aux {suc n}{A ⇒ B}{m} =
let a = ≤-pred m in let A<:A = <:-refl-aux {n}{A}{m+n≤o⇒m≤o _ (≤-pred m) } in
<:-fun (<:-refl-aux{n}{A}{m+n≤o⇒m≤o (ty-size A) a }) let B<:B = <:-refl-aux {n}{B}{m+n≤o⇒n≤o _ (≤-pred m) } in
(<:-refl-aux{n}{B}{m+n≤o⇒n≤o (ty-size A) a}) <:-fun A<:A B<:B
<:-refl-aux {suc n}{｛ fs ⦂ As ｝ {d} }{m} = <:-rcd {d1 = d}{d2 = d} ⊆-refl G <:-refl-aux {suc n}{｛ ls ⦂ As ｝ {d} }{m} = <:-rcd {d1 = d}{d2 = d} ⊆-refl G
where where
G : fs ⦂ As <: fs ⦂ 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 = lookup-vec-ty-size {As = As}{i} (≤-pred m) in let As[i]≤n = 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`
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} → A <: A
<:-refl {A} = <:-refl-aux {ty-size A}{A}{≤-refl} <:-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 {.`ℕ} {`ℕ} {.`ℕ} <:-nat <:-nat = <:-nat
<:-trans {｛ ls ⦂ As ｝{d1} } {｛ ms ⦂ Bs ｝ {d2} } {｛ ns ⦂ Cs ｝ {d3} } <:-trans {｛ ls ⦂ As ｝{d1} } {｛ ms ⦂ Bs ｝ {d2} } {｛ ns ⦂ Cs ｝ {d3} }
(<:-rcd ms⊆ls As<:Bs) (<:-rcd ns⊆ms Bs<:Cs) = (<:-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 where
G : ls ⦂ As <: ns ⦂ Cs As<:Cs : ls ⦂ As <: ns ⦂ Cs
G {i}{j} lij As<:Cs {i}{j} lij
with lookup-⊆ {i = i} ns⊆ms with lookup-⊆ {i = i} ns⊆ms
... | ⟨ k , lik ⟩ ... | ⟨ k , lik ⟩
with lookup-⊆ {i = k} ms⊆ls with lookup-⊆ {i = k} ms⊆ls
@ -338,14 +452,14 @@ data _∋_⦂_ : Context → ℕ → Type → Set where
→ Γ , B ∋ (suc x) ⦂ A → Γ , B ∋ (suc x) ⦂ A
``` ```
## Terms and the typing judgment ## Terms and the typing judgment
``` ```
Id : Set Id : Set
Id = ℕ Id = ℕ
```
```
data Term : Set where data Term : Set where
`_ : Id → Term `_ : Id → Term
ƛ_ : Term → Term ƛ_ : Term → Term
@ -686,13 +800,13 @@ progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L
... | C-zero = step β-zero ... | C-zero = step β-zero
... | C-suc CL = step (β-suc (value CL)) ... | C-suc CL = step (β-suc (value CL))
progress (⊢μ ⊢M) = step β-μ 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 with progress ⊢R
... | step R—→R′ = step (ξ-# R—→R′) ... | step R—→R′ = step (ξ-# R—→R′)
... | done VR ... | done VR
with canonical ⊢R VR with canonical ⊢R VR
... | C-rcd ⊢Ms dks (<:-rcd fs⊆fs' _) ... | C-rcd ⊢Ms dks (<:-rcd ls⊆ls' _)
with lookup-⊆ {i = i} fs⊆fs' with lookup-⊆ {i = i} ls⊆ls'
... | ⟨ k , eq ⟩ rewrite eq = step (β-# {j = k} lif) ... | ⟨ k , eq ⟩ rewrite eq = step (β-# {j = k} lif)
progress (⊢rcd x d) = done V-rcd progress (⊢rcd x d) = done V-rcd
progress (⊢<: {A = A}{B} ⊢M A<:B) = progress ⊢M 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 {ρ = ρ} ρ⦂ (⊢ƛ ⊢N) = ⊢ƛ (rename-pres {ρ = ext ρ} (ext-pres {ρ = ρ} ρ⦂) ⊢N)
rename-pres {ρ = ρ} ρ⦂ (⊢· ⊢L ⊢M)= ⊢· (rename-pres {ρ = ρ} ρ⦂ ⊢L) (rename-pres {ρ = ρ} ρ⦂ ⊢M) rename-pres {ρ = ρ} ρ⦂ (⊢· ⊢L ⊢M)= ⊢· (rename-pres {ρ = ρ} ρ⦂ ⊢L) (rename-pres {ρ = ρ} ρ⦂ ⊢M)
rename-pres {ρ = ρ} ρ⦂ (⊢μ ⊢M) = ⊢μ (rename-pres {ρ = ext ρ} (ext-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 {ρ = ρ} ρ⦂ (⊢# {d = d} ⊢R lif liA) = ⊢# {d = d}(rename-pres {ρ = ρ} ρ⦂ ⊢R) lif liA
rename-pres {ρ = ρ} ρ⦂ (⊢<: ⊢M lt) = ⊢<: (rename-pres {ρ = ρ} ρ⦂ ⊢M) lt rename-pres {ρ = ρ} ρ⦂ (⊢<: ⊢M lt) = ⊢<: (rename-pres {ρ = ρ} ρ⦂ ⊢M) lt
rename-pres ρ⦂ ⊢zero = ⊢zero rename-pres ρ⦂ ⊢zero = ⊢zero
@ -777,7 +891,7 @@ 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 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) = subst-pres {σ = σ} σ⦂ (⊢# {d = d} ⊢R lif liA) =
⊢# {d = d} (subst-pres {σ = σ} σ⦂ ⊢R) lif liA ⊢# {d = d} (subst-pres {σ = σ} σ⦂ ⊢R) lif liA
subst-pres {σ = σ} σ⦂ (⊢<: ⊢N lt) = ⊢<: (subst-pres {σ = σ} σ⦂ ⊢N) lt 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])) ⊢<: ⊢Ms[k] (As<:Bs (sym ls′[i]=ks[k]))
preserve (⊢<: ⊢M A<:B) M—→N = ⊢<: (preserve ⊢M M—→N) A<:B 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.