topics/_week8_division_by_zero.mdwn

   1 [[!toc]]
   2
   3
   4 Towards Monads: Safe division
   5 -----------------------------
   6
   7 [This section used to be near the end of the lecture notes for week 6]
   8
   9 We begin by reasoning about what should happen when someone tries to
  10 divide by zero.  This will lead us to a general programming technique
  11 called a *monad*, which we'll see in many guises in the weeks to come.
  12
  13 Integer division presupposes that its second argument
  14 (the divisor) is not zero, upon pain of presupposition failure.
  15 Here's what my OCaml interpreter says:
  16
  17     # 12/0;;
  18     Exception: Division_by_zero.
  19
  20 So we want to explicitly allow for the possibility that
  21 division will return something other than a number.
  22 We'll use OCaml's `option` type, which works like this:
  23
  24     # type 'a option = None | Some of 'a;;
  25     # None;;
  26     - : 'a option = None
  27     # Some 3;;
  28     - : int option = Some 3
  29
  30 So if a division is normal, we return some number, but if the divisor is
  31 zero, we return `None`. As a mnemonic aid, we'll append a `'` to the end of our new divide function.
  32
  33 <pre>
  34 let div' (x:int) (y:int) =
  35   match y with
  36           0 -> None
  37     | _ -> Some (x / y);;
  38
  39 (*
  40 val div' : int -> int -> int option = fun
  41 # div' 12 2;;
  42 - : int option = Some 6
  43 # div' 12 0;;
  44 - : int option = None
  45 # div' (div' 12 2) 3;;
  46 Characters 4-14:
  47   div' (div' 12 2) 3;;
  48         ^^^^^^^^^^
  49 Error: This expression has type int option
  50        but an expression was expected of type int
  51 *)
  52 </pre>
  53
  54 This starts off well: dividing 12 by 2, no problem; dividing 12 by 0,
  55 just the behavior we were hoping for.  But we want to be able to use
  56 the output of the safe-division function as input for further division
  57 operations.  So we have to jack up the types of the inputs:
  58
  59 <pre>
  60 let div' (u:int option) (v:int option) =
  61   match u with
  62           None -> None
  63         | Some x -> (match v with
  64                                   Some 0 -> None
  65                                 | Some y -> Some (x / y));;
  66
  67 (*
  68 val div' : int option -> int option -> int option = <fun>
  69 # div' (Some 12) (Some 2);;
  70 - : int option = Some 6
  71 # div' (Some 12) (Some 0);;
  72 - : int option = None
  73 # div' (div' (Some 12) (Some 0)) (Some 3);;
  74 - : int option = None
  75 *)
  76 </pre>
  77
  78 Beautiful, just what we need: now we can try to divide by anything we
  79 want, without fear that we're going to trigger any system errors.
  80
  81 I prefer to line up the `match` alternatives by using OCaml's
  82 built-in tuple type:
  83
  84 <pre>
  85 let div' (u:int option) (v:int option) =
  86   match (u, v) with
  87           (None, _) -> None
  88     | (_, None) -> None
  89     | (_, Some 0) -> None
  90         | (Some x, Some y) -> Some (x / y);;
  91 </pre>
  92
  93 So far so good.  But what if we want to combine division with
  94 other arithmetic operations?  We need to make those other operations
  95 aware of the possibility that one of their arguments has triggered a
  96 presupposition failure:
  97
  98 <pre>
  99 let add' (u:int option) (v:int option) =
 100   match (u, v) with
 101           (None, _) -> None
 102     | (_, None) -> None
 103     | (Some x, Some y) -> Some (x + y);;
 104
 105 (*
 106 val add' : int option -> int option -> int option = <fun>
 107 # add' (Some 12) (Some 4);;
 108 - : int option = Some 16
 109 # add' (div' (Some 12) (Some 0)) (Some 4);;
 110 - : int option = None
 111 *)
 112 </pre>
 113
 114 This works, but is somewhat disappointing: the `add'` operation
 115 doesn't trigger any presupposition of its own, so it is a shame that
 116 it needs to be adjusted because someone else might make trouble.
 117
 118 But we can automate the adjustment.  The standard way in OCaml,
 119 Haskell, etc., is to define a `bind` operator (the name `bind` is not
 120 well chosen to resonate with linguists, but what can you do). To continue our mnemonic association, we'll put a `'` after the name "bind" as well.
 121
 122 <pre>
 123 let bind' (u: int option) (f: int -> (int option)) =
 124   match u with
 125           None -> None
 126     | Some x -> f x;;
 127
 128 let add' (u: int option) (v: int option)  =
 129   bind' u (fun x -> bind' v (fun y -> Some (x + y)));;
 130
 131 let div' (u: int option) (v: int option) =
 132   bind' u (fun x -> bind' v (fun y -> if (0 = y) then None else Some (x / y)));;
 133
 134 (*
 135 #  div' (div' (Some 12) (Some 2)) (Some 3);;
 136 - : int option = Some 2
 137 #  div' (div' (Some 12) (Some 0)) (Some 3);;
 138 - : int option = None
 139 # add' (div' (Some 12) (Some 0)) (Some 3);;
 140 - : int option = None
 141 *)
 142 </pre>
 143
 144 Compare the new definitions of `add'` and `div'` closely: the definition
 145 for `add'` shows what it looks like to equip an ordinary operation to
 146 survive in dangerous presupposition-filled world.  Note that the new
 147 definition of `add'` does not need to test whether its arguments are
 148 None objects or real numbers---those details are hidden inside of the
 149 `bind'` function.
 150
 151 The definition of `div'` shows exactly what extra needs to be said in
 152 order to trigger the no-division-by-zero presupposition.
 153
 154 [Linguitics note: Dividing by zero is supposed to feel like a kind of
 155 presupposition failure.  If we wanted to adapt this approach to
 156 building a simple account of presupposition projection, we would have
 157 to do several things.  First, we would have to make use of the
 158 polymorphism of the `option` type.  In the arithmetic example, we only
 159 made use of `int option`s, but when we're composing natural language
 160 expression meanings, we'll need to use types like `N option`, `Det option`,
 161 `VP option`, and so on.  But that works automatically, because we can use
 162 any type for the `'a` in `'a option`.  Ultimately, we'd want to have a
 163 theory of accommodation, and a theory of the situations in which
 164 material within the sentence can satisfy presuppositions for other
 165 material that otherwise would trigger a presupposition violation; but,
 166 not surprisingly, these refinements will require some more
 167 sophisticated techniques than the super-simple Option monad.]
 168
 169