From: jim
Date: Thu, 19 Mar 2015 16:02:34 +0000 (-0400)
Subject: add some tags
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=8be622c594f003684e8348973c5e85911161457b
add some tags
---
diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn
index 61012d55..7acc77cf 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.