In the class handout, we gave the types for `>=>` twice, and once was correct but the other was a typo. The above is the correct typing.
-Also, in the handout we called `mid` `𝟭`. But now we've decided that `mid`
-is better. (Think of it as "m" plus "identity", not as the start of "midway".)
+Haskell's name "bind" for `>>=` is not well chosen from our perspective, but this is too deeply entrenched by now. We've at least preprended an `m` to the front of it.
+
+Haskell's names "return" and "pure" for `mid` are even less well chosen, and we think it will be clearer in our discussion to use a different name. (Also, in other theoretical contexts this notion goes by other names, anyway, like `unit` or `η` --- having nothing to do with `η`-reduction in the Lambda Calculus.) In the handout we called `mid` `𝟭`. But now we've decided that `mid` is better. (Think of it as "m" plus "identity", not as the start of "midway".)
The menagerie isn't quite as bewildering as you might suppose. Many of these will
be interdefinable. For example, here is how `mcomp` and `mbind` are related: <code>k <=< j ≡
if there is a `map` function defined for that box type with the type given above. This
has to obey the following Map Laws:
- <code>map (id : α -> α) = (id : <u>α</u> -> <u>α</u>)</code>
- <code>map (g ○ f) = (map g) ○ (map f)</code>
+ <code>map (id : α -> α) == (id : <u>α</u> -> <u>α</u>)</code>
+ <code>map (g ○ f) == (map g) ○ (map f)</code>
Essentially these say that `map` is a homomorphism from the algebra of `(universe α -> β, operation ○, elsment id)` to that of <code>(<u>α</u> -> <u>β</u>, ○', id')</code>, where `○'` and `id'` are `○` and `id` restricted to arguments of type <code><u>_</u></code>. 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 <code><u>α</u></code>), 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.
- > <small>As mentioned at the top of the page, in Category Theory presentations of monads they usually talk about "endofunctors", which are mappings from a Category to itself. In the uses they make of this notion, the endofunctors combine the role of a box type <code><u>_</u></code> and of the `map` that goes together with it.
+ > <small>As mentioned at the top of the page, in Category Theory presentations of monads they usually talk about "endofunctors", which are mappings from a Category to itself. In the uses they make of this notion, the endofunctors combine the role of a box type <code><u>_</u></code> and of the `map` that goes together with it.</small>
* ***MapNable*** (in Haskelese, "Applicatives") A Mappable box type is *MapNable*
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.
+
+ > <small>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`:
+ > <pre>map f ○ mid == mid ○ f<br>map f ○ join == join ○ map (map f)</pre>
+ > The Monad Laws then take the form:
+ > <pre>join ○ (map join) == join ○ join<br>join ○ mid == id == join ○ map mid</pre>
+ > Or, as the Category Theorist would state it, where `M` is the endofunctor that takes us from type `α` to type <code><u>α</u></code>:
+ > <pre>μ ○ M(μ) == μ ○ μ<br>μ ○ η = id == μ ○ M(η)</pre></small>
-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,