towards_monads.mdwn

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