topics/_week8_using_monads.mdwn

   1 Some applications of monadic machinery...
   2
   3 ## Safe division ##
   4
   5 As we discussed 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.
   6
   7 Integer division presupposes that its second argument
   8 (the divisor) is not zero, upon pain of presupposition failure.
   9 Here's what my OCaml interpreter says:
  10
  11     # 12/0;;
  12     Exception: Division_by_zero.
  13
  14 Say we want to explicitly allow for the possibility that
  15 division will return something other than a number.
  16 To do that, we'll use OCaml's `option` type, which works like this:
  17
  18     # type 'a option = None | Some of 'a;;
  19     # None;;
  20     - : 'a option = None
  21     # Some 3;;
  22     - : int option = Some 3
  23
  24 So if a division is normal, we return some number, but if the divisor is
  25 zero, we return `None`. As a mnemonic aid, we'll prepend a `safe_` to the start of our new divide function.
  26
  27 <pre>
  28 let safe_div (x:int) (y:int) =
  29   match y with
  30     | 0 -> None
  31     | _ -> Some (x / y);;
  32
  33 (*
  34 val safe_div : int -> int -> int option = fun
  35 # safe_div 12 2;;
  36 - : int option = Some 6
  37 # safe_div 12 0;;
  38 - : int option = None
  39 # safe_div (safe_div 12 2) 3;;
  40             ~~~~~~~~~~~~~
  41 Error: This expression has type int option
  42        but an expression was expected of type int
  43 *)
  44 </pre>
  45
  46 This starts off well: dividing `12` by `2`, no problem; dividing `12` by `0`,
  47 just the behavior we were hoping for. But we want to be able to use
  48 the output of the safe-division function as input for further division
  49 operations. So we have to jack up the types of the inputs:
  50
  51 <pre>
  52 let safe_div2 (u:int option) (v:int option) =
  53   match u with
  54   | None -> None
  55   | Some x ->
  56       (match v with
  57       | Some 0 -> None
  58       | Some y -> Some (x / y));;
  59
  60 (*
  61 val safe_div2 : int option -> int option -> int option = <fun>
  62 # safe_div2 (Some 12) (Some 2);;
  63 - : int option = Some 6
  64 # safe_div2 (Some 12) (Some 0);;
  65 - : int option = None
  66 # safe_div2 (safe_div2 (Some 12) (Some 0)) (Some 3);;
  67 - : int option = None
  68 *)
  69 </pre>
  70
  71 Calling the function now involves some extra verbosity, but it gives us what we need: now we can try to divide by anything we
  72 want, without fear that we're going to trigger system errors.
  73
  74 I prefer to line up the `match` alternatives by using OCaml's
  75 built-in tuple type:
  76
  77 <pre>
  78 let safe_div2 (u:int option) (v:int option) =
  79   match (u, v) with
  80   | (None, _) -> None
  81   | (_, None) -> None
  82   | (_, Some 0) -> None
  83   | (Some x, Some y) -> Some (x / y);;
  84 </pre>
  85
  86 So far so good. But what if we want to combine division with
  87 other arithmetic operations? We need to make those other operations
  88 aware of the possibility that one of their arguments has already triggered a
  89 presupposition failure:
  90
  91 <pre>
  92 let safe_add (u:int option) (v:int option) =
  93   match (u, v) with
  94     | (None, _) -> None
  95     | (_, None) -> None
  96     | (Some x, Some y) -> Some (x + y);;
  97
  98 (*
  99 val safe_add : int option -> int option -> int option = <fun>
 100 # safe_add (Some 12) (Some 4);;
 101 - : int option = Some 16
 102 # safe_add (safe_div (Some 12) (Some 0)) (Some 4);;
 103 - : int option = None
 104 *)
 105 </pre>
 106
 107 This works, but is somewhat disappointing: the `safe_add` operation
 108 doesn't trigger any presupposition of its own, so it is a shame that
 109 it needs to be adjusted because someone else might make trouble.
 110
 111 But we can automate the adjustment, using the monadic machinery we introduced above.
 112 As we said, there needs to be different `>>=`, `map2` and so on operations for each
 113 monad or box type we're working with.
 114 Haskell finesses this by "overloading" the single symbol `>>=`; you can just input that
 115 symbol and it will calculate from the context of the surrounding type constraints what
 116 monad you must have meant. In OCaml, the monadic operators are not pre-defined, but we will
 117 give you a library that has definitions for all the standard monads, as in Haskell.
 118 For now, though, we will define our `>>=` and `map2` operations by hand:
 119
 120 <pre>
 121 let (>>=) (u : 'a option) (j : 'a -> 'b option) : 'b option =
 122   match u with
 123     | None -> None
 124     | Some x -> j x;;
 125
 126 let map2 (f : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) : 'c option =
 127   u >>= (fun x -> v >>= (fun y -> Some (f x y)));;
 128
 129 let safe_add3 = map2 (+);;    (* that was easy *)
 130
 131 let safe_div3 (u: int option) (v: int option) =
 132   u >>= (fun x -> v >>= (fun y -> if 0 = y then None else Some (x / y)));;
 133 </pre>
 134
 135 Haskell has an even more user-friendly notation for defining `safe_div3`, namely:
 136
 137     safe_div3 :: Maybe Int -> Maybe Int -> Maybe Int
 138     safe_div3 u v = do {x <- u;
 139                         y <- v;
 140                         if 0 == y then Nothing else Just (x `div` y)}
 141
 142 Let's see our new functions in action:
 143
 144 <pre>
 145 (*
 146 # safe_div3 (safe_div3 (Some 12) (Some 2)) (Some 3);;
 147 - : int option = Some 2
 148 #  safe_div3 (safe_div3 (Some 12) (Some 0)) (Some 3);;
 149 - : int option = None
 150 # safe_add3 (safe_div3 (Some 12) (Some 0)) (Some 3);;
 151 - : int option = None
 152 *)
 153 </pre>
 154
 155 Compare the new definitions of `safe_add3` and `safe_div3` closely: the definition
 156 for `safe_add3` shows what it looks like to equip an ordinary operation to
 157 survive in dangerous presupposition-filled world. Note that the new
 158 definition of `safe_add3` does not need to test whether its arguments are
 159 `None` values or real numbers---those details are hidden inside of the
 160 `bind` function.
 161
 162 Note also that our definition of `safe_div3` recovers some of the simplicity of
 163 the original `safe_div`, without the complexity introduced by `safe_div2`. We now
 164 add exactly what extra is needed to track the no-division-by-zero presupposition. Here, too, we don't
 165 need to keep track of what other presuppositions may have already failed
 166 for whatever reason on our inputs.
 167
 168 (Linguistics note: Dividing by zero is supposed to feel like a kind of
 169 presupposition failure. If we wanted to adapt this approach to
 170 building a simple account of presupposition projection, we would have
 171 to do several things. First, we would have to make use of the
 172 polymorphism of the `option` type. In the arithmetic example, we only
 173 made use of `int option`s, but when we're composing natural language
 174 expression meanings, we'll need to use types like `N option`, `Det option`,
 175 `VP option`, and so on. But that works automatically, because we can use
 176 any type for the `'a` in `'a option`. Ultimately, we'd want to have a
 177 theory of accommodation, and a theory of the situations in which
 178 material within the sentence can satisfy presuppositions for other
 179 material that otherwise would trigger a presupposition violation; but,
 180 not surprisingly, these refinements will require some more
 181 sophisticated techniques than the super-simple Option/Maybe monad.)
 182
 183
 184 ## Scratch, more... ##
 185
 186 We've just seen a way to separate thinking about error conditions
 187 (such as trying to divide by zero) from thinking about normal
 188 arithmetic computations.  We did this by making use of the `option`
 189 type: in each place where we had something of type `int`, we put
 190 instead something of type `int option`, which is a sum type consisting
 191 either of one choice with an `int` payload, or else a `None` choice
 192 which we interpret as signaling that something has gone wrong.
 193
 194 The goal was to make normal computing as convenient as possible: when
 195 we're adding or multiplying, we don't have to worry about generating
 196 any new errors, so we would rather not think about the difference
 197 between `int`s and `int option`s.