(*
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:
(*
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>
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>
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>