Enriching Coq with primitive records.


Up to now, (dependent) records are represented in Coq by the means of
single-constructor inductive types; record subtyping (the possibility
to forget fields when applying a function to a record) is in turn
encoded using coercions. Dependent records are in particular useful
when formalising mathematical structures in a system like Coq.

In this talk, I shall describe an experimental enrichment of Coq with
primitive dependent record types and a notion of subtyping. The idea
is to adapt the work of Betarte and Tasistro (as done in Alf), and to
introduce:

   1/ record types: each field is defined by its label (an identifier)
   and its type, possibly depending on other fields of the record
   type;

   2/ a notion of subtyping between record types: when omitting a
   field in a given record type, we move to a supertype;
   
   3/ record objects, i.e. terms whose type is a record type: each
   field is defined by its label and value;

   4/ record selection, which is our notion of reduction: if r is a
   record object and l is a label, then r#l is the value associated to
   field l in r (if l is present in r)

I will describe this extension, and try to enlighten the
implementation issues that arise when adding record types to Coq. I
will also discuss an effort to recast Coq's "Record" keyword (which is
a macro to generate inductive types) into the setting of primitive
record types. Finally, I will hint on a few extra facilites that can
be added to ease the manipulation of primitive records.