Functors & Opaqueness

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3342
From: @gmalecha
Reported version: unspecified
CC: @silene, @herbelin, @mikeshulman

See also: BZ#3746
See also: BZ#4003

[coqbot]

Comment author: @gmalecha

This is in relation to an old issue raised on the Coq mailing list.

Functors applied within functors can not be transparent. For example, if I want to parameterize over a functor to construct finite maps in an implementation of multimaps (perhaps because i will construct a local type to use as the key) the definitions will never compute.

A simple example that I came up with:

Module Type Foo.
  Parameter n : nat.
End Foo.

Module Type BarF (F : Foo).
  Parameter n : nat.
End BarF.

Module Z (F : BarF).
  Module Arg.
    Definition n := 0.
  End Arg.

  Module B <: Foo := F Arg.
End Z.

Module Bar (F : Foo).
  Definition n := F.n.
End Bar.

Module Z' := Z Bar.

Goal Z'.B.n = 0.
  compute.
Abort. (** Does not work. **)

Print Z'.B.
(** Module Z'.B : Sig Parameter n : nat. End := (Bar Z'.Arg)
 **)
Print Z.
(** Module Z
 ** : Funsig (F:BarF) Sig Module Arg Module B End
 ** := Functor (F:BarF) Struct Module Arg Module B End
 **)

Module Z'' := Bar Z'.Arg.

Goal Z''.n = 0.
  compute. reflexivity.
Qed. (** Works **)

Cedric's response on the Coq mailing list.

Maybe the syntax should be extended for module bindings as:

module_binding ::= ( [Import|Export] ident … ident : module_type )
                 | ( [Import|Export] ident … ident <: module_type )

I let you see if this should be added as a feature request to bugzilla.

What follows is just a simple set of tests which are simple enough to
perform quickly various tests. It is more convenient for me than trying
with "real" examples, such as FMapInterface and so on.

Module Type Mod.
  Parameter T : Type.
  Parameter t : T.
End Mod.

Module Test1 : Mod.
  Definition T := bool.
  Definition t := true.
End Test1.

Module Test2 <: Mod.
  Definition T := bool.
  Definition t := true.
End Test2.

Compute Test1.t.
Compute Test2.t.

Module Type Functor (X : Mod).
  Parameter U : Type.
  Parameter u : X.T -> U.
End Functor.

Module Test3 (X : Mod) : Functor X.
  Definition U := option X.T.
  Definition u := fun (x : X.T) => Some x.
End Test3.

Module Test4 (X : Mod) <: Functor X.
  Definition U := option X.T.
  Definition u := fun (x : X.T) => Some x.
End Test4.

[coqbot]

Comment author: @mikeshulman

I just ran into this too. Any chance of it being fixed?

I also don't understand why one would want a different syntax. Ordinary modules passed as arguments to functors are already transparent, so why would you expect functors passed as arguments to be opaque?

[coqbot]

Comment author: @herbelin

This issue was mentioned again on Gitter yesterday. Indeed, ordinary modules passed as arguments to functors are already transparent, this is obtained by a so-called strengthening rule, which is an eta-expansion of module:

Module Type Foo.
Parameter n : nat.
End Foo.

Module Type BarF (F:Foo).
Parameter n : nat.
End BarF.

Module Arg.
Definition n := 0.
End Arg.

Module Z (E : Foo) (F : BarF).
Module G := E.
Module H := F Arg.
Print Module G.
(* One sees that G.n is defined, actually bound to E.n )
Print Module H.
( One sees that H.n is abstract: no strengthening done on H *).
End Z.

One naive way to implement this would need to have names which include algebraic expressions of modules in their qualification, so as to be able to internally define Z as if defined like this:

Module Z (E : Foo) (F : BarF).
Module G. Definition n := E.n : nat. End G.
Module H. Definition n := (F Arg).n : nat. End H.
End Z.

In the absence of the availability of such a syntax, one may consider, maybe, adding a reference to itself in the definition of the module, in the style of the following pseudo-code:

