The Final Pretty Printer -...

e Final Pretty PrinterDavid ChristiansenIndiana University

[email protected]

David DaraisUniversity of [email protected]

Weixi MaIndiana University

[email protected]

AbstractWidely-used prey printing libraries are built on assump-tions from a previous age of computing that are no longeruniversally true, such as monospace fonts and batch-modecompilers. Furthermore, they are not extensible, which hasled to a plethora of similar libraries. We demonstrate anapproach to prey printing that is independently extensibleand supports proportional fonts and interactive interfaces.

1 IntroductionWith the wealth of available compile-time information, stat-ically typed functional languages should have the richestinteractive programming environments. However, our toolsare typically stuck in the world of monospaced text-basedterminals and ASCII identiers. While textual terminals arestill an importantmode of use that programming tools shouldsupport, they should be the oor rather than the ceiling forour ambition. e rst step towards good programming toolsis good tool-making tools. We present one small part of thesolution: an extensible, exible prey printing system.

A prey printer is the inverse of a parser. While a parserconverts human-wrien text into a structured representa-tion, a prey printer converts a structured representation ofdata into human-readable text.

Ideally, prey printers should be specied compositionally,so that prey printers for dierent productions in an ASTcan be wrien individually and then combined. Oppen [19]described a composable imperative prey printing algorithm,and classic papers by Hughes [15] and Wadler [25] provide adescription of prey printing in a lazy functional language.

Hughes and Wadler consider the prey printing problemin the abstract, using these considerations to derive combi-nator libraries for prey printing. Since these papers werewrien, however, it has become clear that some of theirsimplifying assumptions have become limiting assumptions.For example, libraries for prey printing tend to assume

that each character occupies a xed width when rendered.is is not even true for English text when wrien with aproportionally spaced font, and the vast majority of fontsare proportionally spaced. Features such as kerning, liga-tures, and mixed le-to-right and right-to-le scripts, whichare now standard in most computing contexts, are likewiseignored.

PL ’17, Somewhere2016. .DOI:

Another limiting assumption of prey printing is that textexists only for the understanding of humans, and that onceit is displayed, the computer can oer no further assistance.However, programming environments such as those for Lispand Smalltalk have supported a rich notion of text that issupplemented with information about its meaning, enablingtools and interaction strategies that are not possible for meretext. e interactive environment for Idris, a dependentlytyped functional language, has been modeled on Lisp andSmalltalk using a prey printer with a design like ours. Sec-tion 2 describes some of the tools that this enables.

At the time of writing, there are 19 prey printing librarieson Hackage. Seven of these were created by copying andthen modifying Daan Leijen’s implementation of Wadler’sinterface (wl-pprint), adding extensions such as supportfor ANSI color codes (ansi-wl-pprint), semantic annota-tions (annotated-wl-pprint), or embeddedmonadic eects(wl-pprint-extras). While the ability to improve a pro-gram and share these improvements is an advantage of freesoware, derived libraries do not benet from miscellaneousimprovements made to one another unless active eort ismade to port them. Additionally, these extensions cannot beused together. Our prey printing library is extensible, andeach of these libraries could be implemented as an extensionon top of it. When possible, it is beer to link than to fork.

Because documents are wrien as programs, rather thanas a datatype, we call our library the Final Prey Printer. isname is aspirational as well as descriptive: our intentionis that that supporting extensibility, current user interfacetechnology, and a variety of scripts means that it is the lastprey printer that you’ll ever need.

ContributionsWe make the following contributions to the state of func-tional prey printing library design:• We describe a prey printing library that supportsproportional fonts and non-Roman scripts.• e correctness of our algorithm is derived solelyfrom the laws governing standard functional pro-gramming abstractions, and is stable under extension.• e library supports semantic annotations, makingits output more broadly useful.

2 Challenges and OpportunitiesPast prey printing libraries have been built under a numberof assumptions, which are no longer universally true:• Characters occupy a xed width on the screen

1

PL ’17, Some Date, Somewhere David Christiansen, David Darais, and Weixi Ma

• e rendering of a particular character, and thus itswidth, is independent of the surrounding characters• User interface devices are limited to the display andinput of text

Today, graphical displays are ubiquitous and computers areused in many languages. is presents challenges and op-portunities.

2.1 UnicodeSoware is used all over the world, by speakers of manydierent languages. e syntax of most programming lan-guages, however, is based primarily on characters from theLatin alphabet. Choices about prey printing technologythat assume that all characters are the same width fail towork in contexts where a variety of scripts are used in thesame project, such as a program in which some identiernames are technical terms in a variety of languages.

When represented in a xed-width font, Latin charactersare signicantly narrower than they are tall. is choicedoes not work well for Chinese characters, however, whichare wider. Other scripts, like many of those from the Indiansubcontinent, realize a sequence of characters as a singleglyph, because vowels typically modify the preceding conso-nant character rather than being drawn separately. In somescripts, such as Sinhala, some combining vowels signicantlyincrease the width of the resulting glyph.

Even if a programming language is only intended for usewith English-language identiers and syntax, it can be usefulto support Unicode operators, such as arrows and othermath-ematical operators, that do not t well within a xed-widthformat. Also, because many beautiful fonts are proportional,a prey printer that can use them is strictly more useful thanone that cannot.

2.2 Interactive environmentse computers on which programmers work today are al-most universally equipped with a graphical display and amouse, touchpad, or touchscreen. While early graphicalprogramming environments such as Smalltalk [12], Lisp ma-chines [18], Self [21, 23], and Nuprl [9] made the most of this,allowing the interactive exploration of a live environment,an image-based model is a challenging basis on which todevelop maintainable, reliable, redistributable soware. Inthe retreat from graphical environments to batch processingof plain text, however, something important has been lost.A presentation [7, 18] is a link between an region of pro-

