rename topics/_coroutines_and_aborts.mdwn to topics/week13_coroutines_exceptions_and_...
[lambda.git] / topics / week8_safe_division_with_monads.mdwn
1 As we discussed in class, there are clear patterns shared between lists and option types and trees, so perhaps you can see why people want to figure out the general structures. But it probably isn't obvious yet why it would be useful to do so. To a large extent, this will only emerge over the next few classes. But we'll begin to demonstrate the usefulness of these patterns by talking through a simple example, that uses the monadic functions of the Option/Maybe box type.
2
3 OCaml's `/` operator expresses integer division, which throws away any remainder, thus:
4
5     # 11/3;;
6     - : int = 3
7
8 Integer division presupposes that its second argument
9 (the divisor) is not zero, upon pain of presupposition failure.
10 Here's what my OCaml interpreter says:
11
12     # 11/0;;
13     Exception: Division_by_zero.
14
15 Say we want to explicitly allow for the possibility that
16 division will return something other than a number.
17 To do that, we'll use OCaml's `option` type, which works like this:
18
19     # type 'a option = None | Some of 'a;;
20     # None;;
21     - : 'a option = None
22     # Some 3;;
23     - : int option = Some 3
24
25 So if a division is normal, we return some number, but if the divisor is
26 zero, we return `None`. As a mnemonic aid, we'll prepend a `safe_` to the start of our new divide function.
27
28 <pre>
29 let safe_div (x : int) (y : int) =
30   match y with
31     | 0 -> None
32     | _ -> Some (x / y);;
33
34 (* an Ocaml session could continue with OCaml's response:
35 val safe_div : int -> int -> int option = fun
36 # safe_div 12 2;;
37 - : int option = Some 6
38 # safe_div 12 0;;
39 - : int option = None
40 # safe_div (safe_div 12 2) 3;;
41             ~~~~~~~~~~~~~
42 Error: This expression has type int option
43        but an expression was expected of type int
44 *)
45 </pre>
46
47 This starts off well: dividing `12` by `2`, no problem; dividing `12` by `0`,
48 just the behavior we were hoping for. But we want to be able to use
49 the output of the safe-division function as input for further division
50 operations. So we have to jack up the types of the inputs:
51
52 <pre>
53 let safe_div2 (u : int option) (v : int option) =
54   match u with
55   | None -> None
56   | Some x ->
57       (match v with
58       | None -> None
59       | Some 0 -> None
60       | Some y -> Some (x / y));;
61
62 (* an Ocaml session could continue with OCaml's response:
63 val safe_div2 : int option -> int option -> int option = <fun>
64 # safe_div2 (Some 12) (Some 2);;
65 - : int option = Some 6
66 # safe_div2 (Some 12) (Some 0);;
67 - : int option = None
68 # safe_div2 (safe_div2 (Some 12) (Some 0)) (Some 3);;
69 - : int option = None
70 *)
71 </pre>
72
73 Calling the function now involves some extra verbosity, but it gives us what we need: now we can try to divide by anything we
74 want, without fear that we're going to trigger system errors.
75
76 I prefer to line up the `match` alternatives by using OCaml's
77 built-in tuple type:
78
79 <pre>
80 let safe_div2 (u : int option) (v : int option) =
81   match (u, v) with
82   | (None, _) -> None
83   | (_, None) -> None
84   | (_, Some 0) -> None
85   | (Some x, Some y) -> Some (x / y);;
86 </pre>
87
88 So far so good. But what if we want to combine division with
89 other arithmetic operations? We need to make those other operations
90 aware of the possibility that one of their arguments has already triggered a
91 presupposition failure:
92
93 <pre>
94 let safe_add (u:int option) (v:int option) =
95   match (u, v) with
96     | (None, _) -> None
97     | (_, None) -> None
98     | (Some x, Some y) -> Some (x + y);;
99
100 (* an Ocaml session could continue with OCaml's response:
101 val safe_add : int option -> int option -> int option = <fun>
102 # safe_add (Some 12) (Some 4);;
103 - : int option = Some 16
104 # safe_add (safe_div (Some 12) (Some 0)) (Some 4);;
105 - : int option = None
106 *)
107 </pre>
108
109 So now, wherever before our operations expected an `int`, we'll instead
110 have them accept an `int option`. A `None` input signals that
111 something has gone wrong upstream.
112
113 This works, but is somewhat disappointing: the `safe_add` operation
114 doesn't trigger any presupposition of its own, so it is a shame that
115 it needs to be adjusted because someone else might make trouble.
116
117 But we can automate the adjustment, using the monadic machinery we introduced before.
118 As we said, there needs to be different `>>=`, `map2` and so on operations for each
119 Monad or box type we're working with.
120 Haskell finesses this by "overloading" the single symbol `>>=`; you can just input that
121 symbol and it will calculate from the context of the surrounding type constraints what
122 Monad you must have meant. In OCaml, the monadic operators are not pre-defined, but we will
123 give you a library that has definitions for all the standard Monads, as in Haskell. But you
124 will need to explicitly specify which Monad you mean to be deploying.
125
126 For now, though, we will define our `>>=` and `map2` operations by hand:
127
128 <pre>
129 let (>>=) (u : 'a option) (j : 'a -> 'b option) : 'b option =
130   match u with
131     | None -> None
132     | Some x -> j x;;
133
134 let map2 (f : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) : 'c option =
135   u >>= (fun x -> v >>= (fun y -> Some (f x y)));;
136
137 let safe_add3 = map2 (+);;    (* that was easy *)
138
139 let safe_div3 (u: int option) (v: int option) =
140   u >>= (fun x -> v >>= (fun y -> if 0 = y then None else Some (x / y)));;
141 </pre>
142
143 Haskell has an even more user-friendly notation for defining `safe_div3`, namely:
144
145     safe_div3 :: Maybe Int -> Maybe Int -> Maybe Int
146     safe_div3 u v = do {x <- u;
147                         y <- v;
148                         if 0 == y then Nothing else Just (x `div` y)}
149
150 You can read more about that here:
151
152 *       [Haskell wikibook on do-notation](http://en.wikibooks.org/wiki/Haskell/do_Notation)
153 *       [Yet Another Haskell Tutorial on do-notation](http://en.wikibooks.org/wiki/Haskell/YAHT/Monads#Do_Notation)
154
155
156 Let's see our new functions in action:
157
158 <pre>
159 (* an Ocaml session could continue with OCaml's response:
160 # safe_div3 (safe_div3 (Some 12) (Some 2)) (Some 3);;
161 - : int option = Some 2
162 #  safe_div3 (safe_div3 (Some 12) (Some 0)) (Some 3);;
163 - : int option = None
164 # safe_add3 (safe_div3 (Some 12) (Some 0)) (Some 3);;
165 - : int option = None
166 *)
167 </pre>
168
169 Our definition for `safe_add3` shows what it looks like to equip an ordinary operation to
170 survive in dangerous presupposition-filled world. We just need to `mapN` it "into" the
171 Maybe monad, where `N` is the function's adicity. Note that the new
172 definition of `safe_add3` does not need to test whether its arguments are
173 `None` values or genuine numbers---those details are hidden inside of the
174 `bind` function.
175
176 Note also that our definition of `safe_div3` recovers some of the simplicity of
177 the original `safe_div`, without the complexity introduced by `safe_div2`. We now
178 add exactly what extra is needed to track the no-division-by-zero presupposition. Here, too, we don't
179 need to keep track of what other presuppositions may have already failed
180 for whatever reason on our inputs.
181
182 So what the monadic machinery gives us here is a way to _separate_ thinking
183 about error conditions (such as trying to divide by zero) from thinking about normal
184 arithmetic computations. When we're adding or multiplying, we don't have to worry about generating
185 any new errors, so we would rather not force these operations to explicitly
186 track the difference between `int`s and `int option`s. A linguistics analogy we'll
187 look at soon is that when we're giving the lexical entry for an ordinary
188 extensional verb, we'd rather not be forced to talk about possible worlds. In each case,
189 we instead just have a standard way of "lifting" (`mapN`ing) the relevant notions into
190 the fancier type environment we ultimately want to work in.
191
192 Dividing by zero is supposed to feel like a kind of
193 presupposition failure. If we wanted to adapt this approach to
194 building a simple account of presupposition projection, we would have
195 to do several things. First, we would have to make use of the
196 polymorphism of the `option` type. In the arithmetic example, we only
197 made use of `int option`s, but when we're composing natural language
198 expression meanings, we'll need to use types like `N option`, `Det option`,
199 `VP option`, and so on. But that works automatically, because we can use
200 any type for the `'a` in `'a option`. Ultimately, we'd want to have a
201 theory of accommodation, and a theory of the situations in which
202 material within the sentence can satisfy presuppositions for other
203 material that otherwise would trigger a presupposition violation; but,
204 not surprisingly, these refinements will require some more
205 sophisticated techniques than the super-simple Option/Maybe Monad.
206
207 To illustrate some of the polymorphism, here's how we could `map1` the `is_even` function:
208
209     # let is_even x = (x mod 2 = 0);;
210     val is_even : int -> bool = <fun>
211     # let map (g : 'a -> 'b) (u : 'a option) = u >>= fun x -> Some (g x);;
212     val map : ('a -> 'b) -> 'a option -> 'b option = <fun>
213     # map (is_even);;
214     - : int option -> bool option = <fun>
215
216 Wherever we have a well-defined monad, we can define the `mapN` operations for them in terms
217 of their `>>=` and `⇧`/`mid`. The general pattern is:
218
219     mapN (g : 'a1 -> ... 'an -> 'result) (u1 : 'a1 option) ... (un : 'an option) : 'result option =
220       u1 >>= (fun x1 -> ... un >>= (fun xn -> ⇧(g x1 ... xn)) ...)
221
222 Our above definitions of `map` and `mapN` were of this form, except we just
223 explicitly supplied the definition of `⇧` for the Option/Maybe monad (namely, in OCamlese, the constructor `Some`).
224 If you substitute in the definition of `>>=`, you can see these are equivalent to:
225
226     map (g : 'a -> 'b) (u : 'a option) =
227       match u with
228       | None -> None
229       | Some x -> Some (g x)
230
231     map2 (g : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) =
232       match u with
233       | None -> None
234       | Some x ->
235           (match v with
236           | None -> None
237           | Some y -> Some (g x y));;