Eradicating unlawful Eq & Ord instances, crustacean style

#1

I am exploring the concept of method-less typeclasses that would inherit from a superclass but signal more constraint on their subject. Rust does this™:

For example,


-- | Partial Equivalence Relation.
-- The laws are Symmetry and Transitivity.
class PartialEq a where
    (==), (/=)           :: a -> a -> Bool

    x /= y               = not (x == y)
    x == y              = not (x /= y)

-- | Total Equivalence Relation.
-- Two more laws are brought in:
-- * Reflexivity
-- * (==) and (/=) are strict inverses 
class PartialEq a => Eq a
-- Tumbleweeds…

And similarly, PartialOrd would take from PartialEq, and Ord would take from Eq and PartialOrd.

And we’d be able to say goodbye to those unlawful instances:

Screenshot_20221229_124214
Screenshot_20221229_1242141219×501 43 KB

I’m not advocating (right now) for changing the definitions of what we have in ghc-prim to match these, but if I were, I’d bring tooling on the table that could be easily used by everyday haskellers to automate the verification of those laws for their own instances.

3 Likes
Informal discussion about the progression of `base`
(... cont) Data.Set no Functor/Monad instance
#2

  • Why bring back (/=) as a method?

  • Suggestion: modify (0/0) and other mathematically-meaningless expressions to send the program into an infinite regression after any diagnostic message is displayed: a debugger can then be attached to the still-running program to examine its call stack.

Otherwise, let’s also add PartialMonad, PartialRead, PartialShow, etc…

(…by the way, floating-point arithmetic isn’t commutative - shall we also have a specialised variant of Num?)

#3

Perhaps PartialEq could allow for partial inverses? But it’s not really the point here.

Modify (0/0) and other mathematically-meaningless expressions to send the program into an infinite regression after any diagnostic message is displayed: a debugger can then be attached to the still-running program to examine its call stack.

Is there a question or is it more of a remark? And if yes, what do you expect me to say to this?

#4

I like the idea of method-less class for Eq (extending PartialEq), though I don’t think it would work for PartialOrd.
I don’t think it is possible to express lawful instances of partial order with just compare :: a -> a -> Ordering (what do we return when objects are incomparable?).
I like the design in Rust, where partial_ord from PartialOrd has this signature
fn partial_cmp(&self, other: &Rhs) -> Option<Ordering>;, where incomparable objects just returns None. We could copy that approach from Rust too.

The downside is that solution is that implementation of cmp in Ord needs to either repeat code or unsafely unwrap.

1 Like
#5

…if the objects or values really are incomparable, that would also seem to make testing for equality equally just as problematic, and requiring something like Maybe Bool instead of Bool as the result type of (==).

#6

Is this something Rust needs to deal with?

#7

I find PartialEq distasteful because realistically it exists solely to deal with NaN, and complicating things for the sake of one thing (especially floating point!) seems like a bad idea. Maybe there’s an example in another domain that showcases the general usability better?

(PartialOrd defining compare' :: a -> a -> Maybe Ordering, versus Ord defining compare :: a -> a -> Ordering, I could certainly get behind, but that’s not methodless.)

2 Likes
#8

You’re right, there isn’t much use of partial equality outside of IEEE 666754. That being said I believe it’s important that we remain truthful in our relationship with the real world, and isolate it wherever we can. Strict Partial Orders are certainly more interesting, algebraically speaking, but both have their value.

1 Like
#9
Informal discussion about the progression of `base`
#10

I’m a little discouraged that laws currently in Haskell are just comments in the code. It would be neat if laws were more of a first class language feature that could be marked lawful or unlawful on a per-instance basis, and then that could somehow indicate if a specific rewrite rule was safe or not to be used by the compiler.

#11

The One purpose of type classes is that you only opt into a type class if its instance is lawful. If you can’t write a lawful instance for a type, it shouldn’t have an instance at all. They are the mechanism by which we tell the compiler (and the user!) that certain transformations are possible or not.

2 Likes
#12

(Un)fortunately, Eq and Ord don’t even have laws… only “customary properties”.

Edit: Actually, upon review I see now that Ord should be a total ordering, so that does give laws. That seems like one of fhe few standard classes that do have laws.

#13

TBH, if people are implementing Eq without the standard properties of an equivalence relation [as always, excepting ieee754] then they are being naughty.

#14

I would also like to point to this previous discussion on Reddit:

I don’t have much experience with Rust, but we might actually want to check what their experience is. In that Reddit thread anydalch writes:

i think rust has proven this approach too unergonomic to be reasonable even in a language whose design goals skew much more towards Correctness than haskell’s

I wonder if Rust experts would agree.

Some other interesting suggestions. First by gilgamec:

even if you did this, you’d still have problems with nan. In order to avoid the problem, you would have to explicitly make partial functions, e.g.

class PartialEq a where 
  peq :: a -> a -> Maybe Bool
  pneq :: a -> a -> Maybe Bool

class PartialEq a => Eq a where 
  (==) :: a -> a -> Bool
  (==) a b = case peq a b of Just v -> b -- total by definition!

And by rampion:

I think you’d have an easier time with the “parse, don’t validate” approach, since then you wouldn’t need to shim in a whole new class, just a data type, which is way easier.

instance Eq ComparableDouble
instance Ord ComparableDouble
parseComparableDouble :: Double -> Maybe ComparableDouble
fromComparableDouble :: ComparableDouble -> Double

And by cartazio:

the real fix is to add support for signalling Nans and over time make that the default RTS flags. I’m working on that.

every other approach doesn’t really help anyone.

1 Like
#15

IEEE 754 does define a total order on Double. It’s just that Haskell compare (and min, and max) choose to implement gods know what instead of it.

1 Like
#16

But that doesn’t agree with the equality comparison. E.g. totalOrder -0 0 /= totalOrder 0 -0, but also -0 == 0.

1 Like
#17

The problem with law-only subclasses, as I see them:

  1. Type inference can lie to you. If you write an expression using functions from the superclass but relying on laws from the subclass, you must remember to write the more specific subclass in your constraints. It is no longer safe to let GHC infer the constraints for you.

  2. To avoid point (1), you have to invent new operators in the subclass, which is noisy and annoying.

That isn’t to say they should never be used, but I’d be very cautious about doing so with something as fundamental as Eq.

#18

While I don’t think that unlawful instances should generally be used at all, I do think that there’s a lot of interesting potential for having machine-readable specifications of type class laws. This could serve as a source of test suites, as a source of refactoring suggestions, and many more cool features.

2 Likes