[ re #1993 ] Simplifying the dependency graph

[gallais]

Started with simplifying System.Console.ANSI
Noticed we could take advantage of Data.Product.Base
Got a bit sidetracked and started cleaning up a lot of modules

[jamesmckinna]

Agree with the general philosophy!
But against (per also myself) and most of the changes: has this made the library more brittle?
Against that, I'm presuming/conjecturing: not really?
All other things being equal, my very cursory look at the changes suggests we proceed with this PR.

[gallais]

Yeah I don't think what I have done here is super controversial:

• Use .Base when possible
• Make some import lists explicit
• Drop useless imports
• In rare cases use e.g. Function.Definitions instead of Function

The most controversial (which is "not very" IMO) changes could be:

• Moving the existential quantifiers from Data.Product to Data.Product.Base
• Use → ⊥ instead of ∄ in the type of one (1) auxiliary definition in a where block
  in Data.Nat.Properties because putting ∄ in .Base would create a circular dependency

[jamesmckinna]

Do you make essential use of the import of Σ-syntax here?
if not, then one way to advance your thesis about the imports of Data.Product.Base might be to move both definitions of the syntax for Σ and ∃ to Data.Product?

[gallais]

The syntaxes are used in a few places already. I don't want to rewrite that code to
drop the syntaxes (which are trivial definitions that have no external dependencies)
just for the sake of it.

I think this PR in its current shape should be backwards compatible but moving
Σ-syntax out of Data.Produt.Base would break that.

[jamesmckinna]

Regarding

The most controversial (which is "not very" IMO) changes could be:

• Moving the existential quantifiers from Data.Product to Data.Product.Base
• Use → ⊥ instead of ∄ in the type of one (1) auxiliary definition in a where block
  in Data.Nat.Properties because putting ∄ in .Base would create a circular dependency

I suspect neither of these is much of a problem, but it does leave Data.Product itself as (largely) redundant? I might be tempted, as with my review comment, to push the use of -syntax into Data.Product for the three non-trivial uses you seem to make of it, but does that cause (the same) circular dependency?

[gallais]

It's been very common in the past for Data.X modules to be basically empty
and for the Data.X.Base to contain all the interesting definitions. I don't think
it's a problem, these mostly exist as a way to stratify the dependency graph in
a structured manner across the whole library.

[JacquesCarette]

I'd love to have decent tools for visualizing giant dependency graphs. dot sure isn't that tool.

I've done very aggressive refactoring on my own codes after I saw the complete mess by graphs were (but these were projects with ~50 files, not hundreds). It was extremely satisfying.

[gallais]

@JacquesCarette Good idea. I've added it to my list of MSc projects to offer next year. :)

[gallais]

I've written a first little analysis here: https://github.com/gallais/dot-analysis

1. turns the graphviz thing into something more manageable
2. first (and only) so far analysis sorts the node using a scoring system
   (here √(|depends-upon| + |is-dependended-upon|²)) and then lists
   the 5 modules with the highest scores

Running it on the graph generated by README.agda for this PR, I get
(dependencies elided for concision, each module is accompanied by its score):

Data.Product (74.00676)
Relation.Binary.PropositionalEquality (40.06245)
Function (39.03844)
Relation.Binary (27.018513)
Data.List (21.023796)

so there is still some work to do, and Data.Product is still quite central.

[Taneb]

Relation.Binary.PropositionalEquality stands out to me there, that can bring a whole pile of dependencies in. I'm going to try to eliminate that one

[gallais]

@Taneb That's the dependencies for Relation.Binary.PropositionalEquality:

  ↑Relation.Binary.PropositionalEquality.Algebra
  ↑Function.Equality
  ↑Relation.Nullary.Decidable
  ↑Axiom.UniquenessOfIdentityProofs
  ↑Axiom.Extensionality.Propositional
  ↓Data.Sum.Properties
  ↓Function.Metric.Nat.Structures
  ↓Algebra.Consequences.Propositional
  ↓Data.Product.Properties
  ↓Data.List.Relation.Binary.Subset.Propositional
  ↓Algebra.Properties.Monoid.Mult
  ↓Data.List.Relation.Binary.Pointwise.Properties
  ↓Data.List.Relation.Binary.Sublist.Heterogeneous
  ↓Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties.WithK
  ↓Reflection.AST.Argument.Visibility
  ↓Data.These.Properties
  ↓Data.List.Relation.Binary.Permutation.Propositional
  ↓Data.Unit.Properties
  ↓Function.Equivalence
  ↓Data.Unit.Polymorphic.Properties
  ↓Relation.Binary.Reasoning.MultiSetoid
  ↓Function.Injection
  ↓README.Data.Default
  ↓Data.Vec.Membership.Propositional
  ↓Relation.Binary.Indexed.Homogeneous.Structures
  ↓Data.Word.Base
  ↓Relation.Binary.Construct.Closure.Transitive
  ↓Relation.Binary.Reflection
  ↓Data.Maybe.Relation.Binary.Pointwise
  ↓Relation.Binary.Construct.Closure.Reflexive.Properties
  ↓Data.Maybe.Relation.Binary.Connected
  ↓Data.List.Relation.Binary.Disjoint.Propositional
  ↓Codata.Musical.Conat
  ↓Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
  ↓Codata.Sized.Cofin
  ↓Function.Construct.Identity
  ↓Algebra.Construct.LiftedChoice
  ↓Data.List.Membership.Propositional
  ↓Function.Construct.Symmetry
  ↓Reflection.AST.Argument.Relevance
  ↓Data.List.Relation.Unary.Sufficient
  ↓Data.Maybe.Relation.Unary.Any
  ↓Reflection.AST.Argument.Quantity
  ↓Codata.Sized.Delay.Bisimilarity
  ↓Data.Product.Relation.Binary.Pointwise.Dependent

[JacquesCarette]

@Saransh-cpp this is something that can be dealt with incrementally. For Data.Product, there is likely a whole lot of Agda that imports it but it actually only needs Data.Product.Base - and those can be changed. For any case that is more complicated than that, it should just be left alone. This can be done in a bunch of small PRs; that way the straightforward ones can be merged, and anything that's controversial won't block overall progress.

[Saransh-cpp]

Nice! I'll take that up!

[JacquesCarette]

I've found the related work that I was thinking of TGView3D: a System for 3-Dimensional Visualization of Theory Graphs. There was a nice demo at CICM 2020 (and in 2018 too). The paper points to https://github.com/UniFormal/TGView3D for the sources.

Large graphs are one of the few places where I've seen 3D being actually useful.

[Saransh-cpp]

To avoid duplicate PRs: I've simplified Data.Product, Function, and Data.List imports on my fork. I'm also almost done with Relation.Binary. Will open PRs once this one is merged.

[Taneb]

I opened #2002 for Relation.Binary.PropositionalEquality a few days ago