to instead just look at the formal definition. We'll give that to you below, but it's
sometimes sloganized as
[A monad is just a monoid in the category of endofunctors, what's the problem?](http://stackoverflow.com/questions/3870088).
-Without some intuitive guidance, this can also be unhelpful. We'll try to find a good balance.
+Without some intuitive guidance, this can also be unhelpful. We'll try to find a good balance.
+
The closest we will come to metaphorical talk is to suggest that
monadic types place values inside of *boxes*, and that monads wrap
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:
+[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)
+[4](https://wiki.haskell.org/Category_theory), where you should follow the further links discussing Functors, Natural Transformations, and Monads.</small>
+
+
## Box types: type expressions with one free type variable ##
Recall that we've been using lower-case Greek letters
Identity is a monad. Here is a demonstration that the laws hold:
- mcomp mid k == (\fgx.f(gx)) (\p.p) k
- ~~> \x.(\p.p)(kx)
- ~~> \x.kx
- ~~> k
- mcomp k mid == (\fgx.f(gx)) k (\p.p)
- ~~> \x.k((\p.p)x)
- ~~> \x.kx
- ~~> k
- mcomp (mcomp j k) l == mcomp ((\fgx.f(gx)) j k) l
- ~~> mcomp (\x.j(kx)) l
- == (\fgx.f(gx)) (\x.j(kx)) l
- ~~> \x.(\x.j(kx))(lx)
- ~~> \x.j(k(lx))
- mcomp j (mcomp k l) == mcomp j ((\fgx.f(gx)) k l)
- ~~> mcomp j (\x.k(lx))
- == (\fgx.f(gx)) j (\x.k(lx))
- ~~> \x.j((\x.k(lx)) x)
- ~~> \x.j(k(lx))
-
-The Identity Monad is favored by mimes.
+ mcomp mid k ≡ (\fgx.f(gx)) (\p.p) k
+ ~~> \x.(\p.p)(kx)
+ ~~> \x.kx
+ ~~> k
+ mcomp k mid ≡ (\fgx.f(gx)) k (\p.p)
+ ~~> \x.k((\p.p)x)
+ ~~> \x.kx
+ ~~> k
+ mcomp (mcomp j k) l ≡ mcomp ((\fgx.f(gx)) j k) l
+ ~~> mcomp (\x.j(kx)) l
+ ≡ (\fgx.f(gx)) (\x.j(kx)) l
+ ~~> \x.(\x.j(kx))(lx)
+ ~~> \x.j(k(lx))
+ mcomp j (mcomp k l) ≡ mcomp j ((\fgx.f(gx)) k l)
+ ~~> mcomp j (\x.k(lx))
+ ≡ (\fgx.f(gx)) j (\x.k(lx))
+ ~~> \x.j((\x.k(lx)) x)
+ ~~> \x.j(k(lx))
+
+The Identity monad is favored by mimes.
To take a slightly less trivial (and even more useful) example,
consider the box type `α list`, with the following operations:
mapply gs xs ==> [49, 25, 14, 10]
-As we illustrated in class, there are clear patterns shared between lists and option types and trees, so perhaps you can see why people want to identify the general structures. But it probably isn't obvious yet why it would be useful to do so. To a large extent, this will only emerge over the next few classes. But we'll begin to demonstrate the usefulness of these patterns by talking through a simple example, that uses the Monadic functions of the Option/Maybe box type.
+As we illustrated in class, there are clear patterns shared between lists and option types and trees, so perhaps you can see why people want to identify the general structures. But it probably isn't obvious yet why it would be useful to do so. To a large extent, this will only emerge over the next few classes. But we'll begin to demonstrate the usefulness of these patterns by talking through a simple example, that uses the monadic functions of the Option/Maybe box type.
## Safe division ##
But we can automate the adjustment, using the monadic machinery we introduced above.
As we said, there needs to be different `>>=`, `map2` and so on operations for each
-Monad or box type we're working with.
+monad or box type we're working with.
Haskell finesses this by "overloading" the single symbol `>>=`; you can just input that
symbol and it will calculate from the context of the surrounding type constraints what
monad you must have meant. In OCaml, the monadic operators are not pre-defined, but we will
material within the sentence can satisfy presuppositions for other
material that otherwise would trigger a presupposition violation; but,
not surprisingly, these refinements will require some more
-sophisticated techniques than the super-simple Option monad.)
+sophisticated techniques than the super-simple Option/Maybe monad.)