X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek7_introducing_monads.mdwn;h=244793ff2b49620057e69bc0951be07c6a0a5082;hp=61012d55634d6d847c556a31f8735474a4e4fcd8;hb=7cdd4e2e306a7ceeb5cb2ebe423a2e8395283274;hpb=3d276dedb3ccde00a014e49ced1e438d82f4bcef
diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn
index 61012d55..244793ff 100644
--- a/topics/week7_introducing_monads.mdwn
+++ b/topics/week7_introducing_monads.mdwn
@@ -54,7 +54,7 @@ Warning: although our initial motivating examples are readily thought of as "con
Also, for clarity: the *box type* is the type `Î± list` (or as we might just say, the `list` type operator); the *boxed type* is some specific instantiation of the free type variable `Î±`. We'll often write boxed types as a box containing what the free
type variable instantiates to. So if our box type is `Î± list`, and `Î±` instantiates to the specific type `int`, we would write:
-__int__
+__int__

for the type of a boxed `int`.
@@ -64,21 +64,21 @@ for the type of a boxed `int`.
A lot of what we'll be doing concerns types that are called *Kleisli arrows*. Don't worry about why they're called that, or if you like go read some Category Theory. All we need to know is that these are functions whose type has the form:
-P -> __Q__
+`P -> `__Q__

That is, they are functions from values of one type `P` to a boxed type `Q`, for some choice of type expressions `P` and `Q`.
For instance, the following are Kleisli arrows:
-int -> __bool__
+`int -> `__bool__

-int list -> __int list__
+`int list -> `__int list__

In the first, `P` has become `int` and `Q` has become `bool`. (The boxed type __Q__

is __bool__

).
Note that the left-hand schema `P` is permitted to itself be a boxed type. That is, where
if `Î± list` is our box type, we can write the second arrow as
-__int__ -> __Q__
+__int__ -> __Q__

As semanticists, you are no doubt familiar with the debates between those who insist that propositions are sets of worlds and those who insist they are context change potentials. We hope to show you, in coming weeks, that propositions are (certain sorts of) Kleisli arrows. But this doesn't really compete with the other proposals; it is a generalization of them. Both of the other proposed structures can be construed as specific Kleisli arrows.
@@ -152,8 +152,8 @@ The name "bind" is not well chosen from our perspective, but this is too deeply
To take a trivial (but, as we will see, still useful) example,
consider the Identity box type: `Î±`. So if `Î±` is type `bool`,
-then a boxed `Î±` is ... a `bool`. In terms of the box analogy, the
-Identity box type is a completely invisible box. With the following
+then a boxed `Î±` is ... a `bool`. That is, __Î±__ = Î±

.
+In terms of the box analogy, the Identity box type is a completely invisible box. With the following
definitions:
mid â¡ \p. p