A few propositions about the module system

[herbelin]

This CEP discusses a few limitations of the module system and give propositions to address them.

Rendered here

[silene]

In Why3, we do not distinguish between module implementations and module interfaces. For instance, your following example works fine once translated to WhyML:

Module M. Axiom a:nat. End M.
Module N := M with Definition a:=0.

module M
  constant a : int
end

module N
  constant a : int = 0
  clone M with constant a
end

The system works rather well, including private types and extraction. So, perhaps, some ideas could be reused for Coq. That said, Why3 has a much simpler type system, so hard to tell how bad it would behave if Coq's conversion was thrown into the mix.

Some details are given in this paper: https://hal.inria.fr/hal-02696246

[herbelin]

The simplicity of the module system of Why3 is appealing (and somehow "to the point"). If I understand correctly, it can emulate higher-order functors, <: and even : with some discipline (e.g. to extract M:T I guess you have to explicitly tell that you want to extract M coupled with T since there is no such primitive concept of module sealed behind an interface). It has no Module Type but one can use clone to treat a module as a module type (i.e. so that it is generative). Is that a correct understanding? (As a side note, the frame type theory of X. Montillet, A. Mahboubi and C. Cohen has similar ideas.)

[herbelin]

By the way, shouldn't your example (morally) use Why3's use rather than clone so that (if there were some) the inductive declarations in M are aliased in N, as it would be in Coq.

[silene]

Is that a correct understanding?

Yes.

As for M:T, this is getting added to Why3 and will presumably be part of the next release. The meaning is intermediate between : and <: in Coq, that is, M is sealed when doing proofs (only its interface T is available), but its implementation is actually available for interpretation and extraction. I am not sure whether this would translate well to Coq, since types and proofs are plain values there.

shouldn't your example (morally) use Why3's use rather than clone

No. As in Coq and OCaml, Why3's modules act both for namespacing and as a higher-order type system. Directive use is for the former, while clone is for the latter. You would only use use for a fully concrete module implementation (or one with abstract symbols that are not meant to be instantiated, e.g., int.Int or real.Real), so kind of like Require in Coq.

But you are right that it causes an issue if you want inductive types to be shared (since module cloning is generative). In that case, you would use the same trick as in Coq (which makes it just as tedious):

module K
  type foo = Foo
end

module M
  use export K
  constant a : int
end

Now, any clone of M will contain a symbol foo that is synonymous with K.foo (and same for Foo).