add sentence about Identity Monad

[lambda.git] / topics / week7_introducing_monads.mdwn

diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn
index c702638..244793f 100644 (file)
--- a/topics/week7_introducing_monads.mdwn
+++ b/topics/week7_introducing_monads.mdwn
@@ -1,7 +1,7 @@
 <!-- λ Λ ∀ ≡ α β γ ρ ω Ω -->
 <!-- Loved this one: http://www.stephendiehl.com/posts/monads.html -->
 
 <!-- λ Λ ∀ ≡ α β γ ρ ω Ω -->
 <!-- Loved this one: http://www.stephendiehl.com/posts/monads.html -->
 

-Introduci ng Monads
+Introducing Monads

 ==================
 
 The [[tradition in the functional programming
 ==================
 
 The [[tradition in the functional programming


@@ -54,9 +54,9 @@ 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`. (We'll fool with the markup to make this show a genuine box later; for now it will just display as underlined.)
+for the type of a boxed `int`.

 
 
 
 
 
 


@@ -64,21 +64,21 @@ for the type of a boxed `int`. (We'll fool with the markup to make this show a g
 
 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.
 


@@ -105,7 +105,7 @@ Here are the types of our crucial functions, together with our pronunciation, an
 
 <code>=&lt;&lt; or mdnib (flip mbind) (<u>Q</u>) -> (Q -> <u>R</u>) -> (<u>R</u>)</code>
 
 
 <code>=&lt;&lt; or mdnib (flip mbind) (<u>Q</u>) -> (Q -> <u>R</u>) -> (<u>R</u>)</code>
 

-<code>join: <span class="double">P</span> -> <u>P</u></code> 
+<code>join: <span class="box2">P</span> -> <u>P</u></code> 

 
 
 The menagerie isn't quite as bewildering as you might suppose. Many of these will
 
 
 The menagerie isn't quite as bewildering as you might suppose. Many of these will


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


@@ -371,7 +371,7 @@ Compare the new definitions of `safe_add3` and `safe_div3` closely: the definiti
 for `safe_add3` shows what it looks like to equip an ordinary operation to
 survive in dangerous presupposition-filled world. Note that the new
 definition of `safe_add3` does not need to test whether its arguments are
 for `safe_add3` shows what it looks like to equip an ordinary operation to
 survive in dangerous presupposition-filled world. Note that the new
 definition of `safe_add3` does not need to test whether its arguments are

-None values or real numbers---those details are hidden inside of the
+`None` values or real numbers---those details are hidden inside of the

 `bind` function.
 
 Note also that our definition of `safe_div3` recovers some of the simplicity of
 `bind` function.
 
 Note also that our definition of `safe_div3` recovers some of the simplicity of