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 :)
hmm, the infamous self-cast
I think it fails on the third line because the cast from module to type doesn't work for <+
did I get it right?
So you say the second line works but the third fails?
(I just checked and I am surprised.)
I'm afraid both answers are wrong :)
maybe I shouldn't reveal the behaviour here if others want to play
(I would have got it wrong too, of course, that's why I post)
it does the exact inverse of what I'd have expected
who on earth wrote that code?
(but that's a nice design pattern to remember)
I mean, as a hackish workaround
It's funny to see core developers like us being surprised by three lines of vernac
this is not any vernac, this is modules (Boooh! spooky)
nobody has the least idea of the semantics of that stuff
I thought this one recetly was quite suprising
Comments apparently whatever you like here.
It can be hacked to give backwards compatible vernac >:)
Oh, you didn't know Comments
?
We rediscovered it a few years ago when looking at the list of vernac commands from the grammar :)
is the result different for nonempty M?
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
:)
Gaëtan Gilbert said:
also
Ah! At least I know the answer to this last one.
Nice example, @Gaëtan Gilbert
Oh no!!!
I understand why it does what it does, I think
Looks like horror movies
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.
that's the with definition stuff
yes
it would be "interesting" to combine it with your example
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?
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?
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