Stream: Coq users

Topic: The module system


view this post on Zulip Gergely Buday (Jul 27 2020 at 07:24):

About the module system I have found this terse and technical article:

https://coq.inria.fr/refman/language/module-system.html

Is there a more educative tutorial for it?

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 08:13):

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.

view this post on Zulip Gergely Buday (Jul 27 2020 at 08:20):

Thanks, it is more of tutorial nature now. In the meantime I have found

https://github.com/coq/coq/wiki/ModuleSystemTutorial

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 08:22):

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.

view this post on Zulip Erik Martin-Dorel (Jul 27 2020 at 13:25):

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)

view this post on Zulip Karl Palmskog (Jul 27 2020 at 13:25):

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

view this post on Zulip Paolo Giarrusso (Jul 27 2020 at 14:19):

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.

view this post on Zulip Karl Palmskog (Jul 27 2020 at 14:20):

this was my recommendation as well here: https://coq.discourse.group/t/how-to-learn-coqs-module-system/218

view this post on Zulip Karl Palmskog (Jul 27 2020 at 14:21):

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)

view this post on Zulip Paolo Giarrusso (Jul 27 2020 at 14:25):

I was wondering about OCaml's, but some features of Coq modules (generative functors?) seem closer to SML?

view this post on Zulip Karl Palmskog (Jul 27 2020 at 14:29):

it has some features of both, from my recollection.


Last updated: Feb 06 2023 at 12:04 UTC