[Haskell-cafe] Re: Why?
Patrick.Browne at comp.dit.ie
Fri Dec 11 12:04:08 EST 2009
>From your example, I can appreciate the value of purity. But I am still
unsure how close Haskell terms are to pure *equational logic*. The
operational semantics of languages like CafeOBJ are very close to
their intended logical semantics. CafeOBJ modules contain theories in
equational logic and evaluations can be considered as proof of these
>From your point-free example, it seems that the Haskell compiler can
perform *equational reasoning* to transform higher level (point) terms
into more efficient basic Haskell code. But my questions concerns the
precise semantics of this *basic* Haskell code.
1) Is this correspondence between operational and logical semantics a
desirable property of *purity* in the Haskell world?
2) What, if anything, prevents the execution of a Haskell term from
being a proof in equational logic?
It seems that Haskells type system has this logical purity
My motivation for such questions is that I am researching various
*algebraic styles* such as Haskell, OCAML, Maude, and CafeOBJ.
My current general research question is; how closely do executable terms
in these languages match their *logical* meaning. For example, languages
like Java need additional logical scaffolding (like JML) to give them
logical machine readable meaning.
I *guess* that the gap between operational and logical semantics is
rather less in Haskell that in Java, and I further *guess* that the gap
less again in Maude or CafeOBJ. I think a good answer to question 2)
would remove the *guess* from the Haskell case.
Dan Doel wrote:
> 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
> 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
> 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.
More information about the Haskell-Cafe