One of the most common gripes people have when learning Haskell is the fact that typeclass “laws” are only laws by convention, and aren’t enforced by the language and compiler. When asked why, the typical response is “Haskell can’t do that”, followed by a well-intentioned redirection to quickcheck or some other fuzzing library.
But, to any experienced Haskeller, “Haskell’s type system can’t express X” is always interpreted as a (personal) challenge.
GHC Haskell’s type system has been advanced enough to provide verified typeclasses for a long time, since the introduction of data kinds and associated types. And with the singletons library, it’s now as easy as ever.
(The code for this post is available here if you want to follow along! Some of the examples here involving
Demote and relying on its injectivity will only work with singletons HEAD, even though the necessary patches were made seven months ago1)
Not sure why it’s not on hackage yet, but I will update when it gets there!↩