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. We're part of the backlash that
11 prefers to say that monads are (Just) monads.
13 The closest we will come to metaphorical talk is to suggest that
14 monadic types place objects inside of *boxes*, and that monads wrap
15 and unwrap boxes to expose or enclose the objects inside of them. In
16 any case, the emphasis will be on starting with the abstract structure
17 of monads, followed by instances of monads from the philosophical and
18 linguistics literature.
20 ## Box types: type expressions with one free type variable
22 Recall that we've been using lower-case Greek letters
23 <code>α, β, γ, ...</code> as variables over types. We'll
24 use `P`, `Q`, `R`, and `S` as metavariables over type schemas, where a
25 type schema is a type expression that may or may not contain unbound
26 type variables. For instance, we might have
35 A *box type* will be a type expression that contains exactly one free
36 type variable. Some examples (using OCaml's type conventions):
40 (α, P) Tree (assuming P contains no free type variables)
43 The idea is that whatever type the free type variable α might be,
44 the boxed type will be a box that "contains" an object of type α.
45 For instance, if `α List` is our box type, and α is the basic type
46 Int, then in this context, `Int List` is the type of a boxed integer.
48 We'll often write box types as a box containing the value of the free
49 type variable. So if our box type is `α List`, and `α == Int`, we
54 for the type of a boxed Int.
58 At the most general level, we'll talk about *Kleisli arrows*:
62 A Kleisli arrow is the type of a function from objects of type P to
63 objects of type box Q, for some choice of type expressions P and Q.
64 For instance, the following are arrows:
68 Int List -> <u>Int List</u>
70 Note that the left-hand schema can itself be a boxed type. That is,
71 if `α List` is our box type, we can write the second arrow as
73 <u>Int</u> -> <u><u>Int</u></u>
75 We'll need a number of classes of functions to help us maneuver in the
76 presence of box types. We will want to define a different instance of
77 each of these for whichever box type we're dealing with:
79 <code>mid (/εmaidεnt@tI/ aka unit, return, pure): P -> <u>P</u></code>
81 <code>map (/maep/): (P -> Q) -> <u>P</u> -> <u>Q</u></code>
83 <code>map2 (/maeptu/): (P -> Q -> R) -> <u>P</u> -> <u>Q</u> -> <u>R</u></code>
85 <code>mapply (/εm@plai/): <u>P -> Q</u> -> <u>P</u> -> <u>Q</u></code>
87 <code>mcompose (aka <=<): (Q -> <u>R</u>) -> (P -> <u>Q</u>) -> (P -> <u>R</u>)</code>
89 <code>mbind (aka >>=): ( <u>Q</u>) -> (Q -> <u>R</u>) -> ( <u>R</u>)</code>
91 <code>mflipcompose (aka >=>): (P -> <u>Q</u>) -> (Q -> <u>R</u>) -> (P -> <u>R</u>)</code>
93 <code>mflipbind (aka =<<) ( <u>Q</u>) -> (Q -> <u>R</u>) -> ( <u>R</u>)</code>
95 <code>mjoin: <u><u>P</u></u> -> <u>P</u></code>
97 The managerie isn't quite as bewildering as you might suppose. For
98 one thing, `mcompose` and `mbind` are interdefinable: <code>u >=> k ≡
99 \a. (ja >>= k)</code>.
101 In most cases of interest, instances of these types will provide
102 certain useful guarantees.
104 * ***Mappable*** ("functors") At the most general level, box types are *Mappable*
105 if there is a `map` function defined for that box type with the type given above.
107 * ***MapNable*** ("applicatives") A Mappable box type is *MapNable*
108 if there are in addition `map2`, `mid`, and `mapply`. (With
109 `map2` in hand, `map3`, `map4`, ... `mapN` are easily definable.)
111 * ***Monad*** ("composable") A MapNable box type is a *Monad* if there
112 is in addition an `mcompose` and a `join` such that `mid` is be
113 a left and right identity for `mcompose`, and `mcompose` is
114 associative. That is, the following "laws" must hold:
118 mcompose (mcompose j k) l = mcompose j (mcompose k l)
120 To take a trivial (but, as we will see, still useful) example,
121 consider the identity box type Id: `α -> α`. So if α is type Bool,
122 then a boxed α is ... a Bool. In terms of the box analogy, the
123 Identity box type is a completly invisible box. With the following
127 mcompose ≡ \f\g\x.f(gx)
129 Id is a monad. Here is a demonstration that the laws hold:
131 mcompose mid k == (\f\g\x.f(gx)) (\p.p) k
135 mcompose k mid == (\f\g\x.f(gx)) k (\p.p)
139 mcompose (mcompose j k) l == mcompose ((\f\g\x.f(gx)) j k) l
140 ~~> mcompose (\x.j(kx)) l
141 == (\f\g\x.f(gx)) (\x.j(kx)) l
142 ~~> \x.(\x.j(kx))(lx)
144 mcompose j (mcompose k l) == mcompose j ((\f\g\x.f(gx)) k l)
145 ~~> mcompose j (\x.k(lx))
146 == (\f\g\x.f(gx)) j (\x.k(lx))
147 ~~> \x.j((\x.k(lx)) x)
150 Id is the favorite monad of mimes everywhere.
152 To take a slightly less trivial (and even more useful) example,
153 consider the box type `α List`, with the following operations:
158 mcompose-crossy: (β -> [γ]) -> (α -> [β]) -> (α -> [γ])
159 mcompose-crossy f g a = [c | b <- g a, c <- f b]
161 In words, `mcompose f g a` feeds the a (which has type α) to g, which
162 returns a list of βs; each β in that list is fed to f, which returns a
163 list of γs. The final result is the concatenation of those lists of γs.
166 let f b = [b, b+1] in
167 let g a = [a*a, a+a] in
168 mcompose-crossy f g 7 = [49, 50, 14, 15]
170 It is easy to see that these definitions obey the monad laws (see exercises).
172 There can be multiple monads for any given box type. For isntance,
173 using the same box type and the same mid, we can define
175 mcompose-zippy f g a = match (f,g) with
178 (f:ftail, g:gtail) -> f(ga) && mcompoze-zippy ftail gtail a