About the module system I have found this terse and technical article:
Is there a more educative tutorial for it?
In 8.12, the documentation of the module system in the reference manual has been consolidated into a single page (https://coq.github.io/doc/v8.12/refman/language/core/modules.html) and some examples have been added, so it should be slightly better, although not revolutionary since the content hasn't changed so much.
Thanks, it is more of tutorial nature now. In the meantime I have found
If you do find some additions that would make sense to incorporate into the reference manual to make it better, do not hesitate to contribute.
BTW @Gergely Buday here is an old StackOverflow question you might be interested in: https://stackoverflow.com/a/49717951 (which notably deals with the
Include vernacular and
<+ notation that don't seem to be covered in the ModuleSystemTutorial)
the Coq'Art book also has a module tutorial, here are sources/exercises: https://github.com/coq-community/coq-art/tree/master/ch12_modules/SRC
I don't know if it's a good idea, but I have mostly learned Coq modules after I learned ML modules first — many principles are (intentionally) closely related. Not sure if that's a road to recommend.
this was my recommendation as well here: https://coq.discourse.group/t/how-to-learn-coqs-module-system/218
the SML module system is arguably what all kinds of programming-relevant abstraction principles should be judged against (e.g., in that it subsumes Haskell-style type classes)
I was wondering about OCaml's, but some features of Coq modules (generative functors?) seem closer to SML?
it has some features of both, from my recollection.
Last updated: Feb 06 2023 at 12:04 UTC