-------------------------
To construct a monad, the key element is to settle on a type
-constructor, and the monad naturally follows from that. I'll remind
+constructor, and the monad naturally follows from that. We'll remind
you of some examples of how monads follow from the type constructor in
a moment. This will involve some review of familair material, but
it's worth doing for two reasons: it will set up a pattern for the new
then we can deduce the unit and the bind:
- runit x:'a -> 'a reader = fun (e:env) -> x
+ r_unit x:'a -> 'a reader = fun (e:env) -> x
Since the type of an `'a reader` is `fun e:env -> 'a` (by definition),
-the type of the `runit` function is `'a -> e:env -> 'a`, which is a
+the type of the `r_unit` function is `'a -> e:env -> 'a`, which is a
specific case of the type of the *K* combinator. So it makes sense
that *K* is the unit for the reader monad.
We have to open up the `u` box and get out the `'a` object in order to
feed it to `f`. Since `u` is a function from environments to
-objects of type `'a`, we'll have
+objects of type `'a`, the way we open a box in this monad is
+by applying it to an environment:
.... f (u e) ...
This subexpression types to `'b reader`, which is good. The only
-problem is that we don't have an `e`, so we have to abstract over that
-variable:
+problem is that we invented an environment `e` that we didn't already have ,
+so we have to abstract over that variable to balance the books:
fun e -> f (u e) ...
This types to `env -> 'b reader`, but we want to end up with `env ->
-'b`. The easiest way to turn a 'b reader into a 'b is to apply it to
+'b`. Once again, the easiest way to turn a `'b reader` into a `'b` is to apply it to
an environment. So we end up as follows:
r_bind (u:'a reader) (f:'a -> 'b reader):('b reader) = f (u e) e
And we're done.
+[This bind is a simplified version of the careful `let a = u e in ...`
+constructions we provided in earlier lectures. We use the simplified
+versions here in order to emphasize similarities of structure across
+monads; the official bind is still the one with the plethora of `let`'s.]
+
The **State Monad** is similar. We somehow intuit that we want to use
the following type constructor:
But where is the reasoning that led us to this unit and bind?
And what is the type `['a]`? Magic.
-So let's take a *completely useless digressing* and see if we can
-gain some insight into the details of the List monad. Let's choose
-type constructor that we can peer into, using some of the technology
-we built up so laboriously during the first half of the course. I'm
-going to use type 3 lists, partly because I know they'll give the
-result I want, but also because they're my favorite. These were the
-lists that made lists look like Church numerals with extra bits
-embdded in them:
+So let's indulge ourselves in a completely useless digression and see
+if we can gain some insight into the details of the List monad. Let's
+choose type constructor that we can peer into, using some of the
+technology we built up so laboriously during the first half of the
+course. We're going to use type 3 lists, partly because I know
+they'll give the result I want, but also because they're the coolest.
+These were the lists that made lists look like Church numerals with
+extra bits embdded in them:
empty list: fun f z -> z
list with one element: fun f z -> f 1 z
Finally, we're getting consistent principle types, so we can stop.
These types should remind you of the simply-typed lambda calculus
types for Church numerals (`(o -> o) -> o -> o`) with one extra bit
-thrown in (in this case, and int).
+thrown in (in this case, an int).
So here's our type constructor for our hand-rolled lists:
So an `('a, 'b) list'` is a list containing elements of type `'a`,
where `'b` is the type of some part of the plumbing. This is more
general than an ordinary Ocaml list, but we'll see how to map them
-into Ocaml lists soon. We don't need to grasp the role of the `'b`'s
+into Ocaml lists soon. We don't need to fully grasp the role of the `'b`'s
in order to proceed to build a monad:
l'_unit (x:'a):(('a, 'b) list) = fun x -> fun f z -> f x z
and a `z` that will turn our hand-crafted lists into standard Ocaml
lists, so that they will print out.
+<pre>
# let cons h t = h :: t;; (* Ocaml is stupid about :: *)
# l'_bind (fun f z -> f 1 (f 2 z))
(fun i -> fun f z -> f i (f (i+1) z)) cons [];;
- : int list = [1; 2; 2; 3]
+</pre>
Ta da!
-Just for mnemonic purposes (sneaking in an instance of eta reduction
-to the definition of unit), we can summarize the result as follows:
-
- type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b
- l'_unit x = fun f -> f x
- l'_bind u f = fun k -> u (fun x -> f x k)
-
To bad this digression, though it ties together various
elements of the course, has *no relevance whatsoever* to the topic of
continuations.
This function wraps up an individual in a fancy box. That is to say,
we are in the presence of a monad. The type constructor, the unit and
-the bind follow naturally. We've done this enough times that I won't
+the bind follow naturally. We've done this enough times that we won't
belabor the construction of the bind function, the derivation is
similar to the List monad just given:
l'_unit x = fun f -> f x
l'_bind u f = fun k -> u (fun x -> f x k)
-(I performed a sneaky but valid eta reduction in the unit term.)
+(We performed a sneaky but valid eta reduction in the unit term.)
The unit and the bind for the Montague continuation monad and the
homemade List monad are the same terms! In other words, the behavior
indefinites and Hamblin semantics on the linguistic side, and
non-determinism on the list monad side.
+Refunctionalizing zippers
+-------------------------
+