Type-Classes

The Buddha emphasized the right (adequate, close to what actually is - as a correct map of a certain territory) understanding which is the essential prerequisite to end (or at least diminish) suffering.

The mapping tools, or a modeling framework is based on certain notions from Classical Logic and mathematical Set Theory. With these almost everything could be adequately modeled, to give one the right understanding, or, at least to be less wrong.

The mathematical notion of “such that” is a linguistic abstraction of the innate ability of the mind of an external observer select and group observable phenomena (“objects”) into abstract “categories” (or “classes”) based on a certain common property (an attribute) which all or some objects possess. This ability is at the core of so-called intelligence.

This “works” because the whole Universe is a single unfolding process, so every sub-process is subject to the Causality Principle (there is no randomness, only vastly complex causality) and everything evolves in an imaginary tree-like structures (if we attempt to mentally trace some process back).

In other words, patterns and attributes are there and they are due to causality.

In the context of a Set theory, which could be seen as a generalization and an attempt to formally define a few universal (for the mind and the world) notions, the imaginary, abstract, non-existent universe of “objects” of discourse (or of “values”) is being partitioned into a distinct partitions, called Sets, which are abstract “classes” (of the ancients) with a minimal “structure”.

In mathematics we write (using the set comprehension notation) \[\{x \in S \mid P(x)\}\] which means “the elements x of a given set S such that (the vertical bar) the predicate P is true for every x”.

The result form another Set - a subset of S, which may or may not be equivalent to S itself (when P(x) holds for all elements of S).

It is easy to see that the universal notions of selection (based on some property) and classification (which mind does) has been captured and formalized in this particular piece of mathematics (we do not consider the whole Set Theory here, because some parts of it contradict reality).

Such kind of selection (of “objects”) based on having a certain common property is also known as filtering, and indeed, we have this universal notion captured in a function:

filter p xs = [x | x <- xs, p x]

which is just a different notation for the set comprehension notion of mathematics.

It should be of no surprise that these universal notions are at the core of what we call type systems (or a type-discipline).

Types are just particular subsets of an imaginary Universe of all (possible) values (which we can denote in a given language).

The classic example is Numbers - some are Integers (whole numbers), some are Reals, and so on, as they all sit on an imaginary number line.

We (in our minds) partition this imaginary Universe Of All Possible Numbers into distinct Sets based on particular properties of such numbers. These sets are superimposed onto the set of all numbers.

Again, we just use the mathematical notion “such that” for partitioning.

A type-class is a notation for partitioning the imaginary Universe of All Possible Types (which are defined as just Sets of Values).

Remember that the word “class” has been used by ancient Greek logicians to refer to a particular “group” of “objects”, such as “men” (Socrates is a Man), and the word “set” has been introduce much later.

So, a type-class is just a particular Set of Types.

It is also based on the notion of “such that”, but instead of logical predicated it uses the notion “implements a given set of type-signatures”.

This captures the intuitive, informal notion of a “Duck Typing” - if it walks like a duck and quacks like a duck…

In theory, there should be a proof that every type actually implements a given set of type-signatures (which, by the way, is called an interface) correctly, but for that we need a proof-system.

A set of type-signatures is usually augmented by formally defined “laws” (stated elsewhere), such as associativity for a given operator. These “laws” should have been formally proven too.

Supplying a corresponding test-suite is not a proof, but it acts as self-test of an airplane - it shows that at least nothing is broken yet.

Last, but not least, just like Sets, these type-classes can be “nested”, and there is a special syntax to express it. Nesting means that “to be an X one has to be an Y”, which is just more specialization or more filtering.

So, when we see something like

class  Num a  where
    (+), (-), (*)       :: a -> a -> a
    negate              :: a -> a
    abs                 :: a -> a
    signum              :: a -> a
    fromInteger         :: Integer -> a

(which, by the way, corresponds to another mathematical notion of a Ring which includes associative and commutative binary operations with certain identities) we recognize a definition of a Subset of Types (tagged with the Num tag) “such that” this particular set inteface (a set of type-signatures) has to be implemented.

And that is it. This is why it feels so familiar and “natural”, and when Phil Wadler came up with his proposal, everyone were instantly enlightened - this is just types partitioned by interfaces instead of logical predicates.

I am not surprised that type-classes aren’t incorporated into any other decent languages of the ML-family, because people are arrogant and stupid.