Stream: Coq users

Topic: Yet another module question


view this post on Zulip Pierre Rousselin (Mar 04 2024 at 13:54):

I am facing a very frustrating issue with modules. This basically gets down to this:

Module Type HasFoo.
  Parameter foo : nat.
End HasFoo.

Module HasFooHasBar (Import M : HasFoo).
  Definition bar := foo.
End HasFooHasBar.

Module Type HasFooAndBar.
  Parameter foo : nat.
  Parameter bar : nat.
End HasFooAndBar.

Module BazFromFooBar (Import M : HasFooAndBar).
  Definition baz := foo + bar.
End BazFromFooBar.

Module Type Baz (Import F : HasFoo).
  Include HasFooHasBar F.
  Fail Include BazFromFooBar F.
  (* The field bar is missing in modules.F. *)
  Fail Include BazFromFooBar.
  (* The field foo is missing in modules.Baz. *)
End Baz.

So, in the end I would like to say something like "take foo from the parameter F and use the current functor to obtain bar", but so far my attempts have failed (I guess there is an "all or nothing" policy here).

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 14:03):

Maybe you mean:

Module Type HasFoo.
  Parameter foo : nat.
End HasFoo.

Module HasFooHasBar (Import M : HasFoo).
  Include M.
  Definition bar := foo.
End HasFooHasBar.

Module Type HasFooAndBar.
  Parameter foo : nat.
  Parameter bar : nat.
End HasFooAndBar.

Module BazFromFooBar (Import M : HasFooAndBar).
  Definition baz := foo + bar.
End BazFromFooBar.

Module Type Baz (Import F : HasFoo).
  Module MyHasFooHasBar := HasFooHasBar F.
  Include MyHasFooHasBar.
  Module MyBazFromFooBar := BazFromFooBar MyHasFooHasBar.
  Include MyBazFromFooBar.
End Baz.

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 14:06):

A few notes:

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:20):

Michael Soegtrop said:

A few notes:

Are you sure? These at least display different module types.

Module Type HasFoo.
  Parameter foo : nat.
End HasFoo.

Module HasFooHasBar (Import M : HasFoo).
  Definition bar := foo.
End HasFooHasBar.

Module Type Baz0 (Import F : HasFoo).
  Include F.
  Include HasFooHasBar.
End Baz0.

Print Module Type Baz0.
(*
Module Type
 Baz0 =
 Funsig (F:HasFoo) Sig Definition foo : nat. Definition bar : nat. End
*)

Module Type Baz1 (Import F : HasFoo).
  Include HasFooHasBar F.
End Baz1.

Print Module Type Baz1.
(* Module Type Baz1 = Funsig (F:HasFoo) Sig Definition bar : nat. End *)

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 14:25):

Are you sure? These at least display different module types.

Sorry, I indeed had wrong notes about this - you are right that Include F M. means Include (F M).

I just rarely do an Include (F M) because I usually need this module then as argument to something else, and then I have to do Module FM:=F M. Include FM anyway.

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:29):

Doesn't it add more constants in the module though? I'm trying to add some lemmas with the least amount of extra noise for the user (that's why I used a parameter and not an inclusion).

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 14:31):

Thinking / reviewing what I did in the past ...

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:31):

Thanks a lot.

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 14:36):

@Pierre Rousselin : do you indeed want Module Type Baz or do you want Module Baz?

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:39):

My real case is extension of NSub.v
so it is a module type. But I guess there are not much differences now between module and module types?

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 14:39):

Maybe it is this what you want to express:

Module Type HasFoo.
  Parameter foo : nat.
End HasFoo.

Module Type HasFooAndBar (M : HasFoo).
  Definition bar := M.foo.
End HasFooAndBar.

Module Type BazFromFooBar (F : HasFoo) (M : HasFooAndBar F).
  Definition baz := F.foo + M.bar.
End BazFromFooBar.

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 14:40):

Or the same with BazFromFooBar a module instead of a module type.

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:40):

Is there really a difference? Isn't it just a convenience to Import the parameter?

view this post on Zulip Gaëtan Gilbert (Mar 04 2024 at 14:41):

the difference is the lack of Include

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 14:41):

The difference is that HasFooAndBar is now a module type functor, so that I use this module type functor to specify module M such that it has a bar, and that at the same time this bar is derived from foo.

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 14:42):

