topics/week8_safe_division_with_monads.mdwn

   1 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.
   2
   3 OCaml's `/` operator expresses integer division, which throws away any remainder, thus:
   4
   5     # 11/3;;
   6     - : int = 3
   7
   8 Integer division presupposes that its second argument
   9 (the divisor) is not zero, upon pain of presupposition failure.
  10 Here's what my OCaml interpreter says:
  11
  12     # 11/0;;
  13     Exception: Division_by_zero.
  14
  15 Say we want to explicitly allow for the possibility that
  16 division will return something other than a number.
  17 To do that, we'll use OCaml's `option` type, which works like this:
  18
  19     # type 'a option = None | Some of 'a;;
  20     # None;;
  21     - : 'a option = None
  22     # Some 3;;
  23     - : int option = Some 3
  24
  25 So if a division is normal, we return some number, but if the divisor is
  26 zero, we return `None`. As a mnemonic aid, we'll prepend a `safe_` to the start of our new divide function.
  27
  28 <pre>
  29 let safe_div (x : int) (y : int) =
  30   match y with
  31     | 0 -> None
  32     | _ -> Some (x / y);;
  33
  34 (* an Ocaml session could continue with OCaml's response:
  35 val safe_div : int -> int -> int option = fun
  36 # safe_div 12 2;;
  37 - : int option = Some 6
  38 # safe_div 12 0;;
  39 - : int option = None
  40 # safe_div (safe_div 12 2) 3;;
  41             ~~~~~~~~~~~~~
  42 Error: This expression has type int option
  43        but an expression was expected of type int
  44 *)
  45 </pre>
  46
  47 This starts off well: dividing `12` by `2`, no problem; dividing `12` by `0`,
  48 just the behavior we were hoping for. But we want to be able to use
  49 the output of the safe-division function as input for further division
  50 operations. So we have to jack up the types of the inputs:
  51
  52 <pre>
  53 let safe_div2 (u : int option) (v : int option) =
  54   match u with
  55   | None -> None
  56   | Some x ->
  57       (match v with
  58       | None -> None
  59       | Some 0 -> None
  60       | Some y -> Some (x / y));;
  61
  62 (* an Ocaml session could continue with OCaml's response:
  63 val safe_div2 : int option -> int option -> int option = <fun>
  64 # safe_div2 (Some 12) (Some 2);;
  65 - : int option = Some 6
  66 # safe_div2 (Some 12) (Some 0);;
  67 - : int option = None
  68 # safe_div2 (safe_div2 (Some 12) (Some 0)) (Some 3);;
  69 - : int option = None
  70 *)
  71 </pre>
  72
  73 Calling the function now involves some extra verbosity, but it gives us what we need: now we can try to divide by anything we
  74 want, without fear that we're going to trigger system errors.
  75
  76 I prefer to line up the `match` alternatives by using OCaml's
  77 built-in tuple type:
  78
  79 <pre>
  80 let safe_div2 (u : int option) (v : int option) =
  81   match (u, v) with
  82   | (None, _) -> None
  83   | (_, None) -> None
  84   | (_, Some 0) -> None
  85   | (Some x, Some y) -> Some (x / y);;
  86 </pre>
  87
  88 So far so good. But what if we want to combine division with
  89 other arithmetic operations? We need to make those other operations
  90 aware of the possibility that one of their arguments has already triggered a
  91 presupposition failure:
  92
  93 <pre>
  94 let safe_add (u:int option) (v:int option) =
  95   match (u, v) with
  96     | (None, _) -> None
  97     | (_, None) -> None
  98     | (Some x, Some y) -> Some (x + y);;
  99
 100 (* an Ocaml session could continue with OCaml's response:
 101 val safe_add : int option -> int option -> int option = <fun>
 102 # safe_add (Some 12) (Some 4);;
 103 - : int option = Some 16
 104 # safe_add (safe_div (Some 12) (Some 0)) (Some 4);;
 105 - : int option = None
 106 *)
 107 </pre>
 108
 109 So now, wherever before our operations expected an `int`, we'll instead
 110 have them accept an `int option`. A `None` input signals that
 111 something has gone wrong upstream.
 112
 113 This works, but is somewhat disappointing: the `safe_add` operation
 114 doesn't trigger any presupposition of its own, so it is a shame that
 115 it needs to be adjusted because someone else might make trouble.
 116
 117 But we can automate the adjustment, using the monadic machinery we introduced before.
 118 As we said, there needs to be different `>>=`, `map2` and so on operations for each
 119 Monad or box type we're working with.
 120 Haskell finesses this by "overloading" the single symbol `>>=`; you can just input that
 121 symbol and it will calculate from the context of the surrounding type constraints what
 122 Monad you must have meant. In OCaml, the monadic operators are not pre-defined, but we will
 123 give you a library that has definitions for all the standard Monads, as in Haskell. But you
 124 will need to explicitly specify which Monad you mean to be deploying.
 125
 126 For now, though, we will define our `>>=` and `map2` operations by hand:
 127
 128 <pre>
 129 let (>>=) (u : 'a option) (j : 'a -> 'b option) : 'b option =
 130   match u with
 131     | None -> None
 132     | Some x -> j x;;
 133
 134 let map2 (f : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) : 'c option =
 135   u >>= (fun x -> v >>= (fun y -> Some (f x y)));;
 136
 137 let safe_add3 = map2 (+);;    (* that was easy *)
 138
 139 let safe_div3 (u: int option) (v: int option) =
 140   u >>= (fun x -> v >>= (fun y -> if 0 = y then None else Some (x / y)));;
 141 </pre>
 142
 143 Haskell has an even more user-friendly notation for defining `safe_div3`, namely:
 144
 145     safe_div3 :: Maybe Int -> Maybe Int -> Maybe Int
 146     safe_div3 u v = do {x <- u;
 147                         y <- v;
 148                         if 0 == y then Nothing else Just (x `div` y)}
 149
 150 You can read more about that here:
 151
 152 *       [Haskell wikibook on do-notation](http://en.wikibooks.org/wiki/Haskell/do_Notation)
 153 *       [Yet Another Haskell Tutorial on do-notation](http://en.wikibooks.org/wiki/Haskell/YAHT/Monads#Do_Notation)
 154
 155
 156 Let's see our new functions in action:
 157
 158 <pre>
 159 (* an Ocaml session could continue with OCaml's response:
 160 # safe_div3 (safe_div3 (Some 12) (Some 2)) (Some 3);;
 161 - : int option = Some 2
 162 #  safe_div3 (safe_div3 (Some 12) (Some 0)) (Some 3);;
 163 - : int option = None
 164 # safe_add3 (safe_div3 (Some 12) (Some 0)) (Some 3);;
 165 - : int option = None
 166 *)
 167 </pre>
 168
 169 Our definition for `safe_add3` shows what it looks like to equip an ordinary operation to
 170 survive in dangerous presupposition-filled world. We just need to `mapN` it "into" the
 171 Maybe monad, where `N` is the function's adicity. Note that the new
 172 definition of `safe_add3` does not need to test whether its arguments are
 173 `None` values or genuine numbers---those details are hidden inside of the
 174 `bind` function.
 175
 176 Note also that our definition of `safe_div3` recovers some of the simplicity of
 177 the original `safe_div`, without the complexity introduced by `safe_div2`. We now
 178 add exactly what extra is needed to track the no-division-by-zero presupposition. Here, too, we don't
 179 need to keep track of what other presuppositions may have already failed
 180 for whatever reason on our inputs.
 181
 182 So what the monadic machinery gives us here is a way to _separate_ thinking
 183 about error conditions (such as trying to divide by zero) from thinking about normal
 184 arithmetic computations. When we're adding or multiplying, we don't have to worry about generating
 185 any new errors, so we would rather not force these operations to explicitly
 186 track the difference between `int`s and `int option`s. A linguistics analogy we'll
 187 look at soon is that when we're giving the lexical entry for an ordinary
 188 extensional verb, we'd rather not be forced to talk about possible worlds. In each case,
 189 we instead just have a standard way of "lifting" (`mapN`ing) the relevant notions into
 190 the fancier type environment we ultimately want to work in.
 191
 192 Dividing by zero is supposed to feel like a kind of
 193 presupposition failure. If we wanted to adapt this approach to
 194 building a simple account of presupposition projection, we would have
 195 to do several things. First, we would have to make use of the
 196 polymorphism of the `option` type. In the arithmetic example, we only
 197 made use of `int option`s, but when we're composing natural language
 198 expression meanings, we'll need to use types like `N option`, `Det option`,
 199 `VP option`, and so on. But that works automatically, because we can use
 200 any type for the `'a` in `'a option`. Ultimately, we'd want to have a
 201 theory of accommodation, and a theory of the situations in which
 202 material within the sentence can satisfy presuppositions for other
 203 material that otherwise would trigger a presupposition violation; but,
 204 not surprisingly, these refinements will require some more
 205 sophisticated techniques than the super-simple Option/Maybe Monad.
 206
 207 To illustrate some of the polymorphism, here's how we could `map1` the `is_even` function:
 208
 209     # let is_even x = (x mod 2 = 0);;
 210     val is_even : int -> bool = <fun>
 211     # let map (g : 'a -> 'b) (u : 'a option) = u >>= fun x -> Some (g x);;
 212     val map : ('a -> 'b) -> 'a option -> 'b option = <fun>
 213     # map (is_even);;
 214     - : int option -> bool option = <fun>
 215
 216 Wherever we have a well-defined monad, we can define the `mapN` operations for them in terms
 217 of their `>>=` and `⇧`/`mid`. The general pattern is:
 218
 219     mapN (g : 'a1 -> ... 'an -> 'result) (u1 : 'a1 option) ... (un : 'an option) : 'result option =
 220       u1 >>= (fun x1 -> ... un >>= (fun xn -> ⇧(g x1 ... xn)) ...)
 221
 222 Our above definitions of `map` and `mapN` were of this form, except we just
 223 explicitly supplied the definition of `⇧` for the Option/Maybe monad (namely, in OCamlese, the constructor `Some`).
 224 If you substitute in the definition of `>>=`, you can see these are equivalent to:
 225
 226     map (g : 'a -> 'b) (u : 'a option) =
 227       match u with
 228       | None -> None
 229       | Some x -> Some (g x)
 230
 231     map2 (g : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) =
 232       match u with
 233       | None -> None
 234       | Some x ->
 235           (match v with
 236           | None -> None
 237           | Some y -> Some (g x y));;