Signed-off-by: Jim Pryor <profjim@jimpryor.net>
The base category <b>C</b> will have types as elements, and monadic functions as its morphisms. The source and target of a morphism will be the types of its argument and its result. (As always, there can be multiple distinct morphisms from the same source to the same target.)
The base category <b>C</b> will have types as elements, and monadic functions as its morphisms. The source and target of a morphism will be the types of its argument and its result. (As always, there can be multiple distinct morphisms from the same source to the same target.)
-A monad `M` will consist of a mapping from types `'t` to types `M('t)`, and a mapping from functions <code>f:C1→C2</code> to functions <code>M(f):M(C1)→M(C2)</code>. This is also known as <code>lift<sub>M</sub> f</code> for `M`, and is pronounced "function f lifted into the monad M." For example, where `M` is the list monad, `M` maps every type `'t` into the type `'t list`, and maps every function <code>f:x→y</code> into the function that maps `[x1,x2...]` to `[y1,y2,...]`.
+A monad `M` will consist of a mapping from types `'t` to types `M('t)`, and a mapping from functions <code>f:C1→C2</code> to functions <code>M(f):M(C1)→M(C2)</code>. This is also known as <code>lift<sub>M</sub> f</code> for `M`, and is pronounced "function f lifted into the monad M." For example, where `M` is the List monad, `M` maps every type `'t` into the type `'t list`, and maps every function <code>f:x→y</code> into the function that maps `[x1,x2...]` to `[y1,y2,...]`.
In functional programming, instead of working with natural transformations we work with "monadic values" and polymorphic functions "into the monad."
In functional programming, instead of working with natural transformations we work with "monadic values" and polymorphic functions "into the monad."
-A "monadic value" is any member of a type `M('t)`, for any type `'t`. For example, any `int list` is a monadic value for the list monad. We can think of these monadic values as the result of applying some function `phi`, whose type is `F('t) -> M(F'('t))`. `'t` here is any collection of free type variables, and `F('t)` and `F'('t)` are types parameterized on `'t`. An example, with `M` being the list monad, `'t` being `('t1,'t2)`, `F('t1,'t2)` being `char * 't1 * 't2`, and `F'('t1,'t2)` being `int * 't1 * 't2`:
+A "monadic value" is any member of a type `M('t)`, for any type `'t`. For example, any `int list` is a monadic value for the List monad. We can think of these monadic values as the result of applying some function `phi`, whose type is `F('t) -> M(F'('t))`. `'t` here is any collection of free type variables, and `F('t)` and `F'('t)` are types parameterized on `'t`. An example, with `M` being the List monad, `'t` being `('t1,'t2)`, `F('t1,'t2)` being `char * 't1 * 't2`, and `F'('t1,'t2)` being `int * 't1 * 't2`:
<pre>
let phi = fun ((_:char), x, y) -> [(1,x,y),(2,x,y)]
<pre>
let phi = fun ((_:char), x, y) -> [(1,x,y),(2,x,y)]
-1. **Build a state monad.** Based on the division by zero monad,
+1. **Build a State monad.** Based on the division by zero monad,
build a system that will evaluate arithmetic expressions. Instead of
returning a simple integer as a result, it will deliver the correct
answer along with a count of the number of operations performed during
build a system that will evaluate arithmetic expressions. Instead of
returning a simple integer as a result, it will deliver the correct
answer along with a count of the number of operations performed during
-(* since the continuation monad is parameterized on two types---it's
+(* since the Continuation monad is parameterized on two types---it's
* ('a,'r) cont not ('a) cont---we can't match the type ('a) m that
* Tree_monadizer expects in its parameter. So we have to make a different
* Tree_monadizer2 that takes a ('a,'x) m type constructor in its
* ('a,'r) cont not ('a) cont---we can't match the type ('a) m that
* Tree_monadizer expects in its parameter. So we have to make a different
* Tree_monadizer2 that takes a ('a,'x) m type constructor in its
Code written in the latter form is said to be written in **explicit continuation-passing style** or CPS. Later we'll talk about algorithms that mechanically convert an entire program into CPS.
Code written in the latter form is said to be written in **explicit continuation-passing style** or CPS. Later we'll talk about algorithms that mechanically convert an entire program into CPS.
-There are also different kinds of "syntactic sugar" we can use to hide the continuation plumbing. Of course we'll be talking about how to manipulate continuations **with a continuation monad.** We'll also talk about a style of working with continuations where they're **mostly implicit**, but special syntax allows us to distill the implicit continuaton into a first-class value (the `k` in `(let/cc k ...)` and `(shift k ...)`.
+There are also different kinds of "syntactic sugar" we can use to hide the continuation plumbing. Of course we'll be talking about how to manipulate continuations **with a Continuation monad.** We'll also talk about a style of working with continuations where they're **mostly implicit**, but special syntax allows us to distill the implicit continuaton into a first-class value (the `k` in `(let/cc k ...)` and `(shift k ...)`.
Various of the tools we've been introducing over the past weeks are inter-related. We saw coroutines implemented first with zippers; here we've talked in the abstract about their being implemented with continuations. Oleg says that "Zipper can be viewed as a delimited continuation reified as a data structure." Ken expresses the same idea in terms of a zipper being a "defunctionalized" continuation---that is, take something implemented as a function (a continuation) and implement the same thing as an inert data structure (a zipper).
Various of the tools we've been introducing over the past weeks are inter-related. We saw coroutines implemented first with zippers; here we've talked in the abstract about their being implemented with continuations. Oleg says that "Zipper can be viewed as a delimited continuation reified as a data structure." Ken expresses the same idea in terms of a zipper being a "defunctionalized" continuation---that is, take something implemented as a function (a continuation) and implement the same thing as an inert data structure (a zipper).
-* GS&V's semantics involves elements from several different monads we've been looking at. First, they're working with (epistemic) modalities, so there are worlds playing a role like they did in [[Reader Monad for Intensionality]]. But we're going to ignore the modal element for this exercise. There's also variable binding, which calls for [another reader monad](/reader_monad_for_variable_binding). Next, there is a notion of a store, which some operations add new reference cells to. We implement this with a state monad (and so too, in effect, do they---though they don't conceive of what they're doing in those terms). So we'll be working with a combination of both a reader monad for the variable binding and a state monad to keep track of the new "pegs" or reference cells.
+* GS&V's semantics involves elements from several different monads we've been looking at. First, they're working with (epistemic) modalities, so there are worlds playing a role like they did in [[Reader Monad for Intensionality]]. But we're going to ignore the modal element for this exercise. There's also variable binding, which calls for [another Reader monad](/reader_monad_for_variable_binding). Next, there is a notion of a store, which some operations add new reference cells to. We implement this with a State monad (and so too, in effect, do they---though they don't conceive of what they're doing in those terms). So we'll be working with a combination of both a Reader monad for the variable binding and a State monad to keep track of the new "pegs" or reference cells.
There are systematic ways to layer different monads together. If you want to read about these, a keyword is "monad transformers." Ken Shan discusses them in [his paper](http://arxiv.org/abs/cs/0205026v1) that we recommended earlier.
There are systematic ways to layer different monads together. If you want to read about these, a keyword is "monad transformers." Ken Shan discusses them in [his paper](http://arxiv.org/abs/cs/0205026v1) that we recommended earlier.
- However, since we haven't studied these, we will just combine the reader monad and the state monad in an ad hoc way. The easiest way to do this is to think of the assignment function and the store of reference cells as a combined state, which gets threaded through the computations in the same way that simple states did in your earlier homeworks.
+ However, since we haven't studied these, we will just combine the Reader monad and the State monad in an ad hoc way. The easiest way to do this is to think of the assignment function and the store of reference cells as a combined state, which gets threaded through the computations in the same way that simple states did in your earlier homeworks.
We'll call these "discourse possibility monads," or `dpm`s, and type them as follows:
We'll call these "discourse possibility monads," or `dpm`s, and type them as follows:
Although we're leaving worlds out of the picture, each of these monadic values still represents a different *discourse* possibility: which entities might be being talked about, using which variables.
Although we're leaving worlds out of the picture, each of these monadic values still represents a different *discourse* possibility: which entities might be being talked about, using which variables.
- Since `dpm`s are to be a monad, we have to define a unit and a bind. These are just modeled on the unit and bind for the state monad:
+ Since `dpm`s are to be a monad, we have to define a unit and a bind. These are just modeled on the unit and bind for the State monad:
let unit_dpm (value : 'a) : 'a dpm = fun (r, h) -> (value, r, h);;
let unit_dpm (value : 'a) : 'a dpm = fun (r, h) -> (value, r, h);;
Now some of the `dpm`s we work with will be `bool dpm`s, which are functions from discourse possibilities to `bool`s (and discourse possibilities). It's tempting to think we might just work with `bool dpm`s instead of sets of possibilities. However, I don't think this can work. The reason why is that at a crucial point in GS&Vs semantics, we have to work with not just a *single* way of mutating or "extending" a discourse possibility, but a *range* of different ways to mutate the live discourse possibilities. So we do need to work with sets, after all.
Now some of the `dpm`s we work with will be `bool dpm`s, which are functions from discourse possibilities to `bool`s (and discourse possibilities). It's tempting to think we might just work with `bool dpm`s instead of sets of possibilities. However, I don't think this can work. The reason why is that at a crucial point in GS&Vs semantics, we have to work with not just a *single* way of mutating or "extending" a discourse possibility, but a *range* of different ways to mutate the live discourse possibilities. So we do need to work with sets, after all.
- A set is just another monadic layer. We've already talked about list monads, and we can for these purposes just use list monads to represent set monads. Instead of sets of possibilities, let's work with sets of `dpm`s, that is, sets of discourse possibility monads, or computations on discourse possibilities.
+ A set is just another monadic layer. We've already talked about List monads, and we can for these purposes just use List monads to represent set monads. Instead of sets of possibilities, let's work with sets of `dpm`s, that is, sets of discourse possibility monads, or computations on discourse possibilities.
As I said, for simplicity, we'll represent sets using lists:
As I said, for simplicity, we'll represent sets using lists:
<pre><code>bind_set (bind_set u \[[∃x]]) \[[Px]]
</code></pre>
<pre><code>bind_set (bind_set u \[[∃x]]) \[[Px]]
</code></pre>
-* Let's compare this to what \[[∃xPx]] would look like on a non-dynamic semantics, for example, where we use a simple reader monad to implement variable binding. Reminding ourselves, we'd be working in a framework like this. (Here we implement environments or assignments as functions from variables to entities, instead of as lists of pairs of variables and entities. An assignment `r` here is what `fun c -> List.assoc c r` would have been in [week7](
+* Let's compare this to what \[[∃xPx]] would look like on a non-dynamic semantics, for example, where we use a simple Reader monad to implement variable binding. Reminding ourselves, we'd be working in a framework like this. (Here we implement environments or assignments as functions from variables to entities, instead of as lists of pairs of variables and entities. An assignment `r` here is what `fun c -> List.assoc c r` would have been in [week7](
/reader_monad_for_variable_binding).)
type assignment = char -> entity;;
/reader_monad_for_variable_binding).)
type assignment = char -> entity;;
We're going to come at continuations from three different directions, and each
time we're going to end up at the same place: a particular monad, which we'll
We're going to come at continuations from three different directions, and each
time we're going to end up at the same place: a particular monad, which we'll
-call the continuation monad.
+call the Continuation monad.
-Rethinking the list monad
+Rethinking the List monad
-------------------------
To construct a monad, the key element is to settle on how to implement its type, and
-------------------------
To construct a monad, the key element is to settle on how to implement its type, and
some previously unconnected elements of the course (more specifically,
version 3 lists and monads).
some previously unconnected elements of the course (more specifically,
version 3 lists and monads).
-For instance, take the **Reader Monad**. Once we decide to define its type as:
+For instance, take the **Reader monad**. Once we decide to define its type as:
type 'a reader = env -> 'a
type 'a reader = env -> 'a
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
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
Since the type of the `bind` operator is required to be
Since the type of the `bind` operator is required to be
version here in order to emphasize similarities of structure across
monads.]
version here in order to emphasize similarities of structure across
monads.]
-The **State Monad** is similar. Once we've decided to use the following type constructor:
+The **State monad** is similar. Once we've decided to use the following type constructor:
type 'a state = store -> ('a, store)
type 'a state = store -> ('a, store)
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
+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
follow just as naturally from its type constructor.
won't pause to explore it here, though conceptually its unit and bind
follow just as naturally from its type constructor.
-Our other familiar monad is the **List Monad**, which we were told
+Our other familiar monad is the **List monad**, which we were told
looks like this:
(* type 'a list = ['a];; *)
l_unit (a : 'a) = [a];;
l_bind u f = List.concat (List.map f u);;
looks like this:
(* type 'a list = ['a];; *)
l_unit (a : 'a) = [a];;
l_bind u f = List.concat (List.map f u);;
-Thinking through the list monad will take a little time, but doing so
+Thinking through the List monad will take a little time, but doing so
will provide a connection with continuations.
Recall that `List.map` takes a function and a list and returns the
will provide a connection with continuations.
Recall that `List.map` takes a function and a list and returns the
type `('something list) list`. We can eliminate 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
type `('something list) list`. We can eliminate 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
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
(* an intermediate version, and the fully eta-reduced: *)
fun k -> u (fun a -> f a k)
(* an intermediate version, and the fully eta-reduced: *)
fun k -> u (fun a -> f a k)
-Consider the most eta-reduced versions of `l'_unit` and `l'_bind`. They're the same as the unit and bind for the Montague continuation monad! In other words, the behavior of our v3-list monad and the behavior of the continuations monad are
+Consider the most eta-reduced versions of `l'_unit` and `l'_bind`. They're the same as the unit and bind for the Montague Continuation monad! In other words, the behavior of our v3-List monad and the behavior of the continuations monad are
parallel in a deep sense.
Have we really discovered that lists are secretly continuations? Or
have we merely found a way of simulating lists using list
continuations? Well, strictly speaking, what we have done is shown
that one particular implementation of lists---the right fold
parallel in a deep sense.
Have we really discovered that lists are secretly continuations? Or
have we merely found a way of simulating lists using list
continuations? Well, strictly speaking, what we have done is shown
that one particular implementation of lists---the right fold
-implementation---gives rise to a continuation monad fairly naturally,
+implementation---gives rise to a Continuation monad fairly naturally,
and that this monad can reproduce the behavior of the standard list
monad. But what about other list implementations? Do they give rise
to monads that can be understood in terms of continuations?
and that this monad can reproduce the behavior of the standard list
monad. But what about other list implementations? Do they give rise
to monads that can be understood in terms of continuations?
(* we assume we've settled on some implementation of the environment *)
type env = (char * int) list;;
(* we assume we've settled on some implementation of the environment *)
type env = (char * int) list;;
- (* here's the type of our reader monad *)
+ (* here's the type of our Reader monad *)
type 'a reader = env -> 'a;;
(* here's our unit operation; it creates a reader-monad value that
type 'a reader = env -> 'a;;
(* here's our unit operation; it creates a reader-monad value that
# let result = eval (Let('x',Constant 1,Addition(Variable 'x',Constant 2)));;
- : int reader = <fun>
# let result = eval (Let('x',Constant 1,Addition(Variable 'x',Constant 2)));;
- : int reader = <fun>
-How do we see what integer that evaluates to? Well, it's an int-reader monad, which is a function from an `env` to an `int`, so we need to give it some `env` to operate on. We can give it the empty environment:
+How do we see what integer that evaluates to? Well, it's an int-Reader monad, which is a function from an `env` to an `int`, so we need to give it some `env` to operate on. We can give it the empty environment:
# result [];;
- : int = 3
# result [];;
- : int = 3
= fun v -> (fun e -> S (lookup i ((i, v e) :: e)) Alice)
= fun v -> (fun e -> S (v e) Alice)
= fun v -> (fun e -> S (lookup i ((i, v e) :: e)) Alice)
= fun v -> (fun e -> S (v e) Alice)
-In other words, it's a function from entity reader monads to a function from assignment functions to the result of applying S to the value of that entity reader-monad under that assignment function, and to Alice. Essentially the same as Heim and Kratzer's final value, except here we work with monadic values, such as functions from assignments to entities, rather than bare entities. And our derivation is completely compositional and uses the same composition rules for joining \[[who(i)]] to \[[Alice spurned i]] as it uses for joining \[[spurned]] to \[[i]] and \[[Alice]].
+In other words, it's a function from entity-Reader monads to a function from assignment functions to the result of applying S to the value of that entity reader-monad under that assignment function, and to Alice. Essentially the same as Heim and Kratzer's final value, except here we work with monadic values, such as functions from assignments to entities, rather than bare entities. And our derivation is completely compositional and uses the same composition rules for joining \[[who(i)]] to \[[Alice spurned i]] as it uses for joining \[[spurned]] to \[[i]] and \[[Alice]].
material within the sentence can satisfy presuppositions for other
material that otherwise would trigger a presupposition violation; but,
not surprisingly, these refinements will require some more
material within the sentence can satisfy presuppositions for other
material that otherwise would trigger a presupposition violation; but,
not surprisingly, these refinements will require some more
-sophisticated techniques than the super-simple option monad.]
+sophisticated techniques than the super-simple Option monad.]
So `unit` is a way to put something inside of a monadic box. It's crucial
to the usefulness of monads that there will be monadic boxes that
So `unit` is a way to put something inside of a monadic box. It's crucial
to the usefulness of monads that there will be monadic boxes that
- aren't the result of that operation. In the option/maybe monad, for
+ aren't the result of that operation. In the Option/Maybe monad, for
instance, there's also the empty box `None`. In another (whimsical)
example, you might have, in addition to boxes merely containing integers,
special boxes that contain integers and also sing a song when they're opened.
instance, there's also the empty box `None`. In another (whimsical)
example, you might have, in addition to boxes merely containing integers,
special boxes that contain integers and also sing a song when they're opened.
* Thirdly, an operation that's often called `bind`. As we said before, this is another
unfortunate name: this operation is only very loosely connected to
* Thirdly, an operation that's often called `bind`. As we said before, this is another
unfortunate name: this operation is only very loosely connected to
- what linguists usually mean by "binding." In our option/maybe monad, the
+ what linguists usually mean by "binding." In our Option/Maybe monad, the
bind operation is:
let bind u f = match u with None -> None | Some x -> f x;;
bind operation is:
let bind u f = match u with None -> None | Some x -> f x;;
The guts of the definition of the `bind` operation amount to
specifying how to unbox the monadic value `u`. In the `bind`
The guts of the definition of the `bind` operation amount to
specifying how to unbox the monadic value `u`. In the `bind`
- operator for the option monad, we unboxed the monadic value by
+ operator for the Option monad, we unboxed the monadic value by
matching it with the pattern `Some x`---whenever `u`
happened to be a box containing an integer `x`, this allowed us to
get our hands on that `x` and feed it to `f`.
matching it with the pattern `Some x`---whenever `u`
happened to be a box containing an integer `x`, this allowed us to
get our hands on that `x` and feed it to `f`.
For each new monadic type, this has to be worked out in an
useful way.
For each new monadic type, this has to be worked out in an
useful way.
-So the "option/maybe monad" consists of the polymorphic `option` type, the
+So the "Option/Maybe monad" consists of the polymorphic `option` type, the
`unit`/return function, and the `bind` function.
`unit`/return function, and the `bind` function.
having to do with mutable record fields. We'll be discussing mutation someday
soon.)
having to do with mutable record fields. We'll be discussing mutation someday
soon.)
-As we proceed, we'll be seeing a variety of other monad systems. For example, another monad is the list monad. Here the monadic type is:
+As we proceed, we'll be seeing a variety of other monad systems. For example, another monad is the List monad. Here the monadic type is:
# List.concat [[1]; [1;2]; [1;3]; [1;2;4]]
- : int list = [1; 1; 2; 1; 3; 1; 2; 4]
# List.concat [[1]; [1;2]; [1;3]; [1;2;4]]
- : int list = [1; 1; 2; 1; 3; 1; 2; 4]
-So now we've seen two monads: the option/maybe monad, and the list monad. For any
+So now we've seen two monads: the Option/Maybe monad, and the List monad. For any
monadic system, there has to be a specification of the complex monad type,
which will be parameterized on some simpler type `'a`, and the `unit`/return
operation, and the `bind` operation. These will be different for different
monadic system, there has to be a specification of the complex monad type,
which will be parameterized on some simpler type `'a`, and the `unit`/return
operation, and the `bind` operation. These will be different for different
If you don't understand why the lambda form is necessary (the
"fun x -> ..." part), you need to look again at the type of `bind`.
If you don't understand why the lambda form is necessary (the
"fun x -> ..." part), you need to look again at the type of `bind`.
- Some examples of associativity in the option monad (bear in
+ Some examples of associativity in the Option monad (bear in
mind that in the Ocaml implementation of integer division, 2/3
evaluates to zero, throwing away the remainder):
mind that in the Ocaml implementation of integer division, 2/3
evaluates to zero, throwing away the remainder):
Of course, associativity must hold for *arbitrary* functions of
type `'a -> 'b m`, where `m` is the monad type. It's easy to
Of course, associativity must hold for *arbitrary* functions of
type `'a -> 'b m`, where `m` is the monad type. It's easy to
-convince yourself that the `bind` operation for the option monad
+convince yourself that the `bind` operation for the Option monad
obeys associativity by dividing the inputs into cases: if `u`
matches `None`, both computations will result in `None`; if
`u` matches `Some x`, and `f x` evalutes to `None`, then both
obeys associativity by dividing the inputs into cases: if `u`
matches `None`, both computations will result in `None`; if
`u` matches `Some x`, and `f x` evalutes to `None`, then both
# let even x = (x mod 2 = 0);;
val g : int -> bool = <fun>
# let even x = (x mod 2 = 0);;
val g : int -> bool = <fun>
-`even` has the type `int -> bool`. Now what if we want to convert it into an operation on the option/maybe monad?
+`even` has the type `int -> bool`. Now what if we want to convert it into an operation on the Option/Maybe monad?
# let lift g = fun u -> bind u (fun x -> Some (g x));;
val lift : ('a -> 'b) -> 'a option -> 'b option = <fun>
# let lift g = fun u -> bind u (fun x -> Some (g x));;
val lift : ('a -> 'b) -> 'a option -> 'b option = <fun>
`lift2 (+)` will now be a function from `int option`s and `int option`s to `int option`s. This should look familiar to those who did the homework.
`lift2 (+)` will now be a function from `int option`s and `int option`s to `int option`s. This should look familiar to those who did the homework.
-The `lift` operation (just `lift`, not `lift2`) is sometimes also called the `map` operation. (In Haskell, they say `fmap` or `<$>`.) And indeed when we're working with the list monad, `lift f` is exactly `List.map f`!
+The `lift` operation (just `lift`, not `lift2`) is sometimes also called the `map` operation. (In Haskell, they say `fmap` or `<$>`.) And indeed when we're working with the List monad, `lift f` is exactly `List.map f`!
Wherever we have a well-defined monad, we can define a lift/map operation for that monad. The examples above used `Some (g x)` and so on; in the general case we'd use `unit (g x)`, using the specific `unit` operation for the monad we're working with.
Wherever we have a well-defined monad, we can define a lift/map operation for that monad. The examples above used `Some (g x)` and so on; in the general case we'd use `unit (g x)`, using the specific `unit` operation for the monad we're working with.
ap (unit f) (unit x) = unit (f x)
ap u (unit x) = ap (unit (fun f -> f x)) u
ap (unit f) (unit x) = unit (f x)
ap u (unit x) = ap (unit (fun f -> f x)) u
-Another general monad operation is called `join`. This is the operation that takes you from an iterated monad to a single monad. Remember when we were explaining the `bind` operation for the list monad, there was a step where
+Another general monad operation is called `join`. This is the operation that takes you from an iterated monad to a single monad. Remember when we were explaining the `bind` operation for the List monad, there was a step where
we went from:
[[1]; [1;2]; [1;3]; [1;2;4]]
we went from:
[[1]; [1;2]; [1;3]; [1;2;4]]
But first, we'll look at several linguistic applications for monads, based
on what's called the *Reader monad*.
But first, we'll look at several linguistic applications for monads, based
on what's called the *Reader monad*.
-##[[Reader monad for Variable Binding]]##
+##[[Reader Monad for Variable Binding]]##
-##[[Reader monad for Intensionality]]##
+##[[Reader Monad for Intensionality]]##
uses combinators to impose binding relationships between argument
positions. The system does not make use of assignment functions or
variables. We'll see that from the point of view of our discussion of
uses combinators to impose binding relationships between argument
positions. The system does not make use of assignment functions or
variables. We'll see that from the point of view of our discussion of
-monads, Jacobson's system is essentially a reader monad in which the
+monads, Jacobson's system is essentially a Reader monad in which the
assignment function threaded through the computation is limited to at
most one variable. It will turn out that Jacobson's geach combinator
*g* is exactly our `lift` operator, and her binding combinator *z* is
assignment function threaded through the computation is limited to at
most one variable. It will turn out that Jacobson's geach combinator
*g* is exactly our `lift` operator, and her binding combinator *z* is
before you are about to combine with the binder, when you finish off
with *z*. (There are examples with longer chains of *g*'s below.)
before you are about to combine with the binder, when you finish off
with *z*. (There are examples with longer chains of *g*'s below.)
-Last week we saw a reader monad for tracking variable assignments:
+Last week we saw a Reader monad for tracking variable assignments:
<pre>
type env = (char * int) list;;
<pre>
type env = (char * int) list;;
idea is that a list like `[('a', 2); ('b',5)]` associates the variable
`'a'` with the value 2, and the variable `'b'` with the value 5.
idea is that a list like `[('a', 2); ('b',5)]` associates the variable
`'a'` with the value 2, and the variable `'b'` with the value 5.
-Combining this reader monad with ideas from Jacobson's approach, we
+Combining this Reader monad with ideas from Jacobson's approach, we
can consider the following monad:
<pre>
can consider the following monad:
<pre>
</pre>
I've called this the *link* monad, because it links (exactly one)
</pre>
I've called this the *link* monad, because it links (exactly one)
-pronoun with a binder, but it's a kind of reader monad. (Prove that
+pronoun with a binder, but it's a kind of Reader monad. (Prove that
`ap`, the combinator for applying a linked functor to a linked object,
can be equivalently defined in terms of `bind` and `unit`.)
`ap`, the combinator for applying a linked functor to a linked object,
can be equivalently defined in terms of `bind` and `unit`.)
type `e`. It is easy to make the monad polymorphic in the type of the
linked value, which will be necessary to handle, e.g., paycheck pronouns.
type `e`. It is easy to make the monad polymorphic in the type of the
linked value, which will be necessary to handle, e.g., paycheck pronouns.
-In the standard reader monad, the environment is an assignment
+In the standard Reader monad, the environment is an assignment
function. Here, instead this monad provides a single value. The idea
is that this is the value that will be used to replace the pronoun
linked to it by the monad.
function. Here, instead this monad provides a single value. The idea
is that this is the value that will be used to replace the pronoun
linked to it by the monad.
order), but returns something that is not in the monad. Rather, it
will be a function from individuals to a computation in which the
pronoun in question is bound to that individual. We could emphasize
order), but returns something that is not in the monad. Rather, it
will be a function from individuals to a computation in which the
pronoun in question is bound to that individual. We could emphasize
-the parallel with the reader monad even more by writing a `shift`
+the parallel with the Reader monad even more by writing a `shift`
operator that used `unit` to produce a monadic result, if we wanted to.
The monad version of *Everyone_i thinks he_i left*, then (remembering
operator that used `unit` to produce a monadic result, if we wanted to.
The monad version of *Everyone_i thinks he_i left*, then (remembering
So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z*
is exactly `bind` with the arguments reversed. It appears that
So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z*
is exactly `bind` with the arguments reversed. It appears that
-Jacobson's variable-free semantics is essentially a reader monad.
+Jacobson's variable-free semantics is essentially a Reader monad.
-One of Jacobson's main points survives: restricting the reader monad
+One of Jacobson's main points survives: restricting the Reader monad
to a single-value environment eliminates the need for variable names.
Binding more than one variable at a time
----------------------------------------
It requires some cleverness to use the link monad to bind more than
to a single-value environment eliminates the need for variable names.
Binding more than one variable at a time
----------------------------------------
It requires some cleverness to use the link monad to bind more than
-one variable at a time. Whereas in the standard reader monad a single
+one variable at a time. Whereas in the standard Reader monad a single
environment can record any number of variable assignments, because
Jacobson's monad only tracks a single dependency, binding more than
one pronoun requires layering the monad. (Jacobson provides some
environment can record any number of variable assignments, because
Jacobson's monad only tracks a single dependency, binding more than
one pronoun requires layering the monad. (Jacobson provides some