Module Z (E : Foo) (F : BarF).
Module Type GT. Definition n := E.n : nat. End GT.
Module G : GT := E.
Module Type HT. Definition n := H.n : nat. End HT.
Module H : HT := F Arg.
End Z.

More technical developer note: I'm not an expert at all, but maybe moving strengthen_and_subst_mb outside of Mod_typing.translate_mse, allowing a circularity on mpo, and of course taking care of avoiding possible name captures, could maybe eventually do the job.

[coqbot]

Comment author: @silene

Given the amount of research papers on generative vs applicative functors and since it is still an active topic (e.g. it is only since 4.02 that OCaml supports both kinds of functors), I don't think a bug report is the proper place to discuss such a change. Sure, its consequences are a lot less critical than in side-effect languages, but it is still a change of paradigm.

[coqbot]

Comment author: @herbelin

Hi Guillaume,

I don't think a bug report is the proper place to discuss such a change.

Well, I just started a discussion on Cocorico (https://coq.inria.fr/cocorico/OpenIssuesWithModules). Please contribute.

I actually seized this opportunity to also address other related questions about modules, namely:

1. Do modules need to be type-checked in the kernel?
2. Module and functor transparency
3. Applicative vs generative functors
4. Subtyping inductive types as definitions
5. How far can modules and module types be identified?
6. Towards a richer algebraic language of module constructions

By the way, I'm unsure to understand in which sense you see a relation between generativity of functors and higher-order transparency.

[coqbot]

Comment author: @silene

By the way, I'm unsure to understand in which sense you see a relation between generativity of functors and higher-order transparency.

As soon as "Definition n := (F Arg).n" becomes meaningful (whatever the actual syntax), then F can no longer be a generative functor. The simple fact that the term "(F Arg).n" exists means that F is applicative (by definition). This seems a bit too obvious to me, so maybe I am misunderstanding your remark.

[coqbot]

Comment author: @herbelin

(In reply to Guillaume Melquiond from comment BZ#5)

By the way, I'm unsure to understand in which sense you see a relation between generativity of functors and higher-order transparency.

As soon as "Definition n := (F Arg).n" becomes meaningful (whatever the
actual syntax), then F can no longer be a generative functor. The simple
fact that the term "(F Arg).n" exists means that F is applicative (by
definition). This seems a bit too obvious to me, so maybe I am
misunderstanding your remark.

Yes, you're right, there is indeed a relation between transparency and generativity.

However, allowing (F Arg) in paths is one way to get transparency of signatures of applied module. I'm unsure that this is the only way (see what I wrote on Cocorico).

Now, it is also a question about how we define generativity. If I extend and modify the example of Gregory as follows:

Module Type Foo. Parameter n : nat. End Foo.
Module Type BarF (F : Foo). Parameter n : nat. End BarF.
Module Arg. Definition n := 0. End Arg.
Module Z (F : BarF).
Module B <: Foo := F Arg.
Parameter t : Type.
End Z.
Module Bar (F : Foo). Definition n := F.n. End Bar.
Module Z' := Z Bar.
Module Z'' := Z Bar.

then, the generativity principle says that we should consider Z'.t to be different from Z''.t, but, should we consider the generativity principle to imply Z'.B.n <> Z.B.n or not, knowing that n is not "explicitly generated" by Z but transferred from Arg.

Told otherwise, the absence of higher-order transparency forces this second kind of generativity but is this really the generativity that we want in practice?

Second, even if having applied functors in paths implies generativity of the first form and applied functors in paths is one way to get higher-order transparency, I see no reason why the first form of generativity would be implied by higher-order transparency which I suspect can be implemented without needing applied functors in paths.

[coqbot]

Comment author: @herbelin

One more remark: couldn't generativity be reduced to passing an implicit timestamp argument to any functor application? So, even in a model where (F Arg) can be a component of a path, its generative variant would be (F Arg t_i) with t_i the current time at the time of application. We would then still get transparency because transparency is obtained by applying module projection (the "beta-rule" for module), but we would not get non-generativity because two distinct occurrences of (F Arg) would have different timestamp.