Dividing by zero
----------------
-Integer division operation presupposes that its second argument
+Integer division presupposes that its second argument
(the divisor) is not zero, upon pain of presupposition failure.
Here's what my OCaml interpreter says:
So we want to explicitly allow for the possibility that
division will return something other than a number.
-We'll use OCaml's option type, which works like this:
+We'll use OCaml's `option` type, which works like this:
# type 'a option = None | Some of 'a;;
# None;;
- : int option = Some 3
So if a division is normal, we return some number, but if the divisor is
-zero, we return None. As a mnemonic aid, we'll append a `'` to the end of our new divide function.
+zero, we return `None`. As a mnemonic aid, we'll append a `'` to the end of our new divide function.
<pre>
let div' (x:int) (y:int) =
- match y with 0 -> None |
- _ -> Some (x / y);;
+ match y with
+ 0 -> None
+ | _ -> Some (x / y);;
(*
val div' : int -> int -> int option = fun
-# div' 12 3;;
-- : int option = Some 4
+# div' 12 2;;
+- : int option = Some 6
# div' 12 0;;
- : int option = None
-# div' (div' 12 3) 2;;
+# div' (div' 12 2) 3;;
Characters 4-14:
- div' (div' 12 3) 2;;
- ^^^^^^^^^^
+ div' (div' 12 2) 3;;
+ ^^^^^^^^^^
Error: This expression has type int option
but an expression was expected of type int
*)
</pre>
-This starts off well: dividing 12 by 3, no problem; dividing 12 by 0,
+This starts off well: dividing 12 by 2, no problem; dividing 12 by 0,
just the behavior we were hoping for. But we want to be able to use
the output of the safe-division function as input for further division
operations. So we have to jack up the types of the inputs:
<pre>
-let div' (x:int option) (y:int option) =
- match y with None -> None |
- Some 0 -> None |
- Some n -> (match x with None -> None |
- Some m -> Some (m / n));;
+let div' (u:int option) (v:int option) =
+ match v with
+ None -> None
+ | Some 0 -> None
+ | Some y -> (match u with
+ None -> None
+ | Some x -> Some (x / y));;
(*
val div' : int option -> int option -> int option = <fun>
-# div' (Some 12) (Some 4);;
-- : int option = Some 3
+# div' (Some 12) (Some 2);;
+- : int option = Some 6
# div' (Some 12) (Some 0);;
- : int option = None
-# div' (div' (Some 12) (Some 0)) (Some 4);;
+# div' (div' (Some 12) (Some 0)) (Some 3);;
- : int option = None
*)
</pre>
built-in tuple type:
<pre>
-let div' (x:int option) (y:int option) =
- match (x, y) with (None, _) -> None |
- (_, None) -> None |
- (_, Some 0) -> None |
- (Some m, Some n) -> Some (m / n);;
+let div' (u:int option) (v:int option) =
+ match (u, v) with
+ (None, _) -> None
+ | (_, None) -> None
+ | (_, Some 0) -> None
+ | (Some x, Some y) -> Some (x / y);;
</pre>
So far so good. But what if we want to combine division with
other arithmetic operations? We need to make those other operations
-aware of the possibility that one of their arguments will trigger a
+aware of the possibility that one of their arguments has triggered a
presupposition failure:
<pre>
-let add' (x:int option) (y:int option) =
- match (x, y) with (None, _) -> None |
- (_, None) -> None |
- (Some m, Some n) -> Some (m + n);;
+let add' (u:int option) (v:int option) =
+ match (u, v) with
+ (None, _) -> None
+ | (_, None) -> None
+ | (Some x, Some y) -> Some (x + y);;
(*
val add' : int option -> int option -> int option = <fun>
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.
<pre>
-let bind' (x: int option) (f: int -> (int option)) =
- match x with None -> None |
- Some n -> f n;;
+let bind' (u: int option) (f: int -> (int option)) =
+ match u with
+ None -> None
+ | Some x -> f x;;
-let add' (x: int option) (y: int option) =
- bind' x (fun x -> bind' y (fun y -> Some (x + y)));;
+let add' (u: int option) (v: int option) =
+ bind' u (fun x -> bind' v (fun y -> Some (x + y)));;
-let div' (x: int option) (y: int option) =
- bind' x (fun x -> bind' y (fun y -> if (0 = y) then None else Some (x / y)));;
+let div' (u: int option) (v: int option) =
+ bind' u (fun x -> bind' v (fun y -> if (0 = y) then None else Some (x / y)));;
(*
-# div' (div' (Some 12) (Some 2)) (Some 4);;
-- : int option = Some 1
-# div' (div' (Some 12) (Some 0)) (Some 4);;
+# div' (div' (Some 12) (Some 2)) (Some 3);;
+- : int option = Some 2
+# div' (div' (Some 12) (Some 0)) (Some 3);;
- : int option = None
-# add' (div' (Some 12) (Some 0)) (Some 4);;
+# add' (div' (Some 12) (Some 0)) (Some 3);;
- : int option = None
*)
</pre>