Stream: Coq devs & plugin devs

Topic: Quizz on modules


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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 11 2022 at 14:35):

I can't even parse it, quizz failed :)

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 14:44):

hmm, the infamous self-cast

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

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 14:45):

did I get it right?

view this post on Zulip Maxime Dénès (Mar 11 2022 at 14:46):

So you say the second line works but the third fails?

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 14:46):

(I just checked and I am surprised.)

view this post on Zulip Maxime Dénès (Mar 11 2022 at 14:46):

I'm afraid both answers are wrong :)

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 14:46):

maybe I shouldn't reveal the behaviour here if others want to play

view this post on Zulip Maxime Dénès (Mar 11 2022 at 14:47):

(I would have got it wrong too, of course, that's why I post)

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 14:47):

it does the exact inverse of what I'd have expected

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 14:48):

who on earth wrote that code?

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 14:48):

(but that's a nice design pattern to remember)

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 14:48):

I mean, as a hackish workaround

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

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 14:49):

this is not any vernac, this is modules (Boooh! spooky)

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 14:49):

nobody has the least idea of the semantics of that stuff

view this post on Zulip Ali Caglayan (Mar 11 2022 at 14:49):

I thought this one recetly was quite suprising

Comments apparently whatever you like here.

view this post on Zulip Ali Caglayan (Mar 11 2022 at 14:50):

It can be hacked to give backwards compatible vernac >:)

view this post on Zulip Maxime Dénès (Mar 11 2022 at 14:51):

Oh, you didn't know Comments ?

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

view this post on Zulip Gaëtan Gilbert (Mar 11 2022 at 15:03):

is the result different for nonempty M?

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

view this post on Zulip Maxime Dénès (Mar 11 2022 at 15:07):

Gaëtan Gilbert said:

is the result different for nonempty M?

It depends what you put in M :)

view this post on Zulip Guillaume Melquiond (Mar 11 2022 at 15:08):

Gaëtan Gilbert said:

also

Ah! At least I know the answer to this last one.

view this post on Zulip Maxime Dénès (Mar 11 2022 at 15:08):

Nice example, @Gaëtan Gilbert

view this post on Zulip Maxime Dénès (Mar 11 2022 at 15:09):

Oh no!!!

view this post on Zulip Maxime Dénès (Mar 11 2022 at 15:09):

I understand why it does what it does, I think

view this post on Zulip Maxime Dénès (Mar 11 2022 at 15:09):

Looks like horror movies

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

view this post on Zulip Gaëtan Gilbert (Mar 11 2022 at 15:12):

that's the with definition stuff

view this post on Zulip Maxime Dénès (Mar 11 2022 at 15:13):

yes

view this post on Zulip Maxime Dénès (Mar 11 2022 at 15:13):

it would be "interesting" to combine it with your example

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

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

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?

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