`α, β, γ, ...`

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: (β -> [γ]) -> (α -> [β]) -> (α -> [γ])
mcompose f g a = concat (map f (g a))
= foldr (\b -> \gs -> (f b) ++ gs) [] (g a)
= [c | b <- g a, c <- f b]
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 f g 7 = [49, 50, 14, 15]
It is easy to see that these definitions obey the monad laws (see exercises).