Simplify Show

[gmalecha]

Show got complicated because it tried to do too much. It can generate string, list ascii, etc, any monoid with an injection from ASCII. This means that debugging instances is hard.

[Lysxia]

Another option is to deprecate and remove Show altogether. Even if we fixed it, it seems a good candidate to put into its own library.

I recently created coq-ceres as an alternative, using S-expressions instead of strings as a common format that can easily be pretty-printed and parsed.

A proper pretty-printing library also seems like a good idea.

[gmalecha]

I am generally in favor of small libraries, so I would be in favor of moving Show somewhere else.

I don't think that S-expressions solve everything, so I think there is some benefit to more customizable pretty printing library. Perhaps there is some good way to share some of the formatting logic within ceres? I'm thinking of "boxes" and the like.

[gmalecha]

@Lysxia Do you think there is some pieces of ceres that could be reused for this?

[Lysxia]

Ceres doesn't currently do any kind of pretty printing, it only writes S-expressions on one line. But the idea is that S-expressions can be formatted independently. So there's going to be a pretty-printing library written from scratch and ceres will depend on it to provide a decent pretty-printer for simple debugging needs.

[gmalecha]

Does ceres not generate a string?

[Lysxia]

I'm not sure what you're thinking of. There is a function that converts S-expressions (trees) to strings, but there's not much to be reused from it.

[gmalecha]

I see.