Add Show class

[silas-hw]

Should hopefully resolve #569 and partially address #431.

Opening as a draft to start discussion on design. Points to look into:

• Design of the class itself. Personally I'm happy with how this roughly looks, but discussion and critique is useful!
• metaprogramming / macros for deriving show instances, al a https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda
• implementing instances for existing datatypes
• creating a Parse or Read class that does the inverse
  • and then perhaps proofs on the two working together
• what proofs/properties, if at all, should be added to the class(es)
  • my instincts say none at all, other than when having both Read and Show

[silas-hw]

#569 added ShowOptions, but personally I think this might be too much to carry around? I can't think of when 'verbosity' would be relevant to Show, as I see Show being more concerned with just displaying a value of a datatype, and 'verbosity' seems more concerned with logging.

Although, I'm not strongly opinionated to either direction.

[JacquesCarette]

Comments on just the code.

[JacquesCarette]

You should avoid directly using builtins. Normally there is something in the library that re-exports it. There's a whole Reflection sub-library, it is likely there?

[silas-hw]

It doesn't re-export Precedence from what I can tell (using rgrep)

[JacquesCarette]

Re: macros for deriving instances. 1) very good thing to offer. 2) likely we won't use them internally, as they do evil things to the dependency graph.

Also, one thing Haskell got "wrong" was that Show tried to be both 'pretty' and 'readable'. These are strongly in conflict! We should have a Pretty class that never pretends the reader is anything but a human, and a Write class that is a (one-sided) inverse to Read. What Show does then can be arbitrary...

[silas-hw]

Also, one thing Haskell got "wrong" was that Show tried to be both 'pretty' and 'readable'. These are strongly in conflict! We should have a Pretty class that never pretends the reader is anything but a human, and a Write class that is a (one-sided) inverse to Read. What Show does then can be arbitrary...

As in what is Show here should be renamed Pretty? and that a Write and Read class should be introduced requiring proofs that they mirror each other?

IMO doing the Pretty class first would give the best insights onto what the API for 'showing' would be, which can then be copied over to Write with associated proofs (in this PR still, just in that order).

[JacquesCarette]

Re: Show, Pretty and Write. That is my opinion, yes. And I think an opinion shared by many in the Haskell community (i.e. this is a 'learned' opinion from distilling what many others have written). As such, I would strong want to hear from @gallais @jamesmckinna and @MatthewDaggitt on this. (I think the name Pretty is reasonably settled, but Write is most definitely not.)

[jamesmckinna]

Definitely not an expert, at least from my end! Other than Text.Pretty{.Core} and its test(s), defining Doc/Block types etc. incl. Data.Tree.Rose.Show.show.