Add type-signature in spectral/para to help type-inf
[nofib.git] / spectral / para / Main.lhs
1
2 %       A program by Oege de Moor and Jeremy Gibbons
3 %               Sept 99
4 %
5 %
6 %                     | lines | chars | size(KB) | time(s)  |
7 % ---------------------+-------+-------+----------+----------+
8 % Haskell ghc 4.01     |   183 |  4676 |      453 |     4.72 |
9 % Haskell hbc 0.9999.4 |   183 |  4676 |      196 |    10.34 |
10 % C++ g++ 2.90.27      |   416 |  6310 |        8 |     0.43 |
11
12 % As one of the authors of this paper, I'd like to echo Manuel's warning
13 % about quoting out of context. The paper is about Haskell as a tool in
14 % designing and presenting algorithms, not about performance. The Haskell
15 % program was written for clarity, to explain a fairly tricky algorithm. The
16 % figures are there to show that in spite of that clarity-first style, the
17 % program is still suitable for sizable experiments.
18
19 % The sources (both Haskell and C++) are on my home page at
20
21 % http://www.comlab.ox.ac.uk/oucl/users/oege.demoor/homepage.htm
22
23 %% created by ODM@15:00, August 5, 1995
24 %% modified by ODM@15:00, April 16, 1996
25 %% more modifications JG, 10/6/97, 13/6/97, 16/6/97, ..., 2/7/97
26 %% rearranged JG 14/7/98, 16/11/98, 3/12/98
27 %% minor changes, make suitable for compilation by ghc/hbc, new test results ODM, 3/2/99
28
29
30 \documentclass[12pt]{article}
31 \usepackage{a4}
32
33
34 \begin{document}
35
36 \newif\ifskipspaces
37 \def\marginnote#1{%
38   \ifvmode
39     \leavevmode
40     \skipspacestrue
41   \else
42     \skipspacesfalse
43   \fi
44   \domarginnote{#1}%
45   \ifskipspaces \ignorespaces \fi}
46 \iftrue
47   \def\domarginnote#1{\marginpar{\scriptsize\raggedright\hspace{0pt}#1}}
48 \else
49   \def\domarginnote#1{}
50 \fi
51
52 \makeatletter
53 % "code" environment is like verbatim, but with negative vertical space
54 % before and after (so the verbatim material can start and end with a blank
55 % line, which doesn't appear in the printed result).
56 \begingroup \catcode `|=0 \catcode `[= 1
57 \catcode`]=2 \catcode `\{=12 \catcode `\}=12
58 \catcode`\\=12 |gdef|@xcode#1\end{mcode}[#1|end[mcode]]
59 |endgroup
60 \def\mcode{\unskip \vspace{-\baselineskip}%
61           \@verbatim \frenchspacing\@vobeyspaces \@xcode}
62 \def\endmcode{\if@newlist \leavevmode\fi\endtrivlist\vspace{-\baselineskip}}
63 \makeatother
64
65 \def\implies{\Rightarrow}
66 \def\iff{\Leftrightarrow}
67
68
69 \title{Bridging the Algorithm Gap: \\
70   A Linear-time Functional Program \\ 
71   for Paragraph Formatting}
72 \author{
73   \small\begin{tabular}[t]{l}
74   {\large Oege de Moor}\\
75   Programming Research Group \\ 
76   Oxford University\\
77   % Wolfson Building \\ 
78   % Parks Road \\ 
79   % Oxford OX1 3QD, UK
80   \texttt{oege@comlab.ox.ac.uk}
81   \end{tabular}
82   \and
83   \small\begin{tabular}[t]{l}
84   {\large Jeremy Gibbons}\\
85   School of Computing \& Math.\ Sciences \\ 
86   Oxford Brookes University\\
87   % Gipsy Lane \\ 
88   % Headington \\ 
89   % Oxford OX3 0BP, UK
90   \texttt{jgibbons@brookes.ac.uk}
91   \end{tabular}
92 }
93 \date{\today}
94 \maketitle
95
96 \begin{abstract} \noindent
97 In the constructive programming community it is commonplace to see
98 formal developments of textbook algorithms. In the algorithm design
99 community, on the other hand, it may be well known that the textbook
100 solution to a problem is not the most efficient possible. However, in
101 presenting the more efficient solution, the algorithm designer will
102 usually omit some of the implementation details, thus creating an
103 \emph{algorithm gap} between the abstract algorithm and its concrete
104 implementation. This is in contrast to the formal development, which
105 usually proceeds all the way to the complete concrete implementation of the less
106 efficient solution.
107
108 We claim that the algorithm designer is forced to omit some of the
109 details by the relative expressive poverty of the Pascal-like
110 languages typically used to present the solution. The greater
111 expressiveness provided by a functional language would allow the whole story
112 to be told in a reasonable amount of space. In this paper we use a
113 functional language to present the development of a sophisticated algorithm
114 all the way to the final code. We hope to bridge
115 the algorithm gap between abstract and concrete implementations, 
116 and thereby facilitate communication between the two communities.
117 \end{abstract}
118
119 {\renewcommand{\thefootnote}{\fnsymbol{footnote}}
120 \footnotetext{This paper is a revision of
121 Technical Report CMS-TR-97-03 from the School
122 of Computing and Mathematical Sciences, Oxford Brookes University.
123 %It is currently being submitted for publication.
124 }}
125
126 \section{Introduction}
127
128 The paragraph formatting problem \cite{knuth81} is a favourite 
129 example for demonstrating the effectiveness of formal methods.
130 Two particularly convincing derivations can be found in \cite{bird86} and \cite{morgan94}.
131 The algorithms derived in these references are applications of dynamic 
132 programming, and their time complexity is 
133 $O(min(w n,n^2))$, where $w$ is the 
134 maximum number of words on a line, and $n$ is the number of words to 
135 be formatted.  
136
137 Among algorithm designers it is well-known that one can solve the 
138 paragraph problem in $O(n)$ time, independent of $w$ 
139 \cite{eppstein92b,galil89,hirschberg87a,hirschberg87b}. 
140 Typical presentations of these linear
141 algorithms do however ignore some details (for instance, that the white
142 space on the last line does not count), thus creating an \emph{algorithm
143 gap} between the abstract algorithm and its concrete implementation.
144 This contrasts with the formal developments cited above, which
145 present concrete code, albeit for a less efficient solution.
146
147 This paper is an experiment in bringing formal methods and algorithm
148 design closer together, through the medium of functional programming. 
149 It presents a linear-time algorithm for paragraph formatting in a semi-formal
150 style. The algorithm is given as executable code; in fact, the \LaTeX\ file
151 used to produce this paper is also an executable 
152 \emph{Haskell} program.
153 In writing this paper we
154 hope to convince the reader that 
155 a functional style can be suitable for communicating non-trivial 
156 algorithms, without sacrificing rigour or clarity or introducing an algorithm gap.
157
158 Of course, there exist algorithms that are difficult to express
159 functionally. In fact, it came as a surprise to us that the algorithm 
160 presented here can indeed be implemented without resorting to any 
161 imperative language features. One of us (OdM) first attempted to
162 explain the algorithm (which is very similar to that in \cite{galil89})
163 in 1992, and then implemented it in Modula-2; when 
164 that program was discussed at the Oxford \emph{Problem Solving Club}, it met with
165 a lot of disappointment because of the need for destructive updates.
166 Only recently we realised how the algorithm could be expressed functionally.
167 This paper is therefore also a contribution to the ongoing effort
168 of determining what can be done efficiently in a purely functional
169 style. 
170
171 \iffalse
172 \begin{mcode}
173
174 >module Main where
175
176 >import Data.Char
177 >import System.IO
178 >import System.Environment
179 >import Prelude hiding (Word)
180
181 \end{mcode}
182 \fi
183
184
185 \subsection{Preliminaries}
186
187 We do not assume that the reader is an expert in functional programming;
188 we explain the necessary syntax and standard functions of Haskell as we go. (Of
189 course, some familiarity with a modern lazy functional language
190 such as Haskell, Miranda\footnote{Miranda is a trademark
191 of Research Software Ltd.} or Hope would be helpful; 
192 but we trust that the notation is fairly self-evident.)
193 In addition to the
194 standard functions of Haskell, we use a number of other
195 primitives, which are explained in this section.
196
197 \begin{description}
198
199 \item[fold1:]
200 The function \texttt{fold1} is related to the standard function \texttt{foldr}, 
201 but it operates on non-empty lists. Informally, we have
202 \begin{eqnarray*}
203    \hbox to 0.5in{$\verb"fold1 step start [a0,a1,...,an]"$\hss} \\
204  &=& 
205    \verb"a0 `step` (a1 `step` (... `step` start an))"
206 \end{eqnarray*}
207 (Here, `\verb"[a0,a1,...,an]"' denotes a list, and
208 writing the binary function \texttt{f} inside backwards quotes, \verb"`f`",
209 allows it to be used as an infix operator.)
210 In words, \texttt{fold1} traverses a list from right to left, applying 
211 \texttt{start} to the last element, and `adding in' the next element at each 
212 stage using the function \texttt{step}.
213 The formal definition of \texttt{fold1} is
214 \begin{mcode}
215
216 >fold1 :: (a->b->b) -> (a->b) -> [a] -> b
217 >fold1 f g [a]   = g a
218 >fold1 f g (a:x) = f a (fold1 f g x)
219
220 \end{mcode}
221 (The first line is a \emph{type declaration}, stating that \verb"fold1" 
222 takes three arguments~--- a binary function of type \verb"a->b->b", 
223 a unary function of type \verb"a->b", and a list of type \verb"[a]"~---
224 and returns a value of type \verb"b".
225 The binary operator `\verb":"' is `cons', prepending an element onto a
226 list. The definition of \verb"fold1" is by \emph{pattern matching}:
227 the first equation that matches the argument applies.
228 Because neither equation matches the empty list, \verb"fold1" is undefined there.)
229
230 \item[scan1:]
231 The function \texttt{scan1} records all intermediate results of the
232 computation of \texttt{fold1} in a list:
233 \begin{mcode}
234
235 >scan1 :: (a->b->b) -> (a->b) -> [a] -> [b]
236 >scan1 f g = fold1 f' g'
237 >            where g' a   = [g a]
238 >                  f' a s = f a (head s) : s
239
240 \end{mcode}
241 (Here, the function \texttt{head} returns the first element of a non-empty
242 list.)
243 For example, the function \texttt{tails}, which returns all non-empty suffixes
244 of its argument, can be defined
245 \begin{mcode}
246
247 >tails :: [a] -> [[a]]
248 >tails = scan1 (:) (:[])
249
250 \end{mcode}
251 (The second argument \verb"(:[])" to \texttt{scan1} is the binary operator
252 `\texttt{:}' already supplied with its second argument, in this case the
253 empty list; the function \verb"(:[])" that results is the function
254 taking an element into a singleton list containing just that element.)
255
256 The relationship between \texttt{fold1} and \texttt{scan1} is succinctly
257 expressed in the so-called \emph{scan lemma}:
258 \begin{eqnarray*}
259  \verb"scan1 f g" &=& \verb"map (fold1 f g) . tails"
260 \end{eqnarray*}
261 (Here, the higher-order function \texttt{map} applies the function which is
262 its first argument to every element of the list which is its second
263 argument; the binary operator `\verb"."' is function composition.)
264 The scan lemma will be useful towards the end of this paper.
265
266 \item[single:]
267 The operator \texttt{single} tests whether its
268 argument is a singleton list:
269 \begin{mcode}
270
271 >single :: [a] -> Bool
272 >single [a] = True
273 >single _   = False
274
275 \end{mcode}
276 (The pattern `\verb"_"' matches any argument, thereby acting as a kind
277 of `else' clause.)
278 It is thus similar to the standard Haskell function \texttt{null},
279 which tests for emptiness.
280
281 \item[minWith:]
282 The function \texttt{minWith f} takes a list \texttt{x}
283 and returns an element of \texttt{x} whose \texttt{f}-value is minimal.
284 Formally, \texttt{minWith} can be defined in terms of \texttt{fold1}:
285 \begin{mcode}
286
287 >minWith :: (a->Int) -> [a] -> a
288 >minWith f = fold1 choice id
289 >            where choice a b | f a <  f b = a
290 >                             | otherwise  = b
291
292 \end{mcode}
293 (The expression `\verb"f a <= f b"' here is a \emph{guard}.
294 The first equation for \verb"choice" applies if the guard holds,
295 and the second equation applies if it does not.)
296
297 \end{description}
298
299 \section{Specifying the problem} \label{sec:spec}
300
301 In the paragraph problem, the aim is to lay out a given text 
302 as a paragraph in a visually pleasing way. A text is given 
303 as a list of words, each of which is a string, that is, a sequence of
304 characters: 
305 \begin{mcode}
306  
307 >type Txt = [Word] 
308 >type Word = String
309
310 \end{mcode}
311 A paragraph is a sequence of lines, each of which is a sequence of words: 
312 \begin{mcode}
313
314 >type Paragraph = [Line]
315 >type Line = [Word] 
316
317 \end{mcode}
318 The problem can be specified as
319 \begin{mcode}
320
321 >par0 :: Txt -> Paragraph
322 >par0 = minWith cost . filter feasible . formats
323
324 \end{mcode}
325 or informally, to compute the minimum-cost format among all 
326 feasible formats.
327 (The function \verb"filter p" takes a list \texttt{x} and returns exactly
328 those elements of \texttt{x} that satisfy the predicate \texttt{p}.)
329 In the remainder of this section we formalise the three components of
330 this specification. The result will be an executable program,
331 but one whose execution takes exponential time.
332
333
334 \subsection{Paragraph formats}
335
336 The function \texttt{formats} takes a text and returns all possible formats
337 as a list of paragraphs:
338 \begin{mcode}
339
340 >formats :: Txt -> [Paragraph]
341 >formats = fold1 next_word last_word
342 >          where last_word w = [ [[w]] ]
343 >                next_word w ps = map (new w) ps ++ map (glue w) ps 
344
345 >new w ls      = [w]:ls
346 >glue w (l:ls) = (w:l):ls
347
348 \end{mcode}
349 (Here, the binary operator \verb"++" is list concatenation.)
350 That is, for the last word alone there is just one possible format, and for
351 each remaining word we have the option either of putting it on a new line
352 at the beginning of an existing paragraph, or of gluing it onto the front of
353 the first line of an existing paragraph.
354
355
356 \subsection{Feasible paragraph formats}
357
358 A paragraph format is feasible if every line fits:
359 \begin{mcode}
360
361 >feasible :: Paragraph -> Bool
362 >feasible = all fits
363
364 \end{mcode}
365 (The predicate \verb"all p" holds of a list precisely 
366 when all elements of the list satisfy the predicate \texttt{p}.)
367
368 We define a global constant \texttt{maxw} for the maximum line width:
369 \begin{mcode}
370
371 >maxw :: Int
372 >maxw = 70
373
374 \end{mcode}
375 Of course, for flexibility many of the functions we develop should be
376 parameterized by \texttt{maxw}; however, a global constant makes the
377 presentation of the algorithm less cluttered. It is straightforward to
378 make \texttt{maxw} a parameter throughout.
379
380 A line \texttt{fits} if its width is at most the maximum line width:
381 \begin{mcode}
382
383 >fits :: Line -> Bool
384 >fits xs = (width xs <= maxw)
385
386 \end{mcode}
387 In formatting a text as a paragraph, the maximum line width should
388 never be exceeded. Our programs will halt with a run-time error
389 if an individual word exceeds the maximum line width; in practical
390 applications one would need to deal with such pathological inputs
391 more graciously.
392
393 The \texttt{width} of a line is defined to be its total length when the words
394 are printed next to each other, with one space character between each
395 consecutive pair of words:
396 \begin{mcode}
397
398 >width :: Line -> Int
399 >width = fold1 plus length
400 >        where plus w n = length w + 1 + n
401
402 \end{mcode} 
403 The function \texttt{length} returns the number of elements in a list.
404 This notion of width is appropriate for displaying paragraphs on a device
405 where every character has the same width.
406 The programs presented below can easily be modified to deal with
407 proportional spacing, where different characters may have different
408 widths.
409 In that case, however, one will need constant-time access arrays,
410 which are not available in all functional languages.
411
412
413 \subsection{The cost of a paragraph format}
414
415 In addition to the maximum line width \texttt{maxw}, the problem also
416 depends upon an optimum line width \texttt{optw}, another global constant:
417 \begin{mcode}
418
419 >optw :: Int
420 >optw = 63
421
422 \end{mcode}
423 The optimum line width should of course be
424 at most the maximum line width. 
425
426 A \emph{visually pleasing} paragraph is one in which the width of each
427 line in the paragraph is as close to the optimum line width
428 as possible. More precisely, we wish to minimise the total \emph{cost},
429 the sum of the squares of the deviations of the line widths from the
430 optimum line width: 
431 \begin{mcode}
432
433 >cost :: Paragraph -> Int
434 >cost = fold1 plus (const 0)
435 >       where plus l n = linc l + n
436 >             linc l = (optw - width l)^2
437
438 \end{mcode}
439 Note that the last line gets treated as a special case: it does not
440 count towards the total cost of the paragraph. This is achieved by the
441 function \texttt{const}, which satisfies the equation \verb"const a b = a" for
442 any \texttt{b}.
443
444
445 \section{The standard algorithm} \label{sec:standard}
446
447 The specification in Section~\ref{sec:spec} makes an inefficient program
448 because it maintains too many candidate solutions. It is a \emph{generate and
449 test} algorithm, of the form
450 \begin{verbatim}
451   best . filter ok . generate
452 \end{verbatim}
453 The standard technique for improving algorithms of this form is to \emph{promote}
454 the test \verb"filter ok" and the selection \verb"best" inside the
455 generator, so as to avoid generating unnecessary candidates.
456 Standard theory \cite{bird86,bird90,bird93d} tells us what properties of \verb"generate",
457 \verb"ok" and \verb"best" this requires. In our particular case it is
458 sufficient that
459 \texttt{new} is monotonic in its second argument:
460 \begin{eqnarray}
461    \verb"cost ls" \le \verb"cost ls'"
462    &\implies&
463    \verb"cost (new w ls)" \le \verb"cost (new w ls')"
464    \label{eqn:new-monotonic}
465 \end{eqnarray}
466 and furthermore, that \texttt{glue} is monotonic in its second argument in
467 a slightly
468 weaker sense~--- namely, for paragraphs with the same first line:
469 \begin{eqnarray}
470   \hbox to 0.5in{$\verb"cost (l:ls)" \le \verb"cost (l:ls')"$\hss} \nonumber\\
471   &\implies&
472   \verb"cost (glue w (l:ls))" \le \verb"cost (glue w (l:ls'))"
473   \label{eqn:glue-monotonic}
474 \end{eqnarray}
475 Note that neither of these two properties depends on the precise definition
476 of the cost of individual lines, as returned by the function \texttt{linc};
477 all that matters is that the total cost
478 is the sum of the costs of the individual lines.
479
480 Using the above two monotonicity properties, the standard theory alluded to above
481 concludes that the 
482 following dynamic programming algorithm is a valid solution 
483 to the specification \texttt{par0}. 
484 This is a well-rehearsed development, so we do
485 not repeat it here.
486 \begin{mcode}
487
488 >par1 
489 > = minWith cost . fold1 step start
490 >   where 
491 >     step w ps = filter fitH (new w (minWith cost ps):map (glue w) ps)
492 >     start w   = filter fitH [ [[w]] ]
493 >fitH = fits . head
494
495 \end{mcode}
496 Note that \texttt{par1} is not equal to \texttt{par0}; in particular, if there
497 is more than one optimal paragraph, \texttt{par0} and \texttt{par1} may return
498 different (but still optimal) paragraphs. To express this refinement
499 property formally we would have to generalize from functional
500 programming to relational programming~\cite{bdm96}, a step that is
501 beyond the scope of this paper.
502
503 For efficiency, we need to perform a \emph{tupling transformation} 
504 \cite{pettorossi84,chin90}
505 to avoid recomputing the width of the first line and the cost of the
506 remaining candidate solutions. We represent the paragraph \texttt{(l:ls)} 
507 by the triple 
508 \begin{verbatim}
509   (l:ls, width l, cost ls)
510 \end{verbatim}
511 (Because \texttt{ls} may be empty,
512 we stipulate also that \verb"cost [] = 0".)
513 The program resulting from this data refinement is as follows.
514 \begin{mcode}
515
516 >par1' :: [[a]] -> [[[a]]]
517 >par1'
518 > = the . minWith cost . fold1 step start
519 >   where 
520 >     step w ps = filter fitH (new w (minWith cost ps):map (glue w) ps)
521 >     start w   = filter fitH [([[w]], length w,0)]
522 >     new w ([l],n,0)   = ([w]:[l], length w, 0)
523 >     new w p           = ([w]:ls , length w, cost p) where (ls,n,m) = p
524 >     glue w (l:ls,n,m) = ((w:l):ls, length w + 1 + n, m)
525 >     the (ls,n,m)      = ls
526 >     width_hd (ls,n,m) = n
527 >     cost_tl (ls,n,m)  = m
528 >     linc_hd p         = (optw - width_hd p)^2
529 >     cost ([_],_,_)    = 0
530 >     cost p            = linc_hd p + cost_tl p
531 >     fitH p            = width_hd p <= maxw
532
533 \end{mcode}
534
535 \section{Improving the standard algorithm}
536
537 The algorithm at the end of Section~\ref{sec:standard}
538 is the standard dynamic programming solution to the paragraph
539 problem, and its time complexity is 
540 $O(min(w n, n^2))$ where $w$ is the maximum number of words on a line and
541 $n$ is the number of words in the paragraph.
542 Computational experiments confirm that this is an accurate estimate of
543 the program's behaviour.
544 This algorithm is the final product of the typical textbook
545 derivation. It does not make use of any special properties of
546 \texttt{linc}, the function that returns the cost on an individual line.
547 Indeed, if nothing more is known about \texttt{linc}, it is not possible
548 to improve upon this algorithm,
549 as noted in \cite{hirschberg87a}.  
550 However, as we shall show in Sections~\ref{sec:dominance}
551 to~\ref{sec:differencing}, for our particular choice 
552 of \texttt{linc}, namely
553 \begin{verbatim}
554  linc l = (optw - width l)^2
555 \end{verbatim}
556 substantial improvements are possible; in fact, we will
557 end up with a program linear in $n$ and independent of $w$.
558
559 In Section~\ref{sec:dominance} we determine a \emph{dominance criterion},
560 whereby some candidate solutions can be discarded because they are dominated
561 by other `better' solutions. Therefore, after processing each word of
562 the paragraph we may `trim' the collection of candidate solutions to
563 remove the dominated ones.
564
565 To obtain a linear-time solution we can afford to do at most an
566 amortized constant amount of work for each word in the paragraph.
567 Precisely one new candidate solution is added for each word, so it
568 suffices that the amount of work performed with each word is
569 proportional to the number of candidate solutions discarded.
570 The obvious implementation of the trimming operation introduced in
571 Section~\ref{sec:dominance} involves reconsidering every candidate
572 solution for each word in the paragraph. In Section~\ref{sec:forecasting}
573 we show that this is not necessary: trimming in fact results in removing
574 some candidate solutions from the beginning of the list and some others from
575 the end. Crucially, the solutions in the middle of the list need
576 not be considered; at the beginning and at the end of the list, as soon
577 as one undominated solution is found the trimming can stop.
578
579 That still leaves the \verb"filter" and the \verb"map" in the definition
580 of the function \verb"step", each of which traverses all candidate
581 solutions for each word of the paragraph. In Section~\ref{sec:filtering} we
582 replace the \verb"filter" with a function that performs work proportional
583 to the number of solutions discarded, independently of the number of
584 solutions retained.
585 In Section~\ref{sec:differencing} we eliminate the \verb"map (glue w)", by making a
586 change of representation under which \verb"glue w" is the identity
587 function. The resulting algorithm is linear in the paragraph length and
588 independent of the line width.
589
590
591 \section{Dominance criteria} \label{sec:dominance}
592
593 In this section we determine a \emph{dominance criterion} whereby some
594 paragraph formats can be discarded because they are dominated by another;
595 thus, fewer candidate solutions need be maintained at each step. 
596 Dominance criteria are the basis for most improvements over straightforward
597 dynamic programming. 
598 In our case, the
599 dominance criterion is a consequence of the fact that
600 the function \texttt{linc} is \emph{concave},
601 in the sense that
602 \marginnote{label more equations, and use in cross-refs}
603 \begin{eqnarray*}
604    \verb"linc (l++m) - linc l" &\le& \verb"linc (k++l++m) - linc (k++l)"
605 \end{eqnarray*}
606 Consequently, the monotonicity property of \texttt{glue} 
607 (Equation~\ref{eqn:glue-monotonic}) can be strengthened to:
608 \begin{eqnarray}
609    \hbox to 0.5in{$\verb"cost (l:ls)" \le \verb"cost ((l++m):ms)"$\hss} \nonumber\\
610    &\implies&
611    \verb"cost (glue w (l:ls))" \le \verb"cost (glue w ((l++m):ls))"
612    \label{eqn:glue-monotonic-stronger}
613 \end{eqnarray}
614 In words, the concavity property says that appending a line \verb"m" onto
615 a line \verb"l" has no worse an effect than appending \verb"m" onto a
616 longer line \verb"k++l", and the monotonicity property
617 says that if a paragraph with a shorter
618 first line is better than another paragraph, it will remain better
619 when more words are glued to the first lines of both paragraphs~---
620 a cheaper paragraph with a shorter first line dominates a costlier
621 paragraph with a longer first line.
622
623
624 \subsection{Exploiting concavity} \label{sec:concavity}
625
626 We can exploit the dominance criterion to arrive at an improved definition
627 of \texttt{step}. 
628 Note that \verb"step w" maintains the property `is in
629 strictly increasing order of length of first line' of the list of candidate 
630 solutions. Now suppose that we have two formats \texttt{p} and \texttt{q}, in that
631 order, in the list of candidate solutions; 
632 the first line of \texttt{q} is longer than the
633 first line of~\texttt{p}. Suppose also that $\verb"cost p" \le \verb"cost q"$. 
634 Then \verb"p" dominates \verb"q": 
635 by the monotonicity property of \texttt{new} (Equation~\ref{eqn:new-monotonic})
636 and the stronger property of \texttt{glue} (Equation~\ref{eqn:glue-monotonic-stronger}),
637 it follows that \texttt{q} may be safely discarded, because any
638 candidate solution generated from \texttt{q} will always be beaten by the
639 candidate solution generated in the same way from \texttt{p}. So we may
640 improve the definition of \texttt{step} to
641 \begin{verbatim}
642  step w ps = trim (filter fitH (new w (minWith cost ps):map (glue w) ps))
643 \end{verbatim}
644 where the function \texttt{trim} discards the dominated
645 candidate solutions (namely, the formats~\verb"q" for which there is a
646 format~\verb"p" appearing earlier in the collection with $\verb"cost p"
647 \le \verb"cost q"$):
648 \begin{verbatim}
649  trim []                             = [] 
650  trim [p]                            = [p]
651  trim (ps++[p,q]) | cost p <= cost q = trim (ps++[p])
652                   | otherwise        = trim (ps++[p]) ++ [q]
653 \end{verbatim}
654 This is not a valid definition in Haskell, because patterns
655 involving \verb"++" are not allowed. However, the pattern-matching is easily
656 re-expressed in terms of the standard functions \texttt{last} and
657 \texttt{init}, which return the last element and the remainder of a list,
658 respectively; we omit the details.
659 \iffalse
660 \begin{mcode}
661
662 >par2'
663 > = minWith cost . fold1 step start
664 >   where 
665 >     step w ps = trim (filter fitH (new w (minWith cost ps):map (glue w) ps))
666 >     start w   = filter fitH [ [[w]] ]
667 >     trim []   = []
668 >     trim [p]  = [p]
669 >     trim pspq 
670 >       | cost p <= cost q = trim psp
671 >       | otherwise        = trim psp ++ [q]
672 >       where q   = last pspq
673 >             psp = init pspq
674 >             p   = last psp
675 >             ps  = init psp
676
677 \end{mcode}
678 \fi
679
680 Note that we could trim from the back, as here, or from the front.
681 In Section~\ref{sec:forecasting} we will see that trimming from the back is
682 the better choice, because we will develop a criterion for stopping trimming early.
683
684 \subsection{Trimming introduces order} \label{sec:trim-order}
685
686 Now note further that the result of a \texttt{trim} is in strictly
687 decreasing order of cost, 
688 so the cheapest candidate solution is the last in the
689 list. We can therefore improve the definition of \texttt{step} further, by
690 using \verb"last" instead of \verb"minWith cost":
691 \begin{verbatim}
692  step w ps = trim (filter fitH (new w (last ps):map (glue w) ps))
693 \end{verbatim}
694 The resulting algorithm is an improvement over the standard solution,
695 but it is still not linear because at each step the whole list of
696 intermediate solutions is traversed.
697
698 \section{Forecasting the future} \label{sec:forecasting}
699
700 To remedy this inefficiency we will develop a criterion for stopping
701 trimming before having traversed the whole list of candidate
702 solutions. Observe that we maintain
703 a list of paragraph formats with strictly increasing
704 first line lengths, and strictly decreasing costs. 
705
706 Say that a candidate solution
707 element is \emph{bumped} by its predecessor when it is eliminated
708 in the computation of \texttt{trim}. Can we forecast how much gluing is needed
709 before a particular format \texttt{p} is bumped by its predecessor? If so, we
710 may be able to stop trimming early: if a word shorter than the length
711 forecasted for \texttt{p} has been glued, then \texttt{p} need not be considered
712 for trimming.
713
714 \subsection{The bump factor}
715
716 We introduce a function \verb"cg :: Paragraph -> Int -> Int" (for
717 `cost-glue') such that
718 \marginnote{wouldn't it be simpler with a \texttt{cg'} such that 
719 \texttt{cg'~p~n = cg~p~(n+1)}?}
720 \begin{verbatim}
721  cg p (length w + 1) = cost (glue w p)
722 \end{verbatim}
723 One suitable definition of \texttt{cg} is
724 \begin{verbatim}
725  cg [l] n    = 0
726  cg (l:ls) n = (optw - (n + width l))^2 + cost ls
727 \end{verbatim}
728 In words, \texttt{cg p n} is the total cost of the paragraph formed after a
729 sequence of words whose width is \texttt{n} has been glued to the first
730 line of paragraph \texttt{p}. Note that we do not check whether the maximum line
731 width is exceeded, and so the notion of cost may be meaningless
732 in terms of paragraphs. 
733 We allow negative values of \texttt{n} as
734 arguments of \verb|cg|. 
735
736 Using the function \texttt{cg}, we can forecast when a paragraph \texttt{p}
737 will bump a paragraph \texttt{q} in the process of
738 gluing more 
739 words to both paragraphs. Define 
740 the function \texttt{bf} (for `bump factor') by
741 \begin{verbatim}
742    bf p q
743  =  
744    setmin {n | cg p n <= cg q n}  `min` (maxw - width (head q) + 1)
745 \end{verbatim}
746 (This is not a Haskell definition ---~Haskell does not have sets, and
747 besides, the quantification is over a potentially infinite set~---
748 but it does completely determine \texttt{bf}.)
749 After gluing a width of \texttt{bf p q} to both \texttt{p} and \texttt{q},
750 paragraph \texttt{p} will be at least as good as \texttt{q}; furthermore, if we glue
751 more than \texttt{bf p q}, paragraph \texttt{p} will still be as good as \texttt{q}
752 (by concavity), so \texttt{q} can be discarded. The second term in
753 the definition of \verb|bf| reflects the fact that after gluing
754 \verb|maxw - width (head q) + 1|, paragraph \verb|p| is always better
755 than paragraph \verb|q|, because the first line of \verb|q| exceeds
756 the maximum line width. It can happen that \verb|bf| returns a negative
757 number, namely when \verb|p| is better than \verb|q| to start
758 with. 
759
760 \subsection{Using the bump factor} \label{sec:using-bump-factor}
761
762 Let us now formalise these observations as properties of
763 \texttt{glue}. Starting with \texttt{cg}, we have that
764 \begin{verbatim}
765  cg (glue w p) n = cg p (n + 1 + length w)
766 \end{verbatim}
767 Consequently, \texttt{bf} satisfies
768 \begin{verbatim}
769  bf (glue w p) (glue w q) = bf p q - (1 + length w)
770 \end{verbatim}
771 and therefore
772 \begin{eqnarray}
773   \hbox to 0.5in{$\verb"bf p q" \;<\; \verb"bf r s"$\hss}  \nonumber\\
774   &\iff&
775   \verb"bf (glue w p) (glue w q)" \;<\; \verb"bf (glue w r) (glue w s)"
776   \label{eqn:glue-respects-bf}
777 \end{eqnarray}
778 Finally, define the predicate \texttt{better} by
779 \marginnote{`$\mathtt{better\;w\;p\;q}$' is equivalent to `$\mathtt{1{+}\#w \ge
780 bf\,p\,q}$'}
781 \begin{verbatim}
782  better w p q  =  cost (glue w p) <= cost (glue w q) || 
783                   not (fitH (glue w q))
784 \end{verbatim}
785 (The binary operator \verb"||" is boolean disjunction; later on we use
786 \verb"&&", which is boolean conjunction.)
787 In words, \verb"better w p q" states that, after gluing a word \texttt{w},
788 paragraph \texttt{p} will be better than paragraph \texttt{q}, either on grounds
789 of cost or because the first line of \texttt{q} has become too long.
790 Suppose \verb|p = l0:ls0|, \verb|q = (l0++l1):ls1|, 
791 \verb|r = (l0++l1++l2):ls2|, and  $\verb"bf p q" \le \verb"bf q r"$.
792 We have the following property:
793 \begin{eqnarray*}
794   \verb"better w q r"
795   &\implies&
796   \verb"better w p q" \;\land\; \verb"better w p r"
797 \end{eqnarray*}
798 In words, this property says that whenever \verb|q| gets better than
799 \verb|r| by gluing a word \verb|w|, 
800 then \verb|p| is better than both \verb|q| and \verb|r| after
801 gluing the same word. 
802 It follows that \verb|q| can never be useful, and therefore, if we
803 had a triple like \verb|p|, \verb|q| and \verb|r| in the list of
804 candidate solutions, \verb|q| could be safely discarded. 
805
806 \subsection{Tight lists of solutions}
807
808 We shall exploit this observation by maintaining the list of candidate
809 solutions so that, as well as
810 \begin{enumerate}
811
812 \item \label{property:width}
813 the lengths of the first lines are in strictly increasing order, and
814
815 \item \label{property:cost}
816 the costs of the candidate solutions are in strictly decreasing order,
817
818 \end{enumerate}
819 as before, also
820 \begin{enumerate} \setcounter{enumi}{2}
821
822 \item \label{property:bf}
823 the \texttt{bf}-values of consecutive adjacent pairs of candidate solutions are
824 in strictly decreasing order.
825
826 \end{enumerate}
827 Such a list of candidate solutions
828 we call \emph{tight}.
829
830 To see how we can keep the list of candidate solutions tight,
831 recall the definition of \verb|step| from Section~\ref{sec:trim-order}:
832 \begin{verbatim}
833  step w ps = trim (filter fitH (new w (last ps):map (glue w) ps))
834 \end{verbatim}
835 We argued in Section~\ref{sec:concavity} that \verb"step w" maintains
836 properties~\ref{property:width} and~\ref{property:cost}. We now show how
837 the third property is maintained.
838
839 Notice that all three properties are preserved when taking a subsequence
840 of (that is, deleting some elements from) the list of candidate
841 solutions. For properties~\ref{property:width} and~\ref{property:cost}
842 this is obvious. For property~\ref{property:bf} it follows from the fact
843 that $\verb"bf p q" \ge \verb"bf p r" \ge \verb"bf q r"$, provided that
844 $\verb"bf p q" > \verb"bf q r"$ and \texttt{p}, \texttt{q} and \texttt{r} are in
845 strictly increasing order of length of first line; 
846 \marginnote{I have a marvellous demonstration that this margin is too
847 narrow to hold\ldots}
848 this fact is not too hard to establish.
849
850 Suppose that \verb|ps| satisfies property~\ref{property:bf}.
851 Because \verb|glue| respects the \verb|bf|
852 order (Equation~\ref{eqn:glue-respects-bf}), the list \verb|map (glue w) ps| also
853 satisfies property~\ref{property:bf}. 
854 It is however not necessarily the case that 
855 \verb"new w (last ps) : map (glue w) ps"
856 satisfies property~\ref{property:bf}:
857 the presence of the new element at the beginning may require some of the
858 initial elements of \verb|map (glue w) ps| to be removed. So, the cons operator
859 \verb|(:)| in the definition of \verb"step" is replaced by a \emph{smart constructor}
860 \verb|add|, 
861 which does the required pruning~--- 
862 by the argument at the end of Section~\ref{sec:using-bump-factor}, if we
863 have three consecutive candidate solutions \texttt{p}, \texttt{q} and \texttt{r}
864 with $\verb"bf p q" \le \verb"bf q r"$, solution \texttt{q} can be discarded.
865 \begin{verbatim}
866  add p []                             = [p]
867  add p [q]                            = [p,q]
868  add p ([q,r]++rs) | bf p q <= bf q r = add p ([r]++rs)
869                    | otherwise        = [p,q,r]++rs
870 \end{verbatim}
871 Now the list of candidate solutions \verb"new w (last ps) `add` map (glue w) ps"
872 satisfies property~\ref{property:bf}. 
873 Note that \verb"p `add` ps" is a subsequence of \verb"p:ps", so
874 properties~\ref{property:width} and~\ref{property:cost} are still
875 maintained; for the same reason, all three
876 properties are maintained
877 by the \verb"filter fitH" too.
878
879 Now, however, property~\ref{property:bf} permits an optimization of
880 \texttt{trim}, whereby we can stop trimming early. This was the reason for
881 introducing bump factors in the first place.
882 Suppose that \texttt{ps} satisfies property~\ref{property:bf}; we claim that
883 \verb"trim ps" can be written
884 \begin{verbatim}
885  trim []  = []
886  trim [p] = [p]
887  trim (ps++[p,q]) | cost p <= cost q = trim (ps++[p])
888                   | otherwise        = ps++[p,q]
889 \end{verbatim}
890 without a recursive call in the last clause.
891 Here is the justification.
892 Suppose that \texttt{r},~\texttt{s} are adjacent
893 candidate solutions in \texttt{ps}, and \texttt{p},~\texttt{q} are adjacent
894 candidate solutions in \texttt{ps}, and \texttt{r} is before \texttt{p} in the
895 list. Then $\verb"bf r s" > \verb"bf p q"$, by property~\ref{property:bf}.
896 Suppose also that $\verb"cost p" > \verb"cost q"$. Then the word \texttt{w} that
897 has just been processed was too short for \texttt{p} to bump \texttt{q}, and
898 so was also too short for \texttt{r} to bump \texttt{s} (because of the
899 \texttt{bf} ordering); that is, $\verb"cost r" > \verb"cost s"$ too, and
900 the initial segment of the list of candidate solutions ending
901 with solution \texttt{q} already satisfies property~\ref{property:cost}.
902 Thus, we have
903 \verb"trim (ps++[p,q]) = ps++[p,q]"~--- the second recursive call to
904 \texttt{trim} can be omitted 
905 when \verb"ps++[p,q]" satisfies property~\ref{property:bf} and
906 $\verb"cost p" > \verb"cost q"$.
907
908 Because we are now manipulating the list of candidate solutions at both ends, 
909 it will be profitable
910 to use a symmetric set of list operations, where \texttt{head} and \texttt{last}
911 are equally efficient. Such an implementation of lists is
912 summarized in an appendix to this paper. Below, whenever we use symmetric
913 lists, the familiar list operations are written using a dash~---
914 \texttt{head'}, \texttt{init'}, and so on~--- and the type of symmetric lists over
915 \texttt{a} is written \verb"SymList a".
916
917 In outline, the program now is
918 \begin{verbatim}
919  par2 = last . fold1 step start
920  step w ps = trim (filter fitH (new w (last ps) `add` map (glue w) ps))
921 \end{verbatim}
922 \iffalse
923 \begin{mcode}
924
925 >par2
926 > = last . fold1 step start
927 >   where 
928 >     step w ps = trim(filter fitH (new w (last ps) `add` map (glue w) ps))
929 >     start w   = filter fitH [ [[w]] ]
930 >     add p []                          = [p]
931 >     add p [q]                         = [p,q]
932 >     add p (q:r:rs) | bf p q <= bf q r = add p (r:rs)
933 >                    | otherwise        = p:q:r:rs
934 >     bf p q
935 >       | single q && cost pt == 0 
936 >                   = (optw - wph) `min` rqh
937 >       | single q  = rqh
938 >       | otherwise = ceildiv (cost p - cost q) (2*(wqh-wph)) `min` rqh
939 >         where ph:pt = p
940 >               qh:qt = q
941 >               wph   = width ph
942 >               wqh   = width qh
943 >               rqh   = maxw - wqh + 1
944 >               ceildiv n m = (n+m-1) `div` m
945 >     trim []                      = []
946 >     trim [p]                     = [p]
947 >     trim pspq | cost p <= cost q = trim psp
948 >               | otherwise        = pspq
949 >       where q   = last pspq
950 >             psp = init pspq
951 >             p   = last psp
952 >             ps  = init psp
953
954 \end{mcode}
955 \fi
956 (Note that we have made use again of the fact that a tight list of
957 paragraphs is in strictly decreasing order of cost, replacing the
958 \verb"minWith cost" in \verb"par2" by \verb"last".)
959 This new  program is in fact quite efficient:
960 computational experiments 
961 show that at each step of the computation, only a very small 
962 number of candidate solutions
963 are kept. Still, all candidate solutions get inspected each time \texttt{step}
964 is evaluated, and this remains a source of inefficiency.
965 To make progress, we shall have to remove the subexpressions
966 \texttt{filter fitH} and \texttt{map (glue w)} from the definition of \texttt{step};
967 we do this in Sections~\ref{sec:filtering} and~\ref{sec:differencing}.
968
969 \subsection{Computing the bump factor}
970
971 One point that we have not touched upon is how \texttt{bf} can be efficiently
972 implemented. This is an exercise in high-school algebra. 
973 Note that, when \texttt{p} and \texttt{q} appear in that order in the list of
974 candidate solutions, \texttt{p} cannot be a singleton: 
975 there is just one
976 way of formatting a paragraph into a single line, and if that line fits
977 it will be the last candidate solution because it has the longest first line.
978 Therefore there are just two cases to consider in computing \verb"bf p q": 
979 when \texttt{q} is a singleton, and when \texttt{q} is not.
980 Recall the definition of \verb"bf":
981 \begin{eqnarray*}
982   \hbox to 2em{\rlap{\texttt{bf p q}}} \\
983   &=&
984   \verb"setmin {n | cg p n <= cg q n} `min` (maxw - width (head q) + 1)"
985 \end{eqnarray*}
986 Note that the second term 
987 $\verb"rqh" = \verb"maxw - width (head q) + 1"$ is always greater than zero.
988 \begin{description}
989
990 \item[Case \texttt{q} is a singleton:]
991 so \verb"cg q n" is zero for any \texttt{n}. Thus, the only value of \texttt{n} for
992 which $\verb"cg p n" \le \verb"cg q n"$ would be one for which 
993 \verb"cg p n" is zero; this can only happen when
994 $\verb"n" = \verb"optw - width (head p)"$ and $\verb"cost (tail p)" = \verb"0"$.
995 This case therefore splits into two subcases: 
996 if \verb"cost (tail p)" is zero, then \verb"bf p q" is the smaller of
997 \texttt{rqh} and \verb"optw - width (head p)";
998 otherwise, there are no suitable values of \texttt{n}, and \verb"bf p q" is
999 simply \texttt{rqh}.
1000
1001 \item[Case \texttt{q} is not a singleton:]
1002 Note that, for non-singleton \texttt{p},
1003 \begin{eqnarray*}
1004   \verb"cg p n"  &=&  \verb"cost p + n^2 - 2*n*(optw - width (head p))"
1005 \end{eqnarray*}
1006 and so $\verb"cg p n" \le \verb"cg q n"$ precisely when
1007 \begin{eqnarray*}
1008   \texttt{n} &\ge& \verb"(cost p-cost q)/(2*(width (head q)-width (head p)))"
1009 \end{eqnarray*}
1010 (the divisor is non-zero, because of the ordering on lengths
1011 of first lines).
1012 Therefore, the first term in \verb"bf p q" is the ceiling of the fraction
1013 on the right-hand side of this inequation, and \verb"bf p q" itself is
1014 the smaller of this first term and \texttt{rqh}.
1015
1016 \end{description}
1017 Thus, we can implement \texttt{bf} as follows:
1018 \begin{verbatim}
1019  bf p q 
1020    | single q && cost pt == 0 = (optw - wph) `min` rqh
1021    | single q                 = rqh
1022    | otherwise                = ceildiv (cost p - cost q) 
1023                                         (2*(wqh - wph)) `min` rqh
1024       where
1025         ph:pt = p
1026         qh:qt = q
1027         wph   = width ph
1028         wqh   = width qh
1029         rqh   = maxw - wqh + 1
1030 \end{verbatim}
1031 where \verb"ceildiv x y" rounds the fraction \verb"x/y" up to the next integer.
1032
1033 \section{Filtering} \label{sec:filtering}
1034
1035 Because the list of candidate paragraphs is kept in increasing order of
1036 length of the first line, the \texttt{filter} is easily dealt with. The net
1037 effect of filtering is that the last few formats (namely, those with the
1038 longest first lines) are discarded, and the remainder are
1039 retained. Therefore, instead of \verb"filter fitH" we can use 
1040 \verb"droptail (not . fitH)", where
1041 \begin{verbatim}
1042  droptail :: (a->Bool) -> [a] -> [a]
1043  droptail p []                    = []
1044  droptail p (xs++[x]) | p x       = droptail p xs
1045                       | otherwise = xs ++ [x]
1046 \end{verbatim}
1047 Informally, \verb"droptail p x" discards elements from the end of the
1048 list~\verb"x", stopping when the list is empty or the last element does not
1049 satisfy predicate~\verb"p".
1050 \iffalse
1051 \begin{mcode}
1052
1053 >par2''
1054 > = last . fold1 step start
1055 >   where
1056 >     step w ps = trim(droptail (not.fitH) (new w (last ps) `add` map (glue w) ps))
1057 >     start w   = droptail (not.fitH) [ [[w]] ]
1058 >     droptail p []              = []
1059 >     droptail p xsx | p x       = droptail p xs
1060 >                    | otherwise = xsx
1061 >       where x  = last xsx
1062 >             xs = init xsx
1063 >     add p []                          = [p]
1064 >     add p [q]                         = [p,q]
1065 >     add p (q:r:rs) | bf p q <= bf q r = add p (r:rs)
1066 >                    | otherwise        = p:q:r:rs
1067 >     bf p q
1068 >       | single q && cost pt == 0 
1069 >                   = (optw - wph) `min` rqh
1070 >       | single q  = rqh
1071 >       | otherwise = ceildiv (cost p - cost q) (2*(wqh-wph)) `min` rqh
1072 >         where ph:pt = p
1073 >               qh:qt = q
1074 >               wph   = width ph
1075 >               wqh   = width qh
1076 >               rqh   = maxw - wqh + 1
1077 >               ceildiv n m = (n+m-1) `div` m
1078 >     trim []                      = []
1079 >     trim [p]                     = [p]
1080 >     trim pspq | cost p <= cost q = trim psp
1081 >               | otherwise        = pspq
1082 >       where q   = last pspq
1083 >             psp = init pspq
1084 >             p   = last psp
1085 >             ps  = init psp
1086
1087 \end{mcode}
1088 \fi
1089
1090 \section{Differencing} \label{sec:differencing}
1091
1092 In this section we will get rid of the \verb"map" from the
1093 definition of \verb"step", by making a change of representation under
1094 which \verb"glue w" is the identity function. 
1095 If we assume that the list
1096 operations \verb"head", \verb"tail", \verb"init" and \verb"last" take
1097 amortized constant time, then this gives an amortized linear-time
1098 algorithm for paragraph formatting. Every word of the paragraph
1099 contributes at most one new candidate solution, and the amount of work
1100 performed (by \verb"add" and \verb"trimf") on the list of
1101 candidate solutions is proportional to the number of candidate solutions
1102 discarded.
1103
1104 \subsection{A data refinement}
1105
1106 Elimination of \texttt{glue} can be achieved by computing only the tail
1107 of each paragraph. As long as we have the original text available
1108 (which is the concatenation of the paragraph), 
1109 all necessary quantities can be computed in terms of the tail alone:
1110 \begin{verbatim}
1111  length (head p) = length (concat p) - length (concat (tail p))
1112  width (head p)
1113    | single p    = width (concat p)
1114    | otherwise   = width (concat p) - width (concat (tail p)) - 1
1115  cost p
1116    | single p    = 0
1117    | otherwise   = (optw - width (head p))^2 + cost (tail p)
1118 \end{verbatim}
1119 (Recall that we stipulated that \texttt{cost [] = 0}.)
1120 The exploitation of this type of equation is known as \emph{differencing}.
1121 We shall represent a
1122 paragraph \texttt{p} by the triple \verb"rep p" where
1123 \begin{verbatim}
1124   rep p = ((width.concat.tail) p, (cost.tail) p, (length.concat.tail) p)
1125 \end{verbatim}
1126 It will be useful to have a type synonym
1127 for the new representation of paragraphs:
1128 \begin{mcode}
1129
1130 >type Par    = (Width,Cost,Length) 
1131 >type Width  = Int
1132 >type Cost   = Int
1133 >type Length = Int
1134
1135 >width_tl = fst3
1136 >cost_tl  = snd3
1137 >len_tl   = thd3
1138
1139 \end{mcode}
1140 Here, the functions \texttt{fst3}, \texttt{snd3} and \texttt{thd3} return the first,
1141 second and third components of a triple, respectively.
1142 \begin{mcode}
1143
1144 >fst3 (a,b,c) = a
1145 >snd3 (a,b,c) = b
1146 >thd3 (a,b,c) = c
1147
1148 \end{mcode}
1149 On this representation, the function \texttt{glue w} is the identity function,
1150 as required. 
1151
1152 \subsection{The overall structure}
1153
1154 Before we go into the details of the implementation of other
1155 operators on paragraphs, we outline the structure of the final
1156 program.
1157
1158 The program presented below is based on the fact that
1159 a solution to \texttt{par0} is returned by \texttt{par3}, where
1160 \begin{verbatim}
1161  par3 :: Txt -> Paragraph
1162  par3 ws 
1163    = tile ws (map (length.concat.tail.par0) (tails ws), length ws)
1164 \end{verbatim}
1165 The function \texttt{tile xs} produces the required solution by
1166 exploiting the differencing equation for \verb"length . head":
1167 \begin{mcode}
1168
1169 >tile :: Txt -> ([Length],Length) -> Paragraph
1170 >tile ws ([],n)   = []
1171 >tile ws (m:ms,n) = ws1 : tile ws2 (drop l (m:ms),m)
1172 >                   where l = n - m
1173 >                         (ws1,ws2) = splitAt l ws
1174
1175 \end{mcode}
1176 (Here, 
1177 \verb"splitAt l x" is a pair of lists, the first element of
1178 the pair being the first \texttt{l} elements of \texttt{x} and the second element
1179 being the remainder;
1180 \verb"drop l x" is the second component of \verb"splitAt l x".)
1181 The proof that this works is an induction over all tails of the argument,
1182 and a detailed exposition can be found in \cite{bird93d}. It is perhaps
1183 interesting to note that a program involving \texttt{tile} 
1184 is the starting point
1185 for the paper by Hirschberg and Larmore \cite{hirschberg87a}; 
1186 for us, it is part of a
1187 final optimisation.
1188
1189 Adapting the algorithm developed in previous sections to the new
1190 representation of paragraphs, one
1191 can find functions 
1192 \texttt{stepr} and \texttt{startr} ---~data refinements of 
1193 \texttt{step} and \texttt{start}~--- such that
1194 \begin{verbatim}
1195    fold1 stepr startr (map length ws)
1196  =
1197    (map rep (fold1 step start ws), width ws, length ws)
1198 \end{verbatim}
1199 and so, by the scan lemma of the introductory section,
1200 which showed how the computation of \verb|fold1 f g| on all tails
1201 can be written in terms of \verb|scan1|,
1202 \begin{verbatim}
1203    scan1 stepr startr (map length ws)
1204  =
1205    zip3 (map (map rep . fold1 step start) (tails ws), 
1206          map width (tails ws), 
1207          map length (tails ws))
1208 \end{verbatim}
1209 (The function \texttt{zip3} `zips' in the obvious way a triple of lists, all of the
1210 same length, into a list of triples.)
1211
1212 Let \verb"zs = scan1 stepr startr (map length ws)". Then
1213 \begin{verbatim}
1214    length ws = thd3 (head zs)
1215 \end{verbatim}
1216 and
1217 \begin{verbatim}
1218    map (length . concat . tail . par0) (tails ws)
1219  =   { rep }
1220    map (len_tl . rep . par0) (tails ws)
1221  =   { par0 = last . fold1 step start }
1222    map (len_tl . last . map rep . fold1 step start) (tails ws)
1223  =   { above }
1224    map (len_tl . last . fst3) zs
1225 \end{verbatim}   
1226 The resulting program is below.
1227 (Recall that the dashed list operations are the operations on symmetric
1228 lists, defined in the appendix.)
1229 \begin{mcode}
1230
1231 >par3 :: Txt -> Paragraph 
1232 >par3 ws
1233 > = tile ws (map (len_tl.last'.fst3) zs, thd3 (head zs))
1234 >   where zs = scan1 stepr startr (map length ws)
1235
1236 \end{mcode}
1237
1238
1239
1240
1241 \subsection{Implementing the data refinement}
1242
1243 It remains to give appropriate definitions of \texttt{stepr} and \texttt{startr}.
1244 The definition of \texttt{startr} is 
1245 \begin{mcode}
1246
1247 >startr :: Length -> (SymList Par, Width, Length)
1248 >startr a | a <= maxw = (cons' (0,0,0) nil',a,1)
1249
1250 \end{mcode}
1251
1252 The definition of \texttt{stepr} mirrors that in the preceding section,
1253 except that all operations on paragraphs have been data-refined  
1254 to the new representation of paragraphs.
1255 Those modifications are justified by
1256 the differencing equations stated above,
1257 and the following definitions are 
1258 immediate consequences of those identities:
1259 \begin{mcode}
1260
1261 >stepr :: Length -> 
1262 >        (SymList Par, Cost, Length) -> 
1263 >        (SymList Par, Cost, Length)
1264 >stepr w (ps,tw,tl)  
1265 > = (trim (drop_nofit (new (last' ps) `add` ps)), tot_width, tot_len)
1266 >   where 
1267 >     single p      = len_tl p == 0
1268 >     cost p 
1269 >       | single p  = 0
1270 >       | otherwise = cost_tl p + (optw - width_hd p)^2
1271 >     width_hd p
1272 >       | single p  = tot_width
1273 >       | otherwise = tot_width - width_tl p - 1
1274 >     tot_width     = w + 1 + tw
1275 >     tot_len       = 1 + tl
1276
1277 \end{mcode}
1278 The operator \texttt{new} adds a new line to the front of a paragraph.
1279 It is important that, in computing the cost of the tail of the 
1280 newly created paragraph, we use the old width of the head, that is,
1281 without taking the new word \texttt{w} into account:
1282 \begin{mcode}
1283
1284 >     new p | single p  = (tw,0,tl)
1285 >           | otherwise = (tw,cost_tl p + (optw-old_width_hd p)^2,tl)
1286 >     old_width_hd p | single p  = tw
1287 >                    | otherwise = tw - width_tl p - 1
1288
1289 \end{mcode}
1290 The definition of \texttt{trim} is not changed at all:
1291 \begin{mcode}
1292
1293 >     trim ps_pq | null' ps_pq      = ps_pq
1294 >                | single' ps_pq    = ps_pq
1295 >                | cost p <= cost q = trim ps_p
1296 >                | otherwise        = ps_pq
1297 >                  where ps_p = init' ps_pq
1298 >                        q    = last' ps_pq
1299 >                        p    = last' ps_p
1300
1301 \end{mcode}
1302 whereas \verb"drop_nofit" is an implementation of 
1303 \verb"droptail (not . fitH)", using the new implementation \verb"width_hd"
1304 of \verb"width . head". 
1305 \begin{mcode}
1306
1307 >     drop_nofit ps_p | null' ps_p        = ps_p
1308 >                     | width_hd p > maxw = drop_nofit ps
1309 >                     | otherwise         = ps_p
1310 >                       where ps = init' ps_p
1311 >                             p  = last' ps_p
1312
1313 \end{mcode}
1314 The definition of \texttt{add} is similarly unaffected.
1315 On an intuitive level, there seems to be a duality between
1316 the ways \texttt{trimf} and \texttt{add} operate, but we have been unable
1317 to bring this out in the code, 
1318 partly because \texttt{trimf} also performs
1319 the filtering operation.
1320 \marginnote{also because \texttt{add} compares \texttt{f p} with \texttt{f q},
1321 whereas \texttt{trim} compares \texttt{f p q} with \texttt{f q r}}
1322 \begin{mcode}
1323
1324 >     add p qr_rs | single' qr_rs || null' qr_rs = cons' p qr_rs
1325 >                 | bf p q <= bf q r             = add p r_rs
1326 >                 | otherwise                    = cons' p qr_rs
1327 >                   where r_rs = tail' qr_rs
1328 >                         q  = head' qr_rs
1329 >                         r  = head' r_rs
1330
1331 \end{mcode}
1332 Finally, the data-refined version of \texttt{bf} becomes
1333 \begin{mcode}
1334
1335 >     bf p q 
1336 >       | single q && cost_tl p == 0 = (optw - wph) `min` rqh 
1337 >       | single q                   = rqh
1338 >       | otherwise                  = ceildiv (cost p-cost q) 
1339 >                                              (2*(wqh-wph)) `min` rqh
1340 >          where
1341 >            wph = width_hd p
1342 >            wqh = width_hd q
1343 >            rqh = maxw - wqh + 1
1344
1345 >ceildiv n m = (n+m-1) `div` m
1346
1347 \end{mcode}
1348
1349 It is not hard to check that program \texttt{par3} does indeed
1350 have (amortised) linear time complexity. This theoretical bound
1351 is confirmed in computational experiments, and for all but the
1352 smallest inputs, \texttt{par3} outperforms the standard algorithm
1353 \texttt{par1}.
1354
1355 \section{Haskell vs C++}
1356
1357 We now have the ingredients for writing a program that has the
1358 same functionality as the Unix utility \emph{fmt},
1359 although its output will be far superior (\emph{fmt}
1360 uses a naive greedy strategy, and the resulting
1361 paragraphs are \emph{not} visually pleasing). 
1362 We shall make use of the functions 
1363 \begin{verbatim}
1364  parse :: String -> [Paragraph]
1365  unparse :: [Paragraph] -> String
1366 \end{verbatim}
1367 which are well-known text-processing primitives in
1368 functional programming \cite{bird88}. Their
1369 definitions are included in an appendix to this paper.
1370 Using these primitives, our implementation of \texttt{fmt}
1371 takes a single line:  
1372 \begin{mcode} 
1373
1374 >fmt = unparse . map (par3 . concat) . parse
1375
1376 \end{mcode}
1377 \iffalse
1378 \begin{mcode}
1379
1380 >fmtWith par = unparse . map (par . concat) . parse
1381
1382 \end{mcode}
1383 \fi
1384 Joe Programmer 
1385 may not be happy about this implementation of a high-quality \texttt{fmt}.
1386 Although there is
1387 no algorithm gap, one might expect a \emph{performance gap} between
1388 the Haskell program and an implementation of the same algorithm
1389 in a more conventional language.
1390 To measure the performance gap we compared the
1391 Haskell program for \texttt{fmt} to a hand-coded C++
1392 implementation that is in close correspondence to the program
1393 presented here. 
1394 The conventional program in C++ does make extensive use
1395 of destructive updates, however, 
1396 and the implementation of symmetric lists is replaced by an array implementation.
1397 Because the program only makes use of {\em cons} (and not of {\em snoc}), we can
1398 implement it by declaring an array whose size is an upperbound on the number of
1399 words in a paragraph, with two pointers that indicate the beginning and end of
1400 the symmetric list. (If we also had a {\em snoc} operation, we would need to
1401 use the folklore circular array code for queues.) All data structures in the conventional
1402 program are therefore of fixed size. Appropriate size bounds were determined
1403 by experimentation.
1404 The conventional program is of course longer than 
1405 the Haskell program, but this is mostly due to the unwieldy syntax,
1406 as the difference is only a factor of one third. Personally we
1407 found the 
1408 conventional code much harder to write because it uses a lot of indexing
1409 in arrays, as opposed to the standard list processing functions in 
1410 Haskell. 
1411
1412 In writing the C++ code, we attempted to apply all the standard tricks that good C++ programmers
1413 employ to speed up their programs. For example, index calculations were avoided through use
1414 of pointers, and we provided ample hints to the compiler through {\em const} 
1415 declarations and {\em inline} directives. To check that we did indeed conform to
1416 good practice in writing the C++ program, we compared its performance to that of
1417 the \verb|fmt| utility: our code for the sophisticated algorithm is only 18% 
1418 slower than \verb|fmt|. 
1419 By contrast, the Haskell program in this paper
1420 has {\em not} been fine-tuned for performance at all, and we directly compiled the
1421 \LaTeX source of this paper.
1422 It follows that the performance measurements reported give an edge to C++. 
1423
1424 All three programs were compiled on a Pentium II processor, running RedHat Linux.
1425 For Haskell we used version 4.01 of the Glasgow compiler \texttt{ghc}, 
1426 because it
1427 produces the best code of all Haskell compilers available. 
1428 The same code was also compiled with \texttt{hbc}, which also has a good
1429 reputation for speed and reliability. 
1430 For C++ we used the Gnu compiler.
1431 All three executables were reduced in size using the utility \texttt{strip}.
1432 The Haskell executables are, as expected, vastly larger than the
1433 C++ code ---~they differ by about a factor of 25.
1434 In all cases we switched on all optimizers. This has a spectacular
1435 effect for the \texttt{ghc} program: it ran more than four times faster
1436 than without the optimisation switch. Indeed, this is were we claw back some
1437 of the gains obtained by hand-coded optimisations in the C++ code: the \texttt{ghc}
1438 compiler aggressively applies optimising program transformations \cite{peyton-jones98}. 
1439
1440
1441 To compare the performance of the two executables, we 
1442 formatted the full text of Thomas Hardy's
1443 \emph{Far from the madding crowd}, an ASCII file of approximately
1444 780Kb \cite{gutenberg}. The three programs were run to format this file 
1445 for a maximum line width of 70 characters and an optimum width of 63.
1446 The CPU time was measured
1447 using the \texttt{time} command provided by the Linux \texttt{bash} shell. 
1448 The \texttt{ghc} executable is about twice as fast as the \texttt{hbc} program,
1449  which is shows how much can be achieved by automatic transformation of
1450 Haskell programs. The C++ program is eleven times faster
1451 again, which reflects the effort put into the respective compilers, and
1452 the fact that we did not bother to fine-tune the Haskell code.
1453
1454 The table below summarises the above comparison: the first two columns
1455 compare
1456 the programs with respect to their textual length (lines and characters),
1457 the third column is the
1458 size of the executable (in Kbytes), and the last column shows 
1459 their execution time (in CPU seconds).
1460 \begin{center}
1461 \begin{tabular}{l|rrrrr}
1462                  & lines & chars & size (Kb) & time (s) \\\hline
1463 Haskell (hbc)    &   183 &  4676 &    196~~~ &  10.34~~~ \\
1464 Haskell (ghc)    &   183 &  4676 &    453~~~ &  4.72~~~  \\
1465 C++              &   416 &  6310 &      8~~~ &  0.43~~~~ \\\hline
1466 Haskell (hbc)/(ghc) &  1.00 &  1.00 &   2.31~~~ &   2.19~~~  \\
1467 Haskell (ghc)/C++   &  0.44 &  0.74 &   24.50~~~ &  11.27~~~
1468 \end{tabular}
1469 \end{center}
1470 In summary, the performance gap is not all that great;
1471 it furthermore seems likely that advances in compiler technology
1472 (illustrated by the difference between \texttt{hbc} and \texttt{ghc})
1473 will cancel the remaining advantages of languages like 
1474 C++ over Haskell in the next few years. 
1475
1476 \section{Discussion}
1477
1478 This paper was an experiment in using a functional
1479 language for presenting a non-trivial algorithm in a semi-formal
1480 style. We personally believe that for a large class of problems,
1481 this style of presentation is adequate, at once closing the
1482 algorithm gap and reconciling algorithm design with formal methods.
1483 The comparison with the hand-coded conventional implementations indicates that
1484 for non-trivial algorithms like the one presented here, the performance 
1485 gap is rather small too.
1486 There are, however, two unsatisfactory aspects of the material
1487 presented here:
1488
1489 \begin{itemize}
1490 \item First, we are not entirely satisfied with the semi-formal style of
1491 this paper. Up to the introduction of \texttt{trim}, 
1492 the program derivation is absolutely
1493 standard, and no invention is involved in 
1494 synthesizing the program. That part of the paper could easily be
1495 cast in calculational form, given the right machinery.
1496 The invention of the `bump factor', and its role
1497 in `forecasting the future', is however rather \emph{ad hoc}, and
1498 escapes, at present, an elegant calculational treatment. This is
1499 unsatisfactory, especially since
1500 the technique seems more generally applicable.
1501
1502 \item Second, we are very dissatisfied with the way one has to program 
1503 differencing in
1504 a functional language.
1505 In a sense this is the least interesting part of the programming process,
1506 and yet it is quite error-prone. Moreover, differencing destroys some of the
1507 delightful elegance that characterises the functional expression of
1508 the standard algorithm. Meta-programming features in the spirit of 
1509 Paige's \texttt{invariant} construct \cite{paige86} 
1510 such as those espoused by Smith~\cite{smith90} and Liu~\cite{liu95}
1511 might be used to 
1512 circumvent this problem, but
1513 unfortunately we do not know of any modern functional language that
1514 supports those ideas.
1515 \end{itemize}
1516
1517
1518 Finally, the algorithm presented here is representative of a large
1519 class of ingenious algorithms, collectively known under the name
1520 \emph{sparse dynamic programming}
1521 \cite{eppstein92b}. It would be nice to see whether 
1522 a generic treatment of this class of algorithms is possible, in
1523 the style of \cite{demoor95}. It seems that such a generic approach
1524 is within reach, but we have not investigated this in any depth. 
1525
1526 \iffalse
1527   \bibliographystyle{plain}
1528   \bibliography{new}
1529 \else
1530   \begin{thebibliography}{10} \raggedright
1531
1532   \bibitem{bird86}
1533   R.~S. Bird.
1534   \newblock Transformational programming and the paragraph problem.
1535   \newblock {\em Science of Computer Programming}, 6(2):159--189, 1986.
1536
1537   \bibitem{bird90}
1538   R.~S. Bird.
1539   \newblock A calculus of functions for program derivation.
1540   \newblock In D.~A. Turner, editor, {\em Research Topics in Functional
1541     Programming}, University of Texas at Austin Year of Programming Series, pages
1542     287--308. Addison--Wesley, 1990.
1543
1544   \bibitem{bird93d}
1545   R.~S. Bird and O.~De~Moor.
1546   \newblock List partitions.
1547   \newblock {\em Formal Aspects of Computing}, 5(1):61--78, 1993.
1548
1549   \bibitem{bdm96}
1550   R.~S. Bird and O.~De~Moor.
1551   \newblock \emph{Algebra of Programming}.
1552   \newblock International Series in Computer Science. Prentice--Hall, 1996.
1553
1554   \bibitem{bird88}
1555   R.~S. Bird and P.~Wadler.
1556   \newblock {\em Introduction to Functional Programming}.
1557   \newblock International Series in Computer Science. Prentice--Hall, 1988.
1558
1559   \bibitem{chin90}
1560   W.~N. Chin.
1561   \newblock {\em Automatic Methods for Program Transformation}.
1562   \newblock Ph.\,D. thesis, Imperial College, London, 1990.
1563
1564   \bibitem{demoor95}
1565   O.~De~Moor.
1566   \newblock A generic program for sequential decision processes.
1567   \newblock In M.~Hermenegildo and D.~S. Swierstra, editors, {\em Programming
1568     Languages: Implementations, Logics, and Programs}, volume 982 of {\em Lecture
1569     Notes in Computer Science}. Springer--Verlag, 1995.
1570
1571   \bibitem{eppstein92b}
1572   D.~Eppstein, Z.~Galil, R.~Giancarlo, and G.~F. Italiano.
1573   \newblock Sparse dynamic programming \uppercase{II}: Convex and concave cost
1574     functions.
1575   \newblock {\em Journal of the ACM}, 39(3):546--567, 1992.
1576
1577   \bibitem{galil89}
1578   Z.~Galil and R.~Giancarlo.
1579   \newblock Speeding up dynamic programming with applications to molecular
1580     biology.
1581   \newblock {\em Theoretical Computer Science}, 64:107--118, 1989.
1582
1583   \bibitem{hirschberg87a}
1584   D.~S. Hirschberg and L.~L. Larmore.
1585   \newblock The least weight subsequence problem.
1586   \newblock {\em SIAM Journal on Computing}, 16(4):628--638, 1987.
1587
1588   \bibitem{hirschberg87b}
1589   D.~S. Hirschberg and L.~L. Larmore.
1590   \newblock New applications of failure functions.
1591   \newblock {\em Journal of the Association for Computing Machinery},
1592     34(3):616--625, 1987.
1593
1594   \bibitem{hoogerwoord92}
1595   R.~R. Hoogerwoord.
1596   \newblock A symmetric set of efficient list operations.
1597   \newblock {\em Journal of Functional Programming}, 2(4):505--513, 1992.
1598
1599   \bibitem{knuth81}
1600   D.~E. Knuth and M.~F. Plass.
1601   \newblock Breaking paragraphs into lines.
1602   \newblock {\em Software: Practice and Experience}, 11:1119--1184, 1981.
1603
1604   \bibitem{liu95}
1605   Y.~A.~Liu and T.~Teitelbaum.
1606   \newblock Systematic derivation of incremental programs.
1607   \newblock {\em Science of Computer Programming},
1608     24(1):1--39, 1995.
1609
1610   \bibitem{morgan94}
1611   C.~C. Morgan.
1612   \newblock {\em Programming from Specifications}.
1613   \newblock International Series in Computer Science. 2nd edition,
1614     Prentice--Hall, 1994.
1615
1616   \bibitem{paige86}
1617   R.~Paige.
1618   \newblock Programming with invariants.
1619   \newblock {\em IEEE Software}, 3(1):56--69, 1986.
1620
1621   \bibitem{pettorossi84}
1622   A.~Pettorossi.
1623   \newblock {\em Methodologies for Transformations and Memoing in Applicative
1624         Languages}.
1625   \newblock Ph.\,D.\ thesis, Department of Computer Science, Edinburgh, 1984.
1626
1627   \bibitem{smith90}
1628   D.~R.~Smith.
1629   \newblock KIDS: A Semi-Automatic Program Development System.
1630   \newblock {\em IEEE Transactions on Software Engineering},
1631     16(9):1024--1043, 1990.
1632
1633   \bibitem{gutenberg}
1634   Gutenberg Project.
1635   \newblock Available by ftp from: {\tt mrcnext.cso.uiuc.edu}.
1636   \newblock Many original texts as ASCII files, 1994.
1637
1638   \end{thebibliography}
1639 \fi
1640
1641 \section*{Appendix: Symmetric lists}
1642
1643 The implementation of symmetric lists given below is explained in some
1644 depth in \cite{hoogerwoord92}. Briefly, a 
1645 list \texttt{x} is represented as a pair
1646 of lists \texttt{(y,z)} such that \verb"abs (y,z)"~=~\verb"x", where the
1647 \emph{abstraction function} \texttt{abs} is defined by
1648 \begin{verbatim}
1649  abs (y,z) = y ++ reverse z
1650 \end{verbatim}
1651 Moreover, the following invariant is maintained:
1652 if either of the two lists is empty, the other is
1653 empty or a singleton.
1654
1655 The operations below implement their non-symmetric counterparts
1656 in the sense that
1657 \begin{verbatim}
1658  head' = head . abs
1659  abs . tail' = tail . abs
1660 \end{verbatim}
1661 and so on. The implementation is such that each operation takes
1662 amortised constant time.
1663
1664 \begin{mcode}
1665
1666 >type SymList a = ([a],[a])
1667
1668 >single' (x,y) = (null x && single y) || (single x && null y)
1669
1670 >null' ([],[]) = True
1671 >null' _       = False
1672
1673 >nil' = ([],[])
1674
1675 >head' (x,y) | not (null x) = head x
1676 >            | otherwise = head y
1677
1678 >last' (y,x) | not (null x) = head x
1679 >            | otherwise = head y
1680
1681 >cons' a (x,y) | not (null y) = (a:x,y)
1682 >              | otherwise = ([a],x)
1683
1684 >snoc' a (y,x) | not (null y) = (y,a:x)
1685 >              | otherwise = (x,[a])
1686
1687 >tail' (x,y) | null x    = ([],[])
1688 >            | single x  = (reverse y1, y0)
1689 >            | otherwise = (tail x, y)
1690 >              where (y0,y1) = splitAt (length y `div` 2) y
1691
1692 >init' (y,x) | null x    = ([],[])
1693 >            | single x  = (y0, reverse y1)
1694 >            | otherwise = (y, tail x)
1695 >              where (y0,y1) = splitAt (length y `div` 2) y
1696
1697 \end{mcode}
1698
1699 \section*{Appendix: Text processing}
1700
1701 The text processing package given below 
1702 is explained in \cite{bird88}.
1703 It provides primitives for converting between strings and lines,
1704 lines and words, and paragraphs and lines. In each case, the forward
1705 direction can be programmed using the generic solution \texttt{format},
1706 and the backward conversion using \texttt{unformat}. The definitions of
1707 \texttt{unlines}, \texttt{lines}, \texttt{unwords} and \texttt{words} have been
1708 commented out because they are already defined in the standard
1709 Haskell prelude. The function \texttt{id} is the identity function.
1710 \begin{mcode}
1711
1712 >unformat :: a -> [[a]] -> [a]
1713 >unformat a = fold1 insert id
1714 >         where insert xs ys = xs ++ [a] ++ ys
1715
1716 >format :: Eq a => a -> [a] -> [[a]]
1717 >format a [] = [[]]
1718 >format a x  = fold1 (break a) (start a) x
1719 >       where break a b xs | a == b    = []:xs
1720 >                          | otherwise = (b:head xs):tail xs
1721 >             start a b = break a b [[]]
1722
1723 *unlines = unformat '\n'
1724 *lines = format '\n'
1725
1726 *unwords = unformat ' '
1727 *words = filter (/=[]) . format ' '
1728
1729 >unparas :: [[[String]]] -> [[String]]
1730 >unparas = unformat []
1731
1732 >paras :: [[String]] -> [[[String]]]
1733 >paras   = filter (/=[]) . format []
1734
1735 >parse    = paras . map words . lines
1736 >unparse  = unlines . map unwords . unparas
1737
1738 \end{mcode}
1739
1740 \end{document} 
1741
1742 The simple greedy algorithm:
1743
1744 >parg :: Txt -> Paragraph
1745 >parg = foldl nextword [[]]
1746 >  where
1747 >    nextword p w | fits (last p++[w]) = init p ++ [last p ++ [w]]
1748 >                 | otherwise = p ++ [[w]]
1749 >fmtg = fmtWith parg
1750
1751
1752
1753 For comparison, the quadratic algorithm:
1754
1755 >fmt1 = fmtWith par1
1756
1757
1758 Some test data:
1759
1760 >test = 
1761 >  "In the constructive programming community it is commonplace to see " ++
1762 >  "formal developments of textbook algorithms. In the algorithm design " ++
1763 >  "community, on the other hand, it may be well known that the textbook " ++
1764 >  "solution to a problem is not the most efficient possible. However, in " ++
1765 >  "presenting the more efficient solution, the algorithm designer will " ++
1766 >  "usually omit some of the implementation details, this creating an " ++
1767 >  "algorithm gap between the abstract algorithm and its concrete " ++
1768 >  "implementation. This is in contrast to the formal development, which " ++
1769 >  "usually presents the complete concrete implementation of the less " ++
1770 >  "efficient solution. \n \n"
1771
1772 >tests = concat (repeat test)
1773
1774 >main = getArgs >>= (\as ->
1775 >       if length as /= 1
1776 >       then putStr "usage: para <file name>"
1777 >       else openFile (head as) ReadMode >>= (\h ->
1778 >            hGetContents h >>= (\ws ->
1779 >            putStr (if null ws then [] else (fmt ws)))))
1780
1781
1782
1783