Adding Records

We saw in MoreStlc.v how records can be treated as syntactic sugar for nested uses of products. This is fine for simple examples, but the encoding is informal (in reality, if we really treated records this way, it would be carried out in the parser, which we are eliding here), and anyway it is not very efficient. So it is also interesting to see how records can be treated as first-class citizens of the language. Recall the informal definitions we gave before: Syntax:

       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 type

Reduction:

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

Typing:

Γ ⊢ t1 : T1     ...     Γ ⊢ tn : Tn	(T_Rcd)
Γ ⊢ {i1=t1, ..., in=tn} : {i1:T1, ..., in:Tn}

Γ ⊢ t : {..., i:Ti, ...}	(T_Proj)
Γ ⊢ t.i : Ti

Formalizing Records

Syntax and Operational Semantics

The most obvious way to formalize the syntax of record types would be this:

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.

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.

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.

Some variables, for examples...

{ i1:A }

{ i1:A→B, i2:A }

Well-Formedness

Generalizing our abstract syntax for records (from lists to the nil/cons presentation) introduces the possibility of writing strange types like this

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 just ty_rnil and ty_rcons at the outermost level.

Similarly, a term is a record term if it is built with tm_rnil and tm_rcons

Note that record_ty and record_tm are not recursive — they just check 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, not just types; 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

Substitution

Reduction

Next we define the values of our language. A record is a value if all of its fields are.

Utility functions for extracting one field from record type or term:

The step function uses the term-level lookup function (for the projection rule), while the type-level lookup is needed for has_type.

Typing

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 Γ 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.

Examples

Exercise: 2 stars (examples)

Finish the proofs. 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.

Before starting to prove this fact (or the one above!), make sure you understand what it is saying.

Properties of Typing

The proofs of progress and preservation for this system are essentially the same as for the pure simply typed lambda-calculus, but we need to add some technical lemmas involving records.

Well-Formedness

Field Lookup

Lemma: If empty ⊢ v : T and ty_lookup i T returns Some Ti, then tm_lookup i v returns Some ti for some term ti such that has_type empty ti Ti. Proof: By induction on the typing derivation Htyp. Since ty_lookup i T = Some Ti, T must be a record type, this and the fact that v is a value eliminate most cases by inspection, leaving only the T_RCons case. If the last step in the typing derivation is by T_RCons, then t = tm_rcons i0 t tr and T = ty_rcons i0 T Tr for some i0, t, tr, T and Tr. This leaves two possiblities to consider - either i0 = i or not.

• 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 Tr
  and
  tm_lookup i t = tm_lookup i tr,
  so the result follows from the induction hypothesis. ☐

Progress

Context Invariance

Preservation

☐