Dan, >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 their intended logical semantics. CafeOBJ modules contain theories in equational logic and evaluations can be considered as proof of these theories. >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.
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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
