223c592bc128b77b34c94de0db6420690b478fd5
1 Dividing by zero
2 ----------------
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:
8     # 12/0;;
9     Exception: Division_by_zero.
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:
15     # type 'a option = None | Some of 'a;;
16     # None;;
17     - : 'a option = None
18     # Some 3;;
19     - : int option = Some 3
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.
24 <pre>
25 let div' (x:int) (y:int) =
26   match y with 0 -> None |
27                _ -> Some (x / y);;
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>
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:
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));;
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>
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.
70 I prefer to line up the `match` alternatives by using OCaml's
71 built-in tuple type:
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>
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:
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);;
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>
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.
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.
109 <pre>
110 let bind' (x: int option) (f: int -> (int option)) =
111   match x with None -> None |
112                Some n -> f n;;
114 let add' (x: int option) (y: int option)  =
115   bind' x (fun x -> bind' y (fun y -> Some (x + y)));;
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)));;
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>
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.
137 The definition of `div'` shows exactly what extra needs to be said in
138 order to trigger the no-division-by-zero presupposition.
140 For linguists: this is a complete theory of a particularly simply form
141 of presupposition projection (every predicate is a hole).