1 <!-- λ Λ ∀ ≡ α β γ ρ ω Ω -->
2 <!-- Loved this one: http://www.stephendiehl.com/posts/monads.html -->
7 The [[tradition in the functional programming
8 literature|https://wiki.haskell.org/Monad_tutorials_timeline]] is to
9 introduce monads using a metaphor: monads are spacesuits, monads are
10 monsters, monads are burritos. These metaphors can be helpful, and they
11 can be unhelpful. There's a backlash about the metaphors that tells people
12 to instead just look at the formal definition. We'll give that to you below, but it's
13 sometimes sloganized as
14 [A monad is just a monoid in the category of endofunctors, what's the problem?](http://stackoverflow.com/questions/3870088).
15 Without some intuitive guidance, this can also be unhelpful. We'll try to find a good balance.
17 The closest we will come to metaphorical talk is to suggest that
18 monadic types place objects inside of *boxes*, and that monads wrap
19 and unwrap boxes to expose or enclose the objects inside of them. In
20 any case, our emphasis will be on starting with the abstract structure
21 of monads, followed by instances of monads from the philosophical and
22 linguistics literature.
24 ## Box types: type expressions with one free type variable
26 Recall that we've been using lower-case Greek letters
27 <code>α, β, γ, ...</code> as type variables. We'll
28 use `P`, `Q`, `R`, and `S` as schematic metavariables over type expressions, that may or may not contain unbound
29 type variables. For instance, we might have
38 A *box type* will be a type expression that contains exactly one free
39 type variable. (You could extend this to expressions with more free variables; then you'd have
40 to specify which one of them the box is capturing. But let's keep it simple.) Some examples (using OCaml's type conventions):
44 (α, R) tree (assuming R contains no free type variables)
47 The idea is that whatever type the free type variable α might be,
48 the boxed type will be a box that "contains" an object of type `α`.
49 For instance, if `α list` is our box type, and `α` is the type
50 `int`, then in this context, `int list` is the type of a boxed integer.
52 Warning: although our initial motivating examples are naturally thought of as "containers" (lists, trees, and so on, with `α`s as their "elments"), with later examples we discuss it will less intuitive to describe the box types that way. For example, where `R` is some fixed type, `R -> α` is a box type.
54 The *box type* is the type `α list` (or as we might just say, `list`); the *boxed type* is some specific instantiantion of the free type variable `α`. We'll often write boxed types as a box containing the instance of the free
55 type variable. So if our box type is `α List`, and `α` is instantiated with the specific type `int`, we would write:
59 for the type of a boxed `int`. (We'll fool with the markup to make this a genuine box later; for now it will just display as underlined.)
65 A lot of what we'll be doing concerns types that are called *Kleisli arrows*. Don't worry about why they're called that, or if you like go read some Category Theory. All we need to know is that these are functions whose type has the form:
69 That is, they are functions from objects of one type `P` to a boxed type `Q`, for some choice of type expressions `P` and `Q`.
70 For instance, the following are Kleisli arrows:
74 Int List -> <u>Int List</u>
76 In the first, `P` has become `Int` and `Q` has become `Bool`. (The boxed type <u>Q</u> is <u>Bool</u>).
78 Note that the left-hand schema `P` is permitted to itself be a boxed type. That is, where
79 if `α List` is our box type, we can write the second arrow as
81 <u>Int</u> -> <u>Q</u>
83 We'll need a number of classes of functions to help us maneuver in the
84 presence of box types. We will want to define a different instance of
85 each of these for whichever box type we're dealing with. (This will
86 become clearly shortly.)
88 Here are the types of our crucial functions, together with our pronunciation, and some other names the functions go by. (Usually the type doesn't fix their behavior, which will be discussed below.)
90 <code>map (/maep/): (P -> Q) -> <u>P</u> -> <u>Q</u></code>
92 <code>map2 (/m&ash;ptu/): (P -> Q -> R) -> <u>P</u> -> <u>Q</u> -> <u>R</u></code>
94 <code>mid (/εmaidεnt@tI/ aka unit, return, pure): P -> <u>P</u></code>
96 <code>mapply (/εm@plai/): <u>P -> Q</u> -> <u>P</u> -> <u>Q</u></code>
98 <code>mcomp (aka <=<): (Q -> <u>R</u>) -> (P -> <u>Q</u>) -> (P -> <u>R</u>)</code>
100 <code>mpmoc (or m-flipcomp, aka >=>): (P -> <u>Q</u>) -> (Q -> <u>R</u>) -> (P -> <u>R</u>)</code>
102 <code>mbind (aka >>=): ( <u>Q</u>) -> (Q -> <u>R</u>) -> ( <u>R</u>)</code>
104 <code>mdnib (or m-flipbind, aka =<<) ( <u>Q</u>) -> (Q -> <u>R</u>) -> ( <u>R</u>)</code>
106 <code>join: <u>2<u>P</u></u> -> <u>P</u></code>
108 The managerie isn't quite as bewildering as you might suppose. Many of these will
109 be interdefinable. For example, here is how `mcomp` and `mbind` are related: <code>k <=< j ≡
110 \a. (j a >>= k)</code>.
112 In most cases of interest, instances of these systems of functions will provide
113 certain useful guarantees.
115 * ***Mappable*** ("functors") At the most general level, box types are *Mappable*
116 if there is a `map` function defined for that box type with the type given above.
118 * ***MapNable*** ("applicatives") A Mappable box type is *MapNable*
119 if there are in addition `map2`, `mid`, and `mapply`. (Given either
120 of `map2` and `mapply`, you can define the other, and also `map`.
121 Moreover, with `map2` in hand, `map3`, `map4`, ... `mapN` are easily definable.)
123 * ***Monad*** ("composables") A MapNable box type is a *Monad* if there
124 is in addition an associative `mcomp` having `mid` as its left and
125 right identity. That is, the following "laws" must hold:
127 mcomp mid k (that is, mid <=< k) = k
128 mcomp k mid (that is, k <=< mid) = k
129 mcomp (mcomp j k) l (that is, (j <=< k) <=< l) = mcomp j (mcomp k l)
131 If you have any of `mcomp`, `mpmoc`, `mbind`, or `join`, you can use them to define the others.
132 Also, with the functions you can define `mapply` and `map2` from *MapNables*. So all you really need
133 are a definition of `mid`, on the one hand, and one of `mcomp`, `mbind`, or `join`, on the other.
135 Here are some interdefinitions: TODO. Names in Haskell TODO. Laws TODO.
139 To take a trivial (but, as we will see, still useful) example,
140 consider the identity box type Id: `α`. So if `α` is type `bool`,
141 then a boxed `α` is ... a `bool`. In terms of the box analogy, the
142 Identity box type is a completely invisible box. With the following
146 mcomp ≡ \f g x.f (g x)
148 Identity is a monad. Here is a demonstration that the laws hold:
150 mcomp mid k == (\fgx.f(gx)) (\p.p) k
154 mcomp k mid == (\fgx.f(gx)) k (\p.p)
158 mcomp (mcomp j k) l == mcomp ((\fgx.f(gx)) j k) l
159 ~~> mcomp (\x.j(kx)) l
160 == (\fgx.f(gx)) (\x.j(kx)) l
161 ~~> \x.(\x.j(kx))(lx)
163 mcomp j (mcomp k l) == mcomp j ((\fgx.f(gx)) k l)
164 ~~> mcomp j (\x.k(lx))
165 == (\fgx.f(gx)) j (\x.k(lx))
166 ~~> \x.j((\x.k(lx)) x)
169 Id is the favorite monad of mimes.
171 To take a slightly less trivial (and even more useful) example,
172 consider the box type `α List`, with the following operations:
177 mcomp: (β -> [γ]) -> (α -> [β]) -> (α -> [γ])
178 mcomp f g a = concat (map f (g a))
179 = foldr (\b -> \gs -> (f b) ++ gs) [] (g a)
180 = [c | b <- g a, c <- f b]
182 These three definitions of `mcomp` are all equivalent. In words, `mcomp f g
183 a` feeds the `a` (which has type `α`) to `g`, which returns a list of `β`s;
184 each `β` in that list is fed to `f`, which returns a list of `γ`s. The
185 final result is the concatenation of those lists of `γ`s.
189 let f b = [b, b+1] in
190 let g a = [a*a, a+a] in
191 mcomp f g 7 ==> [49, 50, 14, 15]
193 It is easy to see that these definitions obey the monad laws (see exercises).
195 Contrast the preceding to `mapply`, which operates not on two box-producing *functions*, but instead on two *values of a boxed type*, one containing functions to be applied to the values in the other box, via some predefined scheme. Thus:
197 let gs = [(\a->a*a),(\a->a+a)] in
199 mapply gs xs ==> [49,25,14,10]
208 Towards Monads: Safe division
209 -----------------------------
211 [This section used to be near the end of the lecture notes for week 6]
213 We begin by reasoning about what should happen when someone tries to
214 divide by zero. This will lead us to a general programming technique
215 called a *monad*, which we'll see in many guises in the weeks to come.
217 Integer division presupposes that its second argument
218 (the divisor) is not zero, upon pain of presupposition failure.
219 Here's what my OCaml interpreter says:
222 Exception: Division_by_zero.
224 So we want to explicitly allow for the possibility that
225 division will return something other than a number.
226 We'll use OCaml's `option` type, which works like this:
228 # type 'a option = None | Some of 'a;;
232 - : int option = Some 3
234 So if a division is normal, we return some number, but if the divisor is
235 zero, we return `None`. As a mnemonic aid, we'll append a `'` to the end of our new divide function.
238 let div' (x:int) (y:int) =
241 | _ -> Some (x / y);;
244 val div' : int -> int -> int option = fun
246 - : int option = Some 6
248 - : int option = None
249 # div' (div' 12 2) 3;;
253 Error: This expression has type int option
254 but an expression was expected of type int
258 This starts off well: dividing 12 by 2, no problem; dividing 12 by 0,
259 just the behavior we were hoping for. But we want to be able to use
260 the output of the safe-division function as input for further division
261 operations. So we have to jack up the types of the inputs:
264 let div' (u:int option) (v:int option) =
267 | Some x -> (match v with
269 | Some y -> Some (x / y));;
272 val div' : int option -> int option -> int option = <fun>
273 # div' (Some 12) (Some 2);;
274 - : int option = Some 6
275 # div' (Some 12) (Some 0);;
276 - : int option = None
277 # div' (div' (Some 12) (Some 0)) (Some 3);;
278 - : int option = None
282 Beautiful, just what we need: now we can try to divide by anything we
283 want, without fear that we're going to trigger any system errors.
285 I prefer to line up the `match` alternatives by using OCaml's
289 let div' (u:int option) (v:int option) =
293 | (_, Some 0) -> None
294 | (Some x, Some y) -> Some (x / y);;
297 So far so good. But what if we want to combine division with
298 other arithmetic operations? We need to make those other operations
299 aware of the possibility that one of their arguments has triggered a
300 presupposition failure:
303 let add' (u:int option) (v:int option) =
307 | (Some x, Some y) -> Some (x + y);;
310 val add' : int option -> int option -> int option = <fun>
311 # add' (Some 12) (Some 4);;
312 - : int option = Some 16
313 # add' (div' (Some 12) (Some 0)) (Some 4);;
314 - : int option = None
318 This works, but is somewhat disappointing: the `add'` operation
319 doesn't trigger any presupposition of its own, so it is a shame that
320 it needs to be adjusted because someone else might make trouble.
322 But we can automate the adjustment. The standard way in OCaml,
323 Haskell, etc., is to define a `bind` operator (the name `bind` is not
324 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.
327 let bind' (u: int option) (f: int -> (int option)) =
332 let add' (u: int option) (v: int option) =
333 bind' u (fun x -> bind' v (fun y -> Some (x + y)));;
335 let div' (u: int option) (v: int option) =
336 bind' u (fun x -> bind' v (fun y -> if (0 = y) then None else Some (x / y)));;
339 # div' (div' (Some 12) (Some 2)) (Some 3);;
340 - : int option = Some 2
341 # div' (div' (Some 12) (Some 0)) (Some 3);;
342 - : int option = None
343 # add' (div' (Some 12) (Some 0)) (Some 3);;
344 - : int option = None
348 Compare the new definitions of `add'` and `div'` closely: the definition
349 for `add'` shows what it looks like to equip an ordinary operation to
350 survive in dangerous presupposition-filled world. Note that the new
351 definition of `add'` does not need to test whether its arguments are
352 None objects or real numbers---those details are hidden inside of the
355 The definition of `div'` shows exactly what extra needs to be said in
356 order to trigger the no-division-by-zero presupposition.
358 [Linguitics note: Dividing by zero is supposed to feel like a kind of
359 presupposition failure. If we wanted to adapt this approach to
360 building a simple account of presupposition projection, we would have
361 to do several things. First, we would have to make use of the
362 polymorphism of the `option` type. In the arithmetic example, we only
363 made use of `int option`s, but when we're composing natural language
364 expression meanings, we'll need to use types like `N option`, `Det option`,
365 `VP option`, and so on. But that works automatically, because we can use
366 any type for the `'a` in `'a option`. Ultimately, we'd want to have a
367 theory of accommodation, and a theory of the situations in which
368 material within the sentence can satisfy presuppositions for other
369 material that otherwise would trigger a presupposition violation; but,
370 not surprisingly, these refinements will require some more
371 sophisticated techniques than the super-simple Option monad.]