Dependencies of `System.Console.ANSI`

[gallais]

When loading System.Console.ANSI we're somehow typechecking
the following modules which seems ridiculous:

Function.HalfAdjointEquivalence
Data.Product.Function.Dependent.Propositional

[JacquesCarette]

Glad I'm not the only one who thinks that stdlib 's dependency graph is quite broken.

@Saransh-cpp you might enjoy trying to see what's going on here?

[Taneb]

The best thing to do here would be to replace the use of Data.Nat.Show.show in encode with building up the string "by hand" (which wouldn't be that much more complicated, frankly, and might actually be simpler)

[Saransh-cpp]

On it. Took some time to learn about how modules are structured in agda, but yes agda -i. src/System/Console/ANSI.agda shows that Data.Nat.Show is the culprit here.

I'll try replacing Data.Nat.Show.show's usage such that we don't have to import it (as suggested by @Taneb, thanks!).

[Saransh-cpp]

I tried a few things, but I am not sure how to proceed ahead with this -

• Copying show and related functions to ANSI does work, but I think this won't be the ideal solution?
• Since (layer l + colour c + intensity i) is a Natural number, I could simply convert that to a String, but I guess that isn't very straightforward without using the show function 😬? I did find a nice StackOverflow thread for this, but I think it might be an overkill for this problem.
• Given how limited values (layer l + colour c + intensity i) can take, I thought about hardcoding a solution, but would that be too naive?

[gallais]

I don't think we should give up on code reuse to reduce the dependency graph:
if Data.Nat.Show imports these transitively then we should try to see whether
we can cut the imports down in that module.

[Saransh-cpp]

Thanks, @gallais!

Here is the chain of dependencies (for my future self and everyone else) -

Data.Product.Function.Dependent.Propositional imports Function.HalfAdjointEquivalence (these 2 should be eliminated; hence, Data.Product.Function.Dependent.Propositional must be eliminated)

agda-stdlib/src/Data/Product/Function/Dependent/Propositional.agda

Line 19 in 4fe9439

open import Function.HalfAdjointEquivalence using (↔→≃; _≃_)

Data.List.Relation.Unary.Any.Properties imports Data.Product.Function.Dependent.Propositional (uses Σ.cong)

agda-stdlib/src/Data/List/Relation/Unary/Any/Properties.agda

Line 33 in 4fe9439

import Data.Product.Function.Dependent.Propositional as Σ

Data.List.Membership.Propositional.Properties imports Data.List.Relation.Unary.Any.Properties (uses map↔)

agda-stdlib/src/Data/List/Membership/Propositional/Properties.agda

Line 17 in 4fe9439

open import Data.List.Relation.Unary.Any.Properties

Data.List.Extrema imports Data.List.Membership.Propositional.Properties (can maybe eliminate here, check)

agda-stdlib/src/Data/List/Extrema.agda

Lines 20 to 21 in 4fe9439

	open import Data.List.Membership.Propositional.Properties
	using (foldr-selective)

Data.String imports Data.List.Extrema (uses max, can maybe eliminate here, check)

agda-stdlib/src/Data/String.agda

Line 18 in 4fe9439

open import Data.List.Extrema ℕₚ.≤-totalOrder

Data.Nat.Show imports Data.String

agda-stdlib/src/Data/Nat/Show.agda

Line 20 in 4fe9439

open import Data.String as String using (String)

System.Console.ANSI imports Data.Nat.Show (uses Data.Nat.Show.show, can maybe eliminate here, check)

agda-stdlib/src/System/Console/ANSI.agda

Line 13 in 4fe9439

import Data.Nat.Show as ℕ

[gallais]

Thanks, this is really helpful. Looking at Data.Nat.Show, it seems to me that
replacing the Data.String import with a Data.String.Base should be sufficient
as we only seem to be using toList and fromList.

[Saransh-cpp]

Nice!! That worked with a minor tweak! Thanks!