towards_monads.mdwn

   1 Dividing by zero
   2 ----------------
   3
   4 Integer division presupposes that its second argument
   5 (the divisor) is not zero, upon pain of presupposition failure.
   6 Here's what my OCaml interpreter says:
   7
   8     # 12/0;;
   9     Exception: Division_by_zero.
  10
  11 So we want to explicitly allow for the possibility that
  12 division will return something other than a number.
  13 We'll use OCaml's `option` type, which works like this:
  14
  15     # type 'a option = None | Some of 'a;;
  16     # None;;
  17     - : 'a option = None
  18     # Some 3;;
  19     - : int option = Some 3
  20
  21 So if a division is normal, we return some number, but if the divisor is
  22 zero, we return `None`. As a mnemonic aid, we'll append a `'` to the end of our new divide function.
  23
  24 <pre>
  25 let div' (x:int) (y:int) =
  26   match y with
  27           0 -> None
  28     | _ -> Some (x / y);;
  29
  30 (*
  31 val div' : int -> int -> int option = fun
  32 # div' 12 3;;
  33 - : int option = Some 4
  34 # div' 12 0;;
  35 - : int option = None
  36 # div' (div' 12 3) 2;;
  37 Characters 4-14:
  38   div' (div' 12 3) 2;;
  39         ^^^^^^^^^^
  40 Error: This expression has type int option
  41        but an expression was expected of type int
  42 *)
  43 </pre>
  44
  45 This starts off well: dividing 12 by 3, no problem; dividing 12 by 0,
  46 just the behavior we were hoping for.  But we want to be able to use
  47 the output of the safe-division function as input for further division
  48 operations.  So we have to jack up the types of the inputs:
  49
  50 <pre>
  51 let div' (u:int option) (v:int option) =
  52   match v with
  53           None -> None
  54     | Some 0 -> None
  55         | Some y -> (match u with
  56                                           None -> None
  57                     | Some x -> Some (x / y));;
  58
  59 (*
  60 val div' : int option -> int option -> int option = <fun>
  61 # div' (Some 12) (Some 4);;
  62 - : int option = Some 3
  63 # div' (Some 12) (Some 0);;
  64 - : int option = None
  65 # div' (div' (Some 12) (Some 0)) (Some 4);;
  66 - : int option = None
  67 *)
  68 </pre>
  69
  70 Beautiful, just what we need: now we can try to divide by anything we
  71 want, without fear that we're going to trigger any system errors.
  72
  73 I prefer to line up the `match` alternatives by using OCaml's
  74 built-in tuple type:
  75
  76 <pre>
  77 let div' (u:int option) (v:int option) =
  78   match (u, v) with
  79           (None, _) -> None
  80     | (_, None) -> None
  81     | (_, Some 0) -> None
  82         | (Some x, Some y) -> Some (x / y);;
  83 </pre>
  84
  85 So far so good.  But what if we want to combine division with
  86 other arithmetic operations?  We need to make those other operations
  87 aware of the possibility that one of their arguments has triggered a
  88 presupposition failure:
  89
  90 <pre>
  91 let add' (u:int option) (v:int option) =
  92   match (u, v) with
  93           (None, _) -> None
  94     | (_, None) -> None
  95     | (Some x, Some y) -> Some (x + y);;
  96
  97 (*
  98 val add' : int option -> int option -> int option = <fun>
  99 # add' (Some 12) (Some 4);;
 100 - : int option = Some 16
 101 # add' (div' (Some 12) (Some 0)) (Some 4);;
 102 - : int option = None
 103 *)
 104 </pre>
 105
 106 This works, but is somewhat disappointing: the `add'` operation
 107 doesn't trigger any presupposition of its own, so it is a shame that
 108 it needs to be adjusted because someone else might make trouble.
 109
 110 But we can automate the adjustment.  The standard way in OCaml,
 111 Haskell, etc., is to define a `bind` operator (the name `bind` is not
 112 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.
 113
 114 <pre>
 115 let bind' (u: int option) (f: int -> (int option)) =
 116   match u with
 117           None -> None
 118     | Some x -> f x;;
 119
 120 let add' (u: int option) (v: int option)  =
 121   bind' u (fun x -> bind' v (fun y -> Some (x + y)));;
 122
 123 let div' (u: int option) (v: int option) =
 124   bind' u (fun x -> bind' v (fun y -> if (0 = y) then None else Some (x / y)));;
 125
 126 (*
 127 #  div' (div' (Some 12) (Some 2)) (Some 4);;
 128 - : int option = Some 1
 129 #  div' (div' (Some 12) (Some 0)) (Some 4);;
 130 - : int option = None
 131 # add' (div' (Some 12) (Some 0)) (Some 4);;
 132 - : int option = None
 133 *)
 134 </pre>
 135
 136 Compare the new definitions of `add'` and `div'` closely: the definition
 137 for `add'` shows what it looks like to equip an ordinary operation to
 138 survive in dangerous presupposition-filled world.  Note that the new
 139 definition of `add'` does not need to test whether its arguments are
 140 None objects or real numbers---those details are hidden inside of the
 141 `bind'` function.
 142
 143 The definition of `div'` shows exactly what extra needs to be said in
 144 order to trigger the no-division-by-zero presupposition.
 145
 146 For linguists: this is a complete theory of a particularly simply form
 147 of presupposition projection (every predicate is a hole).
 148