gram output and the underlying application object that itrepresents. Presentations are perhaps best known from theuser interface toolkit of the thoroughly le-oriented Sym-bolics Lisp machines, though similar ideas were later imple-mented by companies such as Lucid [11] as well as in otherLisp environments [17, 20]. In an environment with presen-tations, a REPL might print a result as usual, but a referenceto that result could be obtained for a new evaluation task by

data Bool = True| False

(a) No padding


(b) Right padding


(c) Le padding


(d) Centering

Figure 1. Aligning constructors and padding separators

clicking on it. Other commands could be performed on theunderlying object by interacting with its presentation.Presentations are also useful in programming environ-

ments that do not separate object identity from object struc-ture. For example, the interactive environment for Idris [3]makes heavy use of presentations. All output from the com-piler comes with semantic tags that provide the meaning ofeach name that occurs in them, and all expressions that areoutput by the compiler come with a reference to the under-lying AST object. is AST object can be used to interactdirectly with the compiler, for example by normalizing anexpression in-place in an error message, by seeing the corelanguage representation of a term output in the REPL, or byshowing or hiding implicit arguments.e Final Prey Printer supports presentations through

a system of semantic annotations. When producing a doc-ument from some datatype, it can be annotated with itsmeaning. Later, meanings can be used both to aect the dis-play of the output (e.g. by using dierent fonts for top-leveldenitions and locally-bound variables) and to associate theoutput with commands relevant to its meaning.

2.3 Rendering to the Webe Haskell code in this paper is prey printed with theFinal Prey Printer. Rather than reimplementing the quitecomplex operations needed to render multilingual text, thisprey printer piggybacks on themassive amount of work putinto the text rendering engines ofWeb browsers. Our Haskellprey printer, built with the Haskell to Javascript compilerghcjs,1 runs entirely in a browser. e prey printer’s out-put was converted to PDF for display in this paper.As can be seen in Figure 1a, the customary alignment of

the = character with the vertical bar separators in datatypedenitions becomes more subtle when proportional-widthfonts are used. A vertical bar is much narrower than =, whichleads to the constructors not starting the same distance fromthe le margin. To achieve an appealing layout, it is neces-sary to horizontally pad the documents that represent thevertical bars to the width of the = document, in essence mak-ing them monospaced once more. Right and le padding, inFigures 1b and 1c, cause the constructors to be appropriately

1Available at the time of writing from hps://github.com/ghcjs/ghcjs.2

https://github.com/ghcjs/ghcjs

The Final Prey Printer PL ’17, Some Date, Somewhere

aligned, but we chose to center them with respect to oneanother (Figure 1d). While text formaing is implementedusing CSS rules, spacing and alignment are implemented byinserting HTML elements with explicit widths.

2.4 Interactive documentsA previous prey printer with semantic annotations wasused to write Idris’s prey printer, and work is underway toport Idris to the Final Prey Printer. While Idris’s IDE pro-tocol is editor-independent, the Emacs environment (calledsimply idris-mode) currently makes best use of these fea-tures.In idris-mode, mousing over any identier provides a

tooltip that gives its fully-qualied name, its type, and asummary of its documentation. Right-clicking the nameprovides a menu that allows queries such as reading thefull documentation, geing a list of all denitions that referto that name or all names that its denition refers to, orbrowsing other denitions from the namespace in which itis dened.

Additionally, right-clicking any region of compiler outputthat represents an expression pops up a menu with com-mands to show or hide implicit arguments, to normalize it,and to show its meaning in Idris’s core language. is isespecially useful in error messages. Users can interact withthe expressions that occur in e.g. unication failures withoutneeding to change a seing and re-provoke the error.How does all this work? All output from the Idris com-

piler to an editor has not only a string, but also a list ofoset-length-metadata triples that are derived from the an-notations. e metadata is a serialization of Idris’s internalsemantic annotations. While prey printing, each docu-ment representing a name is annotated with its actual name,and each document representing an expression is annotatedwith that very expression. In other words, these documentspresent their associated objects.

Prior to transmission to the editor, name annotations areenriched with metadata such as documentation and typesignatures, and expression annotations are serialized intoa form suitable for transmission over a text protocol. en,editors can use this serialized representation to request otherviews of the expression, such as the core language or theview in which implicit arguments have been made explicit.

Another advantage of presentations is that they can beused to provide a reference to something for which there isno valid syntax. For example, in systems that have a notionof reference equality and destructive updates, presentationscan be used to destructively update a previous REPL value.In systems like Idris, internal names used by the compilerfor automatically-generated helper functions do not alwayshave a syntax that the user can type. Inspecting these ismuch easier when a presentation can be used to indicatewhich is desired.

(a) Tooltips display metadata for presentations

(b) Contextual menus provide additional commands

(c) Presented terms can be normalized in-place

Figure 2. Interactive error messages in Idris

3 Core LibraryA prey printer constructs a representation of a set of strings,called a document, and then arranges for one string fromthis set to be chosen according to some measure of quality.is set of strings is built from atomic strings, which willalways occur verbatim in the output, and conditional stringcombinations that can be either be rendered in one line oron multiple lines.Like many APIs, a prey printing library can be seen as

a domain-specic embedded language [14]. Hughes’s andWadler’s prey printing libraries [15, 25] can be seen as deepembeddings [2] of a prey printing language in Haskell.On the other hand, our API can be seen as a shallow em-

