`α, β, γ, ...`

as variables over types. We'll
use `P`, `Q`, `R`, and `S` as metavariables over type schemas, where a
type schema is a type expression that may or may not contain unbound
type variables. For instance, we might have
P_1 ≡ Int
P_2 ≡ α -> α
P_3 ≡ ∀α. α -> α
P_4 ≡ ∀α. α -> β
etc.
A *box type* will be a type expression that contains exactly one free
type variable. Some examples (using OCaml's type conventions):
α Maybe
α List
(α, P) Tree (assuming P contains no free type variables)
(α, α) Tree
The idea is that whatever type the free type variable α might be,
the boxed type will be a box that "contains" an object of type α.
For instance, if `α List` is our box type, and α is the basic type
Int, then in this context, `Int List` is the type of a boxed integer.
We'll often write box types as a box containing the value of the free
type variable. So if our box type is `α List`, and `α == Int`, we
would write
`mid (/εmaidεnt@tI/ aka unit, return, pure): P -> `__P__

`map (/maep/): (P -> Q) -> `__P__ -> __Q__

`map2 (/m&ash;ptu/): (P -> Q -> R) -> `__P__ -> __Q__ -> __R__

`mapply (/εm@plai/): `__P -> Q__ -> __P__ -> __Q__

`mcompose (aka <=<): (Q -> `__R__) -> (P -> __Q__) -> (P -> __R__)

`mbind (aka >>=): ( `__Q__) -> (Q -> __R__) -> ( __R__)

`mflipcompose (aka >=>): (P -> `__Q__) -> (Q -> __R__) -> (P -> __R__)

`mflipbind (aka =<<) ( `__Q__) -> (Q -> __R__) -> ( __R__)

`mjoin: `__P__ -> __P__

The managerie isn't quite as bewildering as you might suppose. For
one thing, `mcompose` and `mbind` are interdefinable: ```
u >=> k ≡
\a. (ja >>= k)
```

.
In most cases of interest, instances of these types will provide
certain useful guarantees.
* ***Mappable*** ("functors") At the most general level, box types are *Mappable*
if there is a `map` function defined for that box type with the type given above.
* ***MapNable*** ("applicatives") A Mappable box type is *MapNable*
if there are in addition `map2`, `mid`, and `mapply`. (With
`map2` in hand, `map3`, `map4`, ... `mapN` are easily definable.)
* ***Monad*** ("composables") A MapNable box type is a *Monad* if there
is in addition an `mcompose` and a `join` such that `mid` is
a left and right identity for `mcompose`, and `mcompose` is
associative. That is, the following "laws" must hold:
mcompose mid k = k
mcompose k mid = k
mcompose (mcompose j k) l = mcompose j (mcompose k l)
To take a trivial (but, as we will see, still useful) example,
consider the identity box type Id: `α -> α`. So if α is type Bool,
then a boxed α is ... a Bool. In terms of the box analogy, the
Identity box type is a completly invisible box. With the following
definitions
mid ≡ \p.p
mcompose ≡ \fgx.f(gx)
Id is a monad. Here is a demonstration that the laws hold:
mcompose mid k == (\fgx.f(gx)) (\p.p) k
~~> \x.(\p.p)(kx)
~~> \x.kx
~~> k
mcompose k mid == (\fgx.f(gx)) k (\p.p)
~~> \x.k((\p.p)x)
~~> \x.kx
~~> k
mcompose (mcompose j k) l == mcompose ((\fgx.f(gx)) j k) l
~~> mcompose (\x.j(kx)) l
== (\fgx.f(gx)) (\x.j(kx)) l
~~> \x.(\x.j(kx))(lx)
~~> \x.j(k(lx))
mcompose j (mcompose k l) == mcompose j ((\fgx.f(gx)) k l)
~~> mcompose j (\x.k(lx))
== (\fgx.f(gx)) j (\x.k(lx))
~~> \x.j((\x.k(lx)) x)
~~> \x.j(k(lx))
Id is the favorite monad of mimes everywhere.
To take a slightly less trivial (and even more useful) example,
consider the box type `α List`, with the following operations:
mid: α -> [α]
mid a = [a]
mcompose-crossy: (β -> [γ]) -> (α -> [β]) -> (α -> [γ])
mcompose-crossy f g a = [c | b <- g a, c <- f b]
mcompose-crossy f g a = foldr (\b -> \gs -> (f b) ++ gs) [] (g a)
mcompose-crossy f g a = concat (map f (g a))
These three definitions are all equivalent.
In words, `mcompose f g a` feeds the a (which has type α) to g, which
returns a list of βs; each β in that list is fed to f, which returns a
list of γs.
The final result is the concatenation of those lists of γs.
For example,
let f b = [b, b+1] in
let g a = [a*a, a+a] in
mcompose-crossy f g 7 = [49, 50, 14, 15]
It is easy to see that these definitions obey the monad laws (see exercises).
There can be multiple monads for any given box type. For instance,
using the same box type and the same mid, we can define
mcompose-zippy f g a = foldr (\b -> \gs -> f b ++ gs) (g a) []
so that
mcompose-zippy f g 7 = [49, 14]