move parensIfSpace from Data.String to Data.String.Base

[Sofia-Insa]

In PR#2016, in src/Reflection/AST/Show.agda, parensIfSpace was the only function used from Data.String, while the other were from Data.String.Base.

In the stdl parensIfSpace is only called once : in src/Reflection/AST/Show.agda.

[Taneb]

I don't think we should do this. Importing Data.Char.Properties from Data.String.Base hugely increases the latter module's dependency footprint.

[gallais]

I agree: this feels like going in the wrong direction.

I think the PR we actually need is the one getting rid of parensIfSpace
which is a really horrible way to implement precedence-aware pretty
printing and instead refactor the Reflection.AST.Show to have a showPred
function that takes a precedence level as an extra argument and uses that
to throw in parens in the right places.

[JacquesCarette]

Oops, my bad - I didn't look deeply enough into Data.Char.Properties when I asked @Sofia-Insa to try for this version.

I agree that the showPred solution is much better.

[Saransh-cpp]

I and @Sofia-Insa spent some time on this and went through (surprisingly limited) resources on the internet, but we are not sure how to implement this. We think the type signature should be -

showsPrec : Precedence → String → String
-- or
showsPrec : ℕ → String → String

but we are not sure how the fixity would factor in while adding brackets (also, fractional fixity is a possibility - #1999). Should it be that if showsPrec gets a precedence of 6, it will add brackets around all the operations performed by an operator with fixity 6?

For example, should -

showsPrec 7 "5 + 5 * 5"

output -

"5 + (5 * 5)"

as _*_ has a fixity of 7 and _+_ has a fixity of 6?

https://stackoverflow.com/a/24207467/14746647 and https://stackoverflow.com/a/61160682/14746647 discuss implementing (or overriding?) Haskell's showsPrec but they hardcode it, listing out all the possible cases with the operators they are using. The definition in https://hackage.haskell.org/package/base-4.7.0.0/docs/src/GHC-Show.html does generalize it, but it also has a lot of defined cases. For reference, we also tried locating some examples in Agda containing Precedence in their type signature, but I don't think they would be helpful. How should we proceed ahead with this?

[JacquesCarette]

It is indeed tricky to find good documentation for this. I eventually found some in Haskell's Text.Show documentation.

Certainly the precedence should not be ℕ as that's not what Agda itself uses. Digging into the depths of the Reflection API I see that Float is what is used (though actually, the Precedence type has 2 constructors). To be maximally compatible with Agda itself, you should use Precedence.

As the Haskell doc indicates, precedence gives a total order, so the comparison to use is <.

It is indeed rather odd that stdlib currently does not seem to use Precedence at all!

[gallais]

It is indeed rather odd that stdlib currently does not seem to use Precedence at all!

We don't really have show instances for anything beyond base types.
I think the show for the reflection stuff was hacked in a hurry for
debugging purposes rather than properly designed.

[JacquesCarette]

So we shouldn't use the current Precedence type? Or it's just the show that is a hack?

[gallais]

I think we should definitely use Precedence.

[MatthewDaggitt]

I agree with all the discussion in here so far. Going to close this PR as I think we've agreed this is not the approach we want to follow. Further discussion can continue in #569.