The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

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\...