[Haskell-cafe] Is (==) commutative?

[Joachim Breitner]

[Re-sent as my first post did not make it through.]

Hi Christian,

Am Mittwoch, den 25.07.2012, 10:19 +0900 schrieb Christian Sternagel:
> 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) = _|_

I am slightly worried about the latter two; after all one might find it
reasonable to specify

        instance Eq () where _ == _ = True
        
or, maybe slightly more sensible

        instance Eq Void where _ == _ = True

But I checked and both the instances of (), the instance of Data.Void
(in the void package) and the derived instance for empty data types are
strict:

Prelude> data V
Prelude> :set -XStandaloneDeriving
Prelude> deriving instance Eq V
Prelude> (error "1" :: V) == (error "2" :: V)
*** Exception: Void ==

Greetings,
Joachim


-- 
Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  Jabber-ID: nomeata at joachim-breitner.de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120726/033165b7/attachment.pgp>