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,
@@ -161,60 +203,60 @@ definitions:
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:
- mid: α -> [α]
+ mid : α -> [α]
mid a = [a]
- mcomp: (β -> [γ]) -> (α -> [β]) -> (α -> [γ])
- mcomp f g a = concat (map f (g a))
- = foldr (\b -> \gs -> (f b) ++ gs) [] (g a)
- = [c | b <- g a, c <- f b]
+ mcomp : (β -> [γ]) -> (α -> [β]) -> (α -> [γ])
+ mcomp k j a = concat (map k (j a)) = List.flatten (List.map k (j a))
+ = foldr (\b ks -> (k b) ++ ks) [] (j a) = List.fold_right (fun b ks -> List.append (k b) ks) [] (j a)
+ = [c | b <- j a, c <- k b]
-The last three definitions of `mcomp` are all equivalent, and it is easy to see that they obey the monad laws (see exercises TODO).
+In the first two definitions of `mcomp`, we give the definition first in Haskell and then in the equivalent OCaml. The three different definitions of `mcomp` (one for each line) are all equivalent, and it is easy to show that they obey the Monad Laws. (You will do this in the homework.)
-In words, `mcomp 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
+In words, `mcomp k j a` feeds the `a` (which has type `α`) to `j`, which returns a list of `β`s;
+each `β` in that list is fed to `k`, 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
- mcomp f g 7 ==> [49, 50, 14, 15]
+ let j a = [a*a, a+a] in
+ let k b = [b, b+1] in
+ mcomp k j 7 ==> [49, 50, 14, 15]
-`g 7` produced `[49, 14]`, which after being fed through `f` gave us `[49, 50, 14, 15]`.
+`j 7` produced `[49, 14]`, which after being fed through `k` gave us `[49, 50, 14, 15]`.
Contrast that to `m$` (`mapply`, which operates not on two *box-producing functions*, but instead on two *values of a boxed type*, one containing functions to be applied to the values in the other box, via some predefined scheme. Thus:
- let gs = [(\a->a*a),(\a->a+a)] in
+ let js = [(\a->a*a),(\a->a+a)] in
let xs = [7, 5] in
- mapply gs xs ==> [49, 25, 14, 10]
+ mapply js 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 figure out 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 ##
@@ -325,7 +367,7 @@ it needs to be adjusted because someone else might make trouble.
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
@@ -393,5 +435,5 @@ theory of accommodation, and a theory of the situations in which
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.)