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.
3 OCaml's `/` operator expresses integer division, which throws away any remainder, thus:
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:
13 Exception: Division_by_zero.
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:
19 # type 'a option = None | Some of 'a;;
23 - : int option = Some 3
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.
29 let safe_div (x : int) (y : int) =
34 (* an Ocaml session could continue with OCaml's response:
35 val safe_div : int -> int -> int option = fun
37 - : int option = Some 6
40 # safe_div (safe_div 12 2) 3;;
42 Error: This expression has type int option
43 but an expression was expected of type int
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:
53 let safe_div2 (u : int option) (v : int option) =
60 | Some y -> Some (x / y));;
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);;
68 # safe_div2 (safe_div2 (Some 12) (Some 0)) (Some 3);;
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.
76 I prefer to line up the `match` alternatives by using OCaml's
80 let safe_div2 (u : int option) (v : int option) =
85 | (Some x, Some y) -> Some (x / y);;
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:
94 let safe_add (u:int option) (v:int option) =
98 | (Some x, Some y) -> Some (x + y);;
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
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.
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.
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.
126 For now, though, we will define our `>>=` and `map2` operations by hand:
129 let (>>=) (u : 'a option) (j : 'a -> 'b option) : 'b option =
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)));;
137 let safe_add3 = map2 (+);; (* that was easy *)
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)));;
143 Haskell has an even more user-friendly notation for defining `safe_div3`, namely:
145 safe_div3 :: Maybe Int -> Maybe Int -> Maybe Int
146 safe_div3 u v = do {x <- u;
148 if 0 == y then Nothing else Just (x `div` y)}
150 You can read more about that here:
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)
156 Let's see our new functions in action:
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
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
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.
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.
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.
207 To illustrate some of the polymorphism, here's how we could `map1` the `is_even` function:
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>
214 - : int option -> bool option = <fun>
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:
219 mapN (g : 'a1 -> ... 'an -> 'result) (u1 : 'a1 option) ... (un : 'an option) : 'result option =
220 u1 >>= (fun x1 -> ... un >>= (fun xn -> ⇧(g x1 ... xn)) ...)
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:
226 map (g : 'a -> 'b) (u : 'a option) =
229 | Some x -> Some (g x)
231 map2 (g : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) =
237 | Some y -> Some (g x y));;