bedding of a language similar to that described by Wadler.is approach has the typical advantage of shallow embed-dings: the metalanguage can be directly used to extend theembedded language. Traditionally, it is easier to obtain multi-ple interpretations of deeply embedded languages; we followthe Finally Tagless approach [4] in using type classes torecover multiple interpretations.

3.1 Lines, Widths, and FormattingIn xed-width contexts, a width is simply a character count.Rendering horizontal space consists of inserting the correct

3


data Chunk w = CText Text| CSpace w

deriving (Eq, Ord)

data Atom w = AChunk (Chunk w)| ANewline

deriving (Eq, Ord)

type Line w fmt = [(Chunk w, fmt)]

data Layout = Flat| Break

deriving (Eq, Ord)

data Failure = CanFail| CantFail

deriving (Eq, Ord)

Figure 3. Core datatypes

number of space characters. In order to support proportional-width fonts properly, it is necessary to have a notion of widththat is not just a character count. In proportional-widthcontexts, a width is typically a rational or oating-pointnumber, and rendering horizontal space requires advancinghorizontally through some drawing context or constructingan empty box of the appropriate size, because there is noguarantee that the width of space characters evenly dividesevery horizontal space.

e core datatypes of the library are in Figure 3. Internally,the contents of text lines are represented using the datatypeChunk, which is parameterized over the widths used in thecurrent drawing context.

CText represents a string to be included, and CSpace rep-resents an amount of horizontal space to be skipped. Animportant invariant is that the text included in CText con-tains no newlines, and that any space characters includedare part of a literal string to be produced that are not oppor-tunities for line breaks.

Dierent output contexts support dierent notions of for-maed text. A terminal emulator might support some lim-ited font options, such as boldface and colors, while Webbrowsers and newer TEX implementations such as LuaTEXand XeTEX support the full range of options found in modernOpenType fonts, including customizable ligatures, language-specic glyph variations that share Unicode code points,stylistic sets, and many dierent weights and sizes.

An individual Line of text is represented as a list of pairsof chunks and formaing options. Lines are not the outputof the prey printer. Rather, they are an intermediate datastructure used to track a current line while deciding whereto break lines in the output.

e classMeasurew fmt m in Figure 4 represents amethodfor determining the horizontal width of a line in some contextm, where chunks in the line can be formaed using fmt. efunctional dependencies encode that each rendering context

class Measure w fmt m | m → w, m → fmt wheremeasure :: Line w fmt→ m w

Figure 4. e Measure class

has a unique unit of horizontal measurement as well as aunique collection of formaing options.

ewidths found in Hughes’s andWadler’s prey printerscan be recovered by making formaing trivial, using Int forwidths, and measuring by counting characters (T.length ndsthe length of a Text).instance Measure Int () Identity where

measure = pure ∘ sum ∘ fmap (chunkLength ∘ fst)wherechunkLength (CText t) = T.length tchunkLength (CSpace w) = w

For the Web backend that was used to render the code inthis paper, Measure is more subtle. When prey printing toa Web page, the precise location of the text in the page’s ASTcan change the text’s appearance. us, the prey printer isinvoked on a particular target element into which the docu-ment is to be displayed. Widths are Doubles that measurethe number of horizontal pixels taken up by a document,and formaing consists of a list of strings that represent CSSclass names.

Instead of simulating a browser’s rendering, measurementin the Web backend is empirical. Measurement consists ofadding the formaed text to the output target, and thenchecking its width once the browser’s CSS styles have beenapplied. A similar technique could be applied to other back-ends, such as TEX or a drawing canvas.

Rendering that is accurate to fractional pixels motivates anumber of design considerations. First, the width of a spaceis no longer just one unit. e width of a space charactercan change in dierent contexts, as determined by the cur-rent formaing. us, the library provides primitives formeasuring the width of a string in the current context.

3.2 Pretty PrintingRather than use a datatype to represent a document, weinstead represent the document directly as a monadic com-putation that will select a concrete string when run. Not onlydoes this make the prey printing language extensible, italso enables the re-use of existing Haskell control structuresfor prey printing. e type classMonadPrey captures therequirements for a monad to support prey printing. If thereis a MonadPrey m instance, then we call m a prey monad.

Prey printing monads are parameterized over types rep-resenting widths, semantic annotations, and formaing in-structions. ese are the parameters w, ann, and fmt, re-spectively. If the type w is to be used for widths, then itmust be ordered, numeric, and able to be measured in thepreymonad. Formaing instructions are necessary because

4


class ( Ord w, Num w,Measure w fmt m,Monoid fmt,MonadReader (PEnv w ann fmt) m,MonadWriter (POut w ann) m,MonadState (PState w fmt) m, Alternative m) ⇒MonadPrey w ann fmt m| m → w, m → ann, m → fmtwhere

Figure 5. Prey monads

choices of font might aect the width of a sub-document,and fmt must be a monoid so that there is a neutral format-ting instruction and so that formaing instructions can becombined.e actual process of constructing the next line of a con-

crete string from a document involves backtracking fromlines that are too long. us, a prey monad must also imple-ment Alternative. (We discuss backtracking in more detailin Section 3.5.) Aer each line is completed, it is emied,so prey monads must be aMonadWriters of outputs. eline under construction may be read for purposes of mea-surement, or wrien to when a new segment ts, so preymonads are alsoMonadStates. Finally, information such asthe current formaing, the current indentation level, andwhether the prey printer is currently running in at modeor in line breaking mode has dynamic extent, so prey mon-ads satisfyMonadReader. e environment also maintainsthe maximum line width and the ribbon length, which is amaximum width that excludes indentation. e completedenition of MonadPrey is in Figure 5, Figure 6 lists someof the operations that can be derived for any prey monad,and Figure 7 denes auxiliary datatypes.

