How to learn Coq's module system?

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.

  1. How can I find a module I want? by name? by type? via google? is there a site similar to hoogle for haskell?
  2. How to use an existing module I found? what’s the different between Import/Require?
  3. What is the relationship between Module and Scope?
  4. 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?


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:


Regarding your questions:

  1. I am not aware of any mechanism for this.
  2. 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.
  3. 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.
  4. 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