Imagine a layered structure with different levels of abstraction. It is not a 2d structure, not even a hierarchy, like a tree - there is no notion of a dimension. Imagine a 15 different axis, being orthogonal (having nothing in common with each other). We cannot (because we are conditioned by the shared environment to think in only 3 dimensions, but actually there are none).
So, the only notion we have is an abstraction boundary, sort of a cell membrane of an abstraction, if you wish, with various pumps and triggered gates (interfaces).
The best abstraction we have is a Set which is the notion of a collection (a cloud) of unique items. There is one cloud and another cloud. Most of the time they have nothing in common, but sometimes they intersect, or even morph together, so one is sitting inside of the other (a subset). Eukaryotic cells, if you wish.
For sane people all the categories or classes are merely sets.
A type is a set of values (a cloud), defined (formed) by a set of possible operations (an interface) over values. A filter, if you wish.
A type-class is a definition of the set of possible operations and laws (a protocol). No more, no less.
We use our natural language to say "that-thing of something" - a list of names, a pile of apples, a stack of books.
Names, books, or even apples is a category (a general notion over particular things). General is not abstract, by the way''
So, a list, a stack and a pile are general notions which are labeled in our natural human languages with a distinct sound (a word). And we could say: a pile of apples, a list of names, a stack of books, or just a
list of _, a
pile of _, a
stack of _
To define what it takes to be a
list, or what it takes to be a
stack, or what it takes to be a
pile. is what type-classes are all about. It is a precise, formal answer to the questions like "what is a list?", "what is a stack?", "what is a pile?".
We denote it syntactically as
 a - "list of a" or which is more convenient syntax
