Core Definitions

Syntax

Well-Formedness

Substitution

Reduction

Subtyping

Definition

Examples

Exercise: 2 stars (subtyping_example_1)

Exercise: 1 star (subtyping_example_2)

Exercise: 1 star (subtyping_example_3)

Exercise: 2 stars (subtyping_example_4)

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 (typing_example_0)

Exercise: 2 stars (typing_example_1)

Exercise: 2 stars, optional (typing_example_2)

Properties of Typing

Well-Formedness

Field Lookup

Progress

Exercise: 3 stars (canonical_forms_of_arrow_types)

• The cases where the last step in the typing derivation is T_Abs or T_RNil are immediate because abstractions and {} are always values. The case for 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 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.
  • 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₁.s2 for some x, S₁, and s₂. But then (λx:S₁.s2) 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 are a term tr, a type Tr, and a label i such that t = tr.i, empty ⊢ tr : Tr, and Tlookup i Tr = Some T.
  By the IH, either tr is a value or it steps. If tr ⇒ tr' for some term tr', then tr.i ⇒ tr'.i by rule ST_Proj1.
  If tr is a value, then 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.t12 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.