In this chapter, we combine two significant extensions of the pure STLC -- records (from chapter Records) and subtyping (from chapter Sub) -- and explore their interactions. Most of the concepts have already been discussed in those chapters, so the presentation here is somewhat terse. We just comment where things are nonstandard.
The syntax of terms and types is a bit too loose, in the sense
that it admits things like a record type whose final tail
is
Top or some arrow type rather than Nil. To avoid such cases,
it is useful to assume that all the record types and terms that we
see will obey some simple well-formedness conditions.
An interesting technical question is whether the basic properties of the system -- progress and preservation -- remain true if we drop these conditions. I believe they do, and I would encourage motivated readers to try to check this by dropping the conditions from the definitions of typing and subtyping and adjusting the proofs in the rest of the chapter accordingly. This is not a trivial exercise (or I'd have done it!), but it should not involve changing the basic structure of the proofs. If someone does do it, please let me know. --BCP 5/16.
Substitution and reduction are as before.
Now we come to the interesting part, where the features we've added start to interact. We begin by defining the subtyping relation and developing some of its important technical properties.
The definition of subtyping is essentially just what we sketched
in the discussion of record subtyping in chapter Sub, but we
need to add well-formedness side conditions to some of the rules.
Also, we replace the n-ary
width, depth, and permutation
subtyping rules by binary rules that deal with just the first
field.
The following facts are mostly easy to prove in Coq. To get full benefit, make sure you also understand how to prove them on paper!
To get started proving things about subtyping, we need a couple of technical lemmas that intuitively (1) allow us to extract the well-formedness assumptions embedded in subtyping derivations and (2) record the fact that fields of well-formed record types are themselves well-formed types.
The record matching lemmas get a little more complicated in the presence of subtyping, for two reasons. First, record types no longer necessarily describe the exact structure of the corresponding terms. And second, reasoning by induction on typing derivations becomes harder in general, because typing is no longer syntax directed.
Write a careful informal proof of the rcd_types_match lemma.
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 proceed by induction on the given typing derivation.
The induction hypotheses for these typing derivations yield that t1 is a value or steps, and that t2 is a value or steps.
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.
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:
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.
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.
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.
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.