4 Towards Monads: Safe division
5 -----------------------------
7 [This section used to be near the end of the lecture notes for week 6]
9 We begin by reasoning about what should happen when someone tries to
10 divide by zero. This will lead us to a general programming technique
11 called a *monad*, which we'll see in many guises in the weeks to come.
13 Integer division presupposes that its second argument
14 (the divisor) is not zero, upon pain of presupposition failure.
15 Here's what my OCaml interpreter says:
18 Exception: Division_by_zero.
20 So we want to explicitly allow for the possibility that
21 division will return something other than a number.
22 We'll use OCaml's `option` type, which works like this:
24 # type 'a option = None | Some of 'a;;
28 - : int option = Some 3
30 So if a division is normal, we return some number, but if the divisor is
31 zero, we return `None`. As a mnemonic aid, we'll append a `'` to the end of our new divide function.
34 let div' (x:int) (y:int) =
40 val div' : int -> int -> int option = fun
42 - : int option = Some 6
45 # div' (div' 12 2) 3;;
49 Error: This expression has type int option
50 but an expression was expected of type int
54 This starts off well: dividing 12 by 2, no problem; dividing 12 by 0,
55 just the behavior we were hoping for. But we want to be able to use
56 the output of the safe-division function as input for further division
57 operations. So we have to jack up the types of the inputs:
60 let div' (u:int option) (v:int option) =
63 | Some x -> (match v with
65 | Some y -> Some (x / y));;
68 val div' : int option -> int option -> int option = <fun>
69 # div' (Some 12) (Some 2);;
70 - : int option = Some 6
71 # div' (Some 12) (Some 0);;
73 # div' (div' (Some 12) (Some 0)) (Some 3);;
78 Beautiful, just what we need: now we can try to divide by anything we
79 want, without fear that we're going to trigger any system errors.
81 I prefer to line up the `match` alternatives by using OCaml's
85 let div' (u:int option) (v:int option) =
90 | (Some x, Some y) -> Some (x / y);;
93 So far so good. But what if we want to combine division with
94 other arithmetic operations? We need to make those other operations
95 aware of the possibility that one of their arguments has triggered a
96 presupposition failure:
99 let add' (u:int option) (v:int option) =
103 | (Some x, Some y) -> Some (x + y);;
106 val add' : int option -> int option -> int option = <fun>
107 # add' (Some 12) (Some 4);;
108 - : int option = Some 16
109 # add' (div' (Some 12) (Some 0)) (Some 4);;
110 - : int option = None
114 This works, but is somewhat disappointing: the `add'` operation
115 doesn't trigger any presupposition of its own, so it is a shame that
116 it needs to be adjusted because someone else might make trouble.
118 But we can automate the adjustment. The standard way in OCaml,
119 Haskell, etc., is to define a `bind` operator (the name `bind` is not
120 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.
123 let bind' (u: int option) (f: int -> (int option)) =
128 let add' (u: int option) (v: int option) =
129 bind' u (fun x -> bind' v (fun y -> Some (x + y)));;
131 let div' (u: int option) (v: int option) =
132 bind' u (fun x -> bind' v (fun y -> if (0 = y) then None else Some (x / y)));;
135 # div' (div' (Some 12) (Some 2)) (Some 3);;
136 - : int option = Some 2
137 # div' (div' (Some 12) (Some 0)) (Some 3);;
138 - : int option = None
139 # add' (div' (Some 12) (Some 0)) (Some 3);;
140 - : int option = None
144 Compare the new definitions of `add'` and `div'` closely: the definition
145 for `add'` shows what it looks like to equip an ordinary operation to
146 survive in dangerous presupposition-filled world. Note that the new
147 definition of `add'` does not need to test whether its arguments are
148 None objects or real numbers---those details are hidden inside of the
151 The definition of `div'` shows exactly what extra needs to be said in
152 order to trigger the no-division-by-zero presupposition.
154 [Linguitics note: Dividing by zero is supposed to feel like a kind of
155 presupposition failure. If we wanted to adapt this approach to
156 building a simple account of presupposition projection, we would have
157 to do several things. First, we would have to make use of the
158 polymorphism of the `option` type. In the arithmetic example, we only
159 made use of `int option`s, but when we're composing natural language
160 expression meanings, we'll need to use types like `N option`, `Det option`,
161 `VP option`, and so on. But that works automatically, because we can use
162 any type for the `'a` in `'a option`. Ultimately, we'd want to have a
163 theory of accommodation, and a theory of the situations in which
164 material within the sentence can satisfy presuppositions for other
165 material that otherwise would trigger a presupposition violation; but,
166 not surprisingly, these refinements will require some more
167 sophisticated techniques than the super-simple Option monad.]