Design of Show #569
Description
Standard library needs the Show class,
as in Haskell (only it is desirable a slightly better design, with ShowOptions).
Because show' for arbitrary ``A and B : Set _`` is easily lifted to show' for
A × B, List A, Maybe A, Fraction A, ...
Consider something like
lChar = List Char
pageWidth = 72 -- edit it
Verbosity : Set
Verbosity = ℕ -- Verbosity level in messages:
-- v < 1 is the least verbose, 1 is more verbose ...
data ParensOrNot : Set where Parens : ParensOrNot
ParensNot : ParensOrNot
record ShowOptions : Set where -- something of this sort
field
verbosity : Verbosity
listSeparator : LChar
fieldSeparator : LChar
parInShow : ParensOrNot
-- Options for printing to a string -- related to the Show class.
-- fieldSeparator is for data fields except List.
-- parInShow effects only the case of a data being a Tuple or a List;
-- is defines whether to unparenth the members of this data
-- print at the top level.
-- Examples: 1) a polynomial list is printed as "[x^2+1, x-1]",
-- under parInShow = ParensNot, and it is printed as
-- "[(x^2+1), (x-1)]" under Parens.
-- 2) A pair list is printed as "[(2,1),(1,2)]",
-- under Parens, and it is printed as "[2,1,1,2]"
-- under ParensNot.
record Show {α} (A : Set α) : Set α
where
constructor show′
field shows : ShowOptions → A → LChar → LChar
show : ShowOptions → A → LChar
show opt a = shows opt a []
showsn : ℕ → A → LChar → LChar
showsn n = shows (shOpt n)
shown : ℕ → A → LChar
shown verb = show $ shOpt verb
showS : ShowOptions → A → String
showS opt = Str.fromList ∘ show opt
shownS : ℕ → A → String
shownS verb = Str.fromList ∘ shown verb
showsList : ShowOptions → List A → LChar → LChar
showsList opt xs = id
See the Show instances in DoCon-A.
What people think of this?