= Monad =
{{{Maybe}}} is merely an Algebraic Data Type (''Either of'' type AKA ''Sum'' type).
To be ''of'' the {{{Maybe}}} ''type'' is to be ''Either Nothing'' or ''Just something'' - {{{data Maybe a = Nothing | Just a}}}
{{{Maybe Monad}}} is a ''data type'' together with implementation of two function.
To be a {{{Monad}}} is to implement {{{return :: a -> m a}}} and {{{(>>=) :: m a -> (a -> m b) -> m b}}}
{{{List}}} is just a ''recursive'' Algebraic Data Type
A {{{List}}} is ''Either Empty'' or a ''List of something'' - {{{data [] a = [] | a : [a]}}}
{{{List Monad}}} is a {{{List}}} type '''and''' implementation of {{{return}}} and {{{>>=}}}
To be a {{{Monad}}} is to implement {{{return :: a -> m a}}} and {{{(>>=) :: m a -> (a -> m b) -> m b}}}
...
Just this, a ''Type'' and an ''Interface'' together. Type itself '''is not a Monad'''!. ''Interface'' itself '''is not a Monad'''. The ''type-class'' (''type-trait'') which includes an ''interface'' and ''type-constructors'' is.
The ''interface'' implements explicit strongly-typed transition for a ''lazy language'', which is ''implicit in a eager languages'' and corresponds to {{{;}}}. In a context of a strict (non-lazy) language this interface is an '''unnecessary wrapping''', similar to {{{if x then True else False}}}.
Fucking this and only this.
=== An abstract view - a high-order type, a super-type ===
merely a generalized (and well-defined) super-category - a ''nested'' type (a super-type) which must satisfy certain ''composition laws'' - usually termed (wrongly) as a ''higher-level abstraction''.
Nothing to see here.
== Precisely ==
A Monad is a second-order (higher-order) type. A type of types. A ''type-tagged type''. Literally.
It forms a ''type-class'' with a ''type-constructor'', applying (instantiation) of which to a ''type'' produces a new type.
Thus, a ''value'' bound to the symbol {{{x}}} of type {{{a}}} is just the ''type-tag'' {{{a}}} attached to the symbol {{{x}}} in so-called static environment.
A value of the type {{{m a}}} is a ''type-tag'' {{{a}}}, type-tagged with additional tag {{{m}}}. So, {{{m a}}} are nothing, but two nested types - {{{m}}} of {{{a}}}.
Just this.
{{{M >>= λx.N}}}
* {{{M}}} is an ''expression'' of type {{{m a}}}
* {{{N}}} is an ''expression'' of type {{{m b}}}, which could be the same type as {{{m a}}} or different
* {{{x}}} is a ''value'' of type {{{a}}} (the extra type-tag {{{m}}} has been stripped off).
* {{{λx.N}}} is a ''lambda'' which has type {{{a -> m b}}} ({{{x}}} to be substituted with an actual value in the body of {{{N}}})
* the type of whole thing is {{{m b}}}
{{{λx.N}}}
is ''semantically'' equivalent to
{{{#!haskell
(\x -> N) M
}}}
which in turn is equivalent to
{{{#!haskell
let a = M in N
}}}
Both {{{lambda}}} and {{{let}}} introduce a ''local binding'', and semantically, {{{let}}} is an ''implicit'' {{{lambda}}} plus invocation.
{{{#!scheme
(let ((x 2)) (+ 1 x))
}}}
is
{{{#!scheme
((lambda (x) (+ 1 x)) 2)
}}}
So far, there is nothing but wrapping and unwrapping of values. Remove a type-tag, evaluate an expression, attach a type-tag to the value being {{{return}}}ed.
No more, no less.
== Nested lambdas ==
Nested {{{let}}}s are nested {{{lambda}}}s
{{{#!scheme
(let ((a 1)
(b 2))
(+ a b))
}}}
is semantically equivalent to
{{{#!scheme
(((lambda (a) (lambda (b) (+ a b))) 1) 2)
}}}
which is just a ''curried'' procedure
{{{#!sml
(fn a => fn b => a+b) 1 2
}}}
or
{{{#!sml
let val a = 1
in
let val b = 2
in
a + b
end
end
}}}
Nothing more than nested {{{lambda}}}s.
== Composition ==
for composition to work we need ''associativity'' or ''laws''
{{{#!haskell
}}}
== What it takes to be a Monad ==
To ''be a Monad'' is to implement at least two functions - {{{return}}} and {{{>>=}}} with certain ''signatures'' with follow the protocol (monadic laws) to ensure ''composability''.
{{{#!haskell
return :: a -> m a
}}}
and
{{{#!haskell
(>>=) :: m a -> (a -> m b) -> m b
infixl 1 >>=
}}}
respectively.
== Why? ==
Monadic code is ''generic'', so it could be evaluated no matter ''which particular instance of monad'' is given. The "details" are encapsulated inside {{{(>=)}}} - "compose", and {{{>>}}} - "chain".
No more, no less. Too ''explicit'' wrapping and composition.
== Algebraic Data Types type-tagged as a Monad ==
This is what it is for. ''Sum Types'' (disjoint unions) and ''Product Types'' (structured data) could be wrapped in a ''Monad''.
== State modeled as a Tuple ==
A state being passed explicitly through function composition (as a parameter) is "safe".
== Nesting as the way to Establish Order Of Evaluation ==
Sequential ''function composition'' {{{(f . g . h) x}}} could be viewed as an instance of {{{Monad}}}, however it is already ''completely or totally'' defined using ''nesting'' {{{f(g(h(x)))}}}, which ''implies'' the notion of an ''Order Of Evaluation'' - ({{{h(x)}}} to be evaluated first) in a lazy language.
There is no surprise that monadic composition (using {{{>>=}}} or {{{>>}}} and so called ''do-notation'') is ''desugared'' into a bunch of nested {{{lambda}}}s. This is precisely what a monadic composition is - ''wrapped (tagged with an extra type-tag) nesting of lambdas''.
== Unnecessary Wrapping ==
For a strict (''call-by-value'') languages all the Monadic code is merely ''unnecessary function wrapping'' the way {{{\x -> x}}} is just {{{x}}} or {{{if E then true else false}}} is just {{{E}}}
== Encapsulation of Effects ==
For a lazy (''call-by-need'') language Monadic composition allows to ''explicitly define the order of evaluation'' of a compound expression (implemented as nested {{{lambda}}}s), which is required for serialization of IO, and (orthogonally) to ''encapsulate an effect'' inside a specialized implementation of {{{>>=}}} or {{{>>}}} and to ''encapsulate a state'' as an ''explicit'' parameter being passed through the compound expression (monadic composition).
== Too Explicit Sequential Composition ==
any {{{Sequence}}} (a ''recursive sum-type'') could be wrapped into a {{{Monad}}} (implemented as an instance of a {{{Monad}}}) but this would be an unnecessary wrapping in the context of a strict (call-by-value) language.
a {{{List}}} (a sequential composition of values) could be viewed as an instance of {{{Monad}}} (while it is just a {{{cons}}} of a value a and another {{{List}}})
== Building on top of this ==
A notion of {{{map}}}ping of a function {{{f}}} on values (of type {{{a -> b}}}) over a value wrapped in a {{{Monad}}} (of type {{{m a}}}), which is similar to {{{map}}}ping a function over a singleton {{{List}}}.
Notice how the {{{map}}} function evaluates {{{m}}} (''unwraps'' {{{m}}}) using {{{>>=}}} and lifts (wraps) a value back into a {{{Monad}}} using {{{return}}} (delegation)
{{{#!haskell
map :: (a -> b) -> m a -> m b
map f m = m >>= \x -> return (f x)
}}}
Partially applied {{{map}}} yield a function on Monads {{{m a -> m b}}} (lifting)
This is the notion of {{{flatten}}}ing.
Notice how {{{join}}} ''evaluates'' {{{z}}} (''unwraps one'' {{{m}}}) using {{{>>=}}} (delegation)
{{{#!haskell
join :: Monad m => m (m a) -> m a
join z = z >= \x -> x -- just id
}}}