Under what notion of equality are typeclass laws written?

user_4608364 0
Viewed 259

Haskell typeclasses often come with laws; for instance, instances of Monoid are expected to observe that x <> mempty = mempty <> x = x.

Typeclass laws are often written with single-equals (=) rather than double-equals (==). This suggests that the notion of equality used in typeclass laws is something other than that of Eq (which makes sense, since Eq is not a superclass of Monoid)

Searching around, I was unable to find any authoritative statement on the meaning of = in typeclass laws. For instance:

  • The Haskell 2010 report does not even contain the word "law" in it
  • Speaking with other Haskell users, most people seem to believe that = usually means extensional equality or substitution but is fundamentally context-dependent. Nobody provided any authoritative source for this claim.
  • The Haskell wiki article on monad laws states that = is extensional, but, again, fails to provide a source, and I wasn't able to track down any way to contact the author of the relevant edit.

The question, then: Is there any authoritative source on or standard for the semantics for = in typeclass laws? If so, what is it? Additionally, are there examples where the intended meaning of = is particularly exotic?

(As a side note, treating = extensionally can get tricky. For instance, there is a Monoid (IO a) instance, but it's not really clear what extensional equality of IO values looks like.)

equality haskell
3 Answers

I suspect most folks use = to mean "moral equality" as from Fast and Loose Reasoning is Morally Correct, which you can think of as extensional equality up to defined-ness.

But there's no hard-and-fast rule here. There's a lot of libraries, and a lot of authors, and if you take any two authors they probably have some minor detail about = on which they disagree.

user_7916040

Typeclass laws are not part of the Haskell language, so they are not subject to the same kind of language-theoretic semantic analysis as the language itself.

Instead, these laws are typically presented as an informal mathematical notation. Most presentations do not need a more detailed mathematical exposition, so they do not provide one.

comingstorm_2102110

I agree with comingstorm that the equality in those laws is that of a mathematical language. But I would also say that it is in the respect of the operator ==.

Why? Because == is supposed to implement mathematical equality.

For example, look at fractions (rational numbers). They can be implemented as pairs of integers with some rules. The pair (a, b) represents the fraction a/b. The pairs (a, b) and (c, d) represent the same rational number if a*d == b*c. The two pairs are then said to be equivalent, and we talk about an equivalence relation. In mathematics we let a rational number be an equivalence class of pairs under this equivalence. In programming we instead define the operator == to tell if two pairs are equivalent, i.e. if they represent the same fraction.

user_14125340
Related