One main problem in your first example is that in Include BazFromFooBar F the module F is (by its module type) specified to have only a foo but not a bar.

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:43):

Hmm.. the problem is that the writer of BazFromFooBar wants her functor to work in any HasFooBar case, not just when they are equal.

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:45):

but then, morally, if one has the very specific HasFooAndBar + a module of type HasFoo, one should be able to use all the goodies in BazFromFooBar, no?

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:46):

(there actually is a real case, I'm not just doing this for fun, it is though)

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 14:48):

Well you can't use nothing which is not in the module type. You can write:

Module Type HasFoo.
  Parameter foo : nat.
End HasFoo.

Module Type HasFooAndBar.
  Parameter foo : nat.
  Parameter bar : nat.
End HasFooAndBar.

Module HasFooHasBar (Import M : HasFoo).
  Definition bar := foo.
End HasFooHasBar.

Module BazFromFooBar (Import M : HasFooAndBar).
  Definition baz := foo + bar.
End BazFromFooBar.

Module Type Baz (Import FB : HasFooAndBar).
  Include HasFooHasBar FB.
  Include BazFromFooBar FB.
End Baz.

view this post on Zulip Gaëtan Gilbert (Mar 04 2024 at 14:51):

the functor argument has to be exactly 1 module, either the current one (implicitly) or some named one
so you have to do any module mixing separately
(Include a + b + F or whatever the real syntax is just means a series o includes Include a. Include b. Include F)

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:53):

@Michael Soegtrop I see... maybe I can write it that way. Thank you!
@Gaëtan Gilbert thank you, it's also clearer this way, is there any real reason behind this?

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 14:54):

is there any real reason behind this?

As I said: the reason is that modules define names, and the names need to be proper names of the form "A.B.C". If one would allow unnamed module functor applications, what should the global name of the definition be?

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:55):

Since they are included, they get the names from the modules they are included in.

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:56):

Module Type HasFoo.
  Parameter foo : nat.
End HasFoo.

Module HasFooHasBar (Import M : HasFoo).
  Definition bar := foo.
End HasFooHasBar.

Module IsFoo <: HasFoo.
  Definition foo := 42.
End IsFoo.

Module IsFooIsBar.
  Include HasFooHasBar IsFoo.
End IsFooIsBar.

Compute IsFooIsBar.bar. (* 42 *)

view this post on Zulip Gaëtan Gilbert (Mar 04 2024 at 14:56):

IDK if there's a reason beyond it would make the implementation more complicated (and the modules implementation is already plenty complicated)

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 14:59):

That's certainly a reasonable answer. From the user's perspective it's weird to have such a huge change between 1 parameter and more, though. But then I guess no one wants to mess with modules at this point. So, fair enough.

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 15:02):

Well, this works with your original definitions:

Module Type Baz (Import F : HasFoo).
  Include F.
  Include HasFooHasBar.
  Include BazFromFooBar.
End Baz.

The question is what name foo should have, if you do not include F, either in Baz or in HasFooHasBar.

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 15:06):

The second include is identical to Include HasFooHasBar F, but there is nothing you could write as argument for the third include - only the implicit current module works.

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 15:12):

I think foo could (in theory) not appear in this functor type, it's given by the parameter F. Later, when it is instantiated, it can have a name.
The problem with this approach, if I'm not mistaken can happen when one puts everything together with something like :

Module A.
Definition foo := 42.
Include Baz. (* error: foo is already defined *)
End A.

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 15:13):

Maybe I should write an issue, as a reminder?

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 15:16):

IMHO the module system is fine as it is. I don't think there are restrictions beyond the one that resulting definitions must have proper names and module functors must be checkable against the declared module types at the time they are defined. We don't want to have a mess as with C++ templates, where things are only checked when things are eventually put together. I remember a case where MSVC crashed on a (rather simple) template error, because the error message would overflow memory.

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 15:17):

I guess we should discuss it on the concrete case - it is hard to judge the pros and cons of the various ways of doing it on abstract cases.

view this post on Zulip Pierre Rousselin (Mar 04 2024 at 15:19):

Let me just try things in the direction you mentioned (with the bigger specification as a parameter). If I'm stuck I'll get back to this conversation. And, thanks again!


Last updated: Jun 22 2024 at 16:02 UTC