The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jan,

I have similar issues from time to time. I thought about refactoring parts of 
the standard library such that all the basics are done with records and/or 
type classes and to use modules only as (sometimes) convenient wrappers 
around this. The main advantages of modules over records and type classes are 
that they are less strict (as far as I can tell module types are compared by 
signature equivalence) and that one can embed tactics and database hints in 
modules. The main advantage of records and type calsses is that they can be 
used in inductives. I think a collection of a structure definition and proofs 
could be done using records and type classes as well. It should also be 
possible to keep the flexibility of the module system by making modules which 
derive an "implementation record" from an equivalent module. So the idea is 
that one can use record / type class based definitions of e.g. a MSet in 
inductives and uses modules to create concrete intances of these and to 
prepare a convenient environment for automating proofs for such structures.

The main reason I didn't explore this as yet is that I wonder how agreeable 
something like this would be in the community. Or put more general: the Coq 
standard library looks in some places more evolved than designed and I wonder 
how otheres weight compatibility vs. improvement in the design. I would very 
much enjoy a discussion on how the Coq library should look like and how we 
get there.

Also if someone is interested in working together on exploring such ideas, 
please let me know.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Jan Bessai
Sent: Sunday, August 16, 2015 4:45 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Nesting MSet in an inductive type

Is there any way to get around the limitation by losing abstraction? It would 
probably be ok for me to be restricted e.g. to red-black trees.
Their implementation is backed by Coq.MSets.MSetGenTree and has a concrete 
type independent of the order. Unfortunately, to instantiate the 
Coq.MSets.MSetGenTree.Ops module OrderedType is required again. I would also 
accept duplicating the tree type definition. But then Ops in 
Coq.MSets.MSetRBT is a concrete module rather than a module type, so it 
cannot include the copied (identical..) definition by inheritance.

Would factoring out tree from MSetGenTree.Ops into a separate module
(type?) and parametrizing MSetRBT and MSetAVL over it be something acceptable 
as a pull request for the standard libs?
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928