[Agda] PrettyPrint.agda

[Nils Anders Danielsson]

On Tue, Aug 26, 2008 at 08:42, Yoriyuki Yamagata
<yoriyuki.yamagata at aist.go.jp> wrote:
>
> I have translated Haskell's Pretty Printing library
> (Text.PrettyPrint.HughesPJ) to Agda.

Nice to see a library contribution.

> I welcome any opinion!

Do you need to use impossible/undefined in the code? Maybe some
invariants should be strengthened.

There are a number of pretty-printing libraries for Haskell. Some of
them are documented in these papers:

  Hughes/Peyton Jones:
  http://www.cs.chalmers.se/~rjmh/Papers/pretty.ps
  http://hackage.haskell.org/cgi-bin/hackage-scripts/package/pretty

  Wadler/Leijen:
  http://homepages.inf.ed.ac.uk/wadler/topics/language-design.html#prettier
  http://hackage.haskell.org/cgi-bin/hackage-scripts/package/wl-pprint

  Chitil:
  http://www.cs.kent.ac.uk/pubs/2005/2062/index.html
  http://www.cs.kent.ac.uk/pubs/2005/2366/index.html

  Swierstra:
  http://igitur-archive.library.uu.nl/math/2006-1220-202636/UUindex.html

Maybe some of the newer libraries are easier to use, or easier to
implement in a total language.

-- 
/NAD