The Coq mailing list

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

Dear Cedric,

 

Stephen Lescuyer’s  contribution is definitely an interesting read. He seems to first have followed similar ideas as I outlined below, e.g. there is a file “Bridge.v” to interface module based and type class based orders, but later he seems to have discarded this, since everything in this file is commented out. Still there are quite a few modules with function definitions and theorems in this work and it is not easy to understand why certain things are in modules rather than in records or type classes. My idea would be to keep functions and theorems in records or type classes to maintain the “first class citizen” property on a broad scope and use modules only for convenience features (tactics, hints, syntactic sugar). I guess one really has to use this in order to find out the pros and cons.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Cedric Auger
Sent: Monday, August 24, 2015 2:19 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Nesting MSet in an inductive type

 

Stephane Lescuyer wrote a containers library using type classes instead of modules.

So that may interest you.

Personnaly, I do not see the fact that they can be used in inductives as the main advantage over modules, but rather that they are first class citizens. Indeed you can build an inhabitant "à la volée". It is far more convenient than defining awkward intermediate modules and functors to have something dependant on some parameter.

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