Stream: Coq users

Topic: Yet another module question

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).

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.

Michael Soegtrop (Mar 04 2024 at 14:06):

A few notes:

• Include HasFooHasBar F. is the same as Include HasFooHasBar. Include F.- not Include (HasFooHasBar F).
• one cannot directly include applied functors, because the resulting definitions wouldn't have a proper fully qualified name. There must be a simple symbolic name for each module. You can't have a qualified name like A.F B.C.
• Import just makes the name available without qualification in a module, but does not include it in a module.

Pierre Rousselin (Mar 04 2024 at 14:20):

Michael Soegtrop said:

A few notes:

• Include HasFooHasBar F. is the same as Include HasFooHasBar. Include F.- not Include (HasFooHasBar F).

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 *)

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.

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).

Michael Soegtrop (Mar 04 2024 at 14:31):

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

Pierre Rousselin (Mar 04 2024 at 14:31):

Thanks a lot.

Michael Soegtrop (Mar 04 2024 at 14:36):

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

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?

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.

Michael Soegtrop (Mar 04 2024 at 14:40):

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

Pierre Rousselin (Mar 04 2024 at 14:40):

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

Gaëtan Gilbert (Mar 04 2024 at 14:41):

the difference is the lack of Include

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.

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.

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.

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?

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)

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.

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)

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?

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?

Pierre Rousselin (Mar 04 2024 at 14:55):

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

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 *)

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)

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.

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.

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.

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.

Pierre Rousselin (Mar 04 2024 at 15:13):

Maybe I should write an issue, as a reminder?

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.

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.

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: Oct 13 2024 at 01:02 UTC