I have a module type
A and a functor
F that takes a module of type
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.
reflexivity fails which suggest that those two types are different. My problem is that I have two files
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
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.
Module M := F MA in a separate file used by both B and C
Ok I need more context: both
C.v are generic, so
Module B (MA :A). Module M := (F A). Import M (* stuff that depends on M *) End B
C.v is the same module with renaming of
D.v uses a concrete
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.
C.v are just different files that are part of that library.
Maybe you could parametrize
C with the result of the application
F MA and then pass
M to both
That works in this specific case, but as soon as I have two other files in the generic library that depend on both
C, it will fail again. Honestly I'm just giving up.
A will become a record type,
MA a value of that type. 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.
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.
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?
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?
generative functors are much easier to implement
@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
F contains an inductive that depends on basically everything beforehand. That also means that if
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
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 *)
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.
@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
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
Coq has the equivalent of https://v2.ocaml.org/manual/moduletypeof.html, then I could do it the other way too
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
Oh but I can do:
Module F (A : AT). (* lots of definitions *) End F. Module Type FT (A : AT). Include F A. End FT.
that's what I said
Sorry I just wrote what you said
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.
Does this approach scale or does it have the problems of full functorization?
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.
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!
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: Sep 23 2023 at 07:01 UTC