3.3 GroupingLike Oppen’s, Hughes’s, and Wadler’s libraries, the FinalPrey Printer supports grouping subdocuments. Duringrendering, the library should aempt to keep groups on oneline, if possible, or place them on multiple lines if they donot t. When one group contains another, then the innergroups should, if possible, be placed on individual lines evenif the entire group does not t. e Final Prey Printer usesthe Alternative class to implement this backtracking. eentire library maintains the invariant that prey printingnever ultimately fails; all failures are local, and recoveredfrom.

e grouping operator uses the MonadReader operationsto communicate with its subdocuments. It rst tries to preyprint the subdocument in a context which disables line breaksand allows failure (i.e. calls to empty), and if this fails, thentries prey printing in a context which enables line breaks

askFormat :: (MonadReader (PEnv w ann fmt) m, Monoid fmt)⇒m fmt

modifyLine :: (MonadState (PState w fmt) m)⇒(Line w fmt→ Line w fmt) → m ()

askFailure :: (MonadReader (PEnv w ann fmt) m)⇒m Failure

askMaxWidth :: (MonadReader (PEnv w ann fmt) m)⇒m w

askMaxRibbon :: (MonadReader (PEnv w ann fmt) m) ⇒m w

measureCurLine :: (Measure w fmt m, Monad m, MonadState (PState w fmt) m)⇒m w

askNesting :: (MonadReader (PEnv w ann fmt) m)⇒m w

Figure 6. MonadPrey operations

data PEnv w ann fmt = PEnv { maxWidth :: w, maxRibbon :: w, nesting :: w, layout :: Layout, failure :: Failure, formaing :: fmt, formatAnn :: ann→ fmt}

data POut w ann = PNull| PAtom (Atom w)| PAnn ann (POut w ann)| PSeq (POut w ann) (POut w ann)

deriving (Eq, Ord, Functor)

data PState w fmt = PState { curLine :: Line w fmt }deriving (Eq, Ord)

Figure 7. Auxiliary datatypes

and disallows failure. Because the second aempt disallowsfailure, it is guaranteed to succeed, maintaining the invariantthat prey printing always produces some answer.

Atomic Chunks are prey printed using chunk, in Figure 8.e rst step is to add the chunk to the output, using tell,and to append it and its formaing to the current line. Next,chunk checks whether there is a failure handler in the dy-namic extent of the current document using askFailure. Ifthere is, then the current rendering task is speculative, and

5


chunk :: (MonadPrey w ann fmt m)⇒Chunk w→ m ()

chunk c =do tell $ PAtom $ AChunk c

format ← askFormatmodifyLine $ flip mappend [(c, format)]f← askFailurewhen (f == CanFail) $do wmax← askMaxWidth

rmax ← askMaxRibbonw← measureCurLinen← askNestingwhen (n + w > wmax) emptywhen (w > rmax) empty

grouped :: (MonadPrey w ann fmt m)⇒m a → m a

grouped aM =ifFlat aM $ (makeFlat ∘ allowFail) aM aM

ifFlat :: (MonadPrey w ann fmt m)⇒m a → m a → m a

ifFlat flatAction breakAction =do l← askLayout

case l ofFlat → flatActionBreak → breakAction

Figure 8. Determining line breaks

might be undone if it overows the current line. us, thecurrent line is measured, and its width is used together withthe indentation level to determine whether adding the chunkwas successful.

Previous prey printing libraries provide a conditionalnewline operator that may be replaced with a space wheninside a group. e Final Prey Printer decomposes the con-ditional newline into a more fundamental operation, ifFlat,which conditionally selects one or another document de-pending on whether the current context is at. Wadler’s con-ditional newline can be recovered as ifFlat (space i) newline,where i is the width to use for the space. is decompositionallows newlines to be undone into no space at all. It also al-lows the library to be used to correctly prey print languagessuch as Haskell, where do-notation requires semicolons be-tween statements that are on the same line, and Idris, wherecase expressions should use braces and semicolons when onone line, but the layout rule when breaking lines.

Note that a prey printer computation that always takesthe line-breaking branch for each ifFlat will never fail. is isbecause such computations do not contain any grouping, andwithout grouping, there can be no backtracking. e call toifFlat in grouped should be seen as ameans of communicationwith other calls to grouped — see Section 7 for a proof thatgrouped is idempotent.

Recovering Hughes-Style Printing Although our preyprinter resembles that of Wadler [25], the original Hughesprey printing algorithm [15] can also be recovered in ourseing by changing the implementation of grouped. Hughes-style prey printing allows inner groups to force line breaksin the context of an outer group. For example, if we redenedgroup to always aempt both sides of the branch, regardlessof the inherited context:

grouped aM =(makeFlat ∘ allowFail) aM (makeBroken ∘ disallowFail) aM

thenwewould get the following layout for a nested S-expression:(abd ((a

bc)(abc)))

instead of the current (Wadler-based) algorithm which pro-duces:(abd((a b c)(a b c)))

For more discussion on the dierences betweenWadler-styleand Hughes-style prey printing, and for the origin of thisexample, see Bernardy [1].

3.4 IndentationIndentation in the Final Prey Printer is tracked as part ofthe dynamic environment of prey monad computations.e current indentation level is used to determine whethera line exceeds the ribbon width, and also to insert space atthe beginning of a new line. e nest operator incrementsthis level in its dynamic extent, causing indentation levels tofollow the lexical structure of the programs being displayed.

