of monads, followed by instances of monads from the philosophical and
linguistics literature.
-> <small>After you've read this once and are coming back to re-read it to try to digest the details further, the "endofunctors" that slogan is talking about are the boxing operations. Their "monoidal" character is captured in the Monad Laws, where a "monoid"---don't confuse with a mon*ad*---is a simpler algebraic notion, meaning a universe with some associative operation that has an identity. For advanced study, here are some further links on the relation between monads as we're working with them and monads as they appear in category theory:
+> <small>After you've read this once and are coming back to re-read it to try to digest the details further, the "endofunctors" that slogan is talking about are a combination of our boxes and their associated maps. Their "monoidal" character is captured in the Monad Laws, where a "monoid"---don't confuse with a mon*ad*---is a simpler algebraic notion, meaning a universe with some associative operation that has an identity. For advanced study, here are some further links on the relation between monads as we're working with them and monads as they appear in category theory:
[1](http://en.wikipedia.org/wiki/Outline_of_category_theory)
[2](http://lambda1.jimpryor.net/advanced_topics/monads_in_category_theory/)
[3](http://en.wikibooks.org/wiki/Haskell/Category_theory)
(α, α) tree
The idea is that whatever type the free type variable `α` might be instantiated to,
-we will be a "type box" of a certain sort that "contains" values of type `α`. For instance,
+we will have a "type box" of a certain sort that "contains" values of type `α`. For instance,
if `α list` is our box type, and `α` is the type `int`, then in this context, `int list`
is the type of a boxed integer.
In the first, `P` has become `int` and `Q` has become `bool`. (The boxed type <code><u>Q</u></code> is <code><u>bool</u></code>).
Note that the left-hand schema `P` is permitted to itself be a boxed type. That is, where
-if `α list` is our box type, we can write the second arrow as
+if `α list` is our box type, we can write the second type as:
-<code><u>int</u> -> <u>Q</u></code>
+<code><u>int</u> -> <u>int list</u></code>
As semanticists, you are no doubt familiar with the debates between those who insist that propositions are sets of worlds and those who insist they are context change potentials. We hope to show you, in coming weeks, that propositions are (certain sorts of) Kleisli arrows. But this doesn't really compete with the other proposals; it is a generalization of them. Both of the other proposed structures can be construed as specific Kleisli arrows.
<code><=< or mcomp : (Q -> <u>R</u>) -> (P -> <u>Q</u>) -> (P -> <u>R</u>)</code>
-<code>>=> or mpmoc (flip mcomp): (P -> <u>Q</u>) -> (Q -> <u>R</u>) -> (P -> <u>R</u>)</code>
+<code>>=> (flip mcomp, should we call it mpmoc?): (P -> <u>Q</u>) -> (Q -> <u>R</u>) -> (P -> <u>R</u>)</code>
<code>>>= or mbind : (<u>Q</u>) -> (Q -> <u>R</u>) -> (<u>R</u>)</code>
-<code>=<< or mdnib (flip mbind) (<u>Q</u>) -> (Q -> <u>R</u>) -> (<u>R</u>)</code>
+<code>=<< (flip mbind, should we call it mdnib?) (Q -> <u>R</u>) -> (<u>Q</u>) -> (<u>R</u>)</code>
<code>join: <span class="box2">P</span> -> <u>P</u></code>