The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

Dear Coq users

After a question on this list about Coq records and extraction, I
would like to open a broader discussion about some features that Coq
records have when used in conjonction with modules & signatures. These
features can be called either "unnatural" or "powerful", depending of your
point of view. Anyway, they are certainly "annoying" from my point of
view, which is program extraction to ML (especially Ocaml).

Here comes a quick description of these strange features. Let me first
remind that a Coq record like

  Record R:Set := { a : nat }.

is currently pure syntactic sugar for the following inductive type
and projection:

  Inductive R:Set := Build_R : forall a:nat, R.
  Definition a (r:R) : nat := match r with Build_R a => a end.

So you can define the following signature and module:

  Module Type S.
    Inductive R:Set := Build_R : forall a:nat, R.
  End S.
  Module M:S.
    Record R:Set := { a : nat }.
  End M.

And the (sub)typing relation between M and S is correct. In addition to
mixing records and inductive types, you can also "cheat" with record field
names:

  Module Type S.
    Record R:Set := { a : nat }.
  End S.
  Module M:S.
    Record R:Set := { b : nat }.
    Definition a := b.
  End M.

Here, Coq only checks the two underlying inductive types, the only ones
seen by the kernel, and their constructor types are indeed equal:
(forall a:nat,R)=(forall b:nat,R). Then, you only need to define a new
projection "a" convertible with projection "b", and the subtyping is
allowed.

Of course, these curiousities are a nightmare for extraction, since in
Ocaml, records and inductive types are strictly separated, and one cannot
change the field name of a record between signature and implementation.
Extraction could probably support these examples via tricky functors
wrappers, but I would prefer not to use such a solution. So the questions
are:
- has anyone already taken advantage of these "features" of records ?
- would you object to a change of Coq typing system, in order to enforce:
  1) that a record (resp. an inductive type) in a signature is only
  implemented by a record (resp. an inductive type), and
  2) that the record field names are checked during module subtyping ?

To my knowledge, such a change would be a slight source of incompatibility
with the previous system, but no developments nor documentation (in
particular the Coq'Art) would have to be fixed. More generally, this would
be a first (small) step toward first-class records in Coq.

Any remarks ?

Pierre Letouzey