Oppen’s, Hughes’s, and Wadler’s prey printing librariescause the elements of groups to have the same base indenta-tion. In other words, when the newlines in a group cannot beundone, then the group’s members are le-aligned. is isgood for expression-oriented programming languages, andalso for many block-structured languages. However, popularstyles in languages like Javascript and Haskell sometimescall for subgroups to be indented a xed amount, rather thanaligned with their rst token. For example, in the followingsnippet, the contents of the callback are not indented relativeto the function keyword.window.setTimeout(function () {

console.log("Message");}, 5000);

Likewise, some Haskell users prefer a “dangling do” style,where do introduces a block rather than an expression. edo-expression is grouped, but when rendering on more than

6


one line, those lines should be far to the le of the beginningof the expression.

measureText txt = doformat >=, which implies that the structure of the transformedmonads is preserved. e proofs (in Section 7) that our

7


algorithm satises its specication make use only of theabstract laws of their implementation monad, so they alsohold for T m. �

Two convenient extensions that are widely useful are vari-able environments and precedence and associativity.

5.1 Variable EnvironmentsAn almost universal feature of programming languages isbinding structure, and the scoping rules of a language arenot always easy to discover from its surface syntax. Preyprinters with semantic annotations can use the languageimplementation’s facilities for resolving variable scopes toprovide an implementation that connects binding sites withuse sites. Additionally, bound variables can be annotatedwith type information, documentation, and other metadatathat may not be immediately apparent to readers, and thecontext in which the document is displayed can then use thisinformation to increase the understandability of the output.

Because the structure of a lexical environment correspondsclosely to the structure of an AST, a prey printer thattraverses this structure to produce a document can faith-fully represent the lexical environment using an additionalMonadReader eect.To avoid conicts with the built-in MonadReader con-

straint on MonadPrey, a wrapper is needed. We beginby deningMonadReaderEnv, which represents readers ofsome environment env.

class MonadReaderEnv env m | m → env whereaskEnv :: m envlocalEnv :: (env→ env) → m a → m a

A monad that is both prey and a reader of environments isa MonadPreyEnv.

class (MonadPrey w ann fmt m,MonadReaderEnv env m) ⇒MonadPreyEnv env w ann fmt m| m → w, m → ann, m → fmt, m → envwhere

A newtype wrapper around ReaderT is sucient to deneEnvT as a transformer of prey monads.

5.2 Operator Precedence and AssociativityA reader eect for an environment consisting of operatorprecedence and associativity information as well as the sur-rounding context’s precedence and associativity can be de-ned using a construction similar to EnvT. is additionalstructure can be used to enrich the prey printing languagewith operations for inserting parentheses as necessary.

e precedence environment consists of a current level,whether or not it is bumped, and le and right parentheseswith optional annotations. “Bumping” a precedence level isused as a tiebreaker to implement associativity for nestedapplications of operators with the same precedence. e

data PrecEnv ann = PrecEnv { level :: Int, bumped :: Bool, lparen :: (Text, Maybe ann), rparen :: (Text, Maybe ann)}

Figure 9. e precedence environment

extension provides an operator atLevel that conditionallyinserts parentheses depending on the environment’s leveland a provided level.

6 Performancee performance of our prey printing algorithm is com-parable to Wadler’s. In the best case, the time complexityfor prey printing is O(n) for n atoms in document beingprinted. A pathological worst case for our algorithm occurswhen every atom in the document appears nested inside agroup expression. In this worst case, the time complexity forprey printing is O(nw) for n atoms in the document beingprinted and w as the maximum layout width. Informallythis worst case scenario plays out as follows: at each atom,an aempt is made to format the document on a single line(O(w) work); at this point the current layout branch failsand the algorithm backtracks to introduce a newline aerthe rst atom; and this is repeated for every atom in thedocument, hence O(nw) work.

Notably, our implementation is not sensitive to the strict-ness of the implementation language, as is the case for bothHughes and Wadler.

7 CorrectnessWhile it is important that soware in general be correct,the nature of the correctness argument for the Final PreyPrinter is of special importance. We show that the correct-ness of the core of the implementation is derived entirelyfrom the laws governing the control structures that are em-ployed, rather than just a specic instantiation of these struc-tures. is allows arbitrary monad transformers to be usedto extend the library, hopefully puing an end to the forkingof prey printing libraries.

7.1 Prior Worke original prey printing paper by Hughes [15] consideredthe laws that a minimal prey printing api should satisfy,and derived an algorithm which satised those laws. einterface consisted of document construction operators:(⋄) :: Doc → Doc → Doc Horizontal concatenation($$) :: Doc → Doc → Doc Vertical concatenationtext :: String → Doc Literal textnest :: Int → Doc → Doc Document nesting

and laws which they should satisfy (only some of which wedisplay here):

8


x ⋄ text "" = x(x ⋄ y) ⋄ z = x ⋄ (y ⋄ z)

text s ⋄ text s′ = text (s⧺ s′)(x $$ y) $$ z = x $$ (y $$ z)(x $$ y) ⋄ z = x $$ (y ⋄ z)

nest 0 x = xnest k (nest k′ x) = nest (k + k′) x

nest k (x ⋄ y) = nest k x ⋄ nest k ynest k (x $$ y) = nest k x $$ nest k y

Later work by Wadler [25] modied the combinator inter-face:

nil :: Doc e empty document(⋄) :: Doc → Doc → Doc Horizontal concatenationtext :: String → Doc Literal textline :: Doc Newlinenest :: Int → Doc → Doc Document nestinggroup :: Doc → Doc Grouping() :: Doc → Doc → Doc Nondeterminismflaen :: Doc → Doc Undo line breaks

