I have finished the practices of sf/lf and part of sf/plf , and I’m familiar with many other language’s module system, such as haskell/python/javascript, but still can’t grasp Coq’s module system, I think it is the most complex one.
To learn Coq’s module system, I read the following resources:
First is the official doc, it’s all about definition of abstract noun and formulas, and tells nothing about the situation and usage. I felt helpless.
Then I go to the wiki, it start with telling me how to write my own module. but why I need to write a module for just min and max, and what is the name Sig for? and why there is utf8 ?
The most important things is, I still have a lot of basic problems about Coq’s modules, but these tutorial tells nothing about them, e.g.
- How can I find a module I want? by name? by type? via google? is there a site similar to hoogle for haskell?
- How to use an existing module I found? what’s the different between Import/Require?
- What is the relationship between Module and Scope?
- How does Coq organize it’s internal modules? what is the principle?
Is there any suggestion or better resources for learning Coq’s module system?
3 Likes
Coq’s module system is quite similar to OCaml’s module system, and Coq modules can generally be extracted to OCaml modules. Hence, it may be a good idea to look at documentation for the OCaml module system. OCaml has open instead of Import, and Require (which just makes a module available) is handled by the OCaml compiler.
Adam Chlipala’s book has a short section on modules, towards the end of:
CPDT-Large
Regarding your questions:
- I am not aware of any mechanism for this.
- You Require the file that contains the module definition. Import is used to make the contents of a file or module accessible with a short not fully qualified name. Afaik Import also makes things like notations and hint database definitions defined in a module available. Files are similar to modules in this respect. Another frequent usage of existing modules, or better of module functors, is to define a local module by providing parameters to a module functor.
- In case you are talking about scope in the sense of ‘Open Scope’ and not in the sense of naming modules and definitions inside modules: modules can define new scopes and extend existing scopes with new notations. In case you are talking about name qualification, see the notes on Import above.
- I didn’t find anybody who claimed that there are strong design principles behind naming and structuring modules in the standard library - this is one of the reasons for developing a standard library 2.0. I attached an image (which might be outdated, I did a few years ago) of the structure of the modules for ordered types. This doesn’t include everything and for most modules and module functors there is a variant with ’ which includes notations.
1 Like
