Minimization of dependencies

[eupp]

First of all, I would like to thank all the contributors to this library!
For our project, we've been searching for a Coq library of monad theory and among few alternatives we chose monae.
Currently, we need just a basic stuff: basic hierarchy (functors, natural transformations, monads, nondet monads) and basic instances (list, state, etc). We've been really happy to find everything we need in monae.
However, a big list of library dependencies was a bit disappointing.

For example, a dependency on coq-infotheo was surprising, as well as dependencies on mathcomp-fingroup, mathcomp-solvable, etc. From what I understood after a quick pass over the sources, coq-infotheo is used mostly for the probability monad. The boolp.v library from mathcomp-analysis is used heavily for "classical" reasoning. I haven't understood how mathcomp-fingroup, mathcomp-field, etc are used.

Since the monad theory is a cornerstone of PL theory, it would be really nice to have a core library of monad theory with a minimalistic list of dependencies. If you'll be interested in achieving this goal I would be happy to help with this and prepare a PR.

I think there are two possible ways to achieve this:
(1) split the library into two: something like monae-core with a basic hierarchy of monads and common theory,
and e.g. monae-prob with the probability monad
(2) use opam's depopts feature and install various advanced features of the library (e.g. prob monad) only if the user already has all required packages installed.

[affeldt-aist]

Thank you for your interest!

monae uses infotheo for probabilities and infotheo uses fields for error-correcting codes (in a limited way) iirc,
hence the dependency on mathcomp-field, which triggers the dependency on other MathComp packages.
(So splitting the probability subdirectory out of infotheo might also be another option to reduce
dependencies, though fields are likely to get back through mathcomp-analysis unless it is also split.)

Note also that monae's master now uses Hierarchy Builder and this triggers a new set of dependencies
that are here to stay given the benefits of using Hierarchy Builder (whose recent introduction in monae
improved its usability).

The main reason we didn't do any splitting so far is essentially lack of time and also because
changes in mathcomp-analysis often trigger changes in infotheo and in turn in monae.
I suspect that this situation will continue in the near future because of the introduction of
Hierarchy Builder in MathComp and because we have plans to extend monae that depend
on mathcomp-analysis.
I fear that splitting packages further might make this migration more tedious for us by
requiring even more releases. It might be more efficient to perform it after the situation with
Hierarchy Builder has stabilized.

I didn't know the depopts feature of opam but right now it sounds to me like the most reasonable
option (at least given the resources on our side).

[t6s]

I am afraid that, after the merger of monae-hb branch, even the core part now suffers from a heavy dependency starting from Hierarchy Builder.

[affeldt-aist]

You can also observe that the subdirectory impredicate_set contains a subset of monae (code is duplicated almost verbatim) without the probabilities-related stuff (because in the current state of affairs it is not compatible with the impredicative set option).

[eupp]

Hi @affeldt-aist, thank you for the quick response!

Note also that monae's master now uses Hierarchy Builder and this triggers a new set of dependencies
that are here to stay given the benefits of using Hierarchy Builder.

I guess dependencies on coq-mathcomp-ssreflect and coq-hierarchy-builder are fine. Both packages are basic infrastructure of mathcomp style Coq proofs.

I didn't know the depopts feature of opam but right now it sounds to me like the most reasonable
option.

Thereby, I think the problem can be solved in two steps.
(1) Split the project "internally", use depopts to conditionally enable more advanced features of the library.
(2) Once the Hierarchy Builder and other dependency packages will stabilize, split the monae repo. In the best-case scenario, at this point the repo already be split into subparts, that would be built in several stages with the help of depopts, so the migration to several monae subpackages should go smoothly.

You can also observe that the subdirectory impredicate_set contains a subset of monae (code is duplicated almost verbatim) without the probabilities-related stuff

Do you think the problem with the code duplication should also be solved as a subtask of this issue?

With respect to the solution of this issue, I would really be happy to help here. What can I start from?
Moving the probability monad out of hierarchy.v and unification of hierarchy.v with impredicative_set/ihierarchy.v seems like a reasonable first step. Should I start from it, or do you have another plan in mind?

[affeldt-aist]

What can I start from?

I did a tentative split as PR #57 .

It turns out that some files that are not explicitly depending on probabilities still depend on infotheo for some utilities.
Dependencies on classical_sets_ext.v could be removed by PRing the needed lemmas to mathcomp-analysis.
As for dependencies on ssr_ext.v and ssrZ.v, it is not obvious how to proceed to me right now.

[eupp]

What can I start from?

I did a tentative split as PR #57 .
Dependencies on classical_sets_ext.v could be removed by PRing the needed lemmas to mathcomp-analysis.
As for dependencies on ssr_ext.v and ssrZ.v, it is not obvious how to proceed to me right now.

I've removed some unused dependencies on infotheo in #59

As for the real dependencies that are still there, I've noticed the following:

