The Coq mailing list

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

Dear Benjamin,

I just saw that my answer didn't make it through the mail server - it 
contained an image and was too large.

I wanted to write something down 2016, but I ran into severe issues with my 
samples with the module structure of the standard library. The example was 
about maps implemented as ordered tress and using a module functor to extend 
a given ordered key module with a plus and minus infinity element (and the 
correspondingly extended order). This makes the specification of subtree key 
ranges easier, because one can use infinity as range for the whole tree. 
Doing this, I ended up rewriting half of the order modules of the standard 
library.

I think it is really difficult to come up with a good module system tutorial 
when the methods advocated in there are incompatible with the standard 
library. But it might be that I overdid things 2 years back. If it is really 
as bad as I concluded back then, I guess it would be best to rework the 
standard library and make this serve as a good example.

Something I would like to discuss is an appropriate naming scheme for related 
modules, module types, module functors, module type functors, aggregated 
modules, module types, module functors and module type functors, modules 
providing notations and those containing notations, module types requesting 
functions, module types specifying such functions, modules implementing such 
functions and modules showing that the specifications hold, module types just 
wrapping type classes and the type class name and a few others.

My original post contained an image of how this is done in the standard 
library for orders - it didn't get through I will post it somewhere and send 
the link after I reviewed my rewrites of this.

Best regards,

Michael
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, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928