+
+# unit 2;;
+- : int option = Some 2
# unit 2 * unit;;
- : int option = Some 2
+
+# divide 6 2;;
+- : int option = Some 3
+# unit 2 * divide 6;;
+- : int option = Some 3
+
+# divide 6 0;;
+- : int option = None
+# unit 0 * divide 6;;
+- : int option = None
The parentheses is the magic for telling Ocaml that the
@@ -126,13 +148,23 @@ is `*`, pronounced "bind") is an infix operator, so we write
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.
- For an illustration of associativity in the option monad:
+ Some examples of associativity in the option monad:
-Some 3 * unit * unit;;
+# Some 3 * unit * unit;;
- : int option = Some 3
-Some 3 * (fun x -> unit x * unit);;
+# Some 3 * (fun x -> unit x * unit);;
- : int option = Some 3
+
+# Some 3 * divide 6 * divide 2;;
+- : int option = Some 1
+# Some 3 * (fun x -> divide 6 x * divide 2);;
+- : int option = Some 1
+
+# Some 3 * divide 2 * divide 6;;
+- : int option = None
+# Some 3 * (fun x -> divide 2 x * divide 6);;
+- : int option = None

Of course, associativity must hold for arbitrary functions of
@@ -151,6 +183,8 @@ to `g r`.
# Some 3 * unit;;
- : int option = Some 3
+# None * unit;;
+- : 'a option = None

Now, if you studied algebra, you'll remember that a *monoid* is an
@@ -164,7 +198,7 @@ arguments of a monoid operation) the two arguments of the bind are of
different types. But if we generalize bind so that both arguments are
of type `'a -> M 'a`, then we get plain identity laws and
associativity laws, and the monad laws are exactly like the monoid
-laws (see ).
+laws (see , near the bottom).
Monad outlook
@@ -191,12 +225,15 @@ intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
though without explicitly using monads.
All of the code in the discussion below can be found here: [[intensionality-monad.ml]].
-To run it, download the file, start Ocaml, and say `# #use
-"intensionality-monad.ml";;`.
+To run it, download the file, start Ocaml, and say
+
+ # #use "intensionality-monad.ml";;
+
+Note the extra `#` attached to the directive `use`.
Here's the idea: since people can have different attitudes towards
different propositions that happen to have the same truth value, we
-can't have sentences denoting simple truth values. Then if John
+can't have sentences denoting simple truth values. If we did, then if John
believed that the earth was round, it would force him to believe
Fermat's last theorem holds, since both propositions are equally true.
The traditional solution is to allow sentences to denote a function
@@ -217,16 +254,16 @@ Vs s->t->e->t s->(s->t)->(s->e)->t thought
This system is modeled on the way Montague arranged his grammar.
-(There are significant simplifications: for instance, determiner
+There are significant simplifications: for instance, determiner
phrases are thought of as corresponding to individuals rather than to
-generalized quantifiers.) If you're curious about the initial `s`'s
+generalized quantifiers. If you're curious about the initial `s`'s
in the extensional types, they're there because the behavior of these
expressions depends on which world they're evaluated at. If you are
in a situation in which you can hold the evaluation world constant,
-you can further simplify the extensional types. (Usually, the
+you can further simplify the extensional types. Usually, the
dependence of the extension of an expression on the evaluation world
is hidden in a superscript, or built into the lexical interpretation
-function.)
+function.
The main difference between the intensional types and the extensional
types is that in the intensional types, the arguments are functions
@@ -240,8 +277,9 @@ types. Wouldn't it be nice to keep the complicated types to just
those attitude verbs that need to worry about intensions, and keep the
rest of the grammar as extensional as possible? This desire is
parallel to our earlier desire to limit the concern about division by
-zero to the division function, and let the other functions ignore
-division-by-zero problems as much as possible.
+zero to the division function, and let the other functions, like
+addition or multiplication, ignore division-by-zero problems as much
+as possible.
So here's what we do: