topics/_week7_monads.mdwn

   1 <!-- λ Λ ∀ ≡ α β γ ρ ω Ω -->
   2 <!-- Loved this one: http://www.stephendiehl.com/posts/monads.html -->
   3
   4 Monads
   5 ======
   6
   7 The [[tradition in the functional programming
   8 literature|https://wiki.haskell.org/Monad_tutorials_timeline]] is to
   9 introduce monads using a metaphor: monads are spacesuits, monads are
  10 monsters, monads are burritos.  We're part of the backlash that
  11 prefers to say that monads are (Just) monads.
  12
  13 The closest we will come to metaphorical talk is to suggest that
  14 monadic types place objects inside of *boxes*, and that monads wrap
  15 and unwrap boxes to expose or enclose the objects inside of them.  In
  16 any case, the emphasis will be on starting with the abstract structure
  17 of monads, followed by instances of monads from the philosophical and
  18 linguistics literature.
  19
  20 ## Box types: type expressions with one free type variable
  21
  22 Recall that we've been using lower-case Greek letters
  23 <code>&alpha;, &beta;, &gamma;, ...</code> as variables over types.  We'll
  24 use `P`, `Q`, `R`, and `S` as metavariables over type schemas, where a
  25 type schema is a type expression that may or may not contain unbound
  26 type variables.  For instance, we might have
  27
  28     P_1 ≡ Int
  29     P_2 ≡ α -> α
  30     P_3 ≡ ∀α. α -> α
  31     P_4 ≡ ∀α. α -> β
  32
  33 etc.
  34
  35 A *box type* will be a type expression that contains exactly one free
  36 type variable.  Some examples (using OCaml's type conventions):
  37
  38     α Maybe
  39     α List
  40     (α, P) Tree    (assuming P contains no free type variables)
  41     (α, α) Tree
  42
  43 The idea is that whatever type the free type variable α might be,
  44 the boxed type will be a box that "contains" an object of type α.
  45 For instance, if `α List` is our box type, and α is the basic type
  46 Int, then in this context, `Int List` is the type of a boxed integer.
  47
  48 We'll often write box types as a box containing the value of the free
  49 type variable.  So if our box type is `α List`, and `α == Int`, we
  50 would write
  51
  52 <u>Int</u>
  53
  54 for the type of a boxed Int.
  55
  56 ## Kleisli arrows
  57
  58 At the most general level, we'll talk about *Kleisli arrows*:
  59
  60 P -> <u>Q</u>
  61
  62 A Kleisli arrow is the type of a function from objects of type P to
  63 objects of type box Q, for some choice of type expressions P and Q.
  64 For instance, the following are arrows:
  65
  66 Int -> <u>Bool</u>
  67
  68 Int List -> <u>Int List</u>
  69
  70 Note that the left-hand schema can itself be a boxed type.  That is,
  71 if `α List` is our box type, we can write the second arrow as
  72
  73 <u>Int</u> -> <u><u>Int</u></u>
  74
  75 We'll need a number of classes of functions to help us maneuver in the
  76 presence of box types.  We will want to define a different instance of
  77 each of these for whichever box type we're dealing with.  (This will
  78 become clearly shortly.)
  79
  80 <code>mid (/&epsilon;maid&epsilon;nt@tI/ aka unit, return, pure): P -> <u>P</u></code>
  81
  82 <code>map (/maep/): (P -> Q) -> <u>P</u> -> <u>Q</u></code>
  83
  84 <code>map2 (/m&ash;ptu/): (P -> Q -> R) -> <u>P</u> -> <u>Q</u> -> <u>R</u></code>
  85
  86 <code>mapply (/&epsilon;m@plai/): <u>P -> Q</u> -> <u>P</u> -> <u>Q</u></code>
  87
  88 <code>mcompose (aka <=<): (Q -> <u>R</u>) -> (P -> <u>Q</u>) -> (P -> <u>R</u>)</code>
  89
  90 <code>mbind (aka >>=): (     <u>Q</u>) -> (Q -> <u>R</u>) -> (     <u>R</u>)</code>
  91
  92 <code>mflipcompose (aka >=>): (P -> <u>Q</u>) -> (Q -> <u>R</u>) -> (P -> <u>R</u>)</code>
  93
  94 <code>mflipbind (aka =<<) (     <u>Q</u>) -> (Q -> <u>R</u>) -> (     <u>R</u>)</code>
  95
  96 <code>mjoin: <u><u>P</u></u> -> <u>P</u></code>
  97
  98 The managerie isn't quite as bewildering as you might suppose.  For
  99 one thing, `mcompose` and `mbind` are interdefinable: <code>u >=> k ≡
 100 \a. (ja >>= k)</code>.
 101
 102 In most cases of interest, instances of these types will provide
 103 certain useful guarantees.
 104
 105 *   ***Mappable*** ("functors") At the most general level, box types are *Mappable*
 106 if there is a `map` function defined for that box type with the type given above.
 107
 108 *   ***MapNable*** ("applicatives") A Mappable box type is *MapNable*
 109        if there are in addition `map2`, `mid`, and `mapply`.  (With
 110        `map2` in hand, `map3`, `map4`, ... `mapN` are easily definable.)
 111
 112 * ***Monad*** ("composables") A MapNable box type is a *Monad* if there
 113        is in addition an `mcompose` and a `join` such that `mid` is
 114        a left and right identity for `mcompose`, and `mcompose` is
 115        associative.  That is, the following "laws" must hold:
 116
 117         mcompose mid k = k
 118         mcompose k mid = k
 119         mcompose (mcompose j k) l = mcompose j (mcompose k l)
 120
 121 To take a trivial (but, as we will see, still useful) example,
 122 consider the identity box type Id: `α -> α`.  So if α is type Bool,
 123 then a boxed α is ... a Bool.  In terms of the box analogy, the
 124 Identity box type is a completly invisible box.  With the following
 125 definitions
 126
 127     mid ≡ \p.p
 128     mcompose ≡ \fgx.f(gx)
 129
 130 Id is a monad.  Here is a demonstration that the laws hold:
 131
 132     mcompose mid k == (\fgx.f(gx)) (\p.p) k
 133                    ~~> \x.(\p.p)(kx)
 134                    ~~> \x.kx
 135                    ~~> k
 136     mcompose k mid == (\fgx.f(gx)) k (\p.p)
 137                    ~~> \x.k((\p.p)x)
 138                    ~~> \x.kx
 139                    ~~> k
 140     mcompose (mcompose j k) l == mcompose ((\fgx.f(gx)) j k) l
 141                               ~~> mcompose (\x.j(kx)) l
 142                               == (\fgx.f(gx)) (\x.j(kx)) l
 143                               ~~> \x.(\x.j(kx))(lx)
 144                               ~~> \x.j(k(lx))
 145     mcompose j (mcompose k l) == mcompose j ((\fgx.f(gx)) k l)
 146                               ~~> mcompose j (\x.k(lx))
 147                               == (\fgx.f(gx)) j (\x.k(lx))
 148                               ~~> \x.j((\x.k(lx)) x)
 149                               ~~> \x.j(k(lx))
 150
 151 Id is the favorite monad of mimes everywhere.
 152
 153 To take a slightly less trivial (and even more useful) example,
 154 consider the box type `α List`, with the following operations:
 155
 156     mid: α -> [α]
 157     mid a = [a]
 158
 159     mcompose: (β -> [γ]) -> (α -> [β]) -> (α -> [γ])
 160     mcompose f g a = concat (map f (g a))
 161                    = foldr (\b -> \gs -> (f b) ++ gs) [] (g a)
 162                    = [c | b <- g a, c <- f b]
 163
 164 These three definitions are all equivalent.  In words, `mcompose f g
 165 a` feeds the a (which has type α) to g, which returns a list of βs;
 166 each β in that list is fed to f, which returns a list of γs.  The
 167 final result is the concatenation of those lists of γs.
 168
 169 For example,
 170
 171     let f b = [b, b+1] in
 172     let g a = [a*a, a+a] in
 173     mcompose f g 7 = [49, 50, 14, 15]
 174
 175 It is easy to see that these definitions obey the monad laws (see exercises).
 176