[Haskell-cafe] Re: Why?

[pbrowne]

pbrowne wrote:
> 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?

Pat



--------------------Reason (1)------------------
There are some equations that are not expressible in Haskell. Quoting form:
http://www.mail-archive.com/haskell-cafe@haskell.org/msg64843.html
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 [5]. 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.

--------------------Reason (2)------------------
According to Thompson [1] the equations in Miranda (and I assume
Haskell) are not pure mathematical equations due to *where* and other
reasons. According to Danielsson [2] 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.

--------------------Reason (3)------------------
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[3] and CafeOBJ[4] do).


[1]A Logic for Miranda, Revisited (1994) by Simon Thompson
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.149
[2] Fast and Loose Reasoning is Morally Correct - Danielsson, Hughes
http://citeseer.ist.psu.edu/733155.html
[3] http://maude.cs.uiuc.edu/
[4] http://www.ldl.jaist.ac.jp/cafeobj/
[5]Translating Haskell to Isabelle: Torrini, Lueth,Maeder,Mossakowski
http://es.cs.uni-kl.de/TPHOLs-2007/proceedings/B-178.pdf