Signed-off-by: Jim Pryor <profjim@jimpryor.net>
The main difference between the intensional types and the extensional
types is that in the intensional types, the arguments are functions
from worlds to extensions: intransitive verb phrases like "left" now
The main difference between the intensional types and the extensional
types is that in the intensional types, the arguments are functions
from worlds to extensions: intransitive verb phrases like "left" now
-take individual concepts as arguments (type s->e) rather than plain
+take so-called "individual concepts" as arguments (type s->e) rather than plain
individuals (type e), and attitude verbs like "think" now take
propositions (type s->t) rather than truth values (type t).
In addition, the result of each predicate is an intension.
individuals (type e), and attitude verbs like "think" now take
propositions (type s->t) rather than truth values (type t).
In addition, the result of each predicate is an intension.
into the the lexical meaning function, but we've made it explicit here
in the way that the intensionality monad makes most natural.)
into the the lexical meaning function, but we've made it explicit here
in the way that the intensionality monad makes most natural.)
-The intenstional types are more complicated than the intensional
+The intensional types are more complicated than the extensional
types. Wouldn't it be nice to make the complicated types available
for those expressions like attitude verbs that need to worry about
intensions, and keep the rest of the grammar as extensional as
types. Wouldn't it be nice to make the complicated types available
for those expressions like attitude verbs that need to worry about
intensions, and keep the rest of the grammar as extensional as
-In OCaml, we'll use integers to model possible worlds:
+In OCaml, we'll use integers to model possible worlds. Characters (characters in the computational sense, i.e., letters like `'a'` and `'b'`, not Kaplanian characters) will model individuals, and OCaml booleans will serve for truth values:
type s = int;;
type e = char;;
type t = bool;;
type s = int;;
type e = char;;
type t = bool;;
-Characters (characters in the computational sense, i.e., letters like
-`'a'` and `'b'`, not Kaplanian characters) will model individuals, and
-OCaml booleans will serve for truth values.
+ let ann = 'a';;
+ let bill = 'b';;
+ let cam = 'c';;
-<pre>
-let ann = 'a';;
-let bill = 'b';;
-let cam = 'c';;
-
-let left1 (x:e) = true;;
-let saw1 (x:e) (y:e) = y < x;;
+ let left1 (x:e) = true;;
+ let saw1 (x:e) (y:e) = y < x;;
-left1 ann;;
-saw1 bill ann;; (* true *)
-saw1 ann bill;; (* false *)
-</pre>
+ left1 ann;;
+ saw1 bill ann;; (* true *)
+ saw1 ann bill;; (* false *)
So here's our extensional system: everyone left, including Ann;
and Ann saw Bill, but Bill didn't see Ann. (Note that Ocaml word
So here's our extensional system: everyone left, including Ann;
and Ann saw Bill, but Bill didn't see Ann. (Note that Ocaml word
<pre>
type 'a intension = s -> 'a;;
<pre>
type 'a intension = s -> 'a;;
-let unit x (w:s) = x;;
-let bind m f (w:s) = f (m w) w;;
+let unit x = fun (w:s) -> x;;
+let bind m f = fun (w:s) -> f (m w) w;;
</pre>
Then the individual concept `unit ann` is a rigid designator: a
</pre>
Then the individual concept `unit ann` is a rigid designator: a
Ann did see bill in world 1, but Ann didn't see Bill in world 2.
Finally, we can define our intensional verb *thinks*. *Think* is
Ann did see bill in world 1, but Ann didn't see Bill in world 2.
Finally, we can define our intensional verb *thinks*. *Think* is
-intensional with respect to its sentential complement, but extensional
+intensional with respect to its sentential complement, though still extensional
with respect to its subject. (As Montague noticed, almost all verbs
in English are extensional with respect to their subject; a possible
exception is "appear".)
with respect to its subject. (As Montague noticed, almost all verbs
in English are extensional with respect to their subject; a possible
exception is "appear".)
will be extensional with respect to the nominal they combine with
(using bind), and the non-intersective adjectives will take
intensional arguments.
will be extensional with respect to the nominal they combine with
(using bind), and the non-intersective adjectives will take
intensional arguments.
where `M {x <- N}` is the result of substituting N in for free occurrences of `x` in `M`.
where `M {x <- N}` is the result of substituting N in for free occurrences of `x` in `M`.
-What do I mean by calling this a "semantics"? Wasn't this instead part of our proof-theory? Haven't we been neglected to discuss any model theory for the lambda calculus?
+What do I mean by calling this a "semantics"? Wasn't this instead part of our proof-theory? Haven't we neglected to discuss any model theory for the lambda calculus?
Well, yes, that's right, we haven't much discussed what computer scientists call *denotational semantics* for the lambda calculus. That's what philosophers and linguists tend to think of as "semantics."
Well, yes, that's right, we haven't much discussed what computer scientists call *denotational semantics* for the lambda calculus. That's what philosophers and linguists tend to think of as "semantics."
In any case, the lambda evaluator we use on our website does evaluate expressions using the kind of operational semantics described above. We can call that a "substitution-based" semantics.
In any case, the lambda evaluator we use on our website does evaluate expressions using the kind of operational semantics described above. We can call that a "substitution-based" semantics.
-Let's consider a different kind of operational semantics. Instead of substituting `N` in for `x`, why don't we keep some extra data-structure on the side, where we note that `x` should now be considered to evaluate to whatever `N` does? In computer science jargon, such a data-structure is called an **environment**. Philosophers and linguists would tend to call it an **assignment** (though there are some subtleties about whether these are the same thing, which we'll discuss).
+Let's consider a different kind of operational semantics. Instead of substituting `N` in for `x`, why don't we keep some extra data-structure on the side, where we note that `x` should now be understood to evaluate to whatever `N` does? In computer science jargon, such a data-structure is called an **environment**. Philosophers and linguists would tend to call it an **assignment** (though there are some subtleties about whether these are the same thing, which we'll discuss).
[Often in computer science settings, the lambda expression to be evaluated is first translated into **de Bruijn notation**, which we discussed in the first week of term. That is, instead of:
[Often in computer science settings, the lambda expression to be evaluated is first translated into **de Bruijn notation**, which we discussed in the first week of term. That is, instead of:
we'll instead evaluate them by manipulating their environment. (To intepret `(\x. M) N` in environment `e`, we'll interpret `M` in an environment like `e {x:= N}` where `x` may have been changed to now be assigned to `N`.
we'll instead evaluate them by manipulating their environment. (To intepret `(\x. M) N` in environment `e`, we'll interpret `M` in an environment like `e {x:= N}` where `x` may have been changed to now be assigned to `N`.
-A few comments. First, what the environment associates with the variable `x` will be expressions of the lambda calculus we're evaluating. If we understand the evaluation to be call-by-name, these expressions may be complexes of the form `N P`. If on the other hand, we understand the evaluation to be call-by-value, then these expressions will always be fully evaluated before being inserted into the environment. That means they'll never be of the form `N P`; but onlu of the form `y` or `\y. P`. The latter kinds of expressions are called "values." But "values" here are just certain kinds of expressions. (They could be the denotations of lambda expressions, if one thinks of the lambda expressions as all having (preferably) normal-form lambda terms as their denotations.)
+A few comments. First, what the environment associates with the variable `x` will be expressions of the lambda calculus we're evaluating. If we understand the evaluation to be call-by-name, these expressions may be complexes of the form `N P`. If on the other hand, we understand the evaluation to be call-by-value, then these expressions will always be fully evaluated before being inserted into the environment. That means they'll never be of the form `N P`; but only of the form `y` or `\y. P`. The latter kinds of expressions are called "values." But "values" here are just certain kinds of expressions. (They *could* be the denotations of lambda expressions, if one thinks of the lambda expressions as all having normal-form lambda terms as their denotations, when possible.)
Second, there is a subtlety here we haven't yet discussed. Consider what should be the result of this:
Second, there is a subtlety here we haven't yet discussed. Consider what should be the result of this:
With these ideas settled, then, we can present an environment-based operational semantics for the untyped lambda calculus. Here is a call-by-value version, which assumes that expressions are always fully evaluated before being inserted into the environment.
With these ideas settled, then, we can present an environment-based operational semantics for the untyped lambda calculus. Here is a call-by-value version, which assumes that expressions are always fully evaluated before being inserted into the environment.
-1. When `e` assigns some term `v` to `x`, then `x`reduces in environment `e` to `v`. We write that as: `(e |- x) ==> v`.
+1. When `e` assigns some term `v` to `x`, then `x`fully (that is, terminally) reduces in environment `e` to `v`. We write that as: `(e |- x) ==> v`.
2. `(e |- \x. M) ==> closure(e, \x. M)`, where a closure is some data-structure (it might just be a pair of the data-structure `e` and the formula `\x. M`).
2. `(e |- \x. M) ==> closure(e, \x. M)`, where a closure is some data-structure (it might just be a pair of the data-structure `e` and the formula `\x. M`).
-3. If `(e |- M) ==> closure(e2, \x. M2)` and `(e |- N) ==> v` and `(e2 {x:=v} |- M2) ==> u`, then `(e |- M N) ==> u`. Here `e {x:=v}` is the environment which is just like `e` except it assigns `v` to `x`.
+3. If `(e |- M) ==> closure(e2, \x. M2)` and `(e |- N) ==> v` and `(e2 {x:=v} |- M2) ==> u`, then `(e |- M N) ==> u`. Here `e2 {x:=v}` is the environment which is just like `e2` except it assigns `v` to `x`.
Explicitly manipulating the environment
Explicitly manipulating the environment
For example, a common programming exercise when students are learning languages like OCaml is to implement a simple arithmetic calculator. You'll suppose you're given some expressions of the following type:
For example, a common programming exercise when students are learning languages like OCaml is to implement a simple arithmetic calculator. You'll suppose you're given some expressions of the following type:
- type term = Constant of int | Multiplication of (term * term) | Addition of (term*term) | Variable of char | Let of (char*term*term);;
+ type term = Constant of int
+ | Multiplication of (term * term)
+ | Addition of (term*term)
+ | Variable of char
+ | Let of (char*term*term);;
and then you'd evaluate it something like this:
and then you'd evaluate it something like this:
| Variable c -> ... (* we'll come back to this *)
| Let (c,t1,t2) -> ... (* this too *)
| Variable c -> ... (* we'll come back to this *)
| Let (c,t1,t2) -> ... (* this too *)
-With that in hand, you could then evaluate complex terms like `Addition(Constant 1, Multiplication(2, 3))`.
+With that in hand, you could then evaluate complex terms like `Addition(Constant 1, Multiplication(Constant 2, Constant 3))`.
-But then how should you evaluate terms like `Let('x',Constant 1,Addition(Variable 'x', Constant 2))`? We'd want to carry along an environment that recorded that 'x' had been associated with the term `Constant 1`, so that we could retrieve that value when evaluating `Addition(Variable 'x', Constant 2)`.
+But then how should you evaluate terms like `Let('x',Constant 1,Addition(Variable 'x', Constant 2))`? We'd want to carry along an environment that recorded that `'x'` had been associated with the term `Constant 1`, so that we could retrieve that value when evaluating `Addition(Variable 'x', Constant 2)`.
+
+Notice that here our environments associate variables with (what from the perspective of our calculator language are) *real* values, like `2`, not just value-denoting terms like `Constant 2`.
We'll work with a simple model of environments. They'll just be lists. So the empty environment is `[]`. To modify an environment `e` like this: `e {x:=1}`, we'll use:
We'll work with a simple model of environments. They'll just be lists. So the empty environment is `[]`. To modify an environment `e` like this: `e {x:=1}`, we'll use:
have to explicitly pass around an environment that they're not themselves making any use of. Would there be any way to hide that bit of plumbing behind the drywall?
have to explicitly pass around an environment that they're not themselves making any use of. Would there be any way to hide that bit of plumbing behind the drywall?
-Yes! You can do with a monad, in much the same way we did with our checks for divide-by-zero failures.
+Yes! You can do so with a monad, in much the same way we did with our checks for divide-by-zero failures.
Here we'll use a different monad. It's called the **reader monad**. We define it like this:
Here we'll use a different monad. It's called the **reader monad**. We define it like this:
# 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>
-Now 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
\[[man who(i): Alice spurned i]]
is the result of combining \[[man]], an `e->t` type predicate value, with the adjective-type value of \[[who(i): Alice spurned i]]. As I said, we'll ignore complexities about their treatment of adjectives. But how is \[[who(i): Alice spurned i]] derived? Heim and Kratzer say this is defined only relative to an
\[[man who(i): Alice spurned i]]
is the result of combining \[[man]], an `e->t` type predicate value, with the adjective-type value of \[[who(i): Alice spurned i]]. As I said, we'll ignore complexities about their treatment of adjectives. But how is \[[who(i): Alice spurned i]] derived? Heim and Kratzer say this is defined only relative to an
-assignment g, and it's defined to be a function from objects x in the domain to the value \[[Alice spurned i]] has relative to shifted assignment g{i:=x}, which is like g except for assigning object x to variable i. So this is not the result of taking some value \[[who(i)]], and some separate value \[[Alice spurned i]], and supplying one of them to the other as argument to function.
+assignment g, and it's defined to be a function from objects x in the domain to the value \[[Alice spurned i]] has relative to shifted assignment g {i:=x}, which is like g except for assigning object x to variable i. So this is not the result of taking some value \[[who(i)]], and some separate value \[[Alice spurned i]], and supplying one of them to the other as argument to function.
Finally, we set \[[who(i)]] to be:
fun (u : bool reader) (v : entity reader) ->
Finally, we set \[[who(i)]] to be:
fun (u : bool reader) (v : entity reader) ->
- fun (g : env) -> u (g{i:=v g})
+ fun (g : env) -> u (g {i:=v g})
That is, it takes as arguments a clause-type reader-monad `u`, and an entity-type reader-monad `v`, and returns a reader-monad that evaluates `u` in an environment that's modified to assign `v`'s value in that environment to the variable `i`. In other words, this is:
That is, it takes as arguments a clause-type reader-monad `u`, and an entity-type reader-monad `v`, and returns a reader-monad that evaluates `u` in an environment that's modified to assign `v`'s value in that environment to the variable `i`. In other words, this is:
\[[who(i)]] = fun u v -> shift i v u
\[[who(i)]] = fun u v -> shift i v u
-and some philosophers count assignment-shifters as "monsters" and think there can't be any such thing. Clearly they're wrong.
+and some philosophers count assignment-shifters as "monsters" and think there can't be any such thing. Well, everyone has their own issues they need to work through.
Later, techniques parallel to what we do here can be used to implement semantics for mutation and dynamic predicate logic. And then again, parallel techniques can be used to implement the "coordinated" semantics that Kit Fine and Jim Pryor favor. We just need different monads in each case.
Later, techniques parallel to what we do here can be used to implement semantics for mutation and dynamic predicate logic. And then again, parallel techniques can be used to implement the "coordinated" semantics that Kit Fine and Jim Pryor favor. We just need different monads in each case.
Monads increase the ease with which programs may be modified. They can mimic the effect of impure features such as exceptions, state, and continuations; and also provide effects not easily achieved with such features. The types of a program reflect which effects occur.
The first section is an extended example of the use of monads. A simple interpreter is modified to support various extra features: error messages, state, output, and non-deterministic choice. The second section describes the relation between monads and continuation-passing style. The third section sketches how monads are used in a compiler for Haskell that is written in Haskell.-->
Monads increase the ease with which programs may be modified. They can mimic the effect of impure features such as exceptions, state, and continuations; and also provide effects not easily achieved with such features. The types of a program reflect which effects occur.
The first section is an extended example of the use of monads. A simple interpreter is modified to support various extra features: error messages, state, output, and non-deterministic choice. The second section describes the relation between monads and continuation-passing style. The third section sketches how monads are used in a compiler for Haskell that is written in Haskell.-->
-* [Daniel Friedman. A Schemer's View of Monads](/schemersviewofmonads.ps): from <https://www.cs.indiana.edu/cgi-pub/c311/doku.php?id=home> but the link above is to a local copy.
-
-There's a long list of monad tutorials on the [[Offsite Reading]] page. Skimming the titles makes us laugh.
+There's a long list of monad tutorials on the [[Offsite Reading]] page. (Skimming the titles is somewhat amusing.) If you are confused by monads, make use of these resources. Read around until you find a tutorial pitched at a level that's helpful for you.
In the presentation we gave above---which follows the functional programming conventions---we took `unit`/return and `bind` as the primitive operations. From these a number of other general monad operations can be derived. It's also possible to take some of the others as primitive. The [Monads in Category
Theory](/advanced_topics/monads_in_category_theory) notes do so, for example.
In the presentation we gave above---which follows the functional programming conventions---we took `unit`/return and `bind` as the primitive operations. From these a number of other general monad operations can be derived. It's also possible to take some of the others as primitive. The [Monads in Category
Theory](/advanced_topics/monads_in_category_theory) notes do so, for example.
-------------
We're going to be using monads for a number of different things in the
-------------
We're going to be using monads for a number of different things in the
-weeks to come. The first main application will be the State monad,
+weeks to come. One major application will be the State monad,
which will enable us to model mutation: variables whose values appear
to change as the computation progresses. Later, we will study the
Continuation monad.
which will enable us to model mutation: variables whose values appear
to change as the computation progresses. Later, we will study the
Continuation monad.
-In the meantime, 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*.