Stream: Coq users

Topic: Modules


view this post on Zulip Pierre Rousselin (Oct 12 2023 at 12:53):

I am currently trying to understand the Numbers sublibrary. It makes a constant use of Coq modules and module Types. The same is true for the Structures sublibrary.

Are module types still used a lot in recent developments ? Are there general guidelines about using Modules or not ?

view this post on Zulip Karl Palmskog (Oct 12 2023 at 12:55):

quite few mathematical libraries use module types, probably since typeclasses and canonical structures are much more popular for describing hierarchies of structures. The primary users of module types are probably computer science applications, e.g., https://github.com/coq-community/coq-mmaps

view this post on Zulip Karl Palmskog (Oct 12 2023 at 12:56):

I think the standard argument against module types are that they are not "first class" (require special typing rules), while dependent records are first class and can do most of what you want, most of the time.

view this post on Zulip Paolo Giarrusso (Oct 12 2023 at 17:29):

Are you wondering if Numbers switch away from modules (breakage would be huge), or sth else?


Last updated: Jun 23 2024 at 04:03 UTC