[Haskell-cafe] Re: Why?
lrpalmer at gmail.com
Fri Dec 11 13:06:39 EST 2009
On Fri, Dec 11, 2009 at 10:04 AM, pbrowne <Patrick.Browne at comp.dit.ie> wrote:
> 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
> 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 admit that I don't fully know what you are talking about. What do
you mean by logical meaning -- as opposed to what other sort of
The equational reasoning in Haskell comes from its denotational
semantics (which, mind, is not completely formally specified -- but
once you expand typeclasses to dictionary passing style, you get a
standard DCPO semantics). If terms are equal in denotation, then they
are equal by observation (modulo efficiency).
So it is not equations that directly define the semantics of Haskell,
but rather mapping the syntax to mathematical objects. We derive
Haskell's equational reasoning from the equational reasoning in the
That's how I see it as a user of the language. At the most abstract
level, omitting some of the practical details of the language (such as
the built-in numeric types), Haskell's reduction follows beta
reduction with sharing, and so at that level I think the answer to (2)
> 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.
>  http://rewriting.loria.fr/documents/plaisted.ps.gz
>  http://www.eecs.ucf.edu/~leavens/JML/
> 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe