The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Yes, Matthieu Sozeau has added the option to make records primitive, which gives them judgmental eta and projections that don't (need to) take any of the arguments of the record type.  I don't know if this is enabled for coinductive types or for recursive types.

On Thu, Oct 2, 2014 at 2:19 PM, Gregory Malecha <gmalecha AT cs.harvard.edu> wrote:

Thanks.

I seem to recall hearing somewhere that in 8.5 records were getting some ability to elide parameters, though maybe this is just in projections.

On Thu, Oct 2, 2014 at 12:49 PM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

Record *can* be recursive. It's just that you cannot use the "Record" keyword to that effect (so that you can choose between inductive records and co-inductive records). They cannot appear in mutually inductive type definitions, however, because nobody has managed to make that work properly (but I don't think there is any theoretical issue here). The "Record" keyword is intended for non-recursive records (in trunk, the induction principle is not generated when you use the "Record" keyword, I've also added a dual "Variant" for non-recursive variant types).

Let me print the error message that Coq v8.4 prints when you try to write an inductive record:

Error: Records declared with the keyword Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.

I don't know how I could have been much clearer. Maybe the reference manual needs updating (though I may have done some improvement in trunk already, I don't remember). If so, let me know what is confusing.

CoInductive Stream (A:Type) := {
  head : A;
  tail : Stream A
}.
(* Stream is defined
head is defined
tail is defined *)

/Arnaud

On 2 October 2014 17:15, Cedric Auger <sedrikov AT gmail.com> wrote:

I have complained many times on the fact that records are not allowed to be recursive.
I even tried many times to patch Coq my self to have this feature, but each time I gave up because it was affecting stuff I did not want to modify in the code.
I do not remember the details, but that Coq type classes are implemented over Records for instance. Furthermore the pieces of code I tried to modify relied heavily on type inference, and my brain was not powerfull enough to understand what the underlying types were.

You might be interested by this feature request:
https://coq.inria.fr/bugs/show_bug.cgi?id=2779

I guess that one of the initial arguments against such a feature is that a recursive record is not well founded (well in fact, it is not the case, but it is easy to be tricked).
Counter examples are:

Mutual induction:

Record list_header(A : Type): Type :=
 { head : A;
   tail : list A }
with list(A : Type): Type :=
 | Nil : list A
 | Cons : list_header A -> list A.

Accessibility predicate:

Record Acc(T:Type)(P:T->T->Prop): T->Prop :=
fun (t:T) => { Rec: forall u, P u t -> Acc T P u }.

2014-10-02 16:46 GMT+02:00 Gregory Malecha <gmalecha AT cs.harvard.edu>:

Hi --

Is the a theoretical reason why records can not be recursive? My understanding has always been that [Record] is just syntactic sugar for [Inductive] which generates some extra projection functions. I know that this will change in Coq 8.5 and records will become a new primitive, so will there become a reason why they can't be recursive?

Thanks.

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/

--
.../Sedrikov\...

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/