Ryan Newton wrote:
Here are some examples:

data Foo = Bar | Baz

instance Eq Foo where
  _ == _ = True

instance Ord Foo where
  compare Bar Bar = EQ
  compare Bar Baz = LT
  compare _   _   = error "I'm partial!"

These would allow LVish's "runPar" to non-determinstically return Bar or
Baz (thinking they're the same based on Eq).  Or it would allow runPar to
nondeterministically crash based on different schedulings hitting the
compare error or not [1].


[1] If you're curious why this happens, its because the Ord instance is
used by, say, Data.Set and Data.Map for the keys.  If you're inserting
elements in an arbitrary order, the final contents ARE deterministic, but
the comparisons that are done along the way ARE NOT.

I'm not sure whether the Eq instance you mention is actually incorrect. I had always understood that Eq denotes an equivalence relation, not necessarily equality on the constructor level.

One prominent example would be equality of Data.Map itself: two maps are "equal" if they contain the same key-value pairs,

    map1 == map2  <=>  toAscList map1 == toAscList map2

but that doesn't mean that their internal representation -- the balanced tree -- is the same. Virtually all exported operations in Data.Map preserve this equivalence, but the library is, in principle, still able to distinguish "equal" maps.

In other words, equality of abstract data types is different from equality of algebraic data types (constructors). I don't think you'll ever be able to avoid this proof obligation that the public API of an abstract data type preserves equivalence, so that LVish will yield "results that are deterministic up to equivalence".

However, you are mainly focused on equality of keys for a Map. In this case, it might be possible to move towards pointer equality and use things like Hashable or StableName .

Best regards,
Heinrich Apfelmus


Haskell-Cafe mailing list

Reply via email to