and presented alternative laws (only some of which we dis-play here):

x ⋄ nil = xnil ⋄ x = x

(x ⋄ y) ⋄ z = x ⋄ (y ⋄ z)(x y) z = x (y z)(x y) ⋄ z = (x ⋄ z) (y ⋄ z)x ⋄ (y z) = (x ⋄ y) (x ⋄ z)

nest 0 x = xnest i (nest i′ x) = nest (i + i′) xnest i (x y) = nest i x nest i y

To construct a veried prey printer, Danielsson [10] for-malized a variant of Wadler’s algorithm in Agda and wassuccessful in proving many of these laws. In the process,it was discovered that the following law from Wadler [25]actually doesn’t (and shouldn’t) hold:

(x y) ⋄ z = (x ⋄ z) (y ⋄ z)

7.2 Our Worke core layout algorithm of our prey printer is chunk, inFigure 8. We use chunk to implement higher-level operatorsfor creating and combining documents, a subset of whichcoincide with Wadler’s interface. Our implementation ofWadler’s combinators also obeys Wadler’s prey printinglaws. e challenge in our seing is how to prove that theyhold for any prey monad.

Our prey printer is parameterized by a monad m whichimplements various monadic reader, writer, state, and non-determinism operations. A prey printer document is thena monadic action m () in this arbitrary monad, and we wouldlike to prove that prey printing laws hold for any m thatchunk is executed in, up to possibly some restriction on m.e result we describe in this section is that, not only is itpossible to that our algorithm satises the prey printing

laws with respect to an uninstantiated law-abiding monad,but also that the proofs proceed directly from the monadlaws.

7.3 Monad Lawse monad laws which we assume are standard [24]:

return x ≫= k = k xc ≫= return = c

(c ≫= f) ≫= k = c ≫= λx→f x ≫= kWe additionally assume laws for nondeterminism:

empty ≫= k = emptyc ≫= λ_→empty = empty(c1 c2) c3 = c1 (c2 c3)(c1 c2) ≫= k = (c1 ≫= k) (c2 ≫= k)

c c = cand the standard laws for reader eects:

local f ask = ask ≫=λx→return (f x)

local id c = clocal f (local g c) = local (f ∘ g) clocal f (c1 c2) = local f c1

local f c2local f (c1 ≫= k) = local f c1 ≫=

λx→local f (k x)and writer eects:

tell mempty = niltell o1 ≫ tell o2 = tell (o1⧺ o2)

and state eects:put s ≫ put s′ = put s′put s ≫ get = put s ≫ return sget ≫= put = return ()

get ≫= λs→get ≫= k s = get ≫= λs→k s sWe also require that writer and state eects commute withfailure. When constructing monad transformers to imple-ment our eect interface, this xes the order of StateT andWriterT in relationship to MaybeT, namely that they appearhigher in the stack.

7.4 Pretty Printing Laws from Monad LawsLet’s start small, from our implementation of ⋄ and nil:

(⋄) :: (MonadPrey w ann fmt m) ⇒m () → m () → m ()

c1 ⋄ c2 = c1 ≫ c2

nil :: (MonadPrey w ann fmt m)⇒m ()

nil = return ()

Lemma 7.1. m (), ⋄ and nil form a monoid, that is:

nil ⋄ x = xx ⋄ nil = x

(x ⋄ y) ⋄ z = x ⋄ (y ⋄ z)9


chunk (CText s) =do tellString s

addLine scheckBreak

wheretellString s =

tell $PAtom $AChunk (CText s)

addLine s =do format← askFormat

modifyLine $flip mappend[(CText s, format)]

checkBreak =do f← askFailure

when (f == CanFail) $do wmax← askMaxWidth

rmax← askMaxRibbonw← measureCurLinen← askNestingwhen (n + w > wmax) emptywhen (w > rmax) empty

Figure 10. chunk, specialized to CText, with named subparts

Proof. Directly from monad le unit, right unit, and associa-tivity laws. �

e implementation of text uses chunk to insert a text chunk.text :: (MonadPrey w ann fmt m)⇒ Text → m ()text t = chunk (CText t)

e proofs about text rely on various sub-parts of chunk.Figure 10 names some of the intermediate computationswithin chunk specialized to CText s.

Lemma 7.2. text is a monoid homomorphism, that is:text (s1⧺ s2) = text s1 ⋄ text s2

Our proof relies on the fact that failure discards changesin both the state and output, and therefore commutes withstate and writer eects.

Proof. First, we unfold the denition of chunk in text:text (s1⧺ s2)

= {{ unfolding text }}chunk (CText (s1⧺ s2))

= {{ unfolding chunk }}do tellString (s1⧺ s2)

addLine (s1⧺ s2)checkBreak

= {{ output and line monoid homomorphism }}do tellString s1

tellString s2addLine s1addLine s2checkBreak

= {{ commuting tell and modify eects }}

do tellString s1addLine s1tellString s2addLine s2checkBreak

= {{ idempotent failure eects }}do tellString s1

addLine s1checkBreaktellString s2addLine s2checkBreak

= {{ refolding }}text s1 ⋄ text s2

�

Next, our implementation of nest:nest :: (MonadPrey w ann fmt m)⇒ w→ m () → m ()nest i c = localNesting (λi′→i + i′) c

Lemma 7.3. If the Num instance for w has 0 as a unit for +,then nest has unit 0 and is distributive through +, ⋄ and ,that is:

nest 0 x = xnest i (nest i′ c) = nest (i + i′) cnest i (x ⋄ y) = nest i x ⋄ nest i y

