The Coq mailing list

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

Since nobody seemed to be annoyed by the change I proposed, I've
implemented it. Each inductive type now contains internally a boolean
flag which is true iff this inductive has been defined via "Record".
And the subtyping checks this flag, and also the field names for records.
In particular, the oddities mentioned in my previous mail are now refused
by Coq.

I've also patched the extraction to take advantage of this flag. This
should solve the problems about record extraction encountered by Francois
Armand and David Pichardie.

These modifications are now integrated in Coq cvs. It will hence be part
of Coq next release. In the meantime, if somebody needs to correct his
Coq and is unwilling to use Coq cvs (which is quite calm & stable those
days though), please contact me, I can provide a patch against Coq 8.0.

Thanks for your reports (and your patience)

Pierre Letouzey


On Tue, 8 Jun 2004, Pierre Letouzey wrote:

>
> 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
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>