add sentence about Identity Monad
[lambda.git] / topics / week7_introducing_monads.mdwn
index 61012d5..244793f 100644 (file)
@@ -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:
 
 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:
 
-<u>int</u>
+<code><u>int</u></code>
 
 for the type of a boxed `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:
 
 
 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 -> <u>Q</u>
+<code>P -> <u>Q</u></code>
 
 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:
 
 
 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 -> <u>bool</u>
+<code>int -> <u>bool</u></code>
 
 
-int list -> <u>int list</u>
+<code>int list -> <u>int list</u></code>
 
 In the first, `P` has become `int` and `Q` has become `bool`. (The boxed type <code><u>Q</u></code> is <code><u>bool</u></code>).
 
 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
 
 
 In the first, `P` has become `int` and `Q` has become `bool`. (The boxed type <code><u>Q</u></code> is <code><u>bool</u></code>).
 
 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
 
-<u>int</u> -> <u>Q</u>
+<code><u>int</u> -> <u>Q</u></code>
 
 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.
 
 
 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`,
 
 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, <code><u>α</u> = α</code>.
+In terms of the box analogy, the Identity box type is a completely invisible box. With the following
 definitions:
 
     mid ≡ \p. p
 definitions:
 
     mid ≡ \p. p