[Haskell-cafe] Is (==) commutative?
Christian Sternagel
c.sternagel at gmail.com
Wed Jul 25 03:19:17 CEST 2012
Dear all,
Thanks for your replies. Just to clarify: I am fully aware that inside
Haskell there is no guarantee that certain (intended) requirements on
type class instances are satisfied. I was asking whether the intention
for Eq is that (==) is commutative, because if it was, I would require
that as an axiom for the equivalent of Eq in our formal setting (I'm
using the proof assistant Isabelle/HOLCF [1]). Afterwards only types for
which one could prove commutativity could be instances of Eq. But if
there where already "standard" instances which violated this
requirement, adding it in the formal setting would prevent it from being
applicable to "standard" Haskell programs.
Btw: Isabelle/HOLCF unifies all error values and nontermination in a
single bottom element _|_. Currently we are using the following axioms
for our formal Eq class (where I'm using Haskell syntax although the
real sources [2] use Isabelle/HOLCF syntax which is slightly different;
(=) is meta-equality).
(x == y) = True ==> x = y
(x == y) = False ==> not (x = y)
(x == _|_) = _|_
(_|_ == y) = _|_
Those axioms state that (==) is sound w.r.t. to meta-equality and strict
in both it's arguments. The question is whether we should also add.
(x == y) = _|_ ==> (y == x) = _|_
Which would directly imply
(x == y) = (y == x)
cheers
chris
[1] http://isabelle.in.tum.de (and
http://isabelle.in.tum.de/dist/library/HOL/HOLCF/)
[2] http://sourceforge.net/p/holcf-prelude
More information about the Haskell-Cafe
mailing list