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
S1 <: T1 S2 <: T2 | (S_Prod) |
S1 * S2 <: T1 * T2 |
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
S2 <: T2 | (S_Arrow_Co) |
S1 → S2 <: S1 → T2 |
T1 <: S1 S2 <: T2 | (S_Arrow) |
S1 → S2 <: T1 → T2 |
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 j1..jn, | |
∃ip in i1..im, such that | |
jk=ip and Sp <: Tk | (S_Rcd) |
{i1:S1...im:Sm} <: {j1:T1...jn:Tn} |
n > m | (S_RcdWidth) |
{i1:T1...in:Tn} <: {i1:T1...im:Tm} |
S1 <: T1 ... Sn <: Tn | (S_RcdDepth) |
{i1:S1...in:Sn} <: {i1:T1...in:Tn} |
{i1:S1...in:Sn} is a permutation of {i1:T1...in:Tn} | (S_RcdPerm) |
{i1:S1...in:Sn} <: {i1:T1...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:S1 <: T1 S2 <: T2 | (S_Arrow_wrong) |
S1 → S2 <: T1 → T2 |
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 S1 <: T1 S2 <: T2 (S_Prod) S1 * S2 <: T1 * T2 T1 <: S1 S2 <: T2 (S_Arrow) S1 → S2 <: T1 → T2 n > m (S_RcdWidth) {i1:T1...in:Tn} <: {i1:T1...im:Tm} S1 <: T1 ... Sn <: Tn (S_RcdDepth) {i1:S1...in:Sn} <: {i1:T1...in:Tn} {i1:S1...in:Sn} is a permutation of {i1:T1...in:Tn} (S_RcdPerm) {i1:S1...in:Sn} <: {i1:T1...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 T1 T2,
(S <: T1 → T2) →
∃S1 S2,
S = S1 → S2 ∧ T1 <: S1 ∧ S2 <: T2
∃S,
S <: S→S
∃S,
S→S <: S
∀S T1 T2,
S <: T1*T2 →
∃S1 S2,
S = S1*S2 ∧ S1 <: T1 ∧ S2 <: T2
☐
S <: T →
S→S <: T→T
∀S,
S <: A→A →
∃T,
S = T→T ∧ T <: A
∀S T1 T2,
(S <: T1 → T2) →
∃S1 S2,
S = S1 → S2 ∧ T1 <: S1 ∧ S2 <: T2
∃S,
S <: S→S
∃S,
S→S <: S
∀S T1 T2,
S <: T1*T2 →
∃S1 S2,
S = S1*S2 ∧ S1 <: T1 ∧ S2 <: T2
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
S0, S1, 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 S0, S1, 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 typesS1 <: T1 S2 <: T2 | (S_Prod) |
S1*S2 <: T1*T2 |
T1*T2 <: T2*T1 |
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 t1 ⇒
tabs y T (if beq_id x y then t1 else (subst x s t1))
| tapp t1 t2 ⇒
tapp (subst x s t1) (subst x s t2)
| ttrue ⇒
ttrue
| tfalse ⇒
tfalse
| tif t1 t2 t3 ⇒
tif (subst x s t1) (subst x s t2) (subst x s t3)
| 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 "t1 '⇒' t2" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀x T t12 v2,
value v2 →
(tapp (tabs x T t12) v2) ⇒ [x:=v2]t12
| ST_App1 : ∀t1 t1' t2,
t1 ⇒ t1' →
(tapp t1 t2) ⇒ (tapp t1' t2)
| ST_App2 : ∀v1 t2 t2',
value v1 →
t2 ⇒ t2' →
(tapp v1 t2) ⇒ (tapp v1 t2')
| ST_IfTrue : ∀t1 t2,
(tif ttrue t1 t2) ⇒ t1
| ST_IfFalse : ∀t1 t2,
(tif tfalse t1 t2) ⇒ t2
| ST_If : ∀t1 t1' t2 t3,
t1 ⇒ t1' →
(tif t1 t2 t3) ⇒ (tif t1' t2 t3)
where "t1 '⇒' t2" := (step t1 t2).
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 : ∀S1 S2 T1 T2,
T1 <: S1 →
S2 <: T2 →
(TArrow S1 S2) <: (TArrow T1 T2)
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 T11 T12 t12,
(update Γ x T11) ⊢ t12 ∈ T12 →
Γ ⊢ (tabs x T11 t12) ∈ (TArrow T11 T12)
| T_App : ∀T1 T2 Γ t1 t2,
Γ ⊢ t1 ∈ (TArrow T1 T2) →
Γ ⊢ t2 ∈ T1 →
Γ ⊢ (tapp t1 t2) ∈ T2
| T_True : ∀Γ,
Γ ⊢ ttrue ∈ TBool
| T_False : ∀Γ,
Γ ⊢ tfalse ∈ TBool
| T_If : ∀t1 t2 t3 T Γ,
Γ ⊢ t1 ∈ TBool →
Γ ⊢ t2 ∈ T →
Γ ⊢ t3 ∈ T →
Γ ⊢ (tif t1 t2 t3) ∈ 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 V1 V2,
U <: (TArrow V1 V2) →
∃U1, ∃U2,
U = (TArrow U1 U2) ∧ (V1 <: U1) ∧ (U2 <: V2).
U <: (TArrow V1 V2) →
∃U1, ∃U2,
U = (TArrow U1 U2) ∧ (V1 <: U1) ∧ (U2 <: V2).
Proof with eauto.
intros U V1 V2 Hs.
remember (TArrow V1 V2) as V.
generalize dependent V2. generalize dependent V1.
(* FILL IN HERE *) Admitted.
intros U V1 V2 Hs.
remember (TArrow V1 V2) as V.
generalize dependent V2. generalize dependent V1.
(* FILL IN HERE *) Admitted.
☐
Canonical Forms
Exercise: 3 stars, optional (canonical_forms_of_arrow_types)
Lemma canonical_forms_of_arrow_types : ∀Γ s T1 T2,
Γ ⊢ s ∈ (TArrow T1 T2) →
value s →
∃x, ∃S1, ∃s2,
s = tabs x S1 s2.
Γ ⊢ s ∈ (TArrow T1 T2) →
value s →
∃x, ∃S1, ∃s2,
s = tabs x S1 s2.
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 t1 t2 and types T1 and T2 such that
t = t1 t2, T = T2, empty ⊢ t1 : T1 → T2, and empty ⊢
t2 : T1. Moreover, by the induction hypothesis, either t1 is
a value or it steps, and either t2 is a value or it steps.
There are three possibilities to consider:
- Suppose t1 ⇒ t1' for some term t1'. Then t1 t2 ⇒ t1' t2
by ST_App1.
- Suppose t1 is a value and t2 ⇒ t2' for some term t2'.
Then t1 t2 ⇒ t1 t2' by rule ST_App2 because t1 is a
value.
- Finally, suppose t1 and t2 are both values. By the lemma
about canonical forms for arrow types, we know that t1 has the
form \x:S1.s2 for some x, S1, and s2. But then
(\x:S1.s2) t2 ⇒ [x:=t2]s2 by ST_AppAbs, since t2 is a
value.
- Suppose t1 ⇒ t1' for some term t1'. Then t1 t2 ⇒ t1' t2
by ST_App1.
- If the final step of the derivation uses rule T_If, then there
are terms t1, t2, and t3 such that t = if t1 then t2 else
t3, with empty ⊢ t1 : Bool and with empty ⊢ t2 : T and
empty ⊢ t3 : T. Moreover, by the induction hypothesis,
either t1 is a value or it steps.
- If t1 is a value, then by the canonical forms lemma for
booleans, either t1 = true or t1 = false. In either
case, t can step, using rule ST_IfTrue or ST_IfFalse.
- If t1 can step, then so can t, by rule ST_If.
- If t1 is a value, then by the canonical forms lemma for
booleans, either t1 = true or t1 = 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...
+ (* t1 is a value *)
destruct IHHt2; subst...
* (* t2 is a value *)
destruct (canonical_forms_of_arrow_types empty t1 T1 T2)
as [x [S1 [t12 Heqt1]]]...
subst. ∃([x:=t2]t12)...
* (* t2 steps *)
inversion H0 as [t2' Hstp]. ∃(tapp t1 t2')...
+ (* t1 steps *)
inversion H as [t1' Hstp]. ∃(tapp t1' t2)...
- (* T_If *)
right.
destruct IHHt1.
+ (* t1 is a value *) eauto.
+ assert (t1 = ttrue ∨ t1 = tfalse)
by (eapply canonical_forms_of_Bool; eauto).
inversion H0; subst...
+ inversion H. rename x into t1'. 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...
+ (* t1 is a value *)
destruct IHHt2; subst...
* (* t2 is a value *)
destruct (canonical_forms_of_arrow_types empty t1 T1 T2)
as [x [S1 [t12 Heqt1]]]...
subst. ∃([x:=t2]t12)...
* (* t2 steps *)
inversion H0 as [t2' Hstp]. ∃(tapp t1 t2')...
+ (* t1 steps *)
inversion H as [t1' Hstp]. ∃(tapp t1' t2)...
- (* T_If *)
right.
destruct IHHt1.
+ (* t1 is a value *) eauto.
+ assert (t1 = ttrue ∨ t1 = tfalse)
by (eapply canonical_forms_of_Bool; eauto).
inversion H0; subst...
+ inversion H. rename x into t1'. eauto.
Qed.
Inversion Lemmas for Typing
- If the last step of the derivation is a use of T_Abs then
there is a type T12 such that T = S1 → T12 and Γ,
x:S1 ⊢ t2 : T12. Picking T12 for S2 gives us what we
need: S1 → T12 <: S1 → T12 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:S1.t2 : S. The IH for the typing subderivation tell us that there is some type S2 with S1 → S2 <: S and Γ, x:S1 ⊢ t2 : S2. Picking type S2 gives us what we need, since S1 → S2 <: T then follows by S_Trans.
Lemma typing_inversion_abs : ∀Γ x S1 t2 T,
Γ ⊢ (tabs x S1 t2) ∈ T →
(∃S2, (TArrow S1 S2) <: T
∧ (update Γ x S1) ⊢ t2 ∈ S2).
Proof with eauto.
intros Γ x S1 t2 T H.
remember (tabs x S1 t2) as t.
induction H;
inversion Heqt; subst; intros; try solve by inversion.
- (* T_Abs *)
∃T12...
- (* T_Sub *)
destruct IHhas_type as [S2 [Hsub Hty]]...
Qed.
intros Γ x S1 t2 T H.
remember (tabs x S1 t2) as t.
induction H;
inversion Heqt; subst; intros; try solve by inversion.
- (* T_Abs *)
∃T12...
- (* T_Sub *)
destruct IHhas_type as [S2 [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 : ∀Γ t1 t2 T2,
Γ ⊢ (tapp t1 t2) ∈ T2 →
∃T1,
Γ ⊢ t1 ∈ (TArrow T1 T2) ∧
Γ ⊢ t2 ∈ T1.
Proof with eauto.
intros Γ t1 t2 T2 Hty.
remember (tapp t1 t2) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_App *)
∃T1...
- (* T_Sub *)
destruct IHHty as [U1 [Hty1 Hty2]]...
Qed.
intros Γ t1 t2 T2 Hty.
remember (tapp t1 t2) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_App *)
∃T1...
- (* T_Sub *)
destruct IHHty as [U1 [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 : ∀Γ t1 t2 t3 T,
Γ ⊢ (tif t1 t2 t3) ∈ T →
Γ ⊢ t1 ∈ TBool
∧ Γ ⊢ t2 ∈ T
∧ Γ ⊢ t3 ∈ T.
Proof with eauto.
intros Γ t1 t2 t3 T Hty.
remember (tif t1 t2 t3) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_If *)
auto.
- (* T_Sub *)
destruct (IHHty H0) as [H1 [H2 H3]]...
Qed.
intros Γ t1 t2 t3 T Hty.
remember (tif t1 t2 t3) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_If *)
auto.
- (* T_Sub *)
destruct (IHHty H0) as [H1 [H2 H3]]...
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 S1 s2 T1 T2,
empty ⊢ (tabs x S1 s2) ∈ (TArrow T1 T2) →
T1 <: S1
∧ (update empty x S1) ⊢ s2 ∈ T2.
Proof with eauto.
intros x S1 s2 T1 T2 Hty.
apply typing_inversion_abs in Hty.
inversion Hty as [S2 [Hsub Hty1]].
apply sub_inversion_arrow in Hsub.
inversion Hsub as [U1 [U2 [Heq [Hsub1 Hsub2]]]].
inversion Heq; subst... Qed.
intros x S1 s2 T1 T2 Hty.
apply typing_inversion_abs in Hty.
inversion Hty as [S2 [Hsub Hty1]].
apply sub_inversion_arrow in Hsub.
inversion Hsub as [U1 [U2 [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 t1 t2,
appears_free_in x t1 → appears_free_in x (tapp t1 t2)
| afi_app2 : ∀x t1 t2,
appears_free_in x t2 → appears_free_in x (tapp t1 t2)
| afi_abs : ∀x y T11 t12,
y ≠ x →
appears_free_in x t12 →
appears_free_in x (tabs y T11 t12)
| afi_if1 : ∀x t1 t2 t3,
appears_free_in x t1 →
appears_free_in x (tif t1 t2 t3)
| afi_if2 : ∀x t1 t2 t3,
appears_free_in x t2 →
appears_free_in x (tif t1 t2 t3)
| afi_if3 : ∀x t1 t2 t3,
appears_free_in x t3 →
appears_free_in x (tif t1 t2 t3)
.
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 x0 Hafi.
unfold update, t_update. destruct (beq_idP x x0)...
- (* 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 x0 Hafi.
unfold update, t_update. destruct (beq_idP x x0)...
- (* 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 H4) as [T Hctx]. ∃T.
unfold update, t_update in Hctx.
rewrite ← beq_id_false_iff in H2.
rewrite H2 in Hctx... Qed.
intros x t T Γ Hafi Htyp.
induction Htyp;
subst; inversion Hafi; subst...
- (* T_Abs *)
destruct (IHHtyp H4) as [T Hctx]. ∃T.
unfold update, t_update in Hctx.
rewrite ← beq_id_false_iff in H2.
rewrite H2 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 [T1 [Htypt1 Htypt2]].
eapply T_App...
- (* tabs *)
rename i into y. rename t into T1.
destruct (typing_inversion_abs _ _ _ _ _ Htypt)
as [T2 [Hsub Htypt2]].
apply T_Sub with (TArrow T1 T2)... 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) ⊢ t1 ∈ TBool
∧ (update Γ x U) ⊢ t2 ∈ S
∧ (update Γ x U) ⊢ t3 ∈ S)
by apply (typing_inversion_if _ _ _ _ _ Htypt).
inversion H as [H1 [H2 H3]].
apply IHt1 in H1. apply IHt2 in H2. apply IHt3 in H3.
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 [T1 [Htypt1 Htypt2]].
eapply T_App...
- (* tabs *)
rename i into y. rename t into T1.
destruct (typing_inversion_abs _ _ _ _ _ Htypt)
as [T2 [Hsub Htypt2]].
apply T_Sub with (TArrow T1 T2)... 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) ⊢ t1 ∈ TBool
∧ (update Γ x U) ⊢ t2 ∈ S
∧ (update Γ x U) ⊢ t3 ∈ S)
by apply (typing_inversion_if _ _ _ _ _ Htypt).
inversion H as [H1 [H2 H3]].
apply IHt1 in H1. apply IHt2 in H2. apply IHt3 in H3.
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 t1 and t2 and types T1 and T2 such that
t = t1 t2, T = T2, empty ⊢ t1 : T1 → T2, and
empty ⊢ t2 : T1.
- If the final step of the derivation uses rule T_If, then
there are terms t1, t2, and t3 such that t = if t1 then
t2 else t3, with empty ⊢ t1 : Bool and with empty ⊢ t2 :
T and empty ⊢ t3 : T. Moreover, by the induction
hypothesis, if t1 steps to t1' then empty ⊢ t1' : 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 t1' then t2
else t3 with t1 ⇒ t1'. By the induction hypothesis,
empty ⊢ t1' : Bool, and so empty ⊢ t' : T by T_If.
- If t ⇒ t' by rule ST_IfTrue or ST_IfFalse, then
either t' = t2 or t' = t3, and empty ⊢ t' : T
follows by assumption.
- If t ⇒ t' by rule ST_If, then t' = if t1' then t2
else t3 with t1 ⇒ t1'. By the induction hypothesis,
empty ⊢ t1' : Bool, and so empty ⊢ t' : T by T_If.
- If the final step of the derivation uses rule T_If, then
there are terms t1, t2, and t3 such that t = if t1 then
t2 else t3, with empty ⊢ t1 : Bool and with empty ⊢ t2 :
T and empty ⊢ t3 : T. Moreover, by the induction
hypothesis, if t1 steps to t1' then empty ⊢ t1' : 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 _ _ _ _ _ HT1) as [HA1 HA2].
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 _ _ _ _ _ HT1) as [HA1 HA2].
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 : S1->S2 S1 <: T1 T1 <: S1 S2 <: T2 (T_Funny1) Γ ⊢ t : T1->T2 - 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:
S1 <: T1 S2 <: T2 (S_Arrow') S1->S2 <: T1->T2
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:
S1 <: T1 S2 <: T2 (Sub_Prod) S1 * S2 <: T1 * T2 - 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.)