# How to learn Coq's module system?
**URL:** https://discourse.rocq-prover.org/t/how-to-learn-coqs-module-system/218
**Category:** Using Rocq
**Created:** [March 12, 2019, 7:43am UTC](https://discourse.rocq-prover.org/t/how-to-learn-coqs-module-system/218 "2019-03-12T07:43:29Z")
**Posts on this page:** 3
**Page:** 1
### Author:  [@luochen1990](https://discourse.rocq-prover.org/u/luochen1990)
#### Post date: [March 12, 2019, 7:43am UTC](https://discourse.rocq-prover.org/t/how-to-learn-coqs-module-system/218/1 "2019-03-12T07:43:29Z")
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](https://coq.inria.fr/refman/language/module-system.html), 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](https://github.com/coq/coq/wiki/ModuleSystemTutorial), 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?
---
### Author:  [@palmskog](https://discourse.rocq-prover.org/u/palmskog)
#### Post date: [March 12, 2019, 5:54pm UTC](https://discourse.rocq-prover.org/t/how-to-learn-coqs-module-system/218/2 "2019-03-12T17:54:24Z")
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](https://dev.realworldocaml.org/files-modules-and-programs.html). OCaml has `open` instead of `Import`, and `Require` (which just makes a module available) is handled by the OCaml compiler.
---
### Author:  [@MSoegtrop](https://discourse.rocq-prover.org/u/MSoegtrop)
#### Post date: [August 18, 2019, 8:32am UTC](https://discourse.rocq-prover.org/t/how-to-learn-coqs-module-system/218/3 "2019-08-18T08:32:20Z")
Adam Chlipala’s book has a short section on modules, towards the end of:
[CPDT-Large](http://adam.chlipala.net/cpdt/html/Large.html)
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.
