We saw in chapter MoreStlc how records can be treated as just syntactic sugar for nested uses of products. This is OK for simple examples, but the encoding is informal (in reality, if we actually 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. This chapter shows how.
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'
t1 ==> t1'
Typing:
Gamma |- t1 : T1 ... Gamma |- tn : Tn
Gamma |- t : {..., i:Ti, ...}
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 TRcd 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 the principle we obtain 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 standard Coq list type, we can essentially incorporate its
constructors (nil
and cons
) in the syntax of our types.
Similarly, at the level of terms, we have constructors trnil, for the empty record, and rcons, which adds a single field to the front of a list of fields.
Some examples...
{ i1:A }
{ i1:A->B, i2:A }
One issue with generalizing the abstract syntax for records from lists to the nil/cons presentation is that it 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 ever assigned to terms. To support this, we define predicates 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 RNil and RCons at the outermost level.
With this, we can define well-formed types.
Note that record_ty is not recursive -- it just checks 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 RCons) is a record.
Of course, we should also be concerned about ill-formed terms, not just types; but typechecking can rule those out without the help of an extra well_formed_tm definition because it already examines the structure of terms. All we need is an analog of record_ty saying that a term is a record term if it is built with trnil and rcons.
Substitution extends easily.
A record is a value if all of its fields are.
To define reduction, we'll need a utility function for extracting one field from record term:
The step function uses this term-level lookup function in the projection rule.
Next we define the typing rules. These are nearly direct transcriptions of the inference rules shown above: the only significant 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.
One sanity condition that we'd like to maintain is that, whenever has_type Gamma t T holds, will also be the case that well_formed_ty T, so that 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.
Finish the proofs below. 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 proofs first using the basic features (apply instead of eapply, in particular) and then perhaps compress it using automation. Before starting to prove anything, make sure you understand what it is saying.
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.
Lemma: If empty |- v : T and Tlookup i T returns Some Ti, then tlookup i v returns Some ti for some term ti such that empty |- ti \in Ti.
Proof: By induction on the typing derivation Htyp. Since Tlookup 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 = rcons i0 t tr and T = RCons i0 T Tr for some i0, t, tr, T and Tr.
This leaves two possiblities to consider - either i0 = i or not.
Tlookup i T = Tlookup i Tr
and
tlookup i t = tlookup i tr,
so the result follows from the induction hypothesis.
Here is the formal statement: