From 94af2dbc84f38e23ae79e560300923f458615aeb Mon Sep 17 00:00:00 2001 From: jim Date: Fri, 20 Mar 2015 08:42:29 -0400 Subject: [PATCH] expand Mappable Laws --- topics/week7_introducing_monads.mdwn | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn index 23f4ff6b..2403da77 100644 --- a/topics/week7_introducing_monads.mdwn +++ b/topics/week7_introducing_monads.mdwn @@ -116,12 +116,21 @@ 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. + +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".) + 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 @@ -130,7 +139,9 @@ has to obey the following Map Laws: 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* -- 2.11.0