Applying Functors multiple times · Coq users

I have a module type A and a functor F that takes a module of type A. F defines an inductive type I, If I have MA a module of type A and I do

Module M1 := (F MA).
Module M2 := (F MA).
Goal M1.I = M2.I.
  reflexivity.

Then the reflexivity fails which suggest that those two types are different. My problem is that I have two files B.v and C.v that both depend on F MA, so both files begin with Module M := F MA. Import M. Then I have D.v that uses both B.v and C.v but cannot make them interoperate because they are based on seemingly different instance of I. Is there a way around this?

Module Type A.
End A.

Module F (MA : A).
  Inductive I :=.
End F.

Module MA.
End MA.

Gaëtan Gilbert (Aug 30 2022 at 14:41):

Thibaut Pérami (Aug 30 2022 at 14:50):

Module B (MA :A).
  Module M := (F A).
  Import M
  (* stuff that depends on M *)
End B

and C.v is the same module with renaming of B into C, Only D.v uses a concrete MA. So D.v does:

Module M := (F A).
Import M.
Require Import B.
Module BMA := (B MA).
Import BMA.
Require Import C.
Module CMA := (C MA).
Import CMA.

(* Here I have three non-interoperable instance of `I` *)

More abstractly, I want to make a generic library of multiple files that all depend on the same module parameter of type A. Then I want to use that library in some other context where the concrete module of type A is known. B.v and C.v are just different files that are part of that library.

Kenji Maillard (Aug 30 2022 at 15:16):

Maybe you could parametrize B and C with the result of the application F MA and then pass M to both B and C in D.v ?

Thibaut Pérami (Aug 30 2022 at 15:29):

That works in this specific case, but as soon as I have two other files in the generic library that depend on both B and C, it will fail again. Honestly I'm just giving up. A will become a record type, MA a value of that type. And F, B and C will just be plain files where all definitions take a value of type MA as a first argument. With some use of sections, I can maybe partially avoid having to pass that argument around too much. Coq module system is not powerful enough for that use case.

Paolo Giarrusso (Aug 30 2022 at 21:19):

You could define a (parametric) datatype once, and let the module specialize it:

Inductive I (T : Type) := ...

Module Type A.
  Parameter T : Type.
End A..

Module F (MA : A).
  Definition I := I MA.T.
End F.

Paolo Giarrusso (Aug 30 2022 at 21:21):

I'm not sure "not powerful enough" is the best way to put it, but it seems that Coq functors behave here _generatively_ while OCaml functors are applicative?

Paolo Giarrusso (Aug 30 2022 at 21:23):

I got my ML module lessons from the Dreyer school, and at least he might have suggested the opposite — pure functors should be applicative, effectful functors generative; see the journal version of "F-ing modules" for better discussion. So I guess I'm missing quite a bit here?

Gaëtan Gilbert (Aug 30 2022 at 21:27):

Thibaut Pérami (Aug 31 2022 at 08:43):

@Paolo Giarrusso I admit that this works, but it amounts to defining the entire content of F in a section which depends on all the values in A because F contains an inductive that depends on basically everything beforehand. That also means that if B.v or C.v also want to define an inductive, they have to do the same trick again of defining the inductive outside and piping the arguments everywhere

Gaëtan Gilbert (Aug 31 2022 at 08:50):

Module Type AT.
  Parameter x : nat.
End AT.

Module Type FT(Import A:AT).
  Definition stuff := x + 2 * 3.

  Inductive I := IC : stuff = stuff -> I.
End FT.

Module B (A : AT) (M : FT A).

  Definition bla (x:M.I) := 0.

End B.

Module C (A : AT) (M : FT A).

  Definition bli : M.I := M.IC eq_refl.

End C.

(* only for non generic user after this *)

Module F (A:AT).
  Include FT A. (* magic! *)
End F.

Module A. Definition x := 42. End A.

Module M := F A.

Module MB := B A M.
Module MC := C A M.

Check MB.bla MC.bli. (* they're compatible *)

Thibaut Pérami (Aug 31 2022 at 08:52):

I just realize I will have the same problem with function equality. If end up with a goal like M1.f x = M2.f x then reflexivity won't work, and I will need to open both functions to show their content.

Thibaut Pérami (Aug 31 2022 at 08:56):

@Gaëtan Gilbert That will work. This requires that basically everything in the abstract library that could be depended on will be a Module Type and not a Module. I was thinking about diamond problem, but if B and C are also module types, then this will work:

Module D (A : AT) (M : FT A) (B : BT A M) (C : CT A M).
  (*....*)
End D

I think this might solve the problem at the cost of have the entire code of the generic library in Module Type.

Thibaut Pérami (Aug 31 2022 at 08:59):

Gaëtan Gilbert (Aug 31 2022 at 09:01):

you can include a module in a module type for that
you still need an explicit module type though, you can't use it as a type directly

Thibaut Pérami (Aug 31 2022 at 09:09):

Module F (A : AT).
  (* lots of definitions *)
End F.
Module Type FT (A : AT).
  Include F A.
End FT.

Gaëtan Gilbert (Aug 31 2022 at 09:11):

Thibaut Pérami (Aug 31 2022 at 09:12):

Thibaut Pérami (Aug 31 2022 at 09:15):

The only remaining problem with that approach is that if I have two independent files that both need to use let's say C.v then they need to do the instantiation of the functor in a common file otherwise they'll still get incompatible versions that get uncovered if a third file uses them both. But the generic library itself can be written over multiple files naturally, it's just that the dependency tree needs to be explicit in module definitions. I think all other problems are solved by your approach, thank you very much.

Paolo Giarrusso (Aug 31 2022 at 13:54):

Paolo Giarrusso (Aug 31 2022 at 13:57):

I mean, if you have more layers and C depends on many layers, you'd risk ending up with Module D (A : AT) (M : FT A) (N : FT' A M) (O : FT'' A M N).. The size of such a declaration is quadratic in the hierarchy height. That's not ideal.

Paolo Giarrusso (Aug 31 2022 at 14:01):

Not sure this affects @Thibaut Pérami 's scenario, but I've ended up with such code (inspired the stdlib's number hierarchy!). It wasn't fun!

Thibaut Pérami (Aug 31 2022 at 16:37):

Yes I agree it will end-up with a declaration quadratic in the hierarchy height, but the burden is independent of the size of the content of each file, unlike the alternatives with a record or with inductive types defined outside the functor. I also have Extraction concerns that make me want to avoid a solution that involves having type parameters in the inductive type constructor (compared to having types fixed at the module level)

Stream: Coq users

Topic: Applying Functors multiple times

Thibaut Pérami (Aug 30 2022 at 14:39):