[Haskell-cafe] Re: Why?
Patrick.Browne at comp.dit.ie
Sat Dec 12 09:08:11 EST 2009
> 2) What, if anything, prevents the execution of a Haskell term from
> being a proof in equational logic?
I have done some checking to try to answer my own question. The answer
*seems* to be that there *seems* to be three things that prevent Haskell
terms being true equations. Any feedback on these three reason would be
welcome. If they are valid reasons, what is their possible impact?
There are some equations that are not expressible in Haskell. Quoting form:
Is there any way to achieve such a proof in Haskell itself?
> GHC appears to reject equations such has
> mirror (mirror x) = x
> mirror (mirror(Node x y z)) = Node x y z
Eugene Kirpichov Fri, 25 Sep 2009 04:19:32 -0700
It is not possible at the value level, because Haskell does not
support dependent types and thus cannot express the type of the
proposition "forall a . forall x:Tree a, mirror (mirror x) = x", and
therefore a proof term also cannot be constructed.
Another example from . A partial order that is also linear is called
a total order. The class linorder of total orders is specified using the
usual total order axioms. Of course, such axiomatizations are not
possible in Haskell.
According to Thompson  the equations in Miranda (and I assume
Haskell) are not pure mathematical equations due to *where* and other
reasons. According to Danielsson  the fact that they are not always
structurally equations does not prevent functional programmers from
using them as if they were valid equations. Danielsson show that this
informal *fast and loose* use of equational axioms and theorems is
*morally correct*. In particular, it is impossible to transform a
terminating program into a looping one. These results justify the
informal reasoning that functional programmers use.
There is no formal specification for the meaning of a Haskell program
(i.e. its meaning is not defined in a logic). At the level of precise
logical specification and logical interoperability this could be a
problem (e.g. semantic web likes logic). This should not be a problem
for programming tasks, after all most languages like Java do not have a
formal semantic definition in logic (ML, Maude and CafeOBJ do).
A Logic for Miranda, Revisited (1994) by Simon Thompson
 Fast and Loose Reasoning is Morally Correct - Danielsson, Hughes
Translating Haskell to Isabelle: Torrini, Lueth,Maeder,Mossakowski
More information about the Haskell-Cafe