Stream: Coq devs & plugin devs

Topic: Libobject roles


view this post on Zulip 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:

However, 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 ?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2022 at 16:30):

why would they be unrelated? functor instantiation is precisely about storage

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2022 at 18:02):

tho it is likely I just don't understand Coq's module system

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Apr 04 2022 at 19:17):

see https://link.springer.com/chapter/10.1007/10930755_18, especially section 5.

view this post on Zulip 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: Feb 01 2023 at 16:03 UTC