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

[Jeff Clites]

> On Jul 9, 2021, at 10:10 AM, Galaxy Being <borgauf at gmail.com> wrote:
> 
> 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. 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.

Sort of. But he explicitly says he’s not trying to define a new sequence type (more general than lists or something), but rather see if we could start from some requirements and from there deduce the list type. This is in the context of “deriving functional programs from specifications”, as an example case. I didn't read the whole paper so I'm not sure if this is directly relevant to designing a pretty printing library, or if it's just warm up. I suspect that the paper is more about deriving programs from specification than it is about pretty printing.

> Good. I get it. This is why Haskell is unique.

BTW this isn’t how everyone approaches writing Haskell programs on a day-to-day basis.

> 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?

These are just his requirements for how you’d expect a sequence to behave. (Concatenation is associative and appending an empty sequence does nothing, etc.)

> I've heard the word monoid and semigroup tossed around. Is this germane here?

The first three are the criteria for being a monoid, but that doesn’t explain anything because it doesn’t tell you why you’d want your sequence type to be a monoid. So it’s something to notice but it doesn’t explain the requirements. The requirements he just made up, from thinking about the concept of a sequence.

> 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?

Oh no it’s much simpler. “Term” is just the math/logic version of the concept “value”. In programming, you have types (like Int) and values (like 3). In logic-speak 3 is a term (to distinguish it from “3 + 5”, which is an expression or a formula). A term is a mathematical object.

> 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

He’s talking about how you’d map the logical concepts into Haskell--how you would "represent the terms as values" or how you would decide what Haskell value would faithfully represent the conceptual term. (Basically, “value of the type” is the Haskell side, and “terms of the algebra” is the math/logic side.)

> data Seq a = Nil | Unit a | Seq a `Cat` Seq a

The nil/unit/cat from above are functions for constructing a sequence, so you could take that literally and represent a sequence by just making each of those functions be constructors. That’s sort of the simplest thing you could do, so he’s trying that first.

So in this approach:

  nil = Nil
  unit x = Unit x
  cat x y = Cat x y

> But this trivial representation does not exploit the algebraic laws that we know to hold [huh?]

He’s just saying that doing it this simple way doesn’t satisfy the equalities we want above.

For instance:

  nil `cat` xs

results in:

  Cat Nil xs

which is not the same as xs (but rather, it's a new data structure with xs as part of it).

And then he goes on to build toward a different representation that satisfies the requirements.


I haven't looked at the Real World Haskell book in a while, but this paper is assuredly much more conceptual/abstract than the book, so you are probably getting help from something harder than where you started. It's interesting but keep in mind that research papers are often not simple to understand (and a book is at least trying to be).

I hope that helps a bit.

Jeff