nest i (x y) = nest i x nest i y

Proof. Directly from reader monad unit and distributivitylaws. �

Our implementation ofWadler’s group is a rephrased versionof grouped from Figure 8.

group :: (MonadPrey w ann fmt m)⇒ m a → m agroup c = ifFlat c $ flaen c cwhereflaen = makeFlat ∘ allowFail

Lemma 7.4. group is idempotent and distributes through ,that is:

group (group x) = group xgroup (x y) = group x group y

Proof. For idempotency:group (group x)

= {{ unfolding group }}ifFlat (group x) $flaen (group x) group x

= {{ unfolding ifFlat }}do f← askFlat

if fthen group xelse flaen

(group x) group x

= {{ group under askFlat = True }}10


do f← askFlatif fthen xelse flaen x

group x= {{ group under askFlat = False }}

do f← askFlatif fthen xelse flaen x

flaen x x

= {{ idempotent }}do f← askFlat

if fthen xelse flaen x x

= {{ refolding group }}group x

and for distribution:group (x y)

= {{ unfolding group }}do f← askFlat

if fthen x yelse flaen

(x y) x y

= {{ distributivity of aen }}do f← askFlat

if fthen x yelse flaen x

flaen y x y

= {{ nondeterminism distribution }}(do f← askFlat

if fthen xelse flaen x x)

(do f← askFlatif fthen yelse flaen y y)

= {{ refolding }}group x group y

�

8 Related WorkPrey printing libraries can be evaluated according to anumber of parameters, including the variety of layouts thatthe document language can describe, the space and time

complexity of the string selection algorithm, and the qualityof the string selection with respect to ecient use of screenspace.Goldstein [13] provided an algorithm for prey printing

Lisp code that was extensible with custom formaing in-structions for built-in operators. is prey printing systemwas interactively extensible by users of MacLisp, rather thanbeing a library for expressing a single prey printer for axed language. Goldstein’s algorithm performed a great dealof lookahead, and was therefore not suitable for printinglarge documents.Oppen [19] described the rst ecient general-purpose

prey printing algorithm, in the form of a lile languagefor expressing grouping and literal strings. Presented in animperative style, Oppen’s algorithm requires time linear inthe length of the string to be produced and space linear inthe width to be used.

A paper by Hughes [15] may be responsible for beginningthe Haskell community’s love for prey printing. Hughesprovides prey printing as an exercise in deriving functionalprograms from their algebraic specication. A variation onhis library is used in the Glasgow Haskell Compiler today.

Wadler [25] describes a design for a prey printing librarythat is simpler and faster that Hughes’s, though there aresome layouts that it cannot describe. e Final Prey Printerimplements essentially the same algorithm as Wadler, al-though noticing this fact requires rewriting it to take lessexplicit advantage of lazy evaluation. Indeed, aer imple-menting the Final Prey Printer, the authors noticed that theinterplay of chunk and ifFlat bear a striking resemblance toKen Friis Larsen’s port of Wadler’s library to Standard ML.2While Hughes’s and Wadler’s designs are both elegant

and fast enough for many real applications, they do notenjoy the same asymptotic complexity as Oppen’s algorithm.Chitil [5, 6] demonstrated that Oppen’s algorithm can beimplemented in a functional style using lazy dequeues ordelimited continuations. Swierstra and Chitil [22] later madethis implementation even more clear.Bernardy [1] managed to provide an implementation of

all of Hughes’s layouts while providing the very strong guar-antee that only the shortest realization of the document asa string will be provided. His implementation takes timelinear in the length of the output, using a quality-rankingmethod to rule out exploration of non-optimal documents.

e expressiveness and performance characteristics of theFinal Prey Printer are roughly similar to Wadler’s. In otherwords, it has worse complexity that Chitil’s, and beer com-plexity that Hughes’s. In future work, it would be interestingto explore an adaptation of Bernardy’s algorithm to a nalprey printer.

2Available at the time of writing from hps://github.com/kfl/wpp11

https://github.com/kfl/wpp


9 ConclusionWe described the Final Prey Printer, a prey printing librarythat is both highly expressive and extensible. It derives itsextensibility from the fact that it is correct in any monad, somonad transformers can be used to give it new capabilities,and we demonstrated two widely-applicable extensions. Wehave implemented a new prey printer for cubicaltt, animplementation of Cubical Type eory [8], showing that itis practical for real systems, and work is underway to portIdris’s interactive environment.Semantic annotations enable the prey printer to pro-

duce presentations that link displayed strings to the meaningthat they represent. Presentations have been used in theinteractive environment for Idris, enabling interactive errormessages, pervasive metadata and documentation, and textdecorations that are based on semantics rather than syntax.

By decoupling the measurement of widths from charactercounts, the Final Prey Printer enables language developersto properly support almost every natural language in theworld, as well as proportional fonts and modern text layouttechnology. We have demonstrated that it works in bothterminal emulators and in Web browsers, two very dierentenvironments.ere is no longer any reason to keep our programming

environments stuck in the 1970s. e Final Prey Printersupports today’s hardware and today’s text rendering tech-nology. And with its built-in extensibility, it also supportstomorrow’s.

AcknowledgmentsWe would like to thank Jon Sterling, Ryan Sco, Dan Fried-man, and Sam Tobin-Hochstadt for their feedback on drasof this paper, and Buddhika Chamith for talking with usabout Sinhala on computers.

References[1] Jean-Philippe Bernardy. 2017. Functional Pearl: a prey but not greedy

printer. In International Conference on Functional Programming. Toappear.

