-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.
-