The equations you've posted are laws that the instances of the Eq typeclass must satisfy. If someone creates an instance that does not satisfy all of the laws then the behavior is undefined. Laws are generally not present in the source code outside of the comments, and they typically can not be proved in standard Haskell.

I don't know why the documentation links are broken (bug in hackage?) but you can find the source links here: https://hackage.haskell.org/package/ghc-prim-0.7.0/docs/GHC-Classes.html

Many instances are automatically derived by the compiler (which is usually what you would do for your own data types) or are otherwise dependent on built-in primitives (e.g. eqInt, eqWord, etc.).


On Fri, Apr 2, 2021 at 8:38 AM Galaxy Being <borgauf@gmail.com> wrote:
While learning about type classes, I tried to find the actual source code for Eq. In my beginner books this much is typically given

class Eq a where
  (==), (/=) :: a -> a -> Bool

-- Minimal completion definition:
  x /= y = not (x == y)
  x == y = not (x /= y)


I then found this at hackage.haskell.org, but the "source" links are dead. On this page is a section of what I can't tell is either source code or just commentary on all the different mathematical ideas about equality, i.e., 

Reflexivity
x == x = True
Symmetry
x == y = y == x
Transitivity
if x == y && y == z = True, then x == z = True
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
Negation
x /= y = not (x == y)


I would like to know if this is indeed in the source code or if it's just a sort of commentary. It looks important. Where can I find the actual source for all these basic type classes?

LB
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.