The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

Some time ago, we were deciding whether to use modules or typeclasses as the
primary means of abstraction in bedrock2, and the problem you describe (or at
least, a similar one) seemed so unsolvable that we decided to use typeclasses
and not use modules at all (which I think is sad).

The corresponding discussion is here:
https://github.com/mit-plv/bedrock2/commit/20d5fac26f#r29468057

The problem I'm referring to is: If you put an Inductive inside a module
functor, and instantiate it twice with the same module, you get two
instantiations of the Inductive which Coq considers to be different types.

The only solution seemed to be to define the Inductive outside of the module
functor, but that defeats the point because we'd have to pass it the
parameters each time we use it, which is precisely what we're trying to
avoid.

On Fri, 2018-08-17 at 15:36 -0500, Kevin Hamlen wrote:
> Dear Coq users,
> 
> What do Coq programmers consider the "right way" to organize large 
> projects containing functors?  In particular, how do authors of large 
> projects define collections of modules that all build upon some shared 
> functor without getting duplicate name-conflicts? Here's an example:
> 
> (* Input parameters and axioms are declared as a module type: *)
> Module Type FOO_TYPE.
>    Parameter foo: Type.
> End FOO_TYPE.
> 
> (* Another module builds definitions from the inputs: *)
> Module FooDefs (Foo: FOO_TYPE).
>    Inductive bar := Bar (f:Foo.foo).
>    (* ... hundreds more definitions ... *)
> End FooDefs.
> 
> (* Now we wish to create myriad modules that prove various things about 
> FooDefs given a Foo.  Here's one way that doesn't work well: *)
> Module FooTheory1 (Foo: FOO_TYPE).
>    Module F := FooDefs Foo.
>    Import F.
>    Ltac silly1 := match goal with |- Bar _ = Bar _ => reflexivity end.
>    (* ... more theorems, proofs, and ltacs ... *)
> End FooTheory1.
> 
> (* This doesn't work well because each module defined in this way has 
> its own copy of FooDefs, which Coq doesn't always recognize as equal. *)
> Module Foo:FOO_TYPE.
>    Definition foo:=nat.
> End Foo.
> Module FD := FooDefs Foo.
> Module FT1 := FooTheory1 Foo.
> Import FD.
> Import FT1.
> Theorem silly: forall (x:bar), x=x.
> Proof.
>    destruct x.
>    Fail silly1. (* fails because FD.Bar is not the same as FT1.F.Bar. *)
> Abort.
> 
> 
> Here are two alternative options that also don't seem to work well:
> 
> (2) Using "Export F" in FooTheory1 instead of creating a separate FD 
> module fixes the problem above, but then all FooTheory modules must be 
> arranged in a linear hierarchy to avoid duplicating the definition of 
> F.  They can't be created independently, lest they export two distinctly 
> named versions of F.
> 
> (3) We could make a FOO_DEFS module type (whose content is a verbatim 
> copy of FooDefs) and then parameterize all the FooTheory modules with 
> FOO_DEFS instead of FOO_TYPE modules.  But that leads to a rather 
> tortuous development regimen: Every new FooTheory module must also 
> define a FOO_THEORY type that duplicates all its definitions, and 
> instantiating the new FooTheory requires first laboriously instantiating 
> all the modules it depends upon, just so that they can all import the 
> shared definition of FooDefs.
> 
> What is the "right" way to do this sort of thing?
> 
> Thanks,
> Kevin
> 
> 
>