1. monad_model.v depends on classical_sets_ext.bigcup_ lemmas and also convex.choice_of_Type. The latter I suppose can be moved to boolp.v from mathcomp-analysis in a separate PR.

2. example_nquees.v and example_array.v depend on eqType instance for Z (ssrZ.Z_eqType).
   trace_lib.v also depends on some notations for Z from ssrZ.
   However, my general question was why the vanilla Coq Z is used instead of ssrint?
   It looks like the latter supports exactly the same functionality as required by monae.

3. example_quicksort.v uses bounded sequences from ssr_ext. It is in fact the single usage of ssr_ext.
   Although it looks like it is still WIP, so one possible temporary solution would be just not to build it?
   Another solution would be to try PR bseq to mathcomp.

[affeldt-aist]

I've removed some unused dependencies on infotheo in #59

Thank you for the careful review!

As for the real dependencies that are still there, I've noticed the following:

1. `monad_model.v` depends on `classical_sets_ext.bigcup_` lemmas and also `convex.choice_of_Type`.

The latter I suppose can be moved to boolp.v from mathcomp-analysis in a separate PR.

Let's do that (math-comp/analysis#405, math-comp/analysis#406).

2. `example_nquees.v` and `example_array.v` depend on `eqType` instance for `Z` (`ssrZ.Z_eqType`).
   `trace_lib.v` also depends on some notations for `Z` from `ssrZ`.
   However, my general question was why the vanilla Coq `Z` is used instead of `ssrint`?
   It looks like the latter supports exactly the same functionality as required by `monae`.

We've been using Z instead of ssrint because it is a bit easier to use (in particular, more people are familiar with it),
it lends itself to execution (in particular, it is useful to test examples), and it also appears naturally when using the
reals from the Coq standard library.

3. `example_quicksort.v` uses bounded sequences from `ssr_ext`. It is in fact the single usage of `ssr_ext`.
   Although it looks like it is still WIP, so one possible temporary solution would be just not to build it?
   Another solution would be to try PR `bseq` to `mathcomp`.

Actually, we will soon merge an admit-free version (https://github.com/AyumuSaito/monae/tree/saito_quicksort).
After this merge, some generic lemmas will certainly make there way to lib files and afterwards there will be more
work on the same line to enrich the array monad. So we'd rather like to keep it in master.

Maybe we should go with PRing bseq to mathcomp for this one. It is definitely useful in monae and should
be useful for coding (although it is under exploited in infotheo as of today).

[eupp]

We've been using Z instead of ssrint because it is a bit easier to use (in particular, more people are familiar with it),
it lends itself to execution (in particular, it is useful to test examples), and it also appears naturally when using the
reals from the Coq standard library.

Therefore, I guess, the solution would be to put ssrZ (and, perhaps, ssrR) into a separate small self-contained library?

Maybe we should go with PRing bseq to mathcomp for this one. It is definitely useful in monae and should
be useful for coding (although it is under exploited in infotheo as of today).

Sounds good!
Would you like to do it by yourself?
Otherwise, I can try to prepare a PR in the coming days.

[affeldt-aist]

Therefore, I guess, the solution would be to put ssrZ (and, perhaps, ssrR) into a separate small self-contained library?

In this case, the strategy would be to have a new subdirectory in infotheo for these two libraries
and release infotheo as two opam packages (like it is done for MathComp)? (@t6s, is it ok with you?)

Sounds good!
Would you like to do it by yourself?
Otherwise, I can try to prepare a PR in the coming days.

You may want to PR it because I will lack time in the next few days. :-(

[t6s]

In this case, the strategy would be to have a new subdirectory in infotheo for these two libraries
and release infotheo as two opam packages (like it is done for MathComp)? (@t6s, is it ok with you?)

Okay to separate the package into two. But what would you name them?
infotheo-ssrext and infotheo-infotheo?

[affeldt-aist]

Okay to separate the package into two. But what would you name them?
infotheo-ssrext and infotheo-infotheo?

Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it provides ssr-like naming for standard library's datatypes)?

[t6s]

Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it provides ssr-like naming for standard library's datatypes)?

ssrstd sounds too generic or strong, doesn't it? What about thinssr or thinssrstd?

[affeldt-aist]

Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it provides ssr-like naming for standard library's datatypes)?

ssrstd sounds too generic or strong, doesn't it? What about thinssr or thinssrstd?

Another proposal from riot: ssrwrap-stdnum @garrigue

[affeldt-aist]

Let's do that (math-comp/analysis#405, math-comp/analysis#406).

fyi, those two have been merged

[affeldt-aist]

Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it provides ssr-like naming for standard library's datatypes)?

ssrstd sounds too generic or strong, doesn't it? What about thinssr or thinssrstd?

Another proposal from riot: ssrwrap-stdnum @garrigue

Note that there is https://github.com/math-comp/mczify/blob/master/theories/ssrZ.v
that we could maybe try to reuse instead of spinning off another version of ssrZ.v.