[Haskell-cafe] Re: Why?

pbrowne Patrick.Browne at comp.dit.ie
Fri Dec 11 12:04:08 EST 2009


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.




More information about the Haskell-Cafe mailing list