[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@joachim-breitner.de Homepage: http://www.joachim-breitner.de Jabber-ID: nomeata@joachim-breitner.de