Core Definitions

Syntax

Well-Formedness

Substitution

Reduction

Subtyping

Definition

Subtyping Examples and Exercises

Exercise: 2 stars

Exercise: 1 star

Exercise: 1 star

Exercise: 2 stars

Properties of Subtyping

Well-Formedness

Field Lookup

Exercise: 3 stars (rcd_types_match_informal)

Inversion Lemmas

Exercise: 3 stars, optional (sub_inversion_arrow)

Typing

Typing Examples

Exercise: 1 star

Exercise: 2 stars

Exercise: 2 stars, optional

Properties of Typing

Well-Formedness

Field Lookup

Progress

Exercise: 3 stars (canonical_forms_of_arrow_types)

• 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.
  The induction hypotheses for these typing derivations yield that t1 is a value or steps, and that t2 is a value or steps. We consider each case:
  • 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 ⇒ [x:=t2]s2 by ST_AppAbs, since t2 is a value.
• 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 Tlookup i Tr = Some T.
  The IH for the typing subderivation gives us that either tr is a value or it steps. If tr ⇒ tr' for some term tr', then tr.i ⇒ tr'.i by rule ST_Proj1.
  Otherwise, tr is a value. In this case, lemma lookup_field_in_value yields that there is a term ti such that tlookup i tr = Some ti. It follows that tr.i ⇒ ti by rule ST_ProjRcd.
• 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.
  The induction hypotheses for these typing derivations yield that t1 is a value or steps, and that tr is a value or steps. We consider each case:
  • 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.

Inversion Lemmas

Context Invariance

Preservation

• 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.
  By inspection of the definition of the step relation, there are three ways t1 t2 can step. Cases ST_App1 and ST_App2 follow immediately by the induction hypotheses for the typing subderivations and a use of T_App.
  Suppose instead t1 t2 steps by ST_AppAbs. Then t1 = \x:S.t12 for some type S and term t12, and t' = [x:=t2]t12.
  By Lemma abs_arrow, we have T1 <: S and x:S1 ⊢ s2 : T2. It then follows by lemma substitution_preserves_typing that empty ⊢ [x:=t2] t12 : T2 as desired.
• 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 Tlookup i Tr = Some T.
  The IH for the typing derivation gives us that, for any term tr', if tr ⇒ tr' then empty ⊢ tr' Tr. Inspection of the definition of the step relation reveals that there are two ways a projection can step. Case ST_Proj1 follows immediately by the IH.
  Instead suppose tr.i steps by ST_ProjRcd. Then tr is a value and there is some term vi such that tlookup i tr = Some vi and t' = vi. But by lemma lookup_field_in_value, empty ⊢ vi : Ti as desired.
• 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.
  By the definition of the step relation, t must have stepped by ST_Rcd_Head or ST_Rcd_Tail. In the first case, the result follows by the IH for t1's typing derivation and T_RCons. In the second case, the result follows by the IH for tr's typing derivation, T_RCons, and a use of the step_preserves_record_tm lemma.

Exercises on Typing

Exercise: 2 stars, optional (variations)

• 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)
  {} ⇒ (\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