Add `Show` class by silas-hw · Pull Request #3098 · agda/agda-stdlib

silas-hw · 2026-07-30T20:52:46Z

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 · 2026-07-30T20:56:33Z

#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 · 2026-07-30T22:07:05Z

+module Text.Show where
+
+-- should builtin be used?
+open import Agda.Builtin.Reflection using (Precedence)


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?

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

JacquesCarette · 2026-07-30T22:14:03Z

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 · 2026-07-31T15:06:30Z

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 · 2026-07-31T15:25:18Z

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 · 2026-07-31T16:03:19Z

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.

MatthewDaggitt

I'm happy with the names Show, Pretty, Read, Write

MatthewDaggitt · 2026-08-03T00:52:33Z

+
+instance
+  ListShow : {{ Show A }} → Show (List A)
+  ListShow .showsPrecList prec [] str = '[' ∷ (']' ∷ str)


We should probably define a surround and a concatenate in the library if we don't already have those and define this in terms of them?

silas-hw · 2026-08-14T18:08:10Z

Thoughts on the given interfaces? Still not entirely sure how to go about having properties that Read and Write work together, and I'm not fully happy with the ReadWrite thing I have here. Also, should we definitely use Precedence from Reflection?

gallais · 2026-08-17T09:58:43Z

+private
+  test[ℕ] : String
+  test[ℕ] = write (5 ∷ 2 ∷ 12 ∷ 42 ∷ [])


We may as well make this a unit test?

_ : write (5 ∷ 2 ∷ 12 ∷ 42 ∷ []) ≡ ? _ = refl

(with the ? appropriately filled in)

gallais · 2026-08-17T10:01:07Z

+
+record Read (A : Set a) :  Set a where
+  field
+    read : String → Maybe A


Should this be a derived operation based on a more general String -> Maybe (a, String)?
Or even List rather than Maybe? Maybe even one with a precedence?

Cf. https://hackage-content.haskell.org/package/base-4.22.0.0/docs/Prelude.html#v:readsPrec

Almost certainly

Why would you use List instead of Maybe?

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

silas-hw · 2026-08-17T16:51:22Z

RE: "ReadWrite", I'm somewhat coming around to having the proof in a separate, combined record. In that it is most likely a specific pair of Read and Write instances are designed to work together, which would then be grouped into a ReadWrite?

Anything else seems like it would

create too heavy of an interface (i.e. combine read and write interfaces)
require a proof between all instances of Read/Write on a given type, which would be difficult if not impossible.
possibly create circular dependency

I could be overthinking this, however.

silas-hw · 2026-08-17T20:31:44Z

Text.Pretty has the --with-k option, seemingly because of its import of Data.String.Base.Unsafe. Two notes:

Is is possible to refactor Pretty to not require --with-k, e.g. using list of chars instead of strings?
If 1 is not possible, should Pretty instances be placed in something like .Unsafe.Instances? This should also be added to the style guide.

silas-hw added 3 commits July 30, 2026 15:36

Add show class

d01fd7f

Cleanup code

32907ba

Cleanup code

8776f8e

JacquesCarette requested changes Jul 30, 2026

View reviewed changes

silas-hw added 2 commits July 31, 2026 10:42

Move List Show instance to .Instances module

befbdf1

Move instances to .Instances modules for Nat and Integer

e762d27

MatthewDaggitt reviewed Aug 3, 2026

View reviewed changes

silas-hw added 2 commits August 14, 2026 12:10

Rename Show to Write

4c8232d

Introduce Pretty, Write, Read, and ReadWrite

c9d932a

silas-hw added 2 commits August 14, 2026 14:58

Fix IntWrite

a6496e1

Remove accidental indent in Data.List.Instances

fa521f3

gallais reviewed Aug 17, 2026

View reviewed changes

Fix typo

5986b9e

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

silas-hw added 4 commits August 17, 2026 13:16

Update Read interface

335dd51

Fix whitespace

892fd98

Add Maybe Pretty instance

fe50044

Add 'pretty' function to Pretty

b7823a0

Add NatPretty instance

2c7c8af

Uh oh!

Conversation

silas-hw commented Jul 30, 2026

Uh oh!

silas-hw commented Jul 30, 2026

Uh oh!

JacquesCarette left a comment

Choose a reason for hiding this comment

Uh oh!

JacquesCarette Jul 30, 2026

Choose a reason for hiding this comment

Uh oh!

silas-hw Jul 31, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

JacquesCarette commented Jul 30, 2026

Uh oh!

silas-hw commented Jul 31, 2026

Uh oh!

JacquesCarette commented Jul 31, 2026

Uh oh!

jamesmckinna commented Jul 31, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MatthewDaggitt left a comment

Choose a reason for hiding this comment

Uh oh!

MatthewDaggitt Aug 3, 2026

Choose a reason for hiding this comment

Uh oh!

silas-hw commented Aug 14, 2026

Uh oh!

gallais Aug 17, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

gallais Aug 17, 2026

Choose a reason for hiding this comment

Uh oh!

silas-hw Aug 17, 2026

Choose a reason for hiding this comment

Uh oh!

silas-hw Aug 17, 2026

Choose a reason for hiding this comment

Uh oh!

silas-hw commented Aug 17, 2026

Uh oh!

silas-hw commented Aug 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

jamesmckinna commented Jul 31, 2026 •

edited

Loading