Stream: Coq users

Topic: Applying Functors multiple times


view this post on Zulip Thibaut Pérami (Aug 30 2022 at 14:39):

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?

Example of setup:

Module Type A.
End A.

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

Module MA.
End MA.

view this post on Zulip Gaëtan Gilbert (Aug 30 2022 at 14:41):

put Module M := F MA in a separate file used by both B and C

view this post on Zulip Thibaut Pérami (Aug 30 2022 at 14:50):

Ok I need more context: both B.v and C.v are generic, so B.v is:

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.

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Aug 30 2022 at 21:27):

generative functors are much easier to implement

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Aug 31 2022 at 08:50):

maybe something like

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 *)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Thibaut Pérami (Aug 31 2022 at 08:59):

If Coq has the equivalent of https://v2.ocaml.org/manual/moduletypeof.html, then I could do it the other way too

view this post on Zulip 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

view this post on Zulip Thibaut Pérami (Aug 31 2022 at 09:09):

Oh but I can do:

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

view this post on Zulip Gaëtan Gilbert (Aug 31 2022 at 09:11):

that's what I said

view this post on Zulip Thibaut Pérami (Aug 31 2022 at 09:12):

Sorry I just wrote what you said

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Aug 31 2022 at 13:54):

Does this approach scale or does it have the problems of full functorization?

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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)


Last updated: Jan 31 2023 at 12:01 UTC