SubSubtyping
Require Import SfLib.
Require Import Maps.
Require Import Types.
Concepts
A Motivating Example
Person = {name:String, age:Nat} Student = {name:String, age:Nat, gpa:Nat}
(\r:Person. (r.age)+1) {name="Pat",age=21,gpa=1}is not typable, since it applies a function that wants a one-field record to an argument that actually provides two fields, while the T_App rule demands that the domain type of the function being applied must match the type of the argument precisely.
Subtyping and Object-Oriented Languages
The Subsumption Rule
- Defining a binary subtype relation between types.
- Enriching the typing relation to take subtyping into account.
Γ ⊢ t : S S <: T | (T_Sub) |
Γ ⊢ t : T |
The Subtype Relation
Structural Rules
S <: U U <: T | (S_Trans) |
S <: T |
(S_Refl) | |
T <: T |
Products
S_{1} <: T_{1} S_{2} <: T_{2} | (S_Prod) |
S_{1} * S_{2} <: T_{1} * T_{2} |
Arrows
f : C → Student
g : (C→Person) → D
That is, f is a function that yields a record of type Student,
and g is a (higher-order) function that expects its argument to be
a function yielding a record of type Person. Also suppose that
Student is a subtype of Person. Then the application g f is
safe even though their types do not match up precisely, because
the only thing g can do with f is to apply it to some
argument (of type C); the result will actually be a Student,
while g will be expecting a Person, but this is safe because
the only thing g can then do is to project out the two fields
that it knows about (name and age), and these will certainly
be among the fields that are present.
g : (C→Person) → D
S_{2} <: T_{2} | (S_Arrow_Co) |
S_{1} → S_{2} <: S_{1} → T_{2} |
T_{1} <: S_{1} S_{2} <: T_{2} | (S_Arrow) |
S_{1} → S_{2} <: T_{1} → T_{2} |
f : Person → C
g : (Student → C) → D
The application g f is safe, because the only thing the body of
g can do with f is to apply it to some argument of type
Student. Since f requires records having (at least) the
fields of a Person, this will always work. So Person → C is a
subtype of Student → C since Student is a subtype of
Person.
g : (Student → C) → D
Records
{name:String, age:Nat, gpa:Nat} <: {name:String, age:Nat}
{name:String, age:Nat} <: {name:String} {name:String} <: {}
This is known as "width subtyping" for records.
{name:String, age:Nat} <: {name:String} {name:String} <: {}
{x:Student} <: {x:Person}
This is known as "depth subtyping".
{name:String,age:Nat} <: {age:Nat,name:String}
This is known as "permutation subtyping".
∀jk in j_{1}..jn, | |
∃ip in i_{1}..im, such that | |
jk=ip and Sp <: Tk | (S_Rcd) |
{i_{1}:S_{1}...im:Sm} <: {j_{1}:T_{1}...jn:Tn} |
n > m | (S_RcdWidth) |
{i_{1}:T_{1}...in:Tn} <: {i_{1}:T_{1}...im:Tm} |
S_{1} <: T_{1} ... Sn <: Tn | (S_RcdDepth) |
{i_{1}:S_{1}...in:Sn} <: {i_{1}:T_{1}...in:Tn} |
{i_{1}:S_{1}...in:Sn} is a permutation of {i_{1}:T_{1}...in:Tn} | (S_RcdPerm) |
{i_{1}:S_{1}...in:Sn} <: {i_{1}:T_{1}...in:Tn} |
- A subclass may not change the argument or result types of a
method of its superclass (i.e., no depth subtyping or no arrow
subtyping, depending how you look at it).
- Each class member (field or method) can be assigned a single
index, adding new indices "on the right" as more members are
added in subclasses (i.e., no permutation for classes).
- A class may implement multiple interfaces — so-called "multiple inheritance" of interfaces (i.e., permutation is allowed for interfaces).
Exercise: 2 stars, recommended (arrow_sub_wrong)
Suppose we had incorrectly defined subtyping as covariant on both the right and the left of arrow types:S_{1} <: T_{1} S_{2} <: T_{2} | (S_Arrow_wrong) |
S_{1} → S_{2} <: T_{1} → T_{2} |
f : Student → Nat
g : (Person → Nat) → Nat
... such that the application g f will get stuck during
execution.
g : (Person → Nat) → Nat
Top
(S_Top) | |
S <: Top |
Summary
- adding a base type Top,
- adding the rule of subsumption
to the typing relation, andΓ ⊢ t : S S <: T (T_Sub) Γ ⊢ t : T - defining a subtype relation as follows:
S <: U U <: T (S_Trans) S <: T (S_Refl) T <: T (S_Top) S <: Top S_{1} <: T_{1} S_{2} <: T_{2} (S_Prod) S_{1} * S_{2} <: T_{1} * T_{2} T_{1} <: S_{1} S_{2} <: T_{2} (S_Arrow) S_{1} → S_{2} <: T_{1} → T_{2} n > m (S_RcdWidth) {i_{1}:T_{1}...in:Tn} <: {i_{1}:T_{1}...im:Tm} S_{1} <: T_{1} ... Sn <: Tn (S_RcdDepth) {i_{1}:S_{1}...in:Sn} <: {i_{1}:T_{1}...in:Tn} {i_{1}:S_{1}...in:Sn} is a permutation of {i_{1}:T_{1}...in:Tn} (S_RcdPerm) {i_{1}:S_{1}...in:Sn} <: {i_{1}:T_{1}...in:Tn}
Exercises
Exercise: 1 star, optional (subtype_instances_tf_1)
Suppose we have types S, T, U, and V with S <: T and U <: V. Which of the following subtyping assertions are then true? Write true or false after each one. (A, B, and C here are base types.)- T→S <: T→S
- Top→U <: S→Top
- (C→C) → (A*B) <: (C→C) → (Top*B)
- T→T→U <: S→S→V
- (T→T)→U <: (S→S)→V
- ((T→S)→T)→U <: ((S→T)→S)→V
- S*V <: T*U
Exercise: 2 stars (subtype_order)
The following types happen to form a linear order with respect to subtyping:- Top
- Top → Student
- Student → Person
- Student → Top
- Person → Student
Exercise: 1 star (subtype_instances_tf_2)
Which of the following statements are true? Write true or false after each one.
∀S T,
S <: T →
S→S <: T→T
∀S,
S <: A→A →
∃T,
S = T→T ∧ T <: A
∀S T_{1} T_{2},
(S <: T_{1} → T_{2}) →
∃S_{1} S_{2},
S = S_{1} → S_{2} ∧ T_{1} <: S_{1} ∧ S_{2} <: T_{2}
∃S,
S <: S→S
∃S,
S→S <: S
∀S T_{1} T_{2},
S <: T_{1}*T_{2} →
∃S_{1} S_{2},
S = S_{1}*S_{2} ∧ S_{1} <: T_{1} ∧ S_{2} <: T_{2}
☐
S <: T →
S→S <: T→T
∀S,
S <: A→A →
∃T,
S = T→T ∧ T <: A
∀S T_{1} T_{2},
(S <: T_{1} → T_{2}) →
∃S_{1} S_{2},
S = S_{1} → S_{2} ∧ T_{1} <: S_{1} ∧ S_{2} <: T_{2}
∃S,
S <: S→S
∃S,
S→S <: S
∀S T_{1} T_{2},
S <: T_{1}*T_{2} →
∃S_{1} S_{2},
S = S_{1}*S_{2} ∧ S_{1} <: T_{1} ∧ S_{2} <: T_{2}
Exercise: 1 star (subtype_concepts_tf)
Which of the following statements are true, and which are false?- There exists a type that is a supertype of every other type.
- There exists a type that is a subtype of every other type.
- There exists a pair type that is a supertype of every other
pair type.
- There exists a pair type that is a subtype of every other
pair type.
- There exists an arrow type that is a supertype of every other
arrow type.
- There exists an arrow type that is a subtype of every other
arrow type.
- There is an infinite descending chain of distinct types in the
subtype relation—-that is, an infinite sequence of types
S_{0}, S_{1}, etc., such that all the Si's are different and
each S(i+1) is a subtype of Si.
- There is an infinite ascending chain of distinct types in the subtype relation—-that is, an infinite sequence of types S_{0}, S_{1}, etc., such that all the Si's are different and each S(i+1) is a supertype of Si.
Exercise: 2 stars (proper_subtypes)
Is the following statement true or false? Briefly explain your answer.
∀T,
~(∃n, T = TBase n) →
∃S,
S <: T ∧ S ≠ T
☐
~(∃n, T = TBase n) →
∃S,
S <: T ∧ S ≠ T
Exercise: 2 stars (small_large_1)
- What is the smallest type T ("smallest" in the subtype
relation) that makes the following assertion true? (Assume we
have Unit among the base types and unit as a constant of this
type.)
empty ⊢ (\p:T*Top. p.fst) ((\z:A.z), unit) : A→A
- What is the largest type T that makes the same assertion true?
Exercise: 2 stars (small_large_2)
- What is the smallest type T that makes the following
assertion true?
empty ⊢ (\p:(A→A * B→B). p) ((\z:A.z), (\z:B.z)) : T
- What is the largest type T that makes the same assertion true?
Exercise: 2 stars, optional (small_large_3)
- What is the smallest type T that makes the following
assertion true?
a:A ⊢ (\p:(A*T). (p.snd) (p.fst)) (a , \z:A.z) : A
- What is the largest type T that makes the same assertion true?
Exercise: 2 stars (small_large_4)
- What is the smallest type T that makes the following
assertion true?
∃S,
empty ⊢ (\p:(A*T). (p.snd) (p.fst)) : S - What is the largest type T that makes the same assertion true?
Exercise: 2 stars (smallest_1)
What is the smallest type T that makes the following assertion true?
∃S, ∃t,
empty ⊢ (\x:T. x x) t : S
☐
empty ⊢ (\x:T. x x) t : S
Exercise: 2 stars (smallest_2)
What is the smallest type T that makes the following assertion true?
empty ⊢ (\x:Top. x) ((\z:A.z) , (\z:B.z)) : T
☐
Exercise: 3 stars, optional (count_supertypes)
How many supertypes does the record type {x:A, y:C→C} have? That is, how many different types T are there such that {x:A, y:C→C} <: T? (We consider two types to be different if they are written differently, even if each is a subtype of the other. For example, {x:A,y:B} and {y:B,x:A} are different.)Exercise: 2 stars (pair_permutation)
The subtyping rule for product typesS_{1} <: T_{1} S_{2} <: T_{2} | (S_Prod) |
S_{1}*S_{2} <: T_{1}*T_{2} |
T_{1}*T_{2} <: T_{2}*T_{1} |
Formal Definitions
Syntax
Inductive ty : Type :=
| TTop : ty
| TBool : ty
| TBase : id → ty
| TArrow : ty → ty → ty
| TUnit : ty
.
Inductive tm : Type :=
| tvar : id → tm
| tapp : tm → tm → tm
| tabs : id → ty → tm → tm
| ttrue : tm
| tfalse : tm
| tif : tm → tm → tm → tm
| tunit : tm
.
Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
match t with
| tvar y ⇒
if beq_id x y then s else t
| tabs y T t_{1} ⇒
tabs y T (if beq_id x y then t_{1} else (subst x s t_{1}))
| tapp t_{1} t_{2} ⇒
tapp (subst x s t_{1}) (subst x s t_{2})
| ttrue ⇒
ttrue
| tfalse ⇒
tfalse
| tif t_{1} t_{2} t_{3} ⇒
tif (subst x s t_{1}) (subst x s t_{2}) (subst x s t_{3})
| tunit ⇒
tunit
end.
Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).
Inductive value : tm → Prop :=
| v_abs : ∀x T t,
value (tabs x T t)
| v_true :
value ttrue
| v_false :
value tfalse
| v_unit :
value tunit
.
Hint Constructors value.
Reserved Notation "t_{1} '⇒' t_{2}" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀x T t_{12} v_{2},
value v_{2} →
(tapp (tabs x T t_{12}) v_{2}) ⇒ [x:=v_{2}]t_{12}
| ST_App1 : ∀t_{1} t_{1}' t_{2},
t_{1} ⇒ t_{1}' →
(tapp t_{1} t_{2}) ⇒ (tapp t_{1}' t_{2})
| ST_App2 : ∀v_{1} t_{2} t_{2}',
value v_{1} →
t_{2} ⇒ t_{2}' →
(tapp v_{1} t_{2}) ⇒ (tapp v_{1} t_{2}')
| ST_IfTrue : ∀t_{1} t_{2},
(tif ttrue t_{1} t_{2}) ⇒ t_{1}
| ST_IfFalse : ∀t_{1} t_{2},
(tif tfalse t_{1} t_{2}) ⇒ t_{2}
| ST_If : ∀t_{1} t_{1}' t_{2} t_{3},
t_{1} ⇒ t_{1}' →
(tif t_{1} t_{2} t_{3}) ⇒ (tif t_{1}' t_{2} t_{3})
where "t_{1} '⇒' t_{2}" := (step t_{1} t_{2}).
Hint Constructors step.
Subtyping
Reserved Notation "T '<:' U" (at level 40).
Inductive subtype : ty → ty → Prop :=
| S_Refl : ∀T,
T <: T
| S_Trans : ∀S U T,
S <: U →
U <: T →
S <: T
| S_Top : ∀S,
S <: TTop
| S_Arrow : ∀S_{1} S_{2} T_{1} T_{2},
T_{1} <: S_{1} →
S_{2} <: T_{2} →
(TArrow S_{1} S_{2}) <: (TArrow T_{1} T_{2})
where "T '<:' U" := (subtype T U).
Note that we don't need any special rules for base types: they are
automatically subtypes of themselves (by S_Refl) and Top (by
S_Top), and that's all we want.
Hint Constructors subtype.
Module Examples.
Notation x := (Id 0).
Notation y := (Id 1).
Notation z := (Id 2).
Notation A := (TBase (Id 6)).
Notation B := (TBase (Id 7)).
Notation C := (TBase (Id 8)).
Notation String := (TBase (Id 9)).
Notation Float := (TBase (Id 10)).
Notation Integer := (TBase (Id 11)).
Example subtyping_example_0 :
(TArrow C TBool) <: (TArrow C TTop).
(* C->Bool <: C->Top *)
Proof. auto. Qed.
Exercise: 2 stars, optional (subtyping_judgements)
(Wait to do this exercise after you have added product types to the language — see exercise products — at least up to this point in the file).
Person := { name : String }
Student := { name : String ;
gpa : Float }
Employee := { name : String ;
ssn : Integer }
Student := { name : String ;
gpa : Float }
Employee := { name : String ;
ssn : Integer }
Definition Person : ty :=
(* FILL IN HERE *) admit.
Definition Student : ty :=
(* FILL IN HERE *) admit.
Definition Employee : ty :=
(* FILL IN HERE *) admit.
(* FILL IN HERE *) admit.
Definition Student : ty :=
(* FILL IN HERE *) admit.
Definition Employee : ty :=
(* FILL IN HERE *) admit.
Now use the definition of the subtype relation to prove the following:
Example sub_student_person :
Student <: Person.
Proof.
(* FILL IN HERE *) Admitted.
Example sub_employee_person :
Employee <: Person.
Proof.
(* FILL IN HERE *) Admitted.
☐
The following facts are mostly easy to prove in Coq. To get
full benefit from the exercises, make sure you also
understand how to prove them on paper!
Exercise: 1 star, optional (subtyping_example_1)
Example subtyping_example_1 :
(TArrow TTop Student) <: (TArrow (TArrow C C) Person).
(* Top->Student <: (C->C)->Person *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
(TArrow TTop Student) <: (TArrow (TArrow C C) Person).
(* Top->Student <: (C->C)->Person *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
Example subtyping_example_2 :
(TArrow TTop Person) <: (TArrow Person TTop).
(* Top->Person <: Person->Top *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
(TArrow TTop Person) <: (TArrow Person TTop).
(* Top->Person <: Person->Top *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
End Examples.
Definition context := partial_map ty.
Reserved Notation "Gamma '⊢' t '∈' T" (at level 40).
Inductive has_type : context → tm → ty → Prop :=
(* Same as before *)
| T_Var : ∀Γ x T,
Γ x = Some T →
Γ ⊢ (tvar x) ∈ T
| T_Abs : ∀Γ x T_{11} T_{12} t_{12},
(update Γ x T_{11}) ⊢ t_{12} ∈ T_{12} →
Γ ⊢ (tabs x T_{11} t_{12}) ∈ (TArrow T_{11} T_{12})
| T_App : ∀T_{1} T_{2} Γ t_{1} t_{2},
Γ ⊢ t_{1} ∈ (TArrow T_{1} T_{2}) →
Γ ⊢ t_{2} ∈ T_{1} →
Γ ⊢ (tapp t_{1} t_{2}) ∈ T_{2}
| T_True : ∀Γ,
Γ ⊢ ttrue ∈ TBool
| T_False : ∀Γ,
Γ ⊢ tfalse ∈ TBool
| T_If : ∀t_{1} t_{2} t_{3} T Γ,
Γ ⊢ t_{1} ∈ TBool →
Γ ⊢ t_{2} ∈ T →
Γ ⊢ t_{3} ∈ T →
Γ ⊢ (tif t_{1} t_{2} t_{3}) ∈ T
| T_Unit : ∀Γ,
Γ ⊢ tunit ∈ TUnit
(* New rule of subsumption *)
| T_Sub : ∀Γ t S T,
Γ ⊢ t ∈ S →
S <: T →
Γ ⊢ t ∈ T
where "Gamma '⊢' t '∈' T" := (has_type Γ t T).
Hint Constructors has_type.
The following hints help auto and eauto construct typing
derivations. (See chapter UseAuto for more on hints.)
Hint Extern 2 (has_type _ (tapp _ _) _) ⇒
eapply T_App; auto.
Hint Extern 2 (_ = _) ⇒ compute; reflexivity.
Module Examples2.
Import Examples.
Do the following exercises after you have added product types to
the language. For each informal typing judgement, write it as a
formal statement in Coq and prove it.
Exercise: 1 star, optional (typing_example_0)
(* empty |- ((\z:A.z), (\z:B.z))
: (A->A * B->B) *)
(* FILL IN HERE *)
: (A->A * B->B) *)
(* FILL IN HERE *)
(* empty |- (\x:(Top * B->B). x.snd) ((\z:A.z), (\z:B.z))
: B->B *)
(* FILL IN HERE *)
: B->B *)
(* FILL IN HERE *)
(* empty |- (\z:(C->C)->(Top * B->B). (z (\x:C.x)).snd)
(\z:C->C. ((\z:A.z), (\z:B.z)))
: B->B *)
(* FILL IN HERE *)
(\z:C->C. ((\z:A.z), (\z:B.z)))
: B->B *)
(* FILL IN HERE *)
☐
End Examples2.
Properties
Inversion Lemmas for Subtyping
- Bool is the only subtype of Bool, and
- every subtype of an arrow type is itself an arrow type.
Exercise: 2 stars, optional (sub_inversion_Bool)
Lemma sub_inversion_Bool : ∀U,
U <: TBool →
U = TBool.
U <: TBool →
U = TBool.
Proof with auto.
intros U Hs.
remember TBool as V.
(* FILL IN HERE *) Admitted.
intros U Hs.
remember TBool as V.
(* FILL IN HERE *) Admitted.
Lemma sub_inversion_arrow : ∀U V_{1} V_{2},
U <: (TArrow V_{1} V_{2}) →
∃U_{1}, ∃U_{2},
U = (TArrow U_{1} U_{2}) ∧ (V_{1} <: U_{1}) ∧ (U_{2} <: V_{2}).
U <: (TArrow V_{1} V_{2}) →
∃U_{1}, ∃U_{2},
U = (TArrow U_{1} U_{2}) ∧ (V_{1} <: U_{1}) ∧ (U_{2} <: V_{2}).
Proof with eauto.
intros U V_{1} V_{2} Hs.
remember (TArrow V_{1} V_{2}) as V.
generalize dependent V_{2}. generalize dependent V_{1}.
(* FILL IN HERE *) Admitted.
intros U V_{1} V_{2} Hs.
remember (TArrow V_{1} V_{2}) as V.
generalize dependent V_{2}. generalize dependent V_{1}.
(* FILL IN HERE *) Admitted.
☐
Canonical Forms
Exercise: 3 stars, optional (canonical_forms_of_arrow_types)
Lemma canonical_forms_of_arrow_types : ∀Γ s T_{1} T_{2},
Γ ⊢ s ∈ (TArrow T_{1} T_{2}) →
value s →
∃x, ∃S_{1}, ∃s_{2},
s = tabs x S_{1} s_{2}.
Γ ⊢ s ∈ (TArrow T_{1} T_{2}) →
value s →
∃x, ∃S_{1}, ∃s_{2},
s = tabs x S_{1} s_{2}.
Proof with eauto.
(* FILL IN HERE *) Admitted.
(* FILL IN HERE *) Admitted.
☐
Similarly, the canonical forms of type Bool are the constants
true and false.
Lemma canonical_forms_of_Bool : ∀Γ s,
Γ ⊢ s ∈ TBool →
value s →
(s = ttrue ∨ s = tfalse).
Proof with eauto.
intros Γ s Hty Hv.
remember TBool as T.
induction Hty; try solve by inversion...
- (* T_Sub *)
subst. apply sub_inversion_Bool in H. subst...
Qed.
intros Γ s Hty Hv.
remember TBool as T.
induction Hty; try solve by inversion...
- (* T_Sub *)
subst. apply sub_inversion_Bool in H. subst...
Qed.
Progress
- If the last step in the typing derivation uses rule T_App,
then there are terms t_{1} t_{2} and types T_{1} and T_{2} such that
t = t_{1} t_{2}, T = T_{2}, empty ⊢ t_{1} : T_{1} → T_{2}, and empty ⊢
t_{2} : T_{1}. Moreover, by the induction hypothesis, either t_{1} is
a value or it steps, and either t_{2} is a value or it steps.
There are three possibilities to consider:
- Suppose t_{1} ⇒ t_{1}' for some term t_{1}'. Then t_{1} t_{2} ⇒ t_{1}' t_{2}
by ST_App1.
- Suppose t_{1} is a value and t_{2} ⇒ t_{2}' for some term t_{2}'.
Then t_{1} t_{2} ⇒ t_{1} t_{2}' by rule ST_App2 because t_{1} is a
value.
- Finally, suppose t_{1} and t_{2} are both values. By the lemma
about canonical forms for arrow types, we know that t_{1} has the
form \x:S_{1}.s2 for some x, S_{1}, and s_{2}. But then
(\x:S_{1}.s2) t_{2} ⇒ [x:=t_{2}]s_{2} by ST_AppAbs, since t_{2} is a
value.
- Suppose t_{1} ⇒ t_{1}' for some term t_{1}'. Then t_{1} t_{2} ⇒ t_{1}' t_{2}
by ST_App1.
- If the final step of the derivation uses rule T_If, then there
are terms t_{1}, t_{2}, and t_{3} such that t = if t_{1} then t_{2} else
t_{3}, with empty ⊢ t_{1} : Bool and with empty ⊢ t_{2} : T and
empty ⊢ t_{3} : T. Moreover, by the induction hypothesis,
either t_{1} is a value or it steps.
- If t_{1} is a value, then by the canonical forms lemma for
booleans, either t_{1} = true or t_{1} = false. In either
case, t can step, using rule ST_IfTrue or ST_IfFalse.
- If t_{1} can step, then so can t, by rule ST_If.
- If t_{1} is a value, then by the canonical forms lemma for
booleans, either t_{1} = true or t_{1} = false. In either
case, t can step, using rule ST_IfTrue or ST_IfFalse.
- If the final step of the derivation is by T_Sub, then there is a type S such that S <: T and empty ⊢ t : S. The desired result is exactly the induction hypothesis for the typing subderivation.
Theorem progress : ∀t T,
empty ⊢ t ∈ T →
value t ∨ ∃t', t ⇒ t'.
Proof with eauto.
intros t T Ht.
remember empty as Γ.
revert HeqGamma.
induction Ht;
intros HeqGamma; subst...
- (* T_Var *)
inversion H.
- (* T_App *)
right.
destruct IHHt1; subst...
+ (* t_{1} is a value *)
destruct IHHt2; subst...
* (* t_{2} is a value *)
destruct (canonical_forms_of_arrow_types empty t_{1} T_{1} T_{2})
as [x [S_{1} [t_{12} Heqt1]]]...
subst. ∃([x:=t_{2}]t_{12})...
* (* t_{2} steps *)
inversion H_{0} as [t_{2}' Hstp]. ∃(tapp t_{1} t_{2}')...
+ (* t_{1} steps *)
inversion H as [t_{1}' Hstp]. ∃(tapp t_{1}' t_{2})...
- (* T_If *)
right.
destruct IHHt1.
+ (* t_{1} is a value *) eauto.
+ assert (t_{1} = ttrue ∨ t_{1} = tfalse)
by (eapply canonical_forms_of_Bool; eauto).
inversion H_{0}; subst...
+ inversion H. rename x into t_{1}'. eauto.
Qed.
intros t T Ht.
remember empty as Γ.
revert HeqGamma.
induction Ht;
intros HeqGamma; subst...
- (* T_Var *)
inversion H.
- (* T_App *)
right.
destruct IHHt1; subst...
+ (* t_{1} is a value *)
destruct IHHt2; subst...
* (* t_{2} is a value *)
destruct (canonical_forms_of_arrow_types empty t_{1} T_{1} T_{2})
as [x [S_{1} [t_{12} Heqt1]]]...
subst. ∃([x:=t_{2}]t_{12})...
* (* t_{2} steps *)
inversion H_{0} as [t_{2}' Hstp]. ∃(tapp t_{1} t_{2}')...
+ (* t_{1} steps *)
inversion H as [t_{1}' Hstp]. ∃(tapp t_{1}' t_{2})...
- (* T_If *)
right.
destruct IHHt1.
+ (* t_{1} is a value *) eauto.
+ assert (t_{1} = ttrue ∨ t_{1} = tfalse)
by (eapply canonical_forms_of_Bool; eauto).
inversion H_{0}; subst...
+ inversion H. rename x into t_{1}'. eauto.
Qed.
Inversion Lemmas for Typing
- If the last step of the derivation is a use of T_Abs then
there is a type T_{12} such that T = S_{1} → T_{12} and Γ,
x:S_{1} ⊢ t_{2} : T_{12}. Picking T_{12} for S_{2} gives us what we
need: S_{1} → T_{12} <: S_{1} → T_{12} follows from S_Refl.
- If the last step of the derivation is a use of T_Sub then there is a type S such that S <: T and Γ ⊢ \x:S_{1}.t2 : S. The IH for the typing subderivation tell us that there is some type S_{2} with S_{1} → S_{2} <: S and Γ, x:S_{1} ⊢ t_{2} : S_{2}. Picking type S_{2} gives us what we need, since S_{1} → S_{2} <: T then follows by S_Trans.
Lemma typing_inversion_abs : ∀Γ x S_{1} t_{2} T,
Γ ⊢ (tabs x S_{1} t_{2}) ∈ T →
(∃S_{2}, (TArrow S_{1} S_{2}) <: T
∧ (update Γ x S_{1}) ⊢ t_{2} ∈ S_{2}).
Proof with eauto.
intros Γ x S_{1} t_{2} T H.
remember (tabs x S_{1} t_{2}) as t.
induction H;
inversion Heqt; subst; intros; try solve by inversion.
- (* T_Abs *)
∃T_{12}...
- (* T_Sub *)
destruct IHhas_type as [S_{2} [Hsub Hty]]...
Qed.
intros Γ x S_{1} t_{2} T H.
remember (tabs x S_{1} t_{2}) as t.
induction H;
inversion Heqt; subst; intros; try solve by inversion.
- (* T_Abs *)
∃T_{12}...
- (* T_Sub *)
destruct IHhas_type as [S_{2} [Hsub Hty]]...
Qed.
Similarly...
Lemma typing_inversion_var : ∀Γ x T,
Γ ⊢ (tvar x) ∈ T →
∃S,
Γ x = Some S ∧ S <: T.
Proof with eauto.
intros Γ x T Hty.
remember (tvar x) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_Var *)
∃T...
- (* T_Sub *)
destruct IHHty as [U [Hctx HsubU]]... Qed.
intros Γ x T Hty.
remember (tvar x) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_Var *)
∃T...
- (* T_Sub *)
destruct IHHty as [U [Hctx HsubU]]... Qed.
Lemma typing_inversion_app : ∀Γ t_{1} t_{2} T_{2},
Γ ⊢ (tapp t_{1} t_{2}) ∈ T_{2} →
∃T_{1},
Γ ⊢ t_{1} ∈ (TArrow T_{1} T_{2}) ∧
Γ ⊢ t_{2} ∈ T_{1}.
Proof with eauto.
intros Γ t_{1} t_{2} T_{2} Hty.
remember (tapp t_{1} t_{2}) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_App *)
∃T_{1}...
- (* T_Sub *)
destruct IHHty as [U_{1} [Hty1 Hty2]]...
Qed.
intros Γ t_{1} t_{2} T_{2} Hty.
remember (tapp t_{1} t_{2}) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_App *)
∃T_{1}...
- (* T_Sub *)
destruct IHHty as [U_{1} [Hty1 Hty2]]...
Qed.
Lemma typing_inversion_true : ∀Γ T,
Γ ⊢ ttrue ∈ T →
TBool <: T.
Proof with eauto.
intros Γ T Htyp. remember ttrue as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
intros Γ T Htyp. remember ttrue as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
Lemma typing_inversion_false : ∀Γ T,
Γ ⊢ tfalse ∈ T →
TBool <: T.
Proof with eauto.
intros Γ T Htyp. remember tfalse as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
intros Γ T Htyp. remember tfalse as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
Lemma typing_inversion_if : ∀Γ t_{1} t_{2} t_{3} T,
Γ ⊢ (tif t_{1} t_{2} t_{3}) ∈ T →
Γ ⊢ t_{1} ∈ TBool
∧ Γ ⊢ t_{2} ∈ T
∧ Γ ⊢ t_{3} ∈ T.
Proof with eauto.
intros Γ t_{1} t_{2} t_{3} T Hty.
remember (tif t_{1} t_{2} t_{3}) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_If *)
auto.
- (* T_Sub *)
destruct (IHHty H_{0}) as [H_{1} [H_{2} H_{3}]]...
Qed.
intros Γ t_{1} t_{2} t_{3} T Hty.
remember (tif t_{1} t_{2} t_{3}) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_If *)
auto.
- (* T_Sub *)
destruct (IHHty H_{0}) as [H_{1} [H_{2} H_{3}]]...
Qed.
Lemma typing_inversion_unit : ∀Γ T,
Γ ⊢ tunit ∈ T →
TUnit <: T.
Proof with eauto.
intros Γ T Htyp. remember tunit as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
intros Γ T Htyp. remember tunit as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
The inversion lemmas for typing and for subtyping between arrow
types can be packaged up as a useful "combination lemma" telling
us exactly what we'll actually require below.
Lemma abs_arrow : ∀x S_{1} s_{2} T_{1} T_{2},
empty ⊢ (tabs x S_{1} s_{2}) ∈ (TArrow T_{1} T_{2}) →
T_{1} <: S_{1}
∧ (update empty x S_{1}) ⊢ s_{2} ∈ T_{2}.
Proof with eauto.
intros x S_{1} s_{2} T_{1} T_{2} Hty.
apply typing_inversion_abs in Hty.
inversion Hty as [S_{2} [Hsub Hty1]].
apply sub_inversion_arrow in Hsub.
inversion Hsub as [U_{1} [U_{2} [Heq [Hsub1 Hsub2]]]].
inversion Heq; subst... Qed.
intros x S_{1} s_{2} T_{1} T_{2} Hty.
apply typing_inversion_abs in Hty.
inversion Hty as [S_{2} [Hsub Hty1]].
apply sub_inversion_arrow in Hsub.
inversion Hsub as [U_{1} [U_{2} [Heq [Hsub1 Hsub2]]]].
inversion Heq; subst... Qed.
Inductive appears_free_in : id → tm → Prop :=
| afi_var : ∀x,
appears_free_in x (tvar x)
| afi_app1 : ∀x t_{1} t_{2},
appears_free_in x t_{1} → appears_free_in x (tapp t_{1} t_{2})
| afi_app2 : ∀x t_{1} t_{2},
appears_free_in x t_{2} → appears_free_in x (tapp t_{1} t_{2})
| afi_abs : ∀x y T_{11} t_{12},
y ≠ x →
appears_free_in x t_{12} →
appears_free_in x (tabs y T_{11} t_{12})
| afi_if_{1} : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{1} →
appears_free_in x (tif t_{1} t_{2} t_{3})
| afi_if_{2} : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{2} →
appears_free_in x (tif t_{1} t_{2} t_{3})
| afi_if_{3} : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{3} →
appears_free_in x (tif t_{1} t_{2} t_{3})
.
Hint Constructors appears_free_in.
Lemma context_invariance : ∀Γ Γ' t S,
Γ ⊢ t ∈ S →
(∀x, appears_free_in x t → Γ x = Γ' x) →
Γ' ⊢ t ∈ S.
Proof with eauto.
intros. generalize dependent Γ'.
induction H;
intros Γ' Heqv...
- (* T_Var *)
apply T_Var... rewrite ← Heqv...
- (* T_Abs *)
apply T_Abs... apply IHhas_type. intros x_{0} Hafi.
unfold update, t_update. destruct (beq_idP x x_{0})...
- (* T_If *)
apply T_If...
Qed.
intros. generalize dependent Γ'.
induction H;
intros Γ' Heqv...
- (* T_Var *)
apply T_Var... rewrite ← Heqv...
- (* T_Abs *)
apply T_Abs... apply IHhas_type. intros x_{0} Hafi.
unfold update, t_update. destruct (beq_idP x x_{0})...
- (* T_If *)
apply T_If...
Qed.
Lemma free_in_context : ∀x t T Γ,
appears_free_in x t →
Γ ⊢ t ∈ T →
∃T', Γ x = Some T'.
Proof with eauto.
intros x t T Γ Hafi Htyp.
induction Htyp;
subst; inversion Hafi; subst...
- (* T_Abs *)
destruct (IHHtyp H_{4}) as [T Hctx]. ∃T.
unfold update, t_update in Hctx.
rewrite ← beq_id_false_iff in H_{2}.
rewrite H_{2} in Hctx... Qed.
intros x t T Γ Hafi Htyp.
induction Htyp;
subst; inversion Hafi; subst...
- (* T_Abs *)
destruct (IHHtyp H_{4}) as [T Hctx]. ∃T.
unfold update, t_update in Hctx.
rewrite ← beq_id_false_iff in H_{2}.
rewrite H_{2} in Hctx... Qed.
Substitution
Lemma substitution_preserves_typing : ∀Γ x U v t S,
(update Γ x U) ⊢ t ∈ S →
empty ⊢ v ∈ U →
Γ ⊢ ([x:=v]t) ∈ S.
Proof with eauto.
intros Γ x U v t S Htypt Htypv.
generalize dependent S. generalize dependent Γ.
induction t; intros; simpl.
- (* tvar *)
rename i into y.
destruct (typing_inversion_var _ _ _ Htypt)
as [T [Hctx Hsub]].
unfold update, t_update in Hctx.
destruct (beq_idP x y) as [Hxy|Hxy]; eauto;
subst.
inversion Hctx; subst. clear Hctx.
apply context_invariance with empty...
intros x Hcontra.
destruct (free_in_context _ _ S empty Hcontra)
as [T' HT']...
inversion HT'.
- (* tapp *)
destruct (typing_inversion_app _ _ _ _ Htypt)
as [T_{1} [Htypt1 Htypt2]].
eapply T_App...
- (* tabs *)
rename i into y. rename t into T_{1}.
destruct (typing_inversion_abs _ _ _ _ _ Htypt)
as [T_{2} [Hsub Htypt2]].
apply T_Sub with (TArrow T_{1} T_{2})... apply T_Abs...
destruct (beq_idP x y) as [Hxy|Hxy].
+ (* x=y *)
eapply context_invariance...
subst.
intros x Hafi. unfold update, t_update.
destruct (beq_id y x)...
+ (* x<>y *)
apply IHt. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (beq_idP y z)...
subst.
rewrite ← beq_id_false_iff in Hxy. rewrite Hxy...
- (* ttrue *)
assert (TBool <: S)
by apply (typing_inversion_true _ _ Htypt)...
- (* tfalse *)
assert (TBool <: S)
by apply (typing_inversion_false _ _ Htypt)...
- (* tif *)
assert ((update Γ x U) ⊢ t_{1} ∈ TBool
∧ (update Γ x U) ⊢ t_{2} ∈ S
∧ (update Γ x U) ⊢ t_{3} ∈ S)
by apply (typing_inversion_if _ _ _ _ _ Htypt).
inversion H as [H_{1} [H_{2} H_{3}]].
apply IHt1 in H_{1}. apply IHt2 in H_{2}. apply IHt3 in H_{3}.
auto.
- (* tunit *)
assert (TUnit <: S)
by apply (typing_inversion_unit _ _ Htypt)...
Qed.
intros Γ x U v t S Htypt Htypv.
generalize dependent S. generalize dependent Γ.
induction t; intros; simpl.
- (* tvar *)
rename i into y.
destruct (typing_inversion_var _ _ _ Htypt)
as [T [Hctx Hsub]].
unfold update, t_update in Hctx.
destruct (beq_idP x y) as [Hxy|Hxy]; eauto;
subst.
inversion Hctx; subst. clear Hctx.
apply context_invariance with empty...
intros x Hcontra.
destruct (free_in_context _ _ S empty Hcontra)
as [T' HT']...
inversion HT'.
- (* tapp *)
destruct (typing_inversion_app _ _ _ _ Htypt)
as [T_{1} [Htypt1 Htypt2]].
eapply T_App...
- (* tabs *)
rename i into y. rename t into T_{1}.
destruct (typing_inversion_abs _ _ _ _ _ Htypt)
as [T_{2} [Hsub Htypt2]].
apply T_Sub with (TArrow T_{1} T_{2})... apply T_Abs...
destruct (beq_idP x y) as [Hxy|Hxy].
+ (* x=y *)
eapply context_invariance...
subst.
intros x Hafi. unfold update, t_update.
destruct (beq_id y x)...
+ (* x<>y *)
apply IHt. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (beq_idP y z)...
subst.
rewrite ← beq_id_false_iff in Hxy. rewrite Hxy...
- (* ttrue *)
assert (TBool <: S)
by apply (typing_inversion_true _ _ Htypt)...
- (* tfalse *)
assert (TBool <: S)
by apply (typing_inversion_false _ _ Htypt)...
- (* tif *)
assert ((update Γ x U) ⊢ t_{1} ∈ TBool
∧ (update Γ x U) ⊢ t_{2} ∈ S
∧ (update Γ x U) ⊢ t_{3} ∈ S)
by apply (typing_inversion_if _ _ _ _ _ Htypt).
inversion H as [H_{1} [H_{2} H_{3}]].
apply IHt1 in H_{1}. apply IHt2 in H_{2}. apply IHt3 in H_{3}.
auto.
- (* tunit *)
assert (TUnit <: S)
by apply (typing_inversion_unit _ _ Htypt)...
Qed.
Preservation
- If the final step of the derivation is by T_App, then there
are terms t_{1} and t_{2} and types T_{1} and T_{2} such that
t = t_{1} t_{2}, T = T_{2}, empty ⊢ t_{1} : T_{1} → T_{2}, and
empty ⊢ t_{2} : T_{1}.
- If the final step of the derivation uses rule T_If, then
there are terms t_{1}, t_{2}, and t_{3} such that t = if t_{1} then
t_{2} else t_{3}, with empty ⊢ t_{1} : Bool and with empty ⊢ t_{2} :
T and empty ⊢ t_{3} : T. Moreover, by the induction
hypothesis, if t_{1} steps to t_{1}' then empty ⊢ t_{1}' : Bool.
There are three cases to consider, depending on which rule was
used to show t ⇒ t'.
- If t ⇒ t' by rule ST_If, then t' = if t_{1}' then t_{2}
else t_{3} with t_{1} ⇒ t_{1}'. By the induction hypothesis,
empty ⊢ t_{1}' : Bool, and so empty ⊢ t' : T by T_If.
- If t ⇒ t' by rule ST_IfTrue or ST_IfFalse, then
either t' = t_{2} or t' = t_{3}, and empty ⊢ t' : T
follows by assumption.
- If t ⇒ t' by rule ST_If, then t' = if t_{1}' then t_{2}
else t_{3} with t_{1} ⇒ t_{1}'. By the induction hypothesis,
empty ⊢ t_{1}' : Bool, and so empty ⊢ t' : T by T_If.
- If the final step of the derivation uses rule T_If, then
there are terms t_{1}, t_{2}, and t_{3} such that t = if t_{1} then
t_{2} else t_{3}, with empty ⊢ t_{1} : Bool and with empty ⊢ t_{2} :
T and empty ⊢ t_{3} : T. Moreover, by the induction
hypothesis, if t_{1} steps to t_{1}' then empty ⊢ t_{1}' : Bool.
There are three cases to consider, depending on which rule was
used to show t ⇒ t'.
- If the final step of the derivation is by T_Sub, then there is a type S such that S <: T and empty ⊢ t : S. The result is immediate by the induction hypothesis for the typing subderivation and an application of T_Sub. ☐
Theorem preservation : ∀t t' T,
empty ⊢ t ∈ T →
t ⇒ t' →
empty ⊢ t' ∈ T.
Proof with eauto.
intros t t' T HT.
remember empty as Γ. generalize dependent HeqGamma.
generalize dependent t'.
induction HT;
intros t' HeqGamma HE; subst; inversion HE; subst...
- (* T_App *)
inversion HE; subst...
+ (* ST_AppAbs *)
destruct (abs_arrow _ _ _ _ _ HT_{1}) as [HA_{1} HA_{2}].
apply substitution_preserves_typing with T...
Qed.
intros t t' T HT.
remember empty as Γ. generalize dependent HeqGamma.
generalize dependent t'.
induction HT;
intros t' HeqGamma HE; subst; inversion HE; subst...
- (* T_App *)
inversion HE; subst...
+ (* ST_AppAbs *)
destruct (abs_arrow _ _ _ _ _ HT_{1}) as [HA_{1} HA_{2}].
apply substitution_preserves_typing with T...
Qed.
Records, via Products and Top
{a:Nat, b:Nat} ----> {Nat,Nat} i.e., (Nat,(Nat,Top)) {c:Nat, a:Nat} ----> {Nat,Top,Nat} i.e., (Nat,(Top,(Nat,Top)))The encoding of record values doesn't change at all. It is easy (and instructive) to check that the subtyping rules above are validated by the encoding.
Exercises
Exercise: 2 stars (variations)
Each part of this problem suggests a different way of changing the definition of the STLC with Unit and subtyping. (These changes are not cumulative: each part starts from the original language.) In each part, list which properties (Progress, Preservation, both, or neither) become false. If a property becomes false, give a counterexample.- Suppose we add the following typing rule:
Γ ⊢ t : S_{1}->S_{2} S_{1} <: T_{1} T_{1} <: S_{1} S_{2} <: T_{2} (T_Funny1) Γ ⊢ t : T_{1}->T_{2} - Suppose we add the following reduction rule:
(ST_Funny21) unit ⇒ (\x:Top. x) - Suppose we add the following subtyping rule:
(S_Funny3) Unit <: Top->Top - Suppose we add the following subtyping rule:
(S_Funny4) Top->Top <: Unit - Suppose we add the following reduction rule:
(ST_Funny5) (unit t) ⇒ (t unit) - Suppose we add the same reduction rule and a new typing rule:
(ST_Funny5) (unit t) ⇒ (t unit) (T_Funny6) empty ⊢ Unit : Top->Top - Suppose we change the arrow subtyping rule to:
S_{1} <: T_{1} S_{2} <: T_{2} (S_Arrow') S_{1}->S_{2} <: T_{1}->T_{2}
Exercise: Adding Products
Exercise: 4 stars (products)
Adding pairs, projections, and product types to the system we have defined is a relatively straightforward matter. Carry out this extension:- Add constructors for pairs, first and second projections, and
product types to the definitions of ty and tm. (Don't
forget to add corresponding cases to T_cases and t_cases.)
- Extend the substitution function and value relation as in
chapter MoreSTLC.
- Extend the operational semantics with the same reduction rules
as in chapter MoreSTLC.
- Extend the subtyping relation with this rule:
S_{1} <: T_{1} S_{2} <: T_{2} (Sub_Prod) S_{1} * S_{2} <: T_{1} * T_{2} - Extend the typing relation with the same rules for pairs and
projections as in chapter MoreSTLC.
- Extend the proofs of progress, preservation, and all their supporting lemmas to deal with the new constructs. (You'll also need to add some completely new lemmas.)