Maxime Dénès (Mar 11 2022 at 14:34): Maxime Dénès (Mar 11 2022 at 14:34):It's been a long time since the last quizz :) The challenge is to write down what Coq says on the following input (without running Coq, of course) :
Module M. End M.
Module Type S := M.
Module Type P := M <+ M.
I can't even parse it, quizz failed :)
Pierre-Marie Pédrot (Mar 11 2022 at 14:44):hmm, the infamous self-cast
Pierre-Marie Pédrot (Mar 11 2022 at 14:45):I think it fails on the third line because the cast from module to type doesn't work for <+
Pierre-Marie Pédrot (Mar 11 2022 at 14:45):did I get it right?
Maxime Dénès (Mar 11 2022 at 14:46):So you say the second line works but the third fails?
Pierre-Marie Pédrot (Mar 11 2022 at 14:46):(I just checked and I am surprised.)
Maxime Dénès (Mar 11 2022 at 14:46):I'm afraid both answers are wrong :)
Pierre-Marie Pédrot (Mar 11 2022 at 14:46):maybe I shouldn't reveal the behaviour here if others want to play
Maxime Dénès (Mar 11 2022 at 14:47):(I would have got it wrong too, of course, that's why I post)
Pierre-Marie Pédrot (Mar 11 2022 at 14:47):it does the exact inverse of what I'd have expected
Pierre-Marie Pédrot (Mar 11 2022 at 14:48):who on earth wrote that code?
Pierre-Marie Pédrot (Mar 11 2022 at 14:48):(but that's a nice design pattern to remember)
Pierre-Marie Pédrot (Mar 11 2022 at 14:48):I mean, as a hackish workaround
Maxime Dénès (Mar 11 2022 at 14:48):It's funny to see core developers like us being surprised by three lines of vernac
Pierre-Marie Pédrot (Mar 11 2022 at 14:49):this is not any vernac, this is modules (Boooh! spooky)
Pierre-Marie Pédrot (Mar 11 2022 at 14:49):nobody has the least idea of the semantics of that stuff
Ali Caglayan (Mar 11 2022 at 14:49):I thought this one recetly was quite suprising
Comments apparently whatever you like here.
It can be hacked to give backwards compatible vernac >:)
Maxime Dénès (Mar 11 2022 at 14:51):Oh, you didn't know Comments ?
Maxime Dénès (Mar 11 2022 at 14:52):We rediscovered it a few years ago when looking at the list of vernac commands from the grammar :)
Gaëtan Gilbert (Mar 11 2022 at 15:03):is the result different for nonempty M?
Gaëtan Gilbert (Mar 11 2022 at 15:06):also
Module M1.
Module M. End M.
End M1.
Module M. Axiom a : nat. End M.
Module X := M1 <+ M.
Check X.a.
Gaëtan Gilbert said:
is the result different for nonempty M?
It depends what you put in M :)
Guillaume Melquiond (Mar 11 2022 at 15:08):Gaëtan Gilbert said:
also
Ah! At least I know the answer to this last one.
Maxime Dénès (Mar 11 2022 at 15:08):Nice example, @Gaëtan Gilbert
Maxime Dénès (Mar 11 2022 at 15:09):Oh no!!!
Maxime Dénès (Mar 11 2022 at 15:09):I understand why it does what it does, I think
Maxime Dénès (Mar 11 2022 at 15:09):Looks like horror movies
Maxime Dénès (Mar 11 2022 at 15:11):Btw, if you look deep into the code, we seem to be trying to look for universe polymorphism based on names (M in M1 <+ M, in Gaetan's example). So I wouldn't be surprised if we can derive an even mode "interesting" example.
Gaëtan Gilbert (Mar 11 2022 at 15:12):that's the with definition stuff
Maxime Dénès (Mar 11 2022 at 15:13):yes
Maxime Dénès (Mar 11 2022 at 15:13):it would be "interesting" to combine it with your example
Hugo Herbelin (Mar 11 2022 at 19:06):If I may add my grain of salt... We have to be consistent about when a module can be seen as a module type and Maxime's quizz shows such an inconsistency. We have to be careful about the scoping of names when doing M1 <+ .... Gaëtan's quizz tends to say that the current scoping is not the most intuitive one. So maybe can we change it.
Btw, is it confirmed that universes and inclusion might not follow the same scoping rules?
Hugo Herbelin (Mar 12 2022 at 07:49):Another example:
Module Type T. End T.
Module F (X:T). End F.
Module M := F.
Module N := F <+ F.
Module Type U := F.
Module Type V := F <+ F.
as well as:
Module Type T. Axiom a:nat. End T.
Module F (X:T). Axiom a:nat. End F.
Module M := F.
Module N := F <+ F.
Module Type U := F.
Module Type V := F <+ F.
My suggestion for more uniformity would be:
In M1 <+ ... <+ Mn, if M1 is a functor, consider the whole result as dependent on the parameters than M1, that is interpret (Fun binders1 Body1) <+ (Fun binders2 Body2) as Fun binders1 (Body1 ++ Body2[binders2:=Body1]) (or, equivalently as Fun binders1 (Body1 ++ Include (Fun binders2 Body2))), instead of the current interpretation as Include (Fun binders1 Body1) ++ Include (Fun binders2 Body2) which has no alternative than failing for non empty binders1.
By doing so, Module M := F would typically be the same as Module M := F <+ EmptyModule.
In Module Type M := N or Module Type G := F, do the same as in Module Type M := N <+ EmptyModule or Module Type G := F <+ EmptyModule. I believe this is in Declaremods.declare_modtype where it should be investigated how to replace the call to translate_mse with a call translate_mse_include in the case when the rhs is a module.
With these two changes, it seems that Maxime's code would behave consistently and so, even whenM is a functor. It would also go in the direction of treating uniformly <+ as an operator rather than an ad hoc notation, allowing the factorization mentioned in "Help with module code refactoring". (Being an operator, one would be able to do e.g. F (X : T <+ U) := ....)
Wrt Gaëtan's example, I guess it is a question of doing the Modintern.intern_module_ast of M and N in Declareops.declare_one_include all in advance for M <+ N, versus interleaving them with the effective inclusion of M and N, right?
Hugo Herbelin (Mar 12 2022 at 07:50):For clarity, maybe the implicit coercion from modules to module types should be explicit. Iiuc, it requires an explicit module type of in OCaml??
Last updated: May 28 2023 at 13:30 UTC