[2] Richard J. Boulton, Andrew Gordon, Michael J. C. Gordon, John Har-rison, John Herbert, and John Van Tassel. 1992. Experience withEmbedding Hardware Description Languages in HOL. In eoremProvers in Circuit Design. North-Holland Publishing Co.

[3] Edwin Brady. 2013. Idris, a General Purpose Dependently TypedProgramming Language: Design and Implementation. Journal ofFunctional Programming 23, 05 (9 2013).

[4] Jacques Caree, Oleg Kiselyov, and Chung chieh Shan. 2009. Finallytagless, partially evaluated: tagless staged interpreters for simplertyped languages. Journal of Functional Programming 19, 5 (2009).

[5] Olaf Chitil. 2001. Prey Printing with Lazy Dequeues. In 2001 HaskellWorkshop, Ralf Hinze (Ed.). Firenze, Italy. Universiteit Utrecht UU-CS-2001-23. Final Proceedings to appear in ENTCS 59(2).

[6] Olaf Chitil. 2005. Prey printing with lazy dequeues. Transactions onProgramming Languages and Systems (TOPLAS) 27, 1 (January 2005).

[7] Eugene Charles Ciccarelli. 1984. Presentation Based User Interfaces.Technical Report 794. Massachuses Institute of Technology ArticialIntelligence Laboratory.

[8] Cyril Cohen, ierry Coquand, Simon Huber, and Anders Mörtberg.2016. Cubical Type eory: a constructive interpretation of the univa-lence axiom. ArXiv e-prints (2016). hps://arxiv.org/abs/1611.02108.

[9] Robert L. Constable, Stuart F. Allen, H. M. Bromley, W. R. Cleaveland,J. F. Cremer, R. W. Harper, Douglas J. Howe, T. B. Knoblock, N. P.Mendler, P. Panangaden, James T. Sasaki, and Sco F. Smith. 1986.Implementing Mathematics with the Nuprl Proof Development System.Prentice-Hall, NJ.

[10] Nils Anders Danielsson. 2013. Correct-by-construction prey-printing.In 2013 Workshop on Dependently-typed Programming (DTP ’13). ACM.

[11] Richard P. Gabriel, Nickieben Bourbarki, Mahieu Devin, PatrickDussud, David Gray, and Harlan B. Sexton. 1990. Foundation for aC++ Programming Environment. In Proceeding of C++ at Work.

[12] Adele Goldberg and David Robson. 1983. Smalltalk-80: e Languageand Its Implementation. Addison-Wesley Longman Publishing Co.,Inc., Boston, MA, USA.

[13] Ira Goldstein. 1973. Prey-Printing: Converting List to Linear Struc-ture. Articial Intelligence Memo 279. Massachuses Institute ofTechnology.

[14] Paul Hudak. 1996. Building domain-specic embedded languages.ACM Computing Survey 28, 4es (Dec. 1996).

[15] John Hughes. 1995. e Design of a Prey-printing Library. In Ad-vanced Functional Programming, First International Spring School onAdvanced Functional Programming Techniques, Båstad, Sweden, May24-30, 1995, Tutorial Text.

[16] Sheng Liang, Paul Hudak, and Mark Jones. 1995. Monad Transformersand Modular Interpreters. In Principles of Programming Languages(POPL ’95). ACM, New York, NY, USA.

[17] Sco McKay. 1991. CLIM: e Common Lisp Interface Manager. Com-mun. ACM 34, 9 (Sept. 1991).

[18] Sco McKay, William York, and Michael McMahon. 1989. A Presen-tation Manager Based on Application Semantics. In User InterfaceSoware and Technology (UIST ’89). ACM.

[19] Derek C. Oppen. 1980. Preyprinting. ACM Trans. Program. Lang.Syst. 2, 4 (1980).

[20] Ramana Rao, William M. York, and Dennis Doughty. 1990. A GuidedTour of the Common Lisp Interface Manager. SIGPLAN Lisp PointersIV, 1 (July 1990).

[21] Randall B. Smith, John Maloney, and David Ungar. 1995. e Self-4.0User Interface: Manifesting a System-wide Vision of Concreteness,Uniformity, and Flexibility. In Object-oriented Programming Systems,Languages, and Applications (OOPSLA ’95). ACM, New York, NY, USA.

[22] S. Doaitse Swierstra and Olaf Chitil. 2009. Linear, bounded, functionalprey-printing. Journal of Functional Programming 19, 01 (2009).

[23] David Ungar and Randall B. Smith. 1991. SELF:e power of simplicity.LISP and Symbolic Computation 4, 3 (1991).

[24] Philip Wadler. 1992. e Essence of Functional Programming. Invitedtalk. (January 1992). 19th Symposium on Principles of ProgrammingLanguages.

[25] Philip Wadler. 2003. A preier printer. In e Fun of Programming: ASymposium in Honor of Professor Richard Bird’s 60th Birthday. Oxford.

12

https://arxiv.org/abs/1611.02108

Abstract1 Introduction2 Challenges and Opportunities2.1 Unicode2.2 Interactive environments2.3 Rendering to the Web2.4 Interactive documents

3 Core Library3.1 Lines, Widths, and Formatting3.2 Pretty Printing3.3 Grouping3.4 Indentation3.5 Instantiating the Interface

4 Semantic Annotations5 Extensions5.1 Variable Environments5.2 Operator Precedence and Associativity

6 Performance7 Correctness7.1 Prior Work7.2 Our Work7.3 Monad Laws7.4 Pretty Printing Laws from Monad Laws

8 Related Work9 ConclusionAcknowledgmentsReferences

The Final Pretty Printer -...

Documents

Transcript of The Final Pretty Printer -...