X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek7_introducing_monads.mdwn;h=ec117aa44646b4339cd00e59341470ef6dc83757;hp=23f4ff6b5b245564b1b8d8ad079729188f2d7a77;hb=438540242da915aeb3f439bdbfe9b5d9ffed989d;hpb=5c38807ea1ba6dcaf9abcfc004918e1b2d503def diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn index 23f4ff6b..ec117aa4 100644 --- a/topics/week7_introducing_monads.mdwn +++ b/topics/week7_introducing_monads.mdwn @@ -116,21 +116,33 @@ Here are the types of our crucial functions, together with our pronunciation, an join: P -> P +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. + +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: k <=< j ≡ \a. (j a >>= k). -In most cases of interest, instances of these systems of functions will provide -certain useful guarantees. +We will move freely back and forth between using `>=>` and using `<=<` (aka `mcomp`), which +is just `>=>` with its arguments flipped. `<=<` has the virtue that it corresponds more +closely to the ordinary mathematical symbol `○`. But `>=>` has the virtue +that its types flow more naturally from left to right. + +These functions come together in several systems, and have to be defined in a way that coheres with the other functions in the system: * ***Mappable*** (in Haskelese, "Functors") At the most general level, box types are *Mappable* 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 `(α -> β, ○, id)` to (α -> β, ○', 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. + 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. + + > 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 _ and of the `map` that goes together with it. * ***MapNable*** (in Haskelese, "Applicatives") A Mappable box type is *MapNable* @@ -142,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,