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 t₁ t₂ and types T₁ T₂ such that t = t₁ t₂, T = T₂, empty ⊢ t₁ : T₁ → T₂ and empty ⊢ t₂ : T₁.
  The induction hypotheses for these typing derivations yield that t₁ is a value or steps, and that t₂ is a value or steps. We consider each case:
  • Suppose t₁ ⇒ t₁' for some term t₁'. Then t₁ t₂ ⇒ t₁' t₂ by ST_App1.
  • Otherwise t₁ is a value.
    • Suppose t₂ ⇒ t₂' for some term t₂'. Then t₁ t₂ ⇒ t₁ t₂' by rule ST_App2 because t₁ is a value.
    • Otherwise, t₂ is a value. By lemma canonical_forms_for_arrow_types, t₁ = \x:S₁.s₂ for some x, S₁, and s₂. And (\x:S₁.s₂) t₂ ⇒ [x:=t₂]s₂ by ST_AppAbs, since t₂ 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 t₁ tr, types T₁ Tr and a label t such that t = {i=t₁, tr}, T = {i:T₁, Tr}, record_tm tr, record_tm Tr, empty ⊢ t₁ : T₁ and empty ⊢ tr : Tr.
  The induction hypotheses for these typing derivations yield that t₁ is a value or steps, and that tr is a value or steps. We consider each case:
  • Suppose t₁ ⇒ t₁' for some term t₁'. Then {i=t₁, tr} ⇒ {i=t₁', tr} by rule ST_Rcd_Head.
  • Otherwise t₁ is a value.
    • Suppose tr ⇒ tr' for some term tr'. Then {i=t₁, tr} ⇒ {i=t₁, tr'} by rule ST_Rcd_Tail, since t₁ is a value.
    • Otherwise, tr is also a value. So, {i=t₁, 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 t₁ t₂ and types T₁ T₂ such that t = t₁ t₂, T = T₂, empty ⊢ t₁ : T₁ → T₂ and empty ⊢ t₂ : T₁.
  By inspection of the definition of the step relation, there are three ways t₁ t₂ 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 t₁ t₂ steps by ST_AppAbs. Then t₁ = \x:S.t₁₂ for some type S and term t₁₂, and t' = [x:=t₂]t₁₂.
  By Lemma abs_arrow, we have T₁ <: S and x:S₁ ⊢ s₂ : T₂. It then follows by lemma substitution_preserves_typing that empty ⊢ [x:=t₂] t₁₂ : T₂ 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 t₁ tr, types T₁ Tr and a label t such that t = {i=t₁, tr}, T = {i:T₁, Tr}, record_tm tr, record_tm Tr, empty ⊢ t₁ : T₁ 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 t₁'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