[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: [email protected]
Homepage: http://www.joachim-breitner.de
Jabber-ID: [email protected]
signature.asc
Description: This is a digitally signed message part
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
