Duncan Coutts duncan.coutts at worc.ox.ac.uk
Thu Feb 12 07:18:28 EST 2009

On Tue, 2009-02-10 at 12:39 +0100, Henning Thielemann wrote:
> Heinrich Apfelmus schrieb:
> > Henning Thielemann wrote:
> >> I want for long to write math formulas in a paper in Haskell. Actually,
> >> lhs2TeX can do such transformations but it is quite limited in handling
> >> of parentheses and does not support more complicated transformations
> >> (transforming prefix notation in infix notation or vice versa with
> >> minimal parentheses).
> >>
> >> I would like to write
> >>   sumFor [0..n] (\i -> i^2)
> >>     (with sumFor xs f = sum \$ map f xs)
> >> which is rendered as
> >>   \sum_{i=0}^{n} i^2
> >> or
> >>   integrate 1000 (a,b) (\t -> f t)
> >> to be rendered as
> >>   \int_a^b f(t) \dif t
> >
> > Neat idea! Can't you do implement this as a DSL?
> >
> >     sumFor x xs f =
> >        "\sum_{" ++ x ++ "=" ++ head xs ++ "}^{" ++ last xs ++ "} "
> >        ++ f x
>
>
> My original idea was to use the formulas in papers both for typesetting
> and for unit testing. Thus, when you state that a function fulfills a
> law, that it can be automatically tested by QuickCheck, that this at
> least true for some instances.
> The same would be useful for Haddock documentation. I remember that
> someone proposed to permit Haddock to expose the implementation of some
> functions as examples or as unit-tests/laws. Now we could extend this
> idea to allow Haddock not only to expose the implementation of
> functions, but also to tell Haddock how to render its implementation.

If we want to tell haddock how to render an implementation, surely we
use a derivative of lhs2tex. It requires minimal markup in the standard
case (just spacing for alignment) and has a nice set of standard
presentation rules and allows extending that with formatting directives.

It would not let you write complex display mode maths like
\sum_{i=0}^{n} i^2
but for code, and laws and proofs that look mostly like code it's really
nice.

Duncan