From your example, I can appreciate the value of purity. But I am still unsure how close Haskell terms are to pure *equational logic*[1]. The operational semantics of languages like CafeOBJ[1] are very close to
From your point-free example, it seems that the Haskell compiler can
Dan, their intended logical semantics. CafeOBJ modules contain theories in equational logic and evaluations can be considered as proof of these theories. 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. Two questions 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[4] 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[3]) 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. Pat [1] http://rewriting.loria.fr/documents/plaisted.ps.gz [2]http://www.forsoft.de/~rumpe/icse98-ws/tr/0202Diaconescu.ps [3] http://www.eecs.ucf.edu/~leavens/JML/ [4]http://www.haskell.org/haskellwiki/Type_arithmetic 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 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.