Unfortunately, I don't have Paulson's book (or any other ML book :) at
home. I'm too lazy to figure out the specification from the source code,

I guess the code is too opaque, as my colleague claimed.

The layout the algorithm generates condensed indented blocks. Within a block, it inserts a newline when the distance to the next break point plus the current position is greater than the space remaining on the current line. Thus if S-Expression lists are rendered as blocks with indent two, and every element in a list is separated by a break point of length one, with the proper margin, you would see:

(defthingy name-of-thingy
(one thing) (two thing)
(a-big-thing-made-bigger)
(three thing) (four thing))

As an exercise, the book asks you to implement group indent, where if any break point in a group inserts a newline, they all do. So with that layout, one would get:

(defthingy
name-of-thingy
(one thing)
(two thing)
(a-big-thing-made-bigger)
(there thing)
(four thing))

The C version I wrote supports this layout, but I didn't bother with that extension for the Haskell version.

On the strictness annotations, my reasons for them are the usual ones, primarily to prevent memory leaks due to dragging, but a performance boost is always welcome. At some point, I plan to profile the code with and without the annotations, and find out where they are needed.

John