Eq documentation: substitutivity
Summary
On the customary properties expected from Eq
, you can read:
Substitutivity: if x == y = True and f is a "public" function whose return type is an instance of Eq, then f x == f y = True
A "public" function is described as:
However, == is customarily expected to implement an equivalence relationship where two values comparing equal are indistinguishable by "public" functions, with a "public" function being one not allowing to see implementation details. For example, for a type representing non-normalised natural numbers modulo 100, a "public" function doesn't make the difference between 1 and 201.
Two things:
- I thought — but am not sure — this property is called «extensionality» (or maybe «function extensionality»)?
- I am not sure I understood what a public function is and moreover Haskell function are opaque, so the distinction seems not practically useful?
Proposed improvements or changes
Reword the second paragraph as
The Haskell Report defines no laws for Eq. However, it is expected to have the following properties:
and "Substitutivity" as
Extensionality: if x == y = True and f is a function whose return type is an instance of Eq, then f x == f y = True
I can provide a patch if everyone agrees these changes are sensible.