Stream: Coq users

Topic: ✔ Contents of a typed module


view this post on Zulip James Wood (Aug 10 2022 at 09:49):

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.

view this post on Zulip Li-yao (Aug 10 2022 at 09:50):

The type annotation indeed seals the module. If you just want to check the type without sealing you can do <: foo.

view this post on Zulip James Wood (Aug 10 2022 at 09:56):

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?

view this post on Zulip Li-yao (Aug 10 2022 at 09:59):

Yeah that sounds right.

view this post on Zulip James Wood (Aug 10 2022 at 09:59):

Thanks :smiley:

view this post on Zulip Notification Bot (Aug 10 2022 at 09:59):

James Wood has marked this topic as resolved.

view this post on Zulip James Wood (Aug 10 2022 at 10:04):

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: Jan 29 2023 at 01:02 UTC