The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

NB it's not about importing, it's about functor application

Gaëtan Gilbert

On 05/11/2021 10:01, Chris Dams wrote:
> Dear all,
>
> In case anyone is interested in what I did after asking my question about
> modules in this mailing list, I will describe the final solution that
> I arrived at.
> I tried both the solutions by Guillaume and by Madhukar and they both work
> but also have some disadvantages. In the end I ended up going with my
> own solution (Example-2 in the original post) but basically turning the chain
> of modules that import each other into an implementation detail. I renamed
> some of the files involved adding '_internal' to their name in order to 
> indicate
> that they are not meant to be used separately and added a facade file
> that is just importing the whole chain but with a generic name suggesting
> that it is the file that one is supposed to import as opposed to the other
> internal ones. In future I could imagine putting the 'internal' files in a
> subdirectory to further indicate their internal nature. Now my whole project
> is compiling again, so I am happy :-).
>
> The problem with Guillaumes  solution is that while it works I really have to
> pull out a lot of definitions out of my modules. It is not one
> inductive definition
> that needs to be pulled out of Module1 as in my example. It is 9 of them.
> And then more inductive definitions from the other modules. Also, the 
> inductive
> definitions in subsequent modules do not just refer to inductive definitions 
> in
> the previous modules but also to ordinary definitions, which, as a result 
> would
> also have to be pulled out of the module. At this point it gets quite
> impractical.
> Also, some of these inductive definitions are Records and then I have to not
> just import the name of the Record but also the name of its constructor and
> the names of its fields into the module and give all of these different names.
> I prefixed the 'global' ones with a 'g' which is not very nice either.
>
> The problem with Madhukars solution is that while it also works it has quite
> a bit of syntactic overhead that is quite tricky that is not just in
> the internal
> files but also in the code that uses it. Because of this I decided in the end 
> to
> put the modules behind the facade that I described above so code using this
> can just Import one module and be done with it.
>
> After looking into all of this I cannot really help feeling that the issue 
> that
> importing a module with an inductive definition copies the inductive 
> definition
> such there there are then two incompatible inductive types really should
> be considered a bug in coq. I understand that the current way is the easiest
> way to implement modules and I really do not know whether improving the
> situation is possible but it just seems strange and highly impractical....
>
> Kind Regards,
> Chris