I’m trying to understand how equality is defined in Haskell typeclass laws. For example, the Monoid typeclass has a law that says x <> mempty = mempty <> x = x. But what does that = really mean?
It’s not the same as == from the Eq typeclass. I’ve looked everywhere for an official explanation:
The Haskell 2010 report doesn’t mention laws at all
Other Haskell users think it means extensional equality, but nobody has a solid source
The Haskell wiki says it’s extensional for monads, but doesn’t explain why
Is there any official rule about what = means in these laws? Are there any weird cases where it means something totally different?
Also, how do you handle extensional equality for tricky types like IO a? It seems really hard to define.
Here’s a simple example to illustrate the question:
class MyClass a where
doThing :: a -> a
-- Law: doThing (doThing x) = doThing x
-- But what exactly does that '=' mean?
The ‘=’ in typeclass laws is a thorny issue that’s caused me plenty of headaches. From what I’ve gathered through years of Haskell programming, it’s best understood as a form of observational equivalence. This means the expressions on both sides should behave identically in any context where they might be used.
For most types, this aligns closely with extensional equality. However, for effectful computations like IO, it becomes more about equivalent observable outcomes. This interpretation isn’t perfect, but it’s a pragmatic approach that’s served me well in practice.
Ultimately, these laws are guidelines to help us reason about code behavior, not rigid mathematical proofs. They’re invaluable for designing robust abstractions, even if their formal underpinnings aren’t always crystal clear.
I’ve wrestled with this question too. In my experience, the ‘=’ in typeclass laws is more about behavioral equivalence than strict equality. It’s saying the expressions should be indistinguishable in any context where you’d use them.
For IO actions, it gets tricky. I’ve found it helpful to think about it in terms of observable effects—two IO actions would be considered ‘equal’ if they produce the same side effects and results when executed.
That said, there’s some hand-waving involved. The laws act as guidelines to help reason about code behavior rather than as formal guarantees. In practice, I focus on adhering to the spirit of the laws, despite the challenges of strict formalization.
oh man, this one’s kinda confusing! i’d say ‘=’ is more about showing that diff expressions yield similar behavior rather than strict equality. for IO, it becomes murky, no perfect explanation as of now.