Records
Simple Extensions to STLC
let-bindings
t ::= Terms: | x variable | \x:T. t abstraction | t t application | let x=t in t let-bindingReduction:
t1 --> t1' | (ST_Let1) |
let x=t1 in t2 --> let x=t1' in t2 |
(ST_LetValue) | |
let x=v1 in t2 --> [v1/x] t2 |
Gamma |- t1 : T1 Gamma, x:T1 |- t2 : T2 | (T_Let) |
Gamma |- let x=t1 in t2 : T2 |
Pairs
t ::= Terms: | ... | (t,t) pair | t.fst first projection | t.snd second projection v ::= Values: | \x:T.t | (v,v) pair value T ::= Types: | A base type | T -> T arrow type | T * T product typeReduction:
t1 --> t1' | (ST_Pair1) |
(t1,t2) --> (t1',t2) |
t2 --> t2' | (ST_Pair2) |
(v1,t2) --> (v1,t2') |
t1 --> t1' | (ST_Fst1) |
t1.fst --> t1'.fst |
(ST_FstPair) | |
(v1,v2).fst --> v1 |
t1 --> t1' | (ST_Snd1) |
t1.snd --> t1'.snd |
(ST_SndPair) | |
(v1,v2).snd --> v2 |
Gamma |- t1 : T1 Gamma |- t2 : T2 | (T_Pair) |
Gamma |- (t1,t2) : T1*T2 |
Gamma |- t1 : T1*T2 | (T_Fst) |
Gamma |- t1.fst : T1 |
Gamma |- t1 : T1*T2 | (T_Snd) |
Gamma |- t1.snd : T2 |
t ::= Terms: | ... | {i1=t1, ..., in=tn} record | t.i projection v ::= Values: | ... | {i1=v1, ..., in=vn} record value T ::= Types: | ... | {i1:T1, ..., in:Tn} record typeIntuitively, the generalization is pretty obvious. But it's worth noticing that what we've actually written is rather informal: in particular, we've written "..." in several places to mean "any number of these," and we've omitted explicit mention of the usual side-condition that the labels of a record should not contain repetitions. It is possible to devise informal notations that are more precise, but these tend to be quite heavy and to obscure the main points of the definitions. So we'll leave these a bit loose (they are informal anyway, after all) and do the work of tightening things up when the times comes to translate it all into Coq.
ti --> ti (ST_Rcd) | |
{i1=v1, ..., im=vm, in=tn, ...} --> {i1=v1, ..., im=vm, in=tn', ...} |
t1 --> t1' | (ST_Proj1) |
t1.i --> t1'.i |
(ST_ProjRcd) | |
{..., i=vi, ...}.i --> vi |
Gamma |- t1 : T1 ... Gamma |- tn : Tn | (T_Rcd) |
Gamma |- {i1=t1, ..., in=tn} : {i1:T1, ..., in:Tn} |
Gamma |- t : {..., i:Ti, ...} | (T_Proj) |
Gamma |- t.i : Ti |
Lists
t ::= Terms: | nil T | cons t t | case t of nil -> t | x::x -> t v ::= Values: | ... | nil T nil value | cons v v cons value T ::= Types: | list T | ...Reduction:
t1 --> t1' | (ST_Cons1) |
cons t1 t2 --> cons t1' t2 |
t2 --> t2' | (ST_Cons2) |
cons v1 t2 --> cons v1 t2' |
t1 --> t1 (ST_Case1) | |
(case t1 of nil -> t2 | h::t -> t3) --> (case t1' of nil -> t2 | h::t -> t3) |
(ST_CaseNil) | |
(case nil T of nil -> t2 | h::t -> t3) --> t2 |
(ST_CaseCons) | |
(case (cons vh vt) of nil -> t2 | h::t -> t3) --> [vh/h,vt/t]t3 |
(T_Nil) | |
Gamma |- nil T : list T |
Gamma |- t1 : T Gamma |- t2 : list T | (T_Cons) |
Gamma |- cons t1 t2: list T |
Gamma |- t1 : list T1 Gamma |- t2 : T | |
Gamma, h:T1, t:list T1 |- t3 : T | (T_Case) |
Gamma |- (case t1 of nil -> t2 | h::t -> t3) : T |
General recursion
fact = \x:nat. if x=0 then 1 else x * (fact (pred x)))But this would be require quite a bit of work to formalize: we'd have to introduce a notion of "function definitions" and carry around an "environment" of such definitions in the definition of the step relation.
fact = fix (\f:nat->nat. \x:nat. if x=0 then 1 else x * (f (pred x)))The intuition is that the higher-order function f passed to fix is a generator for the fact function: if f is applied to a function that approximates the desired behavior of fact up to some number n (that is, a function that returns correct results on inputs less than or equal to n), then it returns a better approximation to fact---a function that returns correct results for inputs up to n+1. Applying fix to this generator returns its fixed point---a function that gives the desired behavior for all inputs n.
t ::= Terms: | ... | fix t fixed-point operatorReduction:
t1 --> t1' | (ST_Fix1) |
fix t1 --> fix t1' |
(ST_FixAbs) | |
fix (\x:T1.t2) --> [(fix(\x:T1.t2)) / x] t2 |
Gamma |- t1 : T1->T1 | (T_Fix) |
Gamma |- fix t1 : T1 |
Exercise: 1 star (halve_fix)
Translate this recursive definition into one using fix:halve = \x:nat. if x=0 then 0 else if (pred x)=0 then 0 else 1 + (halve (pred (pred x))))(* FILL IN HERE *)
☐
Exercise: 1 star (fact_steps)
Write down the sequence of steps that the term fact 1 goes through to reduce to a normal form (assuming the usual reduction rules for arithmetic operations).☐
Formalizing the extensions
Exercise: 5 stars (STLC_extensions)
The rest of the file formalizes just the most interesting extension, records. Formalizing the others is left to you. We've provided the necessary extensions to the syntax of terms and types, and we've included a few examples that you can test your definitions with to make sure they are working as expected. You'll fill in the rest of the definitions and extend all the proofs accordingly. (A good strategy is to work on the extensions one at a time, in multiple passes, rather than trying to work through the file from start to finish in a single pass.)Syntax and operational semantics
Module FirstTry.
Definition alist (X : Type) := list (id * X).
Inductive ty : Type :=
| ty_base : id -> ty
| ty_arrow : ty -> ty -> ty
| ty_rcd : (alist ty) -> ty.
Unfortunately, we encounter here a limitation in Coq: this type
does not automatically give us the induction principle we expect
the induction hypothesis in the ty_rcd case doesn't give us
any information about the ty elements of the list, making it
useless for the proofs we want to do.
(* Check ty_ind. *)
(* Yields:
[ ty_ind : forall P : ty -> Prop, (forall i : id, P (ty_base i)) -> (forall t : ty, P t -> forall t0 : ty, P t0 -> P (ty_arrow t t0)) -> (forall a : alist ty, P (ty_rcd a)) -> forall t : ty, P t ]
*)
End FirstTry.
It is possible to get a better induction principle out of Coq, but
the details of how this is done are not very pretty, and it is not
as intuitive to use as the ones Coq generates automatically for
simple Inductive definitions.
Fortunately, there is a different way of formalizing records that
is, in some ways, even simpler and more natural: instead of using
the existing list type, we can essentially include its
constructors ("nil" and "cons") in the syntax of types.
(Since this is the final definition that we'll use for the rest of
the chapter, we also include constructors for and pairs lists and
a base type of numbers.)
Inductive ty : Type :=
| ty_base : id -> ty
| ty_arrow : ty -> ty -> ty
| ty_pair : ty -> ty -> ty
| ty_list : ty -> ty
| ty_nat : ty
| ty_rnil : ty
| ty_rcons : id -> ty -> ty -> ty.
Tactic Notation "ty_cases" tactic(first) tactic(c) :=
first;
[ c "ty_base" | c "ty_arrow" |
c "ty_pair" | c "ty_list" | c "ty_nat" |
c "ty_rnil" | c "ty_rcons" ].
Similarly, at the level of terms, we have constructors tm_rnil
the empty record -- and tm_rcons, which adds a single field to
the front of a list of fields.
Inductive tm : Type :=
| tm_var : id -> tm
| tm_app : tm -> tm -> tm
| tm_abs : id -> ty -> tm -> tm
| tm_proj : tm -> id -> tm
(* pairs *)
| tm_pair : tm -> tm -> tm
| tm_fst : tm -> tm
| tm_snd : tm -> tm
(* lists *)
| tm_nil : ty -> tm
| tm_cons : tm -> tm -> tm
| tm_case : tm -> tm -> id -> id -> tm -> tm
(* i.e., case t1 of | nil -> t2 | x::y -> t3 *)
(* numbers *)
| tm_nat : nat -> tm
| tm_succ : tm -> tm
| tm_pred : tm -> tm
| tm_mult : tm -> tm -> tm
| tm_if0 : tm -> tm -> tm -> tm
(* let *)
| tm_let : id -> tm -> tm -> tm
(* i.e., let x = t1 in t2 *)
(* fix *)
| tm_fix : tm -> tm
(* records *)
| tm_rnil : tm
| tm_rcons : id -> tm -> tm -> tm.
Tactic Notation "tm_cases" tactic(first) tactic(c) :=
first;
[ c "tm_var" | c "tm_app" | c "tm_abs" |
c "tm_proj" |
c "tm_pair" | c "tm_fst" | c "tm_snd" |
c "tm_nil" | c "tm_cons" | c "tm_case" |
c "tm_nat" | c "tm_succ" | c "tm_pred" | c "tm_mult" | c "tm_if0" |
c "tm_let" |
c "tm_fix" |
c "tm_rnil" | c "tm_rcons" ].
Some variables, for examples...
Notation a := (Id 0).
Notation f := (Id 1).
Notation g := (Id 2).
Notation l := (Id 3).
Notation A := (ty_base (Id 4)).
Notation B := (ty_base (Id 5)).
Notation k := (Id 6).
Notation i1 := (Id 7).
Notation i2 := (Id 8).
{ i1:A }
(* Check (ty_rcons i1 A ty_rnil). *)
{ i1:A->B, i2:A }
(* Check (ty_rcons i1 (ty_arrow A B)
(ty_rcons i2 A ty_rnil)). *)
(ty_rcons i2 A ty_rnil)). *)
Well-formedness
where the "tail" of a record type is not actually a record type!
We'll structure our typing judgement so that no ill-formed types
like weird_type are assigned to terms. To support this, we
define record_ty and record_tm, which identify record types
and terms, and well_formed_ty which rules out the ill-formed
types.
First, a type is a record type if it is built with either
ty_rnil or ty_rcons.
Inductive record_ty : ty -> Prop :=
| rty_nil :
record_ty ty_rnil
| rty_cons : forall i T1 T2,
record_ty (ty_rcons i T1 T2).
Similarly, a term is a record term if it is built with tm_rnil
or tm_rcons
Inductive record_tm : tm -> Prop :=
| rtm_nil :
record_tm tm_rnil
| rtm_cons : forall i t1 t2,
record_tm (tm_rcons i t1 t2).
Note that record_ty and record_tm are not recursive -- they
just checkw the outermost constructor. The well_formed_ty
property, on the other hand, verifies that the whole type is well
formed in the sense that the tail of every record (the second
argument to ty_rcons) is a record.
Of course, we should also be concerned about ill-formed terms, but
typechecking can rules those out without the help of an extra
well_formed_tm definition because it already examines the
structure of terms. LATER : should they fill in part of this as an
exercise? We didn't give rules for it above
Inductive well_formed_ty : ty -> Prop :=
| wfty_base : forall i,
well_formed_ty (ty_base i)
| wfty_arrow : forall T1 T2,
well_formed_ty T1 ->
well_formed_ty T2 ->
well_formed_ty (ty_arrow T1 T2)
| wfty_pair : forall T1 T2,
well_formed_ty T1 ->
well_formed_ty T2 ->
well_formed_ty (ty_pair T1 T2)
| wfty_list : forall T1,
well_formed_ty T1 ->
well_formed_ty (ty_list T1)
| wfty_nat :
well_formed_ty ty_nat
| wfty_rnil :
well_formed_ty ty_rnil
| wfty_rcons : forall i T1 T2,
well_formed_ty T1 ->
well_formed_ty T2 ->
record_ty T2 ->
well_formed_ty (ty_rcons i T1 T2).
Hint Constructors record_ty record_tm well_formed_ty.
Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
match t with
| tm_var y => if beq_id x y then s else t
| tm_abs y T t1 => tm_abs y T (if beq_id x y then t1 else (subst x s t1))
| tm_app t1 t2 => tm_app (subst x s t1) (subst x s t2)
| tm_proj t1 i => tm_proj (subst x s t1) i
| tm_rnil => tm_rnil
| tm_rcons i t1 tr1 => tm_rcons i (subst x s t1) (subst x s tr1)
(* FILL IN HERE *)
| _ => t (* ... and delete this line *)
end.
Inductive value : tm -> Prop :=
| v_abs : forall x T11 t12,
value (tm_abs x T11 t12)
(* FILL IN HERE *)
| v_rnil : value tm_rnil
| v_rcons : forall i v1 vr,
value v1 ->
value vr ->
value (tm_rcons i v1 vr).
Hint Constructors value.
Utility functions for extracting one field from record type or
term
Fixpoint ty_lookup (i:id) (Tr:ty) : option ty :=
match Tr with
| ty_rcons i' T Tr' => if beq_id i i' then Some T else ty_lookup i Tr'
| _ => None
end.
Fixpoint tm_lookup (i:id) (tr:tm) : option tm :=
match tr with
| tm_rcons i' t tr' => if beq_id i i' then Some t else tm_lookup i tr'
| _ => None
end.
The step function uses the term-level lookup function (for the
projection rule), while the type-level lookup is needed for
has_type.
Reserved Notation "t1 '-->' t2" (at level 40).
Inductive step : tm -> tm -> Prop :=
| ST_AppAbs : forall x T11 t12 v2,
value v2 ->
(tm_app (tm_abs x T11 t12) v2) --> (subst x v2 t12)
| ST_App1 : forall t1 t1' t2,
t1 --> t1' ->
(tm_app t1 t2) --> (tm_app t1' t2)
| ST_App2 : forall v1 t2 t2',
value v1 ->
t2 --> t2' ->
(tm_app v1 t2) --> (tm_app v1 t2')
| ST_Proj1 : forall t1 t1' i,
t1 --> t1' ->
(tm_proj t1 i) --> (tm_proj t1' i)
| ST_ProjRcd : forall tr i vi,
value tr ->
tm_lookup i tr = Some vi ->
(tm_proj tr i) --> vi
(* FILL IN HERE *)
| ST_Rcd_Head : forall i t1 t1' tr2,
t1 --> t1' ->
(tm_rcons i t1 tr2) --> (tm_rcons i t1' tr2)
| ST_Rcd_Tail : forall i v1 tr2 tr2',
value v1 ->
tr2 --> tr2' ->
(tm_rcons i v1 tr2) --> (tm_rcons i v1 tr2')
where "t1 '-->' t2" := (step t1 t2).
Tactic Notation "step_cases" tactic(first) tactic(c) :=
first;
[ c "ST_AppAbs" | c "ST_App1" | c "ST_App2" |
c "ST_Proj1" | c "ST_ProjRcd" |
(* FILL IN HERE *)
c "ST_Rcd_Head" | c "ST_Rcd_Tail" ].
Notation stepmany := (refl_step_closure step).
Notation "t1 '-->*' t2" := (stepmany t1 t2) (at level 40).
Hint Constructors step.
(* Standard definitions for contexts *)
Definition context := id -> (option ty).
Definition empty : context := (fun _ => None).
Definition extend (Gamma : context) (x:id) (T : ty) :=
fun x' => if beq_id x x' then Some T else Gamma x'.
Next we define the typing rules. These are nearly direct
transcriptions of the inference rules shown above. The only major
difference is the use of well_formed_ty. In the informal
presentation we used a grammar that only allowed well formed
record types, so we didn't have to add a separate check.
We'd like to set things up so that that whenever has_type Gamma t
T holds, we also have well_formed_ty T. That is, has_type
never assigns ill-formed types to terms. In fact, we prove this
theorem below.
However, we don't want to clutter the definition of has_type
with unnecessary uses of well_formed_ty. Instead, we place
well_formed_ty checks only where needed - where an inductive
call to has_type won't already be checking the well-formedness
of a type.
For example, we check well_formed_ty T in the T_Var case,
because there is no inductive has_type call that would
enforce this. Similarly, in the T_Abs case, we require a
proof of well_formed_ty T11 because the inductive call to
has_type only guarantees that T12 is well-formed.
In the rules you must write, the only necessary well_formed_ty
check comes in the tm_nil case.
Inductive has_type : context -> tm -> ty -> Prop :=
(* Typing rules for proper terms *)
| T_Var : forall Gamma x T,
Gamma x = Some T ->
well_formed_ty T ->
has_type Gamma (tm_var x) T
| T_Abs : forall Gamma x T11 T12 t12,
well_formed_ty T11 ->
has_type (extend Gamma x T11) t12 T12 ->
has_type Gamma (tm_abs x T11 t12) (ty_arrow T11 T12)
| T_App : forall T1 T2 Gamma t1 t2,
has_type Gamma t1 (ty_arrow T1 T2) ->
has_type Gamma t2 T1 ->
has_type Gamma (tm_app t1 t2) T2
| T_Proj : forall Gamma i t Ti Tr,
has_type Gamma t Tr ->
ty_lookup i Tr = Some Ti ->
has_type Gamma (tm_proj t i) Ti
(* FILL IN HERE *)
(* Typing rules for record terms *)
| T_RNil : forall Gamma,
has_type Gamma tm_rnil ty_rnil
| T_RCons : forall Gamma i t T tr Tr,
has_type Gamma t T ->
has_type Gamma tr Tr ->
record_ty Tr ->
record_tm tr ->
has_type Gamma (tm_rcons i t tr) (ty_rcons i T Tr).
Hint Constructors has_type.
Tactic Notation "has_type_cases" tactic(first) tactic(c) :=
first;
[ c "T_Var" | c "T_Abs" | c "T_App" | c "T_Proj" |
(* FILL IN HERE *)
c "T_RNil" | c "T_RCons"
].
Examples
Exercise: 2 stars (examples)
Finish the proofs.fact := fix (\f:nat->nat. \a:nat. if a=0 then 1 else a * (f (pred a)))
Definition fact :=
tm_fix
(tm_abs f (ty_arrow ty_nat ty_nat)
(tm_abs a ty_nat
(tm_if0
(tm_var a)
(tm_nat 1)
(tm_mult
(tm_var a)
(tm_app (tm_var f) (tm_pred (tm_var a))))))).
Note that you may be able to type check fact but still have some
rules wrong!
Example fact_typechecks :
has_type empty fact (ty_arrow ty_nat ty_nat).
Proof with auto.
(* FILL IN HERE *) Admitted.
Example fact_example:
(tm_app fact (tm_nat 1)) -->* (tm_nat 1).
Proof.
(* FILL IN HERE *) Admitted.
(* map :=
\g:nat->nat.
fix
(\f:nat->nat.
\l:nat.
case l of
| ->
| x::l -> (g x)::(f l)) *)
Definition map :=
tm_abs g (ty_arrow ty_nat ty_nat)
(tm_fix
(tm_abs f (ty_arrow (ty_list ty_nat) (ty_list ty_nat))
(tm_abs l (ty_list ty_nat)
(tm_case (tm_var l)
(tm_nil ty_nat)
a l (tm_cons (tm_app (tm_var g) (tm_var a))
(tm_app (tm_var f) (tm_var l))))))).
Example map_typechecks :
has_type empty map
(ty_arrow (ty_arrow ty_nat ty_nat)
(ty_arrow (ty_list ty_nat)
(ty_list ty_nat))).
Proof with auto.
(* FILL IN HERE *) Admitted.
Example map_example :
tm_app (tm_app map (tm_abs a ty_nat (tm_succ (tm_var a))))
(tm_cons (tm_nat 1) (tm_cons (tm_nat 2) (tm_nil ty_nat)))
-->* (tm_cons (tm_nat 2) (tm_cons (tm_nat 3) (tm_nil ty_nat))).
Proof with auto.
(* FILL IN HERE *) Admitted.
☐
Example typing_example : forall y,
has_type (extend empty y A)
(tm_app (tm_abs a (ty_rcons k A ty_rnil)
(tm_proj (tm_var a) k))
(tm_rcons k (tm_var y) tm_rnil))
A.
Proof with auto.
intros y.
apply T_App with (T1:= ty_rcons k A ty_rnil).
apply T_Abs... apply T_Proj with (ty_rcons k A ty_rnil).
apply T_Var... reflexivity.
apply T_RCons...
apply T_Var... unfold extend. rewrite <- beq_id_refl... Qed.
Feel free to use Coq's automation features in this proof.
However, if you are not confident about how the type system works,
you may want to carry out the proof first using the basic features
(apply instead of eapply, in particular) and then perhaps
compress it using automation.
Lemma typing_example_2 :
has_type empty
(tm_app (tm_abs a (ty_rcons i1 (ty_arrow A A)
(ty_rcons i2 (ty_arrow B B)
ty_rnil))
(tm_proj (tm_var a) i2))
(tm_rcons i1 (tm_abs a A (tm_var a))
(tm_rcons i2 (tm_abs a B (tm_var a))
tm_rnil)))
(ty_arrow B B).
Proof.
(* FILL IN HERE *) Admitted.
Before starting to prove this fact (or the one above!), make sure
you understand what it is saying.
Example typing_nonexample :
~ exists T,
has_type (extend empty a (ty_rcons i2 (ty_arrow A A)
ty_rnil))
(tm_rcons i1 (tm_abs a B (tm_var a)) (tm_var a))
T.
Proof.
(* FILL IN HERE *) Admitted.
Example typing_nonexample_2 : forall y,
~ exists T,
has_type (extend empty y A)
(tm_app (tm_abs a (ty_rcons i1 A ty_rnil)
(tm_proj (tm_var a) i1))
(tm_rcons i1 (tm_var y) (tm_rcons i2 (tm_var y) tm_rnil)))
T.
Proof.
(* FILL IN HERE *) Admitted.
Properties of typing
Well-formedness
Lemma wf_rcd_lookup : forall i T Ti,
well_formed_ty T ->
ty_lookup i T = Some Ti ->
well_formed_ty Ti.
Proof with eauto.
intros i T.
(ty_cases (induction T) Case); intros; try solve by inversion.
Case "ty_rcons".
inversion H. subst. unfold ty_lookup in H0.
remember (beq_id i i0) as b. destruct b; subst...
inversion H0. subst... Qed.
Lemma step_preserves_record_tm : forall tr tr',
record_tm tr ->
tr --> tr' ->
record_tm tr'.
Proof.
intros tr tr' Hrt Hstp.
inversion Hrt; subst; inversion Hstp; subst; auto.
Qed.
Lemma has_type__wf : forall Gamma t T,
has_type Gamma t T -> well_formed_ty T.
Proof with eauto.
intros Gamma t T Htyp.
(has_type_cases (induction Htyp) Case)...
Case "T_App".
inversion IHHtyp1...
Case "T_Proj".
eapply wf_rcd_lookup...
(* FILL IN HERE *)
Qed.
Field lookup
- If i = i0, then since ty_lookup i (ty_rcons i0 T Tr) = Some
Ti we have T = Ti. It follows that t itself satisfies
the theorem.
- On the other hand, suppose i <> i0. Then
ty_lookup i T = ty_lookup i Trandtm_lookup i t = tm_lookup i tr,so the result follows from the induction hypothesis. ☐
Lemma lookup_field_in_value : forall v T i Ti,
value v ->
has_type empty v T ->
ty_lookup i T = Some Ti ->
exists ti, tm_lookup i v = Some ti /\ has_type empty ti Ti.
Proof with eauto.
intros v T i Ti Hval Htyp Hget.
remember empty as Gamma.
(has_type_cases (induction Htyp) Case); subst; try solve by inversion...
Case "T_RCons".
simpl in Hget. simpl. destruct (beq_id i i0).
SCase "i is first".
simpl. inversion Hget. subst.
exists t...
SCase "get tail".
destruct IHHtyp2 as [vi [Hgeti Htypi]]...
inversion Hval... Qed.
Theorem progress : forall t T,
has_type empty t T ->
value t \/ exists t', t --> t'.
Proof with eauto.
(* Theorem: Suppose empty |- t : T. Then either
1. t is a value, or
2. t --> t' for some t'.
Proof: By induction on the given typing derivation. *)
intros t T Ht.
remember empty as Gamma.
generalize dependent HeqGamma.
(has_type_cases (induction Ht) Case); intros HeqGamma; subst.
Case "T_Var".
(* The final rule in the given typing derivation cannot be T_Var,
since it can never be the case that empty |- x : T (since the
context is empty). *)
inversion H.
Case "T_Abs".
(* If the T_Abs rule was the last used, then t = tm_abs x T11 t12,
which is a value. *)
left...
Case "T_App".
(* If the last rule applied was T_App, then t = t1 t2, and we know
from the form of the rule that
empty |- t1 : T1 -> T2
empty |- t2 : T1
By the induction hypothesis, each of t1 and t2 either is a value
or can take a step. *)
right.
destruct IHHt1; subst...
SCase "t1 is a value".
destruct IHHt2; subst...
SSCase "t2 is a value".
(* If both t1 and t2 are values, then we know that
t1 = tm_abs x T11 t12, since abstractions are the only values
that can have an arrow type. But
(tm_abs x T11 t12) t2 --> subst x t2 t12 by ST_AppAbs. *)
inversion H; subst; try (solve by inversion).
exists (subst x t2 t12)...
SSCase "t2 steps".
(* If t1 is a value and t2 --> t2', then t1 t2 --> t1 t2'
by ST_App2. *)
destruct H0 as [t2' Hstp]. exists (tm_app t1 t2')...
SCase "t1 steps".
(* Finally, If t1 --> t1', then t1 t2 --> t1' t2 by ST_App1. *)
destruct H as [t1' Hstp]. exists (tm_app t1' t2)...
Case "T_Proj".
(* If the last rule in the given derivation is T_Proj, then
t = tm_proj t i and
empty |- t : (ty_rcd Tr)
By the IH, t either is a value or takes a step. *)
right. destruct IHHt...
SCase "rcd is value".
(* If t is a value, then we may use lemma
lookup_field_in_value to show tm_lookup i t = Some ti for
some ti which gives us tm_proj i t --> ti by ST_ProjRcd
*)
destruct (lookup_field_in_value _ _ _ _ H0 Ht H) as [ti [Hlkup _]].
exists ti...
SCase "rcd_steps".
(* On the other hand, if t --> t', then tm_proj t i --> tm_proj t' i
by ST_Proj1. *)
destruct H0 as [t' Hstp]. exists (tm_proj t' i)...
(* FILL IN HERE *)
Case "T_RNil".
(* If the last rule in the given derivation is T_RNil, then
t = tm_rnil, which is a value. *)
left...
Case "T_RCons".
(* If the last rule is T_RCons, then t = tm_rcons i t tr and
empty |- t : T
empty |- tr : Tr
By the IH, each of t and tr either is a value or can take
a step. *)
destruct IHHt1...
SCase "head is a value".
destruct IHHt2; try reflexivity.
SSCase "tail is a value".
(* If t and tr are both values, then tm_rcons i t tr
is a value as well. *)
left...
SSCase "tail steps".
(* If t is a value and tr --> tr', then
tm_rcons i t tr --> tm_rcons i t tr' by
ST_Rcd_Tail. *)
right. destruct H2 as [tr' Hstp].
exists (tm_rcons i t tr')...
SCase "head steps".
(* If t --> t', then
tm_rcons i t tr --> tm_rcons i t' tr
by ST_Rcd_Head. *)
right. destruct H1 as [t' Hstp].
exists (tm_rcons i t' tr)... Qed.
Inductive appears_free_in : id -> tm -> Prop :=
| afi_var : forall x,
appears_free_in x (tm_var x)
| afi_app1 : forall x t1 t2,
appears_free_in x t1 -> appears_free_in x (tm_app t1 t2)
| afi_app2 : forall x t1 t2,
appears_free_in x t2 -> appears_free_in x (tm_app t1 t2)
| afi_abs : forall x y T11 t12,
y <> x ->
appears_free_in x t12 ->
appears_free_in x (tm_abs y T11 t12)
| afi_proj : forall x t i,
appears_free_in x t ->
appears_free_in x (tm_proj t i)
(* FILL IN HERE *)
| afi_rhead : forall x i ti tr,
appears_free_in x ti ->
appears_free_in x (tm_rcons i ti tr)
| afi_rtail : forall x i ti tr,
appears_free_in x tr ->
appears_free_in x (tm_rcons i ti tr).
Hint Constructors appears_free_in.
Lemma context_invariance : forall Gamma Gamma' t S,
has_type Gamma t S ->
(forall x, appears_free_in x t -> Gamma x = Gamma' x) ->
has_type Gamma' t S.
Proof with eauto.
intros. generalize dependent Gamma'.
(has_type_cases (induction H) Case);
intros Gamma' Heqv...
Case "T_Var".
apply T_Var... rewrite <- Heqv...
Case "T_Abs".
apply T_Abs... apply IHhas_type. intros y Hafi.
unfold extend. remember (beq_id x y) as e.
destruct e...
Case "T_App".
apply T_App with T1...
(* FILL IN HERE *)
Case "T_RCons".
apply T_RCons... Qed.
Lemma free_in_context : forall x t T Gamma,
appears_free_in x t ->
has_type Gamma t T ->
exists T', Gamma x = Some T'.
Proof with eauto.
intros x t T Gamma Hafi Htyp.
(has_type_cases (induction Htyp) Case); inversion Hafi; subst...
Case "T_Abs".
destruct IHHtyp as [T' Hctx]... exists T'.
unfold extend in Hctx.
apply not_eq_beq_id_false in H3. rewrite H3 in Hctx...
(* FILL IN HERE *)
Qed.
Lemma substitution_preserves_typing : forall Gamma x U v t S,
has_type (extend Gamma x U) t S ->
has_type empty v U ->
has_type Gamma (subst x v t) S.
Proof with eauto.
(* Theorem: If Gamma,x:U |- t : S and empty |- v : U, then
Gamma |- (subst x v t) S. *)
intros Gamma x U v t S Htypt Htypv.
generalize dependent Gamma. generalize dependent S.
(* Proof: By induction on the term t. Most cases follow directly
from the IH, with the exception of tm_var, tm_abs, tm_rcons.
The former aren't automatic because we must reason about how the
variables interact. In the case of tm_rcons, we must do a little
extra work to show that substituting into a term doesn't change
whether it is a record term. *)
(tm_cases (induction t) Case);
intros S Gamma Htypt; simpl; inversion Htypt; subst...
Case "tm_var".
simpl. rename i into y.
(* If t = y, we know that
empty |- v : U and
Gamma,x:U |- y : S
and, by inversion, extend Gamma x U y = Some S. We want to
show that Gamma |- subst x v y : S.
There are two cases to consider: either x=y or x<>y. *)
remember (beq_id x y) as e. destruct e.
SCase "x=y".
(* If x = y, then we know that U = S, and that subst x v y = v.
So what we really must show is that if empty |- v : U then
Gamma |- v : U. We have already proven a more general version
of this theorem, called context invariance. *)
apply beq_id_eq in Heqe. subst.
unfold extend in H0. rewrite <- beq_id_refl in H0.
inversion H0; subst. clear H0.
eapply context_invariance...
intros x Hcontra.
destruct (free_in_context _ _ S empty Hcontra) as [T' HT']...
inversion HT'.
SCase "x<>y".
(* If x <> y, then Gamma y = Some S and the substitution has no
effect. We can show that Gamma |- y : S by T_Var. *)
apply T_Var... unfold extend in H0. rewrite <- Heqe in H0...
Case "tm_abs".
rename i into y. rename t into T11.
(* If t = tm_abs y T11 t0, then we know that
Gamma,x:U |- tm_abs y T11 t0 : T11->T12
Gamma,x:U,y:T11 |- t0 : T12
empty |- v : U
As our IH, we know that forall S Gamma,
Gamma,x:U |- t0 : S -> Gamma |- subst x v t0 S.
We can calculate that
subst x v t = tm_abs y T11 (if beq_id x y
then t0
else subst x v t0)
And we must show that Gamma |- subst x v t : T11->T12. We know
we will do so using T_Abs, so it remains to be shown that:
Gamma,y:T11 |- if beq_id x y then t0 else subst x v t0 : T12
We consider two cases: x = y and x <> y.
*)
apply T_Abs...
remember (beq_id x y) as e. destruct e.
SCase "x=y".
(* If x = y, then the substitution has no effect. Context
invariance shows that Gamma,y:U,y:T11 and Gamma,y:T11 are
equivalent. Since the former context shows that t0 : T12, so
does the latter. *)
eapply context_invariance...
apply beq_id_eq in Heqe. subst.
intros x Hafi. unfold extend.
destruct (beq_id y x)...
SCase "x<>y".
(* If x <> y, then the IH and context invariance allow us to show that
Gamma,x:U,y:T11 |- t0 : T12 =>
Gamma,y:T11,x:U |- t0 : T12 =>
Gamma,y:T11 |- subst x v t0 : T12 *)
apply IHt. eapply context_invariance...
intros z Hafi. unfold extend.
remember (beq_id y z) as e0. destruct e0...
apply beq_id_eq in Heqe0. subst.
rewrite <- Heqe...
(* FILL IN HERE *)
Case "tm_rcons".
apply T_RCons... inversion H7; subst; simpl...
Qed.
Theorem preservation : forall t t' T,
has_type empty t T ->
t --> t' ->
has_type empty t' T.
Proof with eauto.
intros t t' T HT.
(* Theorem: If empty |- t : T and t --> t', then empty |- t' : T. *)
remember empty as Gamma. generalize dependent HeqGamma.
generalize dependent t'.
(* Proof: By induction on the given typing derivation. Many cases are
contradictory (T_Var, T_Abs) or follow directly from the IH
(T_RCons). We show just the interesting ones. *)
(has_type_cases (induction HT) Case);
intros t' HeqGamma HE; subst; inversion HE; subst...
Case "T_App".
(* If the last rule used was T_App, then t = t1 t2, and three rules
could have been used to show t --> t': ST_App1, ST_App2, and
ST_AppAbs. In the first two cases, the result follows directly from
the IH. *)
inversion HE; subst...
SCase "ST_AppAbs".
(* For the third case, suppose
t1 = tm_abs x T11 t12
and
t2 = v2. We must show that empty |- subst x v2 t12 : T2.
We know by assumption that
empty |- tm_abs x T11 t12 : T1->T2
and by inversion
x:T1 |- t12 : T2
We have already proven that substitution_preserves_typing and
empty |- v2 : T1
by assumption, so we are done. *)
apply substitution_preserves_typing with T1...
inversion HT1...
Case "T_Proj".
(* If the last rule was T_Proj, then t = tm_proj t1 i. Two rules
could have caused t --> t': T_Proj1 and T_ProjRcd. The typing
of t' follows from the IH in the former case, so we only
consider T_ProjRcd.
Here we have that t is a record value. Since rule T_Proj was
used, we know has_type empty t Tr and ty_lookup i Tr = Some Ti for some i and Tr. We may therefore apply lemma
lookup_field_in_value to find the record element this
projection steps to. *)
destruct (lookup_field_in_value _ _ _ _ H2 HT H)
as [vi [Hget Htyp]].
rewrite H4 in Hget. inversion Hget. subst...
(* FILL IN HERE *)
Case "T_RCons".
(* If the last rule was T_RCons, then t = tm_rcons i t tr for
some i, t and tr such that record_tm tr. If the step is
by ST_Rcd_Head, the result is immediate by the IH. If the step
is by ST_Rcd_Tail, tr --> tr2' for some tr2' and we must also
use lemma step_preserves_record_tm to show record_tm tr2'. *)
apply T_RCons... eapply step_preserves_record_tm...
Qed.
☐
Subtyping
A motivating example
(\r:{y:nat}. r.y + 1) {x=10,y=11}is not typable: it involves an application of 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 subtyping as a binary relation between types.
- Enriching the typing relation to take subtyping into account.
Gamma |- t : S S <: T | (T_Sub) |
Gamma |- t : T |
The subtype relation
for each jk in j1..jn, exists ip in i1..im with jk=ip and Sp <: Tk | (S_Rcd) |
{i1:S1...im:Sm} <: {j1:T1...jn:Tn} |
{x:nat,y:bool} <: {x:nat} "width subtyping" {x:nat} <: {} {x:nat,y:bool} <: {y:bool,x:nat} "permutation" {x:nat,y:bool} <: {y:bool} {a:{x:nat}} <: {a:{}} "depth subtyping"Formally, our record types are presented in a "binary" form (with constructors for nil and cons, rather than a single constructor that assembles a whole multi-field record all at once), and so we'll need to formulate subtyping in the same way. This can be accomplished by replacing the single rule above with a combination of three rules.
j:A;k:B;l:C;{}and
{j:A,k:B,l:C}will mean the very same thing -- they will both denote this formal record type:
ty_rcons j (ty_base A) (ty_rcons k (ty_base B) (ty_rcons l (ty_base C) ty_rnil))With these notations in hand, we're ready to talk about the three subtyping rules for records.
(S_RcdWidth) | |
Tr <: {} |
S1 <: T1 Sr2 <: Tr2 | (S_RcdDepth) |
i1:S1; Sr2 <: i1:T1; Tr2 |
i1 <> i2 | (S_RcdPerm) |
i1:T1; i2:T2; Tr3 <: i2:T2; i1:T1; Tr3 |
S <: U U <: T | (S_Trans) |
S <: T |
f : C -> {x:A->A,y:B->B} g : (C->{y:B->B}) -> DThat is, f is a function that yields a record of type {x:A->A,y:B->B}, and g is a higher-order function that expects its (function) argument to yield a record of type {y:B->B}. 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 two-field record, while g will be expecting only a record with a single field, but this is safe because the only thing g can then do is to project out the single field that it knows about, and this will certainly be among the two fields that are present.
S2 <: T2 | (S_Arrow) |
S1->S2 <: S1->T2 |
T1 <: S1 S2 <: T2 | (S_Arrow) |
S1->S2 <: T1->T2 |
(S_Refl) | |
T <: T |
(S_Top) | |
S <: Top |
- {}->{j:A} <: {k:B}->Top
- Top->{k:A->A,j:B->B} <: (C->C)->{j:B->B}
Variations
- 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 has just one superclass ("single inheritance" of
classes)
- 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
- 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
- A class may implement multiple interfaces ("multiple
inheritance" of interfaces)
- i.e., permutation is allowed for interfaces.
Core definitions
Syntax
Inductive ty : Type :=
(* proper types *)
| ty_top : ty
| ty_base : id -> ty
| ty_arrow : ty -> ty -> ty
(* record types *)
| ty_rnil : ty
| ty_rcons : id -> ty -> ty -> ty.
Tactic Notation "ty_cases" tactic(first) tactic(c) :=
first;
[ c "ty_top" | c "ty_base" | c "ty_arrow" |
c "ty_rnil" | c "ty_rcons"
].
Inductive tm : Type :=
(* proper terms *)
| tm_var : id -> tm
| tm_app : tm -> tm -> tm
| tm_abs : id -> ty -> tm -> tm
| tm_proj : tm -> id -> tm
(* record terms *)
| tm_rnil : tm
| tm_rcons : id -> tm -> tm -> tm.
Tactic Notation "tm_cases" tactic(first) tactic(c) :=
first;
[ c "tm_var" | c "tm_app" | c "tm_abs" | c "tm_proj" |
c "tm_rnil" | c "tm_rcons" ].
Well-formedness
Inductive record_ty : ty -> Prop :=
| rty_nil :
record_ty ty_rnil
| rty_cons : forall i T1 T2,
record_ty (ty_rcons i T1 T2).
Inductive record_tm : tm -> Prop :=
| rtm_nil :
record_tm tm_rnil
| rtm_cons : forall i t1 t2,
record_tm (tm_rcons i t1 t2).
Note that record_ty is not recursive -- it just checks the
outermost constructor. The well_formed_ty property, on
the other hand, verifies that the whole type is well formed
in the sense that the tail of every record (the second
argument to ty_rcons) is a record.
Inductive well_formed_ty : ty -> Prop :=
| wfty_top :
well_formed_ty ty_top
| wfty_base : forall i,
well_formed_ty (ty_base i)
| wfty_arrow : forall T1 T2,
well_formed_ty T1 ->
well_formed_ty T2 ->
well_formed_ty (ty_arrow T1 T2)
| wfty_rnil :
well_formed_ty ty_rnil
| wfty_rcons : forall i T1 T2,
well_formed_ty T1 ->
well_formed_ty T2 ->
record_ty T2 ->
well_formed_ty (ty_rcons i T1 T2).
Hint Constructors record_ty record_tm well_formed_ty.
Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
match t with
| tm_var y => if beq_id x y then s else t
| tm_abs y T t1 => tm_abs y T (if beq_id x y then t1 else (subst x s t1))
| tm_app t1 t2 => tm_app (subst x s t1) (subst x s t2)
| tm_proj t1 i => tm_proj (subst x s t1) i
| tm_rnil => tm_rnil
| tm_rcons i t1 tr2 => tm_rcons i (subst x s t1) (subst x s tr2)
end.
Inductive value : tm -> Prop :=
| v_abs : forall x T t,
value (tm_abs x T t)
| v_rnil : value tm_rnil
| v_rcons : forall i v vr,
value v ->
value vr ->
value (tm_rcons i v vr).
Hint Constructors value.
Fixpoint ty_lookup (i:id) (Tr:ty) : option ty :=
match Tr with
| ty_rcons i' T Tr' => if beq_id i i' then Some T else ty_lookup i Tr'
| _ => None
end.
Fixpoint tm_lookup (i:id) (tr:tm) : option tm :=
match tr with
| tm_rcons i' t tr' => if beq_id i i' then Some t else tm_lookup i tr'
| _ => None
end.
Reserved Notation "t1 '-->' t2" (at level 40).
Inductive step : tm -> tm -> Prop :=
| ST_AppAbs : forall x T t12 v2,
value v2 ->
(tm_app (tm_abs x T t12) v2) --> (subst x v2 t12)
| ST_App1 : forall t1 t1' t2,
t1 --> t1' ->
(tm_app t1 t2) --> (tm_app t1' t2)
| ST_App2 : forall v1 t2 t2',
value v1 ->
t2 --> t2' ->
(tm_app v1 t2) --> (tm_app v1 t2')
| ST_Proj1 : forall tr tr' i,
tr --> tr' ->
(tm_proj tr i) --> (tm_proj tr' i)
| ST_ProjRcd : forall tr i vi,
value tr ->
tm_lookup i tr = Some vi ->
(tm_proj tr i) --> vi
| ST_Rcd_Head : forall i t1 t1' tr2,
t1 --> t1' ->
(tm_rcons i t1 tr2) --> (tm_rcons i t1' tr2)
| ST_Rcd_Tail : forall i v1 tr2 tr2',
value v1 ->
tr2 --> tr2' ->
(tm_rcons i v1 tr2) --> (tm_rcons i v1 tr2')
where "t1 '-->' t2" := (step t1 t2).
Tactic Notation "step_cases" tactic(first) tactic(c) :=
first;
[ c "ST_AppAbs" | c "ST_App1" | c "ST_App2" |
c "ST_Proj1" | c "ST_ProjRcd" |
c "ST_Rcd" | c "ST_Rcd_Head" | c "ST_Rcd_Tail" ].
Hint Constructors step.
Subtyping
Definition
Inductive subtype : ty -> ty -> Prop :=
(* Subtyping between proper types *)
| S_Refl : forall T,
well_formed_ty T ->
subtype T T
| S_Trans : forall S U T,
subtype S U ->
subtype U T ->
subtype S T
| S_Top : forall S,
well_formed_ty S ->
subtype S ty_top
| S_Arrow : forall S1 S2 T1 T2,
subtype T1 S1 ->
subtype S2 T2 ->
subtype (ty_arrow S1 S2) (ty_arrow T1 T2)
(* Subtyping between record types *)
| S_RcdWidth : forall i T1 T2,
well_formed_ty (ty_rcons i T1 T2) ->
subtype (ty_rcons i T1 T2) ty_rnil
| S_RcdDepth : forall i S1 T1 Sr2 Tr2,
subtype S1 T1 ->
subtype Sr2 Tr2 ->
record_ty Sr2 ->
record_ty Tr2 ->
subtype (ty_rcons i S1 Sr2) (ty_rcons i T1 Tr2)
| S_RcdPerm : forall i1 i2 T1 T2 Tr3,
well_formed_ty (ty_rcons i1 T1 (ty_rcons i2 T2 Tr3)) ->
i1 <> i2 ->
subtype (ty_rcons i1 T1 (ty_rcons i2 T2 Tr3))
(ty_rcons i2 T2 (ty_rcons i1 T1 Tr3)).
Hint Constructors subtype.
Tactic Notation "subtype_cases" tactic(first) tactic(c) :=
first;
[ c "S_Refl" | c "S_Trans" | c "S_Top" | c "S_Arrow" |
c "S_RcdWidth" | c "S_RcdDepth" | c "S_RcdPerm" ].
Module Examples.
Notation x := (Id 0).
Notation y := (Id 1).
Notation z := (Id 2).
Notation j := (Id 3).
Notation k := (Id 4).
Notation i := (Id 5).
Notation A := (ty_base (Id 6)).
Notation B := (ty_base (Id 7)).
Notation C := (ty_base (Id 8)).
Definition ty_rcd_j :=
(ty_rcons j (ty_arrow B B) ty_rnil). (* {j:B->B} *)
Definition ty_rcd_kj :=
ty_rcons k (ty_arrow A A) ty_rcd_j. (* {k:C->C,j:B->B} *)
Example subtyping_example_0 :
subtype (ty_arrow C ty_rcd_kj)
(ty_arrow C ty_rnil).
(* C->{k:A->A,j:B->B} <: C->{} *)
Proof.
apply S_Arrow.
apply S_Refl. auto.
unfold ty_rcd_kj, ty_rcd_j. apply S_RcdWidth; auto.
Qed.
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: 2 stars
Example subtyping_example_1 :
subtype ty_rcd_kj ty_rcd_j.
(* {k:A->A,j:B->B} <: {j:B->B} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
subtype ty_rcd_kj ty_rcd_j.
(* {k:A->A,j:B->B} <: {j:B->B} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
Example subtyping_example_2 :
subtype (ty_arrow ty_top ty_rcd_kj)
(ty_arrow (ty_arrow C C) ty_rcd_j).
(* Top->{k:A->A,j:B->B} <: (C->C)->{j:B->B} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
subtype (ty_arrow ty_top ty_rcd_kj)
(ty_arrow (ty_arrow C C) ty_rcd_j).
(* Top->{k:A->A,j:B->B} <: (C->C)->{j:B->B} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
Example subtyping_example_3 :
subtype (ty_arrow ty_rnil (ty_rcons j A ty_rnil))
(ty_arrow (ty_rcons k B ty_rnil) ty_rnil).
(* {}->{j:A} <: {k:B}->{} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
subtype (ty_arrow ty_rnil (ty_rcons j A ty_rnil))
(ty_arrow (ty_rcons k B ty_rnil) ty_rnil).
(* {}->{j:A} <: {k:B}->{} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
Example subtyping_example_4 :
subtype (ty_rcons x A (ty_rcons y B (ty_rcons z C ty_rnil)))
(ty_rcons z C (ty_rcons y B (ty_rcons x A ty_rnil))).
(* {x:A,y:B,z:C} <: {z:C,y:B,x:A} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
subtype (ty_rcons x A (ty_rcons y B (ty_rcons z C ty_rnil)))
(ty_rcons z C (ty_rcons y B (ty_rcons x A ty_rnil))).
(* {x:A,y:B,z:C} <: {z:C,y:B,x:A} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Definition tm_rcd_kj :=
(tm_rcons k (tm_abs z A (tm_var z))
(tm_rcons j (tm_abs z B (tm_var z))
tm_rnil)).
End Examples.
Exercise: 1 star (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.- T->S <: T->S
- Top->U <: S->Top
- (C->C)->{x:A->A,y:B->B} <: (C->C)->{y:B->B}
- ty_rnil -> ty_rnil <: {x:A} -> Top
- T->T->U <: S->S->V
- (T->T)->U <: (S->S)->V
- ((T->S)->T)->U <: ((S->T)->S)->V
- {a:S, b:V} <: {a:T, b:U}
Exercise: 1 star (subtype_instances_tf_2)
Which of the following statements are true? Write TRUE or FALSE after each one.-
forall S T,
S <: T ->
S->S <: T->T -
forall S T,
S <: A->A ->
exists T,
S = T->T /\ T <: A -
forall S T1 T1,
S <: T1 -> T2 ->
exists S1 S2,
S = S1 -> S2 /\ T1 <: S1 /\ S2 <: T2 -
exists S,
S <: S->S -
exists S,
S->S <: S -
forall S T2 T2,
S <: {j:T1,k:T2} ->
exists S1 S2,
S = {j:S1,k: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 record type that is a subtype of every other
record type.
- There exists a record type that is a supertype of every other
record type.
- There exists an arrow type that is a subtype of every other
arrow type.
- There exists an arrow type that is a supertype 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: 1 star (proper_subtypes)
Is the following statement true or false? Briefly explain your answer.
forall T,
~(exists n, T = ty_base n) ->
exists S,
S <: T /\ S <> T
~(exists n, T = ty_base n) ->
exists S,
S <: T /\ S <> T
Exercise: 1 star (small_large_1)
- What is the smallest type T ("smallest" in the subtype
relation) that makes the following assertion true?
empty |- (\r:{x:T}. r.x) {x=(\z:A.z)} : A->A
- What is the largest type T that makes the same assertion true?
Exercise: 1 star (small_large_2)
- What is the smallest type T that makes the following
assertion true?
empty |- (\r:{y:B->B, x:A->A}. r) {x=(\z:A.z), y=(\z:B.z)} : T
- What is the largest type T that makes the same assertion true?
Exercise: 1 star (small_large_3)
- What is the smallest record type T that makes the following
assertion true?
a:A |- (\r:(x:A;T)}. (r.y) (r.x)) {y=(\z:A.z), x=a} : A
- What is the largest record type T that makes the same assertion true?
Exercise: 1 star (small_large_4)
- What is the smallest record type T that makes the following
assertion true?
exists S,
empty |- (\r:(x:A;T). (r.y) (r.x)) : S - What is the largest record type T that makes the same assertion true?
Exercise: 1 star (smallest_1)
What is the smallest type T that makes the following assertion true?
exists S, exists t,
empty |- (\r:{x:T}. (r.x) (r.x)) t : S
empty |- (\r:{x:T}. (r.x) (r.x)) t : S
Exercise: 1 star (smallest_2)
What is the smallest type T that makes the following assertion true?
empty |- (\x:Top. x) {a=(\z:A.z), b=(\z:B.z)} : T
Exercise: 1 star (count_supertypes)
How many supertypes does the 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.)Properties of subtyping
Well-formedness
Lemma subtype__wf : forall S T,
subtype S T ->
well_formed_ty T /\ well_formed_ty S.
Proof with eauto.
intros S T Hsub.
(subtype_cases (induction Hsub) Case);
intros; try (destruct IHHsub1; destruct IHHsub2)...
Case "S_RcdPerm".
split... inversion H. subst. inversion H5... Qed.
Lemma wf_rcd_lookup : forall i T Ti,
well_formed_ty T ->
ty_lookup i T = Some Ti ->
well_formed_ty Ti.
Proof with eauto.
intros i T.
(ty_cases (induction T) Case); intros; try solve by inversion.
Case "ty_rcons".
inversion H. subst. unfold ty_lookup in H0.
remember (beq_id i i0) as b. destruct b; subst...
inversion H0. subst... Qed.
Exercise: 1 star (wf_variation)
The proof of the subtype__wf lemma goes by induction on the derivation of S <: T. Suppose we change the statement of the lemma to
Lemma subtype__wf : forall S T,
S <: T ->
well_formed_ty T
and again start the proof by induction on the derivation of S <: T.
Will we succeed in completing it? Briefly explain.
S <: T ->
well_formed_ty T
Field lookup
Lemma rcd_types_match : forall S T i Ti,
subtype S T ->
ty_lookup i T = Some Ti ->
exists Si, ty_lookup i S = Some Si /\ subtype Si Ti.
Proof with (eauto using wf_rcd_lookup).
intros S T i Ti Hsub Hget. generalize dependent Ti.
(subtype_cases (induction Hsub) Case); intros Ti Hget;
try solve by inversion.
Case "S_Refl".
exists Ti...
Case "S_Trans".
destruct (IHHsub2 Ti) as [Ui Hui]... destruct Hui.
destruct (IHHsub1 Ui) as [Si Hsi]... destruct Hsi.
exists Si...
Case "S_RcdDepth".
rename i0 into k.
unfold ty_lookup. unfold ty_lookup in Hget.
remember (beq_id i k) as b. destruct b...
SCase "i = k -- we're looking up the first field".
inversion Hget. subst. exists S1...
Case "S_RcdPerm".
exists Ti. split.
SCase "lookup".
unfold ty_lookup. unfold ty_lookup in Hget.
remember (beq_id i i1) as b. destruct b...
SSCase "i = i1 -- we're looking up the first field".
remember (beq_id i i2) as b. destruct b...
SSSCase "i = i2 - -contradictory".
destruct H0.
apply beq_id_eq in Heqb. apply beq_id_eq in Heqb0.
subst...
SCase "subtype".
inversion H. subst. inversion H5. subst... Qed.
Exercise: 3 stars (rcd_types_match_informal)
Write a careful informal proof of the rcd_types_match lemma.
(* FILL IN HERE *)
Lemma sub_inversion_arrow : forall U V1 V2,
subtype U (ty_arrow V1 V2) ->
exists U1, exists U2,
(U=(ty_arrow U1 U2)) /\ (subtype V1 U1) /\ (subtype U2 V2).
Proof with eauto.
intros U V1 V2 Hs.
remember (ty_arrow V1 V2) as V.
generalize dependent V2. generalize dependent V1.
(* FILL IN HERE *) Admitted.
subtype U (ty_arrow V1 V2) ->
exists U1, exists U2,
(U=(ty_arrow U1 U2)) /\ (subtype V1 U1) /\ (subtype U2 V2).
Proof with eauto.
intros U V1 V2 Hs.
remember (ty_arrow V1 V2) as V.
generalize dependent V2. generalize dependent V1.
(* FILL IN HERE *) Admitted.
☐
Again, the typing relation is exactly the same, except for
(a) the rule of subsumption, T_Sub, and (b) some
well-formedness side conditions.
Typing
Definition context := id -> (option ty).
Definition empty : context := (fun _ => None).
Definition extend (Gamma : context) (x:id) (T : ty) :=
fun x' => if beq_id x x' then Some T else Gamma x'.
Inductive has_type : context -> tm -> ty -> Prop :=
| T_Var : forall Gamma x T,
Gamma x = Some T ->
well_formed_ty T ->
has_type Gamma (tm_var x) T
| T_Abs : forall Gamma x T11 T12 t12,
well_formed_ty T11 ->
has_type (extend Gamma x T11) t12 T12 ->
has_type Gamma (tm_abs x T11 t12) (ty_arrow T11 T12)
| T_App : forall T1 T2 Gamma t1 t2,
has_type Gamma t1 (ty_arrow T1 T2) ->
has_type Gamma t2 T1 ->
has_type Gamma (tm_app t1 t2) T2
| T_Proj : forall Gamma i t T Ti,
has_type Gamma t T ->
ty_lookup i T = Some Ti ->
has_type Gamma (tm_proj t i) Ti
(* Subsumption *)
| T_Sub : forall Gamma t S T,
has_type Gamma t S ->
subtype S T ->
has_type Gamma t T
(* Rules for record terms *)
| T_RNil : forall Gamma,
has_type Gamma tm_rnil ty_rnil
| T_RCons : forall Gamma i t T tr Tr,
has_type Gamma t T ->
has_type Gamma tr Tr ->
record_ty Tr ->
record_tm tr ->
has_type Gamma (tm_rcons i t tr) (ty_rcons i T Tr).
Hint Constructors has_type.
Tactic Notation "has_type_cases" tactic(first) tactic(c) :=
first;
[ c "T_Var" | c "T_Abs" | c "T_App" | c "T_Proj" |
c "T_Sub" | c "T_RNil" | c "T_RCons" ].
Example typing_example_0 :
has_type empty
(tm_rcons k (tm_abs z A (tm_var z))
(tm_rcons j (tm_abs z B (tm_var z))
tm_rnil))
ty_rcd_kj.
(* empty |- {k=(\z:A.z), j=(\z:B.z)} : {k:A->A,j:B->B} *)
Proof.
(* FILL IN HERE *) Admitted.
has_type empty
(tm_rcons k (tm_abs z A (tm_var z))
(tm_rcons j (tm_abs z B (tm_var z))
tm_rnil))
ty_rcd_kj.
(* empty |- {k=(\z:A.z), j=(\z:B.z)} : {k:A->A,j:B->B} *)
Proof.
(* FILL IN HERE *) Admitted.
Example typing_example_1 :
has_type empty
(tm_app (tm_abs x ty_rcd_j (tm_proj (tm_var x) j))
(tm_rcd_kj))
(ty_arrow B B).
(* empty |- (\x:{k:A->A,j:B->B}. x.j) {k=(\z:A.z), j=(\z:B.z)} : B->B *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
has_type empty
(tm_app (tm_abs x ty_rcd_j (tm_proj (tm_var x) j))
(tm_rcd_kj))
(ty_arrow B B).
(* empty |- (\x:{k:A->A,j:B->B}. x.j) {k=(\z:A.z), j=(\z:B.z)} : B->B *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
Example typing_example_2 :
has_type empty
(tm_app (tm_abs z (ty_arrow (ty_arrow C C) ty_rcd_j)
(tm_proj (tm_app (tm_var z)
(tm_abs x C (tm_var x)))
j))
(tm_abs z (ty_arrow C C) tm_rcd_kj))
(ty_arrow B B).
(* empty |- (\z:(C->C)->{j:B->B}. (z (\x:C.x)).j)
(\z:C->C. {k=(\z:A.z), j=(\z:B.z)})
: B->B *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
has_type empty
(tm_app (tm_abs z (ty_arrow (ty_arrow C C) ty_rcd_j)
(tm_proj (tm_app (tm_var z)
(tm_abs x C (tm_var x)))
j))
(tm_abs z (ty_arrow C C) tm_rcd_kj))
(ty_arrow B B).
(* empty |- (\z:(C->C)->{j:B->B}. (z (\x:C.x)).j)
(\z:C->C. {k=(\z:A.z), j=(\z:B.z)})
: B->B *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Lemma has_type__wf : forall Gamma t T,
has_type Gamma t T -> well_formed_ty T.
Proof with eauto.
intros Gamma t T Htyp.
(has_type_cases (induction Htyp) Case)...
Case "T_App".
inversion IHHtyp1...
Case "T_Proj".
eapply wf_rcd_lookup...
Case "T_Sub".
apply subtype__wf in H.
destruct H...
Qed.
Lemma step_preserves_record_tm : forall tr tr',
record_tm tr ->
tr --> tr' ->
record_tm tr'.
Proof.
intros tr tr' Hrt Hstp.
inversion Hrt; subst; inversion Hstp; subst; eauto.
Qed.
Lemma lookup_field_in_value : forall v T i Ti,
value v ->
has_type empty v T ->
ty_lookup i T = Some Ti ->
exists vi, tm_lookup i v = Some vi /\ has_type empty vi Ti.
Proof with eauto.
remember empty as Gamma.
intros t T i Ti Hval Htyp. revert Ti HeqGamma Hval.
(has_type_cases (induction Htyp) Case); intros; subst; try solve by inversion.
Case "T_Sub".
apply (rcd_types_match S) in H0... destruct H0 as [Si [HgetSi Hsub]].
destruct (IHHtyp Si) as [vi [Hget Htyvi]]...
Case "T_RCons".
simpl in H0. simpl. simpl in H1.
remember (beq_id i i0) as b. destruct b.
SCase "i is first".
inversion H1. subst. exists t...
SCase "i in tail".
destruct (IHHtyp2 Ti) as [vi [get Htyvi]]...
inversion Hval... Qed.
Lemma canonical_forms_of_arrow_types : forall Gamma s T1 T2,
has_type Gamma s (ty_arrow T1 T2) ->
value s ->
exists x, exists S1, exists s2,
s = tm_abs x S1 s2.
Proof with eauto.
(* FILL IN HERE *) Admitted.
has_type Gamma s (ty_arrow T1 T2) ->
value s ->
exists x, exists S1, exists s2,
s = tm_abs x S1 s2.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Theorem progress : forall t T,
has_type empty t T ->
value t \/ exists t', t --> t'.
Proof with eauto.
intros t T Ht.
remember empty as Gamma.
revert HeqGamma.
(has_type_cases (induction Ht) Case);
intros HeqGamma; subst...
Case "T_Var".
inversion H.
Case "T_App".
right.
destruct IHHt1; subst...
SCase "t1 is a value".
destruct IHHt2; subst...
SSCase "t2 is a value".
destruct (canonical_forms_of_arrow_types empty t1 T1 T2)
as [x [S1 [t12 Heqt1]]]...
subst. exists (subst x t2 t12)...
SSCase "t2 steps".
destruct H0 as [t2' Hstp]. exists (tm_app t1 t2')...
SCase "t1 steps".
destruct H as [t1' Hstp]. exists (tm_app t1' t2)...
Case "T_Proj".
right. destruct IHHt...
SCase "rcd is value".
destruct (lookup_field_in_value t T i Ti) as [t' [Hget Ht']]...
SCase "rcd_steps".
destruct H0 as [t' Hstp]. exists (tm_proj t' i)...
Case "T_RCons".
destruct IHHt1...
SCase "head is a value".
destruct IHHt2...
SSCase "tail steps".
right. destruct H2 as [tr' Hstp].
exists (tm_rcons i t tr')...
SCase "head steps".
right. destruct H1 as [t' Hstp].
exists (tm_rcons i t' tr)... Qed.
Informal proof of progress:
Theorem : For any term t and type T, if empty |- t : T
then t is a value or t --> t' for some term t'.
Proof : Let t and T be given such that empty |- t : T. We go
by induction on the typing derivation. Cases T_Abs and
T_RNil are immediate because abstractions and {} are always
values. Case T_Var is vacuous because variables cannot be
typed in the empty context.
- If the last step in the typing derivation is by T_App, then
there are terms t1 t2 and types T1 T2 such that
t = t1 t2, T = T2, empty |- t1 : T1 -> T2 and
empty |- t2 : T1.
- Suppose t1 --> t1' for some term t1'. Then
t1 t2 --> t1' t2 by ST_App1.
- Otherwise t1 is a value.
- Suppose t2 --> t2' for some term t2'. Then
t1 t2 --> t1 t2' by rule ST_App2 because t1 is a value.
- Otherwise, t2 is a value. By lemma
canonical_forms_for_arrow_types, t1 = \x:S1.s2 for some
x, S1, and s2. And (\x:S1.s2) t2 --> [t2/x]s2 by
ST_AppAbs, since t2 is a value.
- Suppose t2 --> t2' for some term t2'. Then
t1 t2 --> t1 t2' by rule ST_App2 because t1 is a value.
- Suppose t1 --> t1' for some term t1'. Then
t1 t2 --> t1' t2 by ST_App1.
- If the last step of the derivation is by T_Proj, then there
is a term tr, type Tr and label i such that t = tr.i,
empty |- tr : Tr, and ty_lookup i Tr = Some 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
desired result is exactly the induction hypothesis for the
typing subderivation.
- If the final step of the derivation is by T_RCons, then there
exist some terms t1 tr, types T1 Tr and a label t such
that t = {i=t1, tr}, T = {i:T1, Tr}, record_tm tr,
record_tm Tr, empty |- t1 : T1 and empty |- tr : Tr.
- Suppose t1 --> t1' for some term t1'. Then
{i=t1, tr} --> {i=t1', tr} by rule ST_Rcd_Head.
- Otherwise t1 is a value.
- Suppose tr --> tr' for some term tr'. Then
{i=t1, tr} --> {i=t1, tr'} by rule ST_Rcd_Tail,
since t1 is a value.
- Otherwise, tr is also a value. So, {i=t1, tr} is a value by v_rcons.
- Suppose tr --> tr' for some term tr'. Then
{i=t1, tr} --> {i=t1, tr'} by rule ST_Rcd_Tail,
since t1 is a value.
- Suppose t1 --> t1' for some term t1'. Then
{i=t1, tr} --> {i=t1', tr} by rule ST_Rcd_Head.
Inversion lemmas
Lemma typing_inversion_var : forall Gamma x T,
has_type Gamma (tm_var x) T ->
exists S,
Gamma x = Some S /\ subtype S T.
Proof with eauto.
intros Gamma x T Hty.
remember (tm_var x) as t.
(has_type_cases (induction Hty) Case); intros;
inversion Heqt; subst; try solve by inversion.
Case "T_Var".
exists T...
Case "T_Sub".
destruct IHHty as [U [Hctx HsubU]]... Qed.
Lemma typing_inversion_app : forall Gamma t1 t2 T2,
has_type Gamma (tm_app t1 t2) T2 ->
exists T1,
has_type Gamma t1 (ty_arrow T1 T2) /\
has_type Gamma t2 T1.
Proof with eauto.
intros Gamma t1 t2 T2 Hty.
remember (tm_app t1 t2) as t.
(has_type_cases (induction Hty) Case); intros;
inversion Heqt; subst; try solve by inversion.
Case "T_App".
exists T1...
Case "T_Sub".
destruct IHHty as [U1 [Hty1 Hty2]]...
assert (Hwf := has_type__wf _ _ _ Hty2).
exists U1... Qed.
Lemma typing_inversion_abs : forall Gamma x S1 t2 T,
has_type Gamma (tm_abs x S1 t2) T ->
(exists S2, subtype (ty_arrow S1 S2) T
/\ has_type (extend Gamma x S1) t2 S2).
Proof with eauto.
intros Gamma x S1 t2 T H.
remember (tm_abs x S1 t2) as t.
(has_type_cases (induction H) Case);
inversion Heqt; subst; intros; try solve by inversion.
Case "T_Abs".
assert (Hwf := has_type__wf _ _ _ H0).
exists T12...
Case "T_Sub".
destruct IHhas_type as [S2 [Hsub Hty]]...
Qed.
An informal proof of typing_inversion_abs. Note that
analogous inversion lemmas weren't stated in previous files
because Coq's built in inversion tactic gave them to us for
free. But, in STLC with subtyping, there are multiple ways
of deriving has_type instances for any particular term, so
this is no longer the case.
Theorem: If Gamma |- \x:S1.t2 : T, then there is a type
S2 such that Gamma, x:S1 |- t2 : S2 and S1 -> S2 <: T.
Proof: Let Gamma, x, S1, t2 and T be given as
described. Proceed by induction on the derivation of Gamma
|- \x:S1.t2 : T. Cases T_Var, T_App, T_Proj,
T_RNil and T_RCons are vacuous as those rules cannot be
used to give a type to a syntactic abstraction.
- If the last step of the derivation is by T_Abs then
there is a type T12 such that T = S1 -> T12 and
Gamma, x:S1 |- t2 : T12. Then picking T12 for S2
satisfies the theorem: S1 -> T12 <: S1 -> T12 follows
from S_Refl and the well-formedness theorem for
has_type.
- If the last step of the derivation is by T_Sub then there is a type S such that S <: T and Gamma |- \x:S1.t2 : S. The IH for the typing subderivation yields that there exists a type S2 such that S1 -> S2 <: S and Gamma, x:S1 |- t2 : S2. Picking type S2 satisfies the theorem, with S1 -> S2 <: T following by S_Trans.
Lemma typing_inversion_proj : forall Gamma i t1 Ti,
has_type Gamma (tm_proj t1 i) Ti ->
exists T, exists Si,
ty_lookup i T = Some Si /\ subtype Si Ti /\ has_type Gamma t1 T.
Proof with eauto.
intros Gamma i t1 Ti H.
remember (tm_proj t1 i) as t.
(has_type_cases (induction H) Case);
inversion Heqt; subst; intros; try solve by inversion.
Case "T_Proj".
assert (well_formed_ty Ti) as Hwf.
SCase "pf of assertion".
apply (wf_rcd_lookup i T Ti)...
apply has_type__wf in H...
exists T. exists Ti...
Case "T_Sub".
destruct IHhas_type as [U [Ui [Hget [Hsub Hty]]]]...
exists U. exists Ui... Qed.
Lemma typing_inversion_rcons : forall Gamma i ti tr T,
has_type Gamma (tm_rcons i ti tr) T ->
exists Si, exists Sr,
subtype (ty_rcons i Si Sr) T /\ has_type Gamma ti Si /\
record_tm tr /\ has_type Gamma tr Sr.
Proof with eauto.
intros Gamma i ti tr T Hty.
remember (tm_rcons i ti tr) as t.
(has_type_cases (induction Hty) Case);
inversion Heqt; subst...
Case "T_Sub".
apply IHHty in H0.
destruct H0 as [Ri [Rr [HsubRS [HtypRi HtypRr]]]].
exists Ri. exists Rr...
Case "T_RCons".
assert (well_formed_ty (ty_rcons i T Tr)) as Hwf.
SCase "pf of assertion".
apply has_type__wf in Hty1.
apply has_type__wf in Hty2...
exists T. exists Tr... Qed.
Lemma abs_arrow : forall x S1 s2 T1 T2,
has_type empty (tm_abs x S1 s2) (ty_arrow T1 T2) ->
subtype T1 S1
/\ has_type (extend empty x S1) s2 T2.
Proof with eauto.
intros x S1 s2 T1 T2 Hty.
apply typing_inversion_abs in Hty.
destruct Hty as [S2 [Hsub Hty]].
apply sub_inversion_arrow in Hsub.
destruct Hsub as [U1 [U2 [Heq [Hsub1 Hsub2]]]].
inversion Heq; subst... Qed.
Inductive appears_free_in : id -> tm -> Prop :=
| afi_var : forall x,
appears_free_in x (tm_var x)
| afi_app1 : forall x t1 t2,
appears_free_in x t1 -> appears_free_in x (tm_app t1 t2)
| afi_app2 : forall x t1 t2,
appears_free_in x t2 -> appears_free_in x (tm_app t1 t2)
| afi_abs : forall x y T11 t12,
y <> x ->
appears_free_in x t12 ->
appears_free_in x (tm_abs y T11 t12)
| afi_proj : forall x t i,
appears_free_in x t ->
appears_free_in x (tm_proj t i)
| afi_rhead : forall x i t tr,
appears_free_in x t ->
appears_free_in x (tm_rcons i t tr)
| afi_rtail : forall x i t tr,
appears_free_in x tr ->
appears_free_in x (tm_rcons i t tr).
Hint Constructors appears_free_in.
Lemma context_invariance : forall Gamma Gamma' t S,
has_type Gamma t S ->
(forall x, appears_free_in x t -> Gamma x = Gamma' x) ->
has_type Gamma' t S.
Proof with eauto.
intros. generalize dependent Gamma'.
(has_type_cases (induction H) Case);
intros Gamma' Heqv...
Case "T_Var".
apply T_Var... rewrite <- Heqv...
Case "T_Abs".
apply T_Abs... apply IHhas_type. intros x0 Hafi.
unfold extend. remember (beq_id x x0) as e.
destruct e...
Case "T_App".
apply T_App with T1...
Case "T_RCons".
apply T_RCons... Qed.
Lemma free_in_context : forall x t T Gamma,
appears_free_in x t ->
has_type Gamma t T ->
exists T', Gamma x = Some T'.
Proof with eauto.
intros x t T Gamma Hafi Htyp.
(has_type_cases (induction Htyp) Case); subst; inversion Hafi; subst...
Case "T_Abs".
destruct (IHHtyp H5) as [T Hctx]. exists T.
unfold extend in Hctx. apply not_eq_beq_id_false in H3.
rewrite H3 in Hctx... Qed.
Lemma substitution_preserves_typing : forall Gamma x U v t S,
has_type (extend Gamma x U) t S ->
has_type empty v U ->
has_type Gamma (subst x v t) S.
Proof with eauto.
intros Gamma x U v t S Htypt Htypv.
generalize dependent S. generalize dependent Gamma.
(tm_cases (induction t) Case); intros; simpl.
Case "tm_var".
rename i into y.
destruct (typing_inversion_var _ _ _ Htypt) as [T [Hctx Hsub]].
unfold extend in Hctx.
remember (beq_id x y) as e. destruct e...
SCase "x=y".
apply beq_id_eq in Heqe. 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'.
SCase "x<>y".
destruct (subtype__wf _ _ Hsub)...
Case "tm_app".
destruct (typing_inversion_app _ _ _ _ Htypt) as [T1 [Htypt1 Htypt2]].
eapply T_App...
Case "tm_abs".
rename i into y. rename t into T1.
destruct (typing_inversion_abs _ _ _ _ _ Htypt)
as [T2 [Hsub Htypt2]].
destruct (subtype__wf _ _ Hsub) as [Hwf1 Hwf2].
inversion Hwf2. subst.
apply T_Sub with (ty_arrow T1 T2)... apply T_Abs...
remember (beq_id x y) as e. destruct e.
SCase "x=y".
eapply context_invariance...
apply beq_id_eq in Heqe. subst.
intros x Hafi. unfold extend.
destruct (beq_id y x)...
SCase "x<>y".
apply IHt. eapply context_invariance...
intros z Hafi. unfold extend.
remember (beq_id y z) as e0. destruct e0...
apply beq_id_eq in Heqe0. subst.
rewrite <- Heqe...
Case "tm_proj".
destruct (typing_inversion_proj _ _ _ _ Htypt)
as [T [Ti [Hget [Hsub Htypt1]]]]...
Case "tm_rnil".
eapply context_invariance...
intros y Hcontra. inversion Hcontra.
Case "tm_rcons".
destruct (typing_inversion_rcons _ _ _ _ _ Htypt) as
[Ti [Tr [Hsub [HtypTi [Hrcdt2 HtypTr]]]]].
apply T_Sub with (ty_rcons i Ti Tr)...
apply T_RCons...
SCase "record_ty Tr".
apply subtype__wf in Hsub. destruct Hsub. inversion H0...
SCase "record_tm (subst x v t2)".
inversion Hrcdt2; subst; simpl... Qed.
Theorem preservation : forall t t' T,
has_type empty t T ->
t --> t' ->
has_type empty t' T.
Proof with eauto.
intros t t' T HT.
remember empty as Gamma. generalize dependent HeqGamma.
generalize dependent t'.
(has_type_cases (induction HT) Case);
intros t' HeqGamma HE; subst; inversion HE; subst...
Case "T_App".
inversion HE; subst...
SCase "ST_AppAbs".
destruct (abs_arrow _ _ _ _ _ HT1) as [HA1 HA2].
apply substitution_preserves_typing with T...
Case "T_Proj".
destruct (lookup_field_in_value _ _ _ _ H2 HT H)
as [vi [Hget Hty]].
rewrite H4 in Hget. inversion Hget. subst...
Case "T_RCons".
eauto using step_preserves_record_tm. Qed.
Informal proof of preservation:
Theorem: If t, t' are terms and T is a type such that
empty |- t : T and t --> t', then empty |- t' : T.
Proof: Let t and T be given such that empty |- t : T. We go
by induction on the structure of this typing derivation, leaving
t' general. Cases T_Abs and T_RNil are vacuous because
abstractions and {} don't step. Case T_Var is vacuous as well,
since the context is empty.
☐
- If the final step of the derivation is by T_App, then there
are terms t1 t2 and types T1 T2 such that t = t1 t2,
T = T2, empty |- t1 : T1 -> T2 and empty |- t2 : T1.
- If the final step of the derivation is by T_Proj, then there
is a term tr, type Tr and label i such that t = tr.i,
empty |- tr : Tr, and ty_lookup i Tr = Some 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.
- If the final step of the derivation is by T_RCons, then there
exist some terms t1 tr, types T1 Tr and a label t such
that t = {i=t1, tr}, T = {i:T1, Tr}, record_tm tr,
record_tm Tr, empty |- t1 : T1 and empty |- tr : Tr.
Exercises on typing
Exercise: 2 stars, optional (variations)
Each part of this problem suggests a different way of changing the definition of the STLC with records 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:
Gamma |- t : S1->S2 S1 <: T1 T1 <: S1 S2 <: T2 (T_Funny1) Gamma |- t : T1->T2 - Suppose we add the following reduction rule:
(ST_Funny21) {} --> (\x:Top. x) - Suppose we add the following subtyping rule:
(S_Funny3) {} <: Top->Top - Suppose we add the following subtyping rule:
(S_Funny4) Top->Top <: {} - Suppose we add the following evaluation rule:
(ST_Funny5) ({} t) --> (t {}) - Suppose we add the same evaluation rule *and* a new typing rule:
(ST_Funny5) ({} t) --> (t {}) (T_Funny6) empty |- {} : Top->Top - Suppose we *change* the arrow subtyping rule to:
S1 <: T1 S2 <: T2 (S_Arrow') S1->S2 <: T1->T2
Major exercise: adding sums and 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 ty_cases and tm_cases.)
- Extend the well-formedness relation in the obvious way.
- Extend the operational semantics with the same reduction rules as
in the last chapter.
- 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 the last chapter.
- 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.)