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.