Split up ReflectiveSubuniverse.v into smaller files

[Alizter]

I think splitting up ReflectiveSubuniverse.v will be beneficial for readability. At the moment we have one big file (~2000 lines) which makes it very difficult to read and find things in. I propose splitting these up into smaller files as follows:

• Core.v containing the definition of ReflectiveSubuniverses (basically up to ln 252). And Restrictions and Unions from the end.
• Functor.v containg results about the functoriality of ReflectiveSubuniveres.
• Equiv.v containg results about O-equivalences (O_inverts)
• Type.v contain results about the interaction of RSUs and various type constructors
• Decidable.v about the interaction with decidability
• Monad.v about the monad stuff
• Connected.v about O-connected types
• Map.v about O-local maps
• ConnMap.v about O-connected maps

These would all of course be indexed by a ReflectiveSubuniverse.v file which means the rest of the library would remain untouched.

[mikeshulman]

In principle, I'm certainly in favor of this (and perhaps something similar for Modality.v). Probably they should all be in a subdirectory Modalities/ReflectiveSubuniverse.

The reason I haven't done this before is that the module-wrangling seemed difficult. I wanted there to be just one "ReflectiveSubuniverse_Theory" module that a user could import rather than having to import separate modules for all the separate files, and a single Coq module can't span multiple files. Perhaps the main index file could contain one module that Exports all the modules from all the sub-files. But the individual sub-files would have to manually import the appropriate modules from each other, and if for instance the ConnMap_Theory module imports the Connected_Theory module and then both are imported from the index file, I think we might end up with two copies of the Connected_Theory module, which might be a problem for typeclass inference, unification, etc. Some multiple-inheritance issue like that already arose somewhere in the modalities library I think. But please try it and find out!

[Alizter]

It's also come to my attention that there are people working on universe minimization in coq currently. As I understand, this will lead to a point where records can be just as polymorphic as modules. If this is the case, the modalities library ought to be redesigned using records (or classes). Hopefully we won't have the overly restrictive universe levels that I ran into recently with the seperation RSU.

[mikeshulman]

I don't know what universe minimization refers to here, but I can't imagine a semantically consistent way that records could be as polymorphic as modules, since a polymorphic object is itself larger than any given universe and hence cannot belong to any universe.

[Alizter]

@mikeshulman I don't know the details fully yet either, but we will see in the future. Regarding semantics I have even less of an idea.

[Alizter]

@mikeshulman Also, what does "replete" mean? I couldn't find it in RSS or in HTT. Should we perhaps include a definition in the documentation?

[mikeshulman]

On what are you basing your expectation that universe minimization would enable records with polymorphic fields?

https://ncatlab.org/nlab/show/replete+subcategory

[Alizter]

@mikeshulman Nothing serious, I have just been chatting with Andreas Lynge. Looking back over the emails, I think I may have misunderstood. He suggested that it may be possible to rewrite the parts of the library using records and classes (might be speculation I don't know).

He did however agree that it would seem possible to relax the signature requirements of modules with respect to universes. I.e. have some sort of mechanism that coq can insert extra universes if it needs to, without having to change the signature of a parameter of a module type.

But most likely I have misunderstood.

[Alizter]

@mikeshulman I had an attempt at splitting it up but as you said there are multiple copies of the same things floating around which is causing unification problems. It doesn't look like this is possible currently.

[Alizter]

I'm going to close this issue for now since I don't see anything coming out of it. You are correct that "module-wrangling" is causing much difficulty here. If in the future we manage to rid ourselves of having to use modules somehow, this might serve as a basis for refactoring the modalities library.

[andreaslyn]

I do not understand why we use module types instead records and classes. Considering the inflexibility with universes in module types, I would try using records and classes before module types. Records and classes instead of module types might make the modalities library easier to understand as well. But @mikeshulman maybe you know the reason for using module types in the modalities library?

[mikeshulman]

The issue with records and classes is that an individual instance of a record or class is not universe-polymorphic. With module types we can have that "a modality" is simultaneously defined on all universes, rather than having separate notions of "modality on U" for all universes U. This matters when considering for instance whether the universe of modal types is modal.

[Alizter]

Now that #1238 has been done we can actually do this.