I'm generally confused about the module system, but specifically confused about the following point. I have a module type
foo containing a parameter declaration, and a module
myfoo : foo instantiating that parameter with a definition. However, when I try to use anything from
myfoo, it behaves as if no instantiation actually happened. The definition does not compute to its own body, and printing the definition prints something weird. If I remove the
: foo type annotation, things work as I'd expect. What's going on here, and why?
Module Type foo. Parameter n : nat. End foo. Module myfoo : foo. Definition n := 3. End myfoo. Eval cbv in myfoo.n. (* = myfoo.n * : nat *) Print myfoo.n. (* *** [ myfoo.n : nat ] *) Goal myfoo.n = 3. Fail reflexivity.
The type annotation indeed seals the module. If you just want to check the type without sealing you can do
Aha, I'd seen that syntactic form in the documentation, but thought that the only difference was whether the interface was restricted to just the parameters of the module type. I guess the mnemonic here is that
: restricts the entire observable behaviour of the module to what is specified by the module type, right?
Yeah that sounds right.
James Wood has marked this topic as resolved.
Incidentally, if someone is looking for some documentation to improve, The Module System would be a good one to do, in my opinion. I'd be willing to discuss my problems with it.
Last updated: Oct 03 2023 at 02:34 UTC