[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