The reason this is a fairly natural choice is that because the type of
an `'a reader` is `env -> 'a` (by definition), the type of the
`r_unit` function is `'a -> env -> 'a`, which is an instance of the
-type of the *K* combinator. So it makes sense that *K* is the unit
+type of the **K** combinator. So it makes sense that **K** is the unit
for the reader monad.
Since the type of the `bind` operator is required to be
objects of type `'a`, the way we open a box in this monad is
by applying it to an environment:
-<pre>
... f (u e) ...
-</pre>
This subexpression types to `'b reader`, which is good. The only
problem is that we made use of an environment `e` that we didn't already have,
This types to `env -> 'b reader`, but we want to end up with `env ->
'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:
-<pre>
-r_bind (u : 'a reader) (f : 'a -> 'b reader) : ('b reader) = f (u e) e
-</pre>
+ r_bind (u : 'a reader) (f : 'a -> 'b reader) : ('b reader) = f (u e) e
And we're done. This gives us a bind function of the right type. We can then check whether, in combination with the unit function we chose, it satisfies the monad laws, and behaves in the way we intend. And it does.
And we can reason our way to the bind function in a way similar to the reasoning given above. First, we need to apply `f` to the contents of the `u` box:
- let s_bind (u : 'a state) (f : 'a -> 'b state) : 'b state =
- ... f (...) ...
+ let s_bind (u : 'a state) (f : 'a -> 'b state) : 'b state =
+ ... f (...) ...
But unlocking the `u` box is a little more complicated. As before, we
-need to posit a state `s` that we can apply `u` to. Once we do so,
-however, we won't have an `'a`, we'll have a pair whose first element
+need to posit a store `s` that we can apply `u` to. Once we do so,
+however, we won't have an `'a`; we'll have a pair whose first element
is an `'a`. So we have to unpack the pair:
... let (a, s') = u s in ... (f a) ...
Abstracting over the `s` and adjusting the types gives the result:
- let s_bind (u : 'a state) (f : 'a -> 'b state) : 'b state =
- fun (s : store) -> let (a, s') = u s in f a s'
+ let s_bind (u : 'a state) (f : 'a -> 'b state) : 'b state =
+ fun (s : store) -> let (a, s') = u s in f a s'
The **Option/Maybe Monad** doesn't follow the same pattern so closely, so we
won't pause to explore it here, though conceptually its unit and bind
List.concat [[1; 2]; [2; 3]] ~~> [1; 2; 2; 3]
-And sure enough,
+And sure enough,
l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3]
type `'b list list`. We can elimiate that restriction by flattening
the list of lists into a single list: this is
just List.concat applied to the output of List.map. So there is some logic to the
-choice of unit and bind for the list monad.
+choice of unit and bind for the list monad.
Yet we can still desire to go deeper, and see if the appropriate bind
behavior emerges from the types, as it did for the previously
As usual, we need to unpack the `u` box. Examine the type of `u`.
This time, `u` will only deliver up its contents if we give `u` an
-argument that is a function expecting an `'a` and a `'b`. `u` will
+argument that is a function expecting an `'a` and a `'b`. `u` will
fold that function over its type `'a` members, and that's how we'll get the `'a`s we need. Thus:
... u (fun (a : 'a) (b : 'b) -> ... f a ... ) ...
l'_bind (u : ('a -> 'b -> 'b) -> 'b -> 'b)
(f : 'a -> ('c -> 'b -> 'b) -> 'b -> 'b)
- : ('c -> 'b -> 'b) -> 'b -> 'b =
+ : ('c -> 'b -> 'b) -> 'b -> 'b =
fun k -> u (fun a b -> f a k b)
That is a function of the right type for our bind, but to check whether it works, we have to verify it (with the unit we chose) against the monad laws, and reason whether it will have the right behavior.
Or rather, it should give us a list' version of that, which takes a function `k` and value `z` as arguments, and returns the right fold of `k` and `z` over those elements. What does our formula
fun k z -> u (fun a b -> f a k b) z
-
+
do? Well, for each element `a` in `u`, it applies `f` to that `a`, getting one of the lists:
[]
l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3]
- l'_bind (fun f z -> f 1 (f 2 z))
+ l'_bind (fun f z -> f 1 (f 2 z))
(fun i -> fun f z -> f i (f (i+1) z)) ~~> <fun>
Sigh. OCaml won't show us our own list. So we have to choose an `f`
lists, so that they will print out.
# 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 [];;
+ # 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]
Ta da!
We've hinted that Montague's treatment of DPs as generalized
quantifiers embodies the spirit of continuations (see de Groote 2001,
-Barker 2002 for lengthy discussion). Let's see why.
+Barker 2002 for lengthy discussion). Let's see why.
-First, we'll need a type constructor. As you probably know,
+First, we'll need a type constructor. As you probably know,
Montague replaced individual-denoting determiner phrases (with type `e`)
with generalized quantifiers (with [extensional] type `(e -> t) -> t`.
In particular, the denotation of a proper name like *John*, which
above:
type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b
- l'_unit a = fun f -> f a
+ l'_unit a = fun f -> f a
l'_bind u f = fun k -> u (fun a -> f a k)
(We performed a sneaky but valid eta reduction in the unit term.)