ModulesNotRecords
soraros edited this page May 12, 2019
·
6 revisions
In facts before deciding between Records and Modules, consider the following:
- Will you need to build a structure of this "type" "à la volée"
- If so, a Record is probably better as you can't do inside terms a
let m := ⟨module⟩ in ⟨expr⟩
- If so, a Record is probably better as you can't do inside terms a
- Do you want something very modular; for instance given three module types
A
,B
andC
, and two functors,f : A → B
andg : B → C
, be able to define the functorh : A → C
, byh = g ∘ f
?- If so, Records are more ... modular than ... modules...
- Will your structure be extracted or do you want it extractable to caml/Haskell/...?
- If so, I don't recommend use of Record (except maybe if you can express it directly with a record in the target language)
- Will you need to define useful tactics inside your module?
- If so you won't be able to define them inside Records, and lose the "dot" notation.
- Will you need some toplevel instructions, such as "Implicit Arguments", "Print" and so...
- Use Modules (Note that for Notations, you have a way to use "Reserved Notation" and "where" for Records)
- Will you need some performances?
- Use Modules, all is defined at toplevel and won't require function calls
In all other cases, Records are often a better solution.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.