From 6c44248b27640d43b5a683bb580f83e5cef08a28 Mon Sep 17 00:00:00 2001
From: Chris Barker
Date: Mon, 1 Nov 2010 10:20:44 0400
Subject: [PATCH] edits

week7.mdwn  86 +++++++++++++++++++++++++++++++
1 file changed, 43 insertions(+), 43 deletions()
diff git a/week7.mdwn b/week7.mdwn
index d3e4b47d..e4e884bc 100644
 a/week7.mdwn
+++ b/week7.mdwn
@@ 152,35 +152,6 @@ None objects or real numbersthose details are hidden inside of the
The definition of `div'` shows exactly what extra needs to be said in
order to trigger the nodivisionbyzero presupposition.
For linguists: this is a complete theory of a particularly simply form
of presupposition projection (every predicate is a hole).




Monads in General


Start by (re)reading the discussion of monads in the lecture notes for
week 6 [[Towards Monads]].
In those notes, we saw a way to separate thinking about error
conditions (such as trying to divide by zero) from thinking about
normal arithmetic computations. We did this by making use of the
`option` type: in each place where we had something of type `int`, we
put instead something of type `int option`, which is a sum type
consisting either of one choice with an `int` payload, or else a `None`
choice which we interpret as signaling that something has gone wrong.

The goal was to make normal computing as convenient as possible: when
we're adding or multiplying, we don't have to worry about generating
any new errors, so we do want to think about the difference between
`int`s and `int option`s. We tried to accomplish this by defining a
`bind` operator, which enabled us to peel away the `option` husk to get
at the delicious integer inside. There was also a homework problem
which made this even more convenient by mapping any binary operation
on plain integers into a lifted operation that understands how to deal
with `int option`s in a sensible way.

[Linguitics note: Dividing by zero is supposed to feel like a kind of
presupposition failure. If we wanted to adapt this approach to
building a simple account of presupposition projection, we would have
@@ 196,6 +167,29 @@ material that otherwise would trigger a presupposition violation; but,
not surprisingly, these refinements will require some more
sophisticated techniques than the supersimple option monad.]
+
+Monads in General
+
+
+We've just seen a way to separate thinking about error conditions
+(such as trying to divide by zero) from thinking about normal
+arithmetic computations. We did this by making use of the `option`
+type: in each place where we had something of type `int`, we put
+instead something of type `int option`, which is a sum type consisting
+either of one choice with an `int` payload, or else a `None` choice
+which we interpret as signaling that something has gone wrong.
+
+The goal was to make normal computing as convenient as possible: when
+we're adding or multiplying, we don't have to worry about generating
+any new errors, so we would rather not think about the difference
+between `int`s and `int option`s. We tried to accomplish this by
+defining a `bind` operator, which enabled us to peel away the `option`
+husk to get at the delicious integer inside. There was also a
+homework problem which made this even more convenient by defining a
+`lift` operator that mapped any binary operation on plain integers
+into a lifted operation that understands how to deal with `int
+option`s in a sensible way.
+
So what exactly is a monad? We can consider a monad to be a system
that provides at least the following three elements:
@@ 216,7 +210,12 @@ that provides at least the following three elements:
discussing earlier (whose value is written `()`). It's also only
very loosely connected to the "return" keyword in many other
programming languages like C. But these are the names that the literature
 uses.
+ uses. [The rationale for "unit" comes from the monad laws
+ (see below), where the unit function serves as an identity,
+ just like the unit number (i.e., 1) serves as the identity
+ object for multiplication. The rationale for "return" comes
+ from a misguided desire to resonate with C programmers and
+ other imperative types.]
The unit/return operation is a way of lifting an ordinary object into
the monadic box you've defined, in the simplest way possible. You can think
@@ 276,6 +275,8 @@ that provides at least the following three elements:
be defined so as to make sure that the result of `f x` was also
a singing box. If `f` also wanted to insert a song, you'd have to decide
whether both songs would be carried through, or only one of them.
+ (Are you beginning to realize how wierd and wonderful monads
+ can be?)
There is no single `bind` function that dictates how this must go.
For each new monadic type, this has to be worked out in an
@@ 285,17 +286,11 @@ So the "option/maybe monad" consists of the polymorphic `option` type, the
`unit`/return function, and the `bind` function.
A note on notation: Haskell uses the infix operator `>>=` to stand
for `bind`. Chris really hates that symbol. Following Wadler, he prefers to
use an infix fivepointed star ⋆, or on a keyboard, `*`. Jim on the other hand
thinks `>>=` is what the literature uses and students won't be able to
avoid it. Moreover, although ⋆ is OK (though not a convention that's been picked up), overloading the multiplication symbol invites its own confusion
and Jim feels very uneasy about that. If not `>>=` then we should use
some other unfamiliar infix symbol (but `>>=` already is such...)
+A note on notation: Haskell uses the infix operator `>>=` to stand for
+`bind`: wherever you see `u >>= f`, that means `bind u f`.
+Wadler uses ⋆, but that hasn't been widely adopted (unfortunately).
In any case, the course leaders will work this out somehow. In the meantime,
as you read around, wherever you see `u >>= f`, that means `bind u f`. Also,
if you ever see this notation:
+Also, if you ever see this notation:
do
x < u
@@ 309,9 +304,14 @@ Similarly:
y < v
f x y
is shorthand for `u >>= (\x > v >>= (\y > f x y))`, that is, `bind u (fun x
> bind v (fun y > f x y))`. Those who did last week's homework may recognize
this last expression.
+is shorthand for `u >>= (\x > v >>= (\y > f x y))`, that is, `bind u
+(fun x > bind v (fun y > f x y))`. Those who did last week's
+homework may recognize this last expression. You can think of the
+notation like this: take the singing box `u` and evaluate it (which
+includes listening to the song). Take the int contained in the
+singing box (the end result of evaluting `u`) and bind the variable
+`x` to that int. So `x < u` means "Sing me up an int, and I'll call
+it `x`".
(Note that the above "do" notation comes from Haskell. We're mentioning it here
because you're likely to see it when reading about monads. It won't work in

2.11.0