Stream: Coq users

Topic: Return a module from a function?


view this post on Zulip Audrey Seo (Jul 07 2023 at 01:26):

Can you return a module from a function? I would like to construct modules that may differ in one or more fields. Functors only take modules, and I don't want to construct a whole module to modify one field of the module that the functor is returning. I can provide an example if more explanation is needed.

view this post on Zulip Paolo Giarrusso (Jul 07 2023 at 02:25):

no, Coq functions can't manipulate modules, but they can return the same info through records

view this post on Zulip Paolo Giarrusso (Jul 07 2023 at 02:28):

but you _can_ combine modules with their arguments:

Module Type Intf. Axiom x : nat. End Intf.
Module Type abstraction (I : Intf). (* Use [i.x] *) End abstraction.
Module Type IntfAbstr := Intf <+ abstraction.
Module user <: IntfAbstr.
  Definition x := 0.
  Include abstraction.
End user. (* this is both [abstraction]'s argument and [abstraction] itself. *)

view this post on Zulip Paolo Giarrusso (Jul 07 2023 at 02:29):

such uses appear in the stdlib's number library

view this post on Zulip Paolo Giarrusso (Jul 07 2023 at 02:31):

but to be clear, your annoyance is justified: modules _are_ often annoying like that, IME even for ML module experts. It's not an accident most projects prefer first-class records.


Last updated: Jun 23 2024 at 05:02 UTC