[Haskell-cafe] Re: Why?

[Dan Doel]

On Friday 11 December 2009 3:24:03 am pbrowne wrote:
> The issue of *purity* in Haskell and this thread has confused me.
> 
> At value level (not type level) is this linked with *equational reasoning*?
> Are the operational semantics of Haskell similar but not the same as
> equational logic?
> 
> Why are theorem provers such as Haskabelle need?
> http://www.mail-archive.com/haskell-cafe@haskell.org/msg64843.html

The use of equational reasoning in a language like Haskell (as advocated by, 
say, Richard Bird) is that of writing down naive programs, and transforming 
them by equational laws into more efficient programs. Simple examples of this 
are fusion laws for maps and folds, so if we have:

    foo = foldr f z . map g . map h

we can deforest it like so:

    foldr f z . map g . map h
      = (map f . map g = map (f . g))
    foldr f z . map (g . h)
      = (foldr f z . map g = foldr (f . g) z)
    foldr (f . g . h) z

now, this example is so simple that GHC can do it automatically, and that's a 
side benefit: a sufficiently smart compiler can use arbitrarily complex 
equational rules to optimize your program. But, for instance, Bird (I think) 
has a functional pearl paper on incrementally optimizing a sudoku solver* 
using equational reasoning such as this.

Now, you can still do this process in an impure language, but impurity ruins 
most of these equations. It is not true that:

    map f . map g = map (f . g)

if f and g are not pure, because if f has side effects represented by S, and g 
has side effects represented by T, then the left hand side has side effects 
like:

    T T T ... S S S ...

while the right hand side has side effects like:

    T S T S T S ...

so the equation does not hold.

This is all, of course, tweaking programs using equational rules you've 
checked by hand. Theorem provers are for getting machines to check your 
proofs.

Hope that helps.
-- Dan

* If you check the haskell wiki page on sudoku solvers, there's an entry 
something like 'sudoku ala Bird', written by someone else (Graham Hutton, 
comes to mind), that demonstrates using Bird's method.