Stream: Coq users

Topic: ✔ Yet another module question


view this post on Zulip Pierre Rousselin (Mar 05 2024 at 09:30):

I have solved my problem. The key is to separate requirement HasFooAndBar into two module types HasFoo and HasBar. This way, Coq merrily accepts to fulfil one requirement with the argument of the functor and the other with the current functor.

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

Module Type HasBar.
  Parameter bar : nat.
End HasBar.

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

Module BazFromFooBar (Import M : HasFoo) (Import M' : HasBar).
  Definition baz := foo + bar.
End BazFromFooBar.

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

view this post on Zulip Pierre Rousselin (Mar 05 2024 at 09:32):

So I guess the morality is that when one extends a specification, it's easier to give the extension as a separate constraint.

view this post on Zulip Notification Bot (Mar 05 2024 at 09:43):

Pierre Rousselin has marked this topic as resolved.

view this post on Zulip Michael Soegtrop (Mar 05 2024 at 09:54):

Pierre Rousselin said:

So I guess the morality is that when one extends a specification, it's easier to give the extension as a separate constraint.

This indeed seems to be common practice, e.g. looking at the module (type) structure of orders in the standard library. It is also common practice to define various combined module types. If this is a good idea or not is hard to say. The module type structures of orders in the standard library got rather complicated and hard to see through cause of this. I would say it does make sense to have a few commonly used combinations, but IMHO it doesn't hurt to keep some things separate.


Last updated: Jun 13 2024 at 19:02 UTC