k <=< j â¡
@@ 136,8 +137,8 @@ These functions come together in several systems, and have to be defined in a wa
if there is a `map` function defined for that box type with the type given above. This
has to obey the following Map Laws:
 map (id : Î± > Î±) = (id : Î± > Î±)
 map (g â f) = (map g) â (map f)
+ map (id : Î± > Î±) == (id : Î± > Î±)
+ map (g â f) == (map g) â (map f)
Essentially these say that `map` is a homomorphism from the algebra of `(universe Î± > Î², operation â, elsment id)` to that of (Î± > Î², â', id')
, where `â'` and `id'` are `â` and `id` restricted to arguments of type _
. That might be hard to digest because it's so abstract. Think of the following concrete example: if you take a `Î± list` (that's our Î±
), and apply `id` to each of its elements, that's the same as applying `id` to the list itself. That's the first law. And if you apply the composition of functions `g â f` to each of the list's elements, that's the same as first applying `f` to each of the elements, and then going through the elements of the resulting list and applying `g` to each of those elements. That's the second law. These laws obviously hold for our familiar notion of `map` in relation to lists.
@@ 153,24 +154,42 @@ has to obey the following Map Laws:
TODO LAWS
* ***Monad*** (or "Composables") A MapNable box type is a *Monad* if there
+* ***Monad*** (or "Composables") A MapNable box type is a *Monad* if there
is in addition an associative `mcomp` having `mid` as its left and
right identity. That is, the following Monad Laws must hold:
 mcomp (mcomp j k) l (that is, (j <=< k) <=< l) = mcomp j (mcomp k l)
 mcomp mid k (that is, mid <=< k) = k
 mcomp k mid (that is, k <=< mid) = k
+ mcomp (mcomp j k) l (that is, (j <=< k) <=< l) == mcomp j (mcomp k l)
+ mcomp mid k (that is, mid <=< k) == k
+ mcomp k mid (that is, k <=< mid) == k
+
+ You could just as well express the Monad laws using `>=>`:
+
+ l >=> (k >=> j) == (l >=> k) >> j
+ k >=> mid == k
+ mid >=> k == k
+
+ If you have any of `mcomp`, `mpmoc`, `mbind`, or `join`, you can use them to define the others. Also, with these functions you can define `m$` and `map2` from *MapNables*. So with Monads, all you really need to get the whole system of functions are a definition of `mid`, on the one hand, and one of `mcomp`, `mbind`, or `join`, on the other.
+
+ In practice, you will often work with `>>=`. In the Haskell manuals, they express the Monad Laws using `>>=` instead of the composition operators. This looks similar, but doesn't have the same symmetry:
+
+ u >>= (\a > k a >>= j) == (u >>= k) >>= j
+ u >>= mid == u
+ mid a >>= k == k a
+
+ Also, Haskell calls `mid` `return` or `pure`, but we've stuck to our terminology in this context.
+
+ > In Category Theory discussion, the Monad Laws are instead expressed in terms of `join` (which they call `Î¼`) and `mid` (which they call `Î·`). These are assumed to be "natural transformations" for their box type, which means that they satisfy these equations with that box type's `map`:
+ > map f â mid == mid â f
map f â join == join â map (map f)
+ > The Monad Laws then take the form:
+ > join â (map join) == join â join
join â mid == id == join â map mid
+ > Or, as the Category Theorist would state it, where `M` is the endofunctor that takes us from type `Î±` to type Î±
:
+ > Î¼ â M(Î¼) == Î¼ â Î¼
Î¼ â Î· = id == Î¼ â M(Î·)
If you have any of `mcomp`, `mpmoc`, `mbind`, or `join`, you can use them to define the others.
Also, with these functions you can define `m$` and `map2` from *MapNables*. So all you really need
are a definition of `mid`, on the one hand, and one of `mcomp`, `mbind`, or `join`, on the other.
Here are some interdefinitions: TODO
Names in Haskell: TODO
The name "bind" is not well chosen from our perspective, but this is too deeply entrenched by now.

## Examples ##
To take a trivial (but, as we will see, still useful) example,

2.11.0