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

[Alizter]

Don't we have private inductive types in coq?

[ppedrot]

Yes, but it does not mean the same and it's not a kernel feature (read: it's a broken hack).

[SkySkimmer]

ocaml private is used to enforce guarantees about the values in the type.
In Coq this is can done by explicitly manipulating proofs about the values in the type, so there seems to be no need to for ocaml-style private.
Also I'm not sure how it would work, consider

Module Import SortedList.

Private(ocaml) Inductive t := Nil | Cons : nat -> t -> t.

Definition nil := Nil.
Definition cons x l := (* add x to l keeping it sorted *).
End SortedList.
Compute nil. (* Nil : t ??? *)

[silene]

I suppose opaque types would have abstract values, as in OCaml: <abstract> : t.

[Alizter]

Have you got any more combinators in mind?

[herbelin]

Not really. I was mostly thinking at the oppportunity to integrate Include and the quite powerful <+ in the kernel.

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

[SkySkimmer]

Can this lead to a type-in-type inconsistency?

[Blaisorblade]

Could this proposal be clarified? Is this Declare Module Type Foo. where Foo is then an abstract signature?

[Blaisorblade]

@herbelin Are you proposing mixin modules, a bit like in Scala or MixML? I’ve often wanted them, and I’ve actually spent a couple of years studying the Scala case.

Here’s a small example:

Module Type Base.
  Axiom a : nat.
  Definition b := 1 + a.
End Base.

Module Derived1 <: Base.
  Definition a : nat := 0.
  Include Base.
  (* Include should _merge_ the axiom `a` with the `Definition `` as long as the definition is a subtype of the interface — if Coq satisfies the usual metatheory of subtyping, definitions using `a` should still typecheck and need not be rechecked, except for universe constraints since those are not modular. *)
End Derived1.

Module Derived2 <: Base.
  Include Base.
  Fail Definition a : nat := b. (* This creates a new kind of infinite loop, which must be forbidden. *)
  Definition a : nat := 0.
  (* Such things work in Scala but is harder, since we have to _replace_ a definition; rejecting this might be fine here, but not so well with FancyBase below. To make this work, we could replace [Include] by some other “inheritance” mechanism. *)
End Derived2.

Module FancyBase.
  Include Base.
  Axiom c : Fin b.
  Definition d := (c, c).
End FancyBase.

Module FancyDerived1 <: FancyBase.
  Definition a : nat := 0.
  Definition c : Fin 1 := Fin.FZ. (* We cannot write [Fin b], and we might be unable to write this definition at all. *)
  Include FancyBase.
End FancyDerived1.

Module FancyDerived2 <: Base.
  Include FancyBase.
  (* Now we can fill in the axioms *)
  Definition a : nat := 0.
  Definition c : Fin b := Fin.FZ.
End FancyDerived2. (* *)

This code can be translated to avoid mixing modules — Coq’s numerical hierarchy shows how. But the encoding is pretty annoying, since you can never mix axioms and definitions if the axioms are to be later instantiated.

I also realize that working out the details is not trivial; but I am not sure what you get if you stop short of mixin modules.