Hi folks, in the meeting we had last week about Coq-DB some discussion about libobject happened. I made the following claim:
libobject
seems 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 ?
why would they be unrelated? functor instantiation is precisely about storage
@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
tho it is likely I just don't understand Coq's module system
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
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
see https://link.springer.com/chapter/10.1007/10930755_18, especially section 5.
(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