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 ?
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
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.
Are you wondering if Numbers
switch away from modules (breakage would be huge), or sth else?
Last updated: Oct 13 2024 at 01:02 UTC