[Haskell-cafe] Help understanding John Hughes' "The Design of a Pretty-printing Library"

[Galaxy Being]

Getting stuck in *Real World Haskell*'s chapter on pretty printing (chap
5), I decided to take a look at one of the suggested sources, i.e., John
Hughes' *The Design of a Pretty-printing Library
<https://www.researchgate.net/publication/226525714_The_Design_of_a_Pretty-printing_Library>*.
Not that I fully got the first three section, still, let me skip ahead to
section 4, *Designing a Sequence Type *where we're designing a supposedly
generic sequence type, I'm guessing in the same universal, fundamental way
that Peano's Axioms give a generic underpinning of the natural numbers.
Good. I get it. This is why Haskell is unique. So he says we take the
following *signature* as our starting point

nil :: Seq a
unit :: a -> Seq a
cat :: Seq a -> Seq a -> Seq a
list :: Seq a -> [a]

where nil , unit , and cat give us ways to build sequences, and list
is an *observation
*[explained before]. The correspondence with the usual list operations is

nil = []
unit x = [x]
cat = (++)

These operations are to satisfy the following laws:

xs `cat` ( ys `cat` zs ) = ( xs `cat` ys ) `cat` zs
nil `cat` xs = xs
xs `cat` nil = xs
list nil = []
list ( unit x `cat` xs ) = x : list xs

My first question is why must we satisfy these laws? Where did these laws
come from? Is this a universal truth thing? I've heard the word *monoid *and
*semigroup* tossed around. Is this germane here?

Next in *4.1 Term Representation* I'm immediately lost with the
concept of *term.
*On a hunch, I borrowed a book *Term Rewriting and All That *from Baader
and Nipkow which I'm sure goes very deep into the concept of terms, but I'm
not there yet. What is meant by *term*? As 4.1 continues, confusing is this
passage

The most direct way to represent values of [the?] sequence type is just as
terms of the
algebra [huh?], for example using

data Seq a = Nil j Unit a j Seq a `Cat` Seq a

But this trivial representation does not exploit the algebraic laws that we
know to
hold [huh?], and moreover the list observation will be a little tricky to
de ne (ideally we would like to implement observations by very simple,
non-recursive functions: the real work should be done in the
implementations of the Seq operators themselves). Instead, we may choose a
restricted subset of terms -- call them simplified forms -- into which
every term can be put using the algebraic laws. Then we can represent
sequences using a datatype that represents the syntax of simplified forms.

In this case, there is an obvious candidate for simplified forms: terms of
the form nil and unit x `cat` xs , where xs is also in simplified form.
Simplified forms can be represented using the type

data Seq a = Nil j a `UnitCat` Seq a

with the interpretation

Nil = nil
x `UnitCat` xs = unit x `cat` xs

All of this presupposes much math lore that I'm hereby asking someone on
this mailing list to point me towards. I threw in a few [huh?] as specific
points, but in general, I'm not there yet. Any explanations appreciated.


⨽
Lawrence Bottorff
Grand Marais, MN, USA
borgauf at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210709/40c13f6b/attachment.html>