Emilio Jesús Gallego Arias (Apr 04 2022 at 16:01): Emilio Jesús Gallego Arias (Apr 04 2022 at 16:01):Hi folks, in the meeting we had last week about Coq-DB some discussion about libobject happened. I made the following claim:
libobjectseems to fullfill two roles: generic object storage, and a key part of the implemenation of the module systemHowever, I don't know enought about the module system as to be sure of that. WDYT?
[by the way the meeting was recorded so you can replay in Youtube once I get to upload it]
cc: @Maxime Dénès @Pierre-Marie Pédrot @Gaëtan Gilbert maybe @Guillaume Melquiond ?
Pierre-Marie Pédrot (Apr 04 2022 at 16:30):why would they be unrelated? functor instantiation is precisely about storage
Emilio Jesús Gallego Arias (Apr 04 2022 at 18:02):@Pierre-Marie Pédrot in my view persistent objects and modules seen a bit of separate concerns, for example, first-class modules don't require any storage system
Emilio Jesús Gallego Arias (Apr 04 2022 at 18:02):tho it is likely I just don't understand Coq's module system
Paolo Giarrusso (Apr 04 2022 at 19:13):I think the 2003-2004 papers on Coq modules explain how functors interact with non-logical state, and they seem surprisingly current, down to same of the bugs they describe
Paolo Giarrusso (Apr 04 2022 at 19:14):At a high level, functor instantiation and Include both operate on <all objects stored inside the module/module type/functor>, after any necessary functor substitution
Paolo Giarrusso (Apr 04 2022 at 19:17):see https://link.springer.com/chapter/10.1007/10930755_18, especially section 5.
Paolo Giarrusso (Apr 04 2022 at 19:18):(of course, I couldn’t tell what’s outdated, but you can, and this paper has more time than PMP)
Last updated: Dec 05 2023 at 05:01 UTC