[a], which conveys the general notion a
list of As.
Even more generally, we could say a
XX of _ which would mean a named well-defined notion (we usually call such thing a class) of some other general notion.
Notice that we are only talking about how our human languages evolved to describe reality, what is. We've captured here a certain pattern - This of that or
f of x or just
f x. Notice that it looks exactly like an application of a function, and it is indeed an application of one notion to another notion, or what people call "generic functions". More about this later.
Notice that there is no bullshit - we are not talking about abstract categories, higher dimensions, monoids, semigroups, etc. No bulshit. We are talking about what is real.
Last but not least, the recursive property of human languages gives us "a list of names of books in the stack" or "a list of lists of names of books", etc. General notions could be nested (composed).
Types are abstract names. A type consists of a set of values restricted by a set of functions which define the boundaries of the set. That set of functions (an interface) could be thought as a filter - values which could pass through the filter are members of the set. That is it.
A named interface which defines the criteria (filter) for values - this is what a type is technically.
A named protocol (a set of "laws" and functions) is a type-class. It defines what is takes for _ to be a _.
Nothing but a set defined by an interface _, which implements a protocol _.
- type-classes are templates of types
Polymorphic types (which are defined as type-classes) are parametrized (by type-variables)
- they describe families of types, such as a
Just nested filters. A filtering (narrowing down) pipeline. Two or more nested filters (functions) is a pipeline. So, when we apply one notion to another we actually nest types. Nesting is a composition.
This precisely what is defined by
instance (Eq a) => Eq [a] where  ==  = True (x:xs) == (y:ys) = (x == y) && (xs == ys)
[a] (a list of As) to be
Eq is to implement the
(==) function, in terms of the function
(==) defined for values - the members of the
Eq a set.
To see nesting of notions (types) clearly just rewrite
Eq [a] as
Eq  a - Equality of Lists of As. The notion of Equality applied to the notion of a List of As, which must be themselves Equable. Remarcably,
of in English is right-associative.
There are few orthogonal notions involved in the concept of a Monad as it is being discussed in the context of CS, and lazy pure-functional language such as Haskell, so it produced a pile, or rather a cathedral of bullshit, similar to Kundalini.
The notion it captures is rising to a higher level of abstraction, or rather switching to a different level of abstraction, since most of the time the new abstraction (a new type) is more restricted (has less functions and laws in its protocol) than it was before.
It is similar to coercion of numeric types but more general. The crucial difference is that numeric coercion changes the actual value and its type, while in the case of a monad we have type-application (or nesting of types) - promotion of a type into another type. The good operational definition would be changing or switching of the implicit context (hello, Scala!). Merely this.
The usage of an abstraction is its concretization or a specialization defined by a concrete implementation.
Monad is defined as a type-class in the first place. This means it is a second-order abstraction (generalization over) types. This means that the domain and range of it are types. It is only applicable to types and it produces types as a result. It is mere a type-class, which defines a specialized ADT. That is it.
The second notion is explicit sequencing in a lazy pure-functional language. This makes sense only in the context of static typing.
It is stated that the minimal sufficient definition is to have
(>>=) implemented. This is bullshit. This is as an instance of a Monad to implement an explicit transition from one state to another. This is usage of the concept of a Monad, a specialization. With this understanding everything falls to its places.
To my view a monad is defined by
return which should be called a
@x in Lisps.
It is even better to define it in terms of type-signatures only
a -> M a and
M a -> a Transition from one state to another
m a -> (a -> m b) -> m b is an orthogonal notion and has been included as definitive one because it has been originated in some abstract category theory - another cathedral of bulshit.
A Monad type-class has been used to promote (or rather downcast) an expression from the realm of pure ones (pure ideas!) of mathematics to the lower planes of the Mundane Real World. To distinguish impure expressions, which will be polluted by the mundane world of lower realms, such an expression has to be put inside of a condom, a type-condom, if you wish, to perform an interaction with the dirty and sinful World outside of the Universe of Ideas.
All the action happens on the type level. Once an expression has been promoted to a certain monadic type (an ADT), it now implicitly carries with it a corresponding dictionary of implementations of the functions which defines what it takes to be a value of this ADT (instance of this type-class).
The type-checker ensures (guarantees) that only these overloaded functions could be applied to values of the type, by ruling out any ill-typed expressions involving
M a - All other functions simply do not have the
M a type in its signature, so they cannot be applied in principle.
This enforced by the type-checker restriction to a small set of functions which defines a type-class is used to implement explicit serialization and even atomic operations by explicitly passing the context of computation, so literally no one has any other reference to it. Explicit Whole-World-Passing-Style, or a explicit context-passing style for mere mortals. This is how STM works.
Now lets go back to
(>>=) which is the source of all the bullshit.
Lets read its type -
m a -> (a -> m b) -> m b. It says, given a value of the type
m a and the function from a to m b
a -> m b, the result of the application will be a value of type
m b. What the hell is this?
Well, this is precisely the one step of evaluation of function in a lazy settings (call-by-name pure functional language). The first
m a is just a thunk in which every value in a lazy language is implicitly wrapped. This is how laziness is implemented - with thunks (All you need is Lambda!). In order to apply some function to a value we have to take it out of the thunk first. This is what the first
m a corresponds to.
Evaluation of a thunk corresponds to forcing the value out of it, and is done implicitly by the evaluator, so no
splice function is needed.
a -> m b is actually an ordinary function from
b but in the lazy settings the actual evaluation is delayed, and a new thunk
m b is returned instead.
This is what the type-signature of
(>>=) means. This is why it is the central notion in the concept of a Monad in Haskell, specialized to a single step of evaluation of an expression in a lazy setting. This is a single step of a lazy evaluation abstracted out and implemented as a type-class.
A special, promoted (or rather down-casted) evaluation step is what a Monad is in Haskell. This
(>>=) generic function abstracts out a single evaluation, is and used to define and implement an explicit transition from one state to another or an absence of a value
Maybe - option type, or choice - this or that, or any specialized evaluation step you need, including interacting with that dirty sinful mundane reality as it is.
Technically, an ordinary function must explicitly use the overloaded
return :: a -> m a function as its last expression, so the corresponding implementation will be selected from an implicit dictionary for the concrete instance of a type-class.
Look, ma, no category theory bullshit!
In a strict statically typed language, such as Scala implicit contexts and strict interfaces is enough, so in an imaginary mortal combat fight between mr. Odersky and mr. Peyton-Jones mr. Odersky is the winner by resisting to incorporate irrelevant bullshit into Scala when implicits and type-classes are sufficient.
This, by the way, not in the least impoverishes the cleverness of the idea of abstracting out a single step of evaluation in a lazy language as a "higher order abstraction" and implement it as a type-class, so the static type-checker will protect every pure function these risky expressions by wrapping them in a type-safe condoms.
I hope someday Go will embrace implicits and type-classes, but no Monads, Functors and all that crap.