liese

[ləˈiːs]

Grad student in CS. Monotropic nerd who spends way too much time with computers (and books (and computer books)). Likes space.



prophet
@prophet

When I first learned Haskell, one of the first habits I picked up was adding deriving (Show, Eq) to every type definition I write.
Eventually I added Generic to this list, but if you looked at my code now, you wouldn't find Eq in there anymore.

To motivate this I'm going to start off with a pretty strong claim: deep equality checking is almost never actually what you want.

If you ever talked to someone working with dependent types, they probably talked your ear off about equality and they probably had a point, but that's not the kind of equality we're talking about here.
(==) is not a property you can use in proofs or anything like that, it's just a function that lets you check at runtime if two things are equal.
Now I want you to ask yourself: how often do you actually need this operation on interesting data types?

Integers? Sure.
Strings? Yes, although if you're doing it a lot you should probably intern your strings anyway.
But beyond that? There's really not a lot.

On the flip side, deep equality (the kind deriving Eq generates) is linear in the size of your data and a great way to kill your performance.
I work on compilers a lot and I deliberately make sure to never derive Eq on syntax trees because checking those for equality is probably the easiest way to create quadratic runtime behavior.


You must log in to comment.

in reply to @prophet's post:

I think I agree in application code, but how about test code? Being able to pose input-output specifications, i.e. f x == y, seems not only useful but important. Do you prefer to write equality predicates by hand for this purpose, or do you do verification in other ways? (Personally, I'm very accustomed to writing proofs in Agda, and I wouldn't be writing unit tests in those situations. But it seems like an important use-case!)

it's true that Eq Double is not law-abiding, and therefore Officially Speaking breaks all your proofs, but in my experience this one single special case has never been an issue in practice