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 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 ### Boxes: 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> to represent 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 ≡ Int
  29     P ≡ α -> α
  30     P ≡ ∀α. α -> α
  31     P ≡ ∀α. α -> β
  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 At the most general level, we'll talk about *Kleisli arrows*:
  57
  58 P -> <u>Q</u>
  59
  60 A Kleisli arrow is the type of a function from objects of type P to
  61 objects of type box Q, for some choice of type expressions P and Q.
  62 For instance, the following are arrows:
  63
  64 Int -> <u>Bool</u>
  65
  66 Int List -> <u>Int List</u>
  67
  68 Note that the left-hand schema can itself be a boxed type.  That is,
  69 if `α List` is our box type, we can write the second arrow as
  70
  71 <u>Int</u> -> <u><u>Int</u></u>
  72
  73 We'll need a number of schematic functions to help us maneuver in the presence
  74 of box types.  We will want to define a different instance of each of
  75 these for whichever box type we're dealing with:
  76
  77 <code>mid (/&epsilon;maid&epsilon;nt@tI/ aka unit, return, pure): P -> <u>P</u></code>
  78
  79 <code>map (/maep/): (P -> Q) -> <u>P</u> -> <u>Q</u></code>
  80
  81 <code>map2 (/maep/): (P -> Q -> R) -> <u>P</u> -> <u>Q</u> -> <u>R</u></code>
  82
  83 <code>mapply (/&epsilon;m@plai/): <u>P -> Q</u> -> <u>P</u> -> <u>Q</u></code>
  84
  85 <code>mcompose (aka <=<): (Q -> <u>R</u>) -> (P -> <u>Q</u>) -> (P -> <u>R</u>)</code>
  86
  87 <code>mbind (aka >>=): (     <u>Q</u>) -> (Q -> <u>R</u>) -> (     <u>R</u>)</code>
  88
  89 <code>mflipcompose (aka >=>): (P -> <u>Q</u>) -> (Q -> <u>R</u>) -> (P -> <u>R</u>)</code>
  90
  91 <code>mflipbind (aka =<<) (     <u>Q</u>) -> (Q -> <u>R</u>) -> (     <u>R</u>)</code>
  92
  93 <code>mjoin: <u><u>P</u></u> -> <u>P</u></code>
  94
  95 Note that `mcompose` and `mbind` are interdefinable: <code>u >=> k ≡ \a. (ja >>= k)</code>.
  96
  97 In most cases of interest, the specific instances of these types will
  98 provide certain useful guarantees.
  99
 100 *   ***Mappable*** ("functors") At the most general level, some box types are *Mappable*
 101 if there is a `map` function defined for that boxt type with the type given above.
 102
 103 *   ***MapNable*** ("applicatives") A Mappable box type is *MapNable*
 104        if there are in addition `map2`, `mid`, and `mapply`.
 105
 106 *   ***Monad*** ("composable") A MapNable box type is a *Monad* if
 107        there is in addition a `mcompose` and `join`.  In addition, in
 108        order to qualify as a monad, `mid` must be a left and right
 109        identity for mcompose, and mcompose must be associative.  That
 110        is, the following "laws" must hold:
 111
 112         mcompose mid k = k
 113         mcompose k mid = k
 114         mcompose (mcompose j k) l = mcompose j (mcompose k l)
 115
 116 To take a trivial example (but still useful, as we will see), consider
 117 the identity box type Id: `α -> α`.  In terms of the box analogy, the
 118 Identity box type is an invisible box.  With the following definitions
 119
 120     mid ≡ \p.p
 121     mcompose ≡ \f\g\x.f(gx)
 122
 123 Id is a monad.  Here is a demonstration that the laws hold:
 124
 125     mcompose mid k == (\f\g\x.f(gx)) (\p.p) k
 126                    ~~> \x.(\p.p)(kx)
 127                    ~~> \x.kx
 128                    ~~> k
 129     mcompose k mid == (\f\g\x.f(gx)) k (\p.p)
 130                    ~~> \x.k((\p.p)x)
 131                    ~~> \x.kx
 132                    ~~> k
 133     mcompose (mcompose j k) l == mcompose ((\f\g\x.f(gx)) j k) l
 134                               ~~> mcompose (\x.j(kx)) l
 135                               == (\f\g\x.f(gx)) (\x.j(kx)) l
 136                               ~~> \x.(\x.j(kx))(lx)
 137                               ~~> \x.j(k(lx))
 138     mcompose j (mcompose k l) == mcompose j ((\f\g\x.f(gx)) k l)
 139                               ~~> mcompose j (\x.k(lx))
 140                               == (\f\g\x.f(gx)) j (\x.k(lx))
 141                               ~~> \x.j((\x.k(lx)) x)
 142                               ~~> \x.j(k(lx))
 143
 144 Id is the favorite monad of mimes everywhere.
 145
 146 To take a slightly less trivial example, consider the box type `α
 147 List`, with the following operations:
 148
 149     mcompose f g p = [r | q <- g p, r <- f q]
 150
 151 In words, if g maps a P to a list of Qs, and f maps a Q to a list of
 152 Rs, then mcompose f g maps a P to a list of Rs by first feeding the P
 153 to g, then feeding each of the Qs delivered by g to f.  For example,
 154
 155     let f q = [q, q+1] in
 156     let g p = [p*p, p+p] in
 157     mcompose f g 7 = [49, 50, 14, 15]
 158
 159 It is easy to see that these definitions obey the monad laws (see exercises).
 160