monads

diff --git a/topics/_week7_monads.mdwn b/topics/_week7_monads.mdwn
index 21ac2f5..a751da2 100644 (file)
--- a/topics/_week7_monads.mdwn
+++ b/topics/_week7_monads.mdwn
@@ -1,3 +1,5 @@
+<!-- λ Λ ∀ ≡ α β ρ ω Ω -->
+

 Monads
 ======
 
 Monads
 ======
 


@@ -8,10 +10,44 @@ monsters, monads are burritos.  We're part of the backlash that
 prefers to say that monads are monads.  
 
 The closest we will come to metaphorical talk is to suggest that
 prefers to say that monads are monads.  
 
 The closest we will come to metaphorical talk is to suggest that

-monadic types place objects inside of boxes, and that monads wrap and
-unwrap boxes to expose or enclose the objects inside of them.  In any
-case, the emphasis will be on starting with the abstract structure of
-monads, followed by instances of monads from the philosophical and
+monadic types place objects inside of *boxes*, and that monads wrap
+and unwrap boxes to expose or enclose the objects inside of them.  In
+any case, the emphasis will be on starting with the abstract structure
+of monads, followed by instances of monads from the philosophical and

 linguistics literature.
 
 linguistics literature.
 

-To 
+### Boxes: type expressions with one free type variable
+
+Recall that we've been using lower-case Greek letters
+<code>&alpha;, &beta;, &gamma;, ...</code> to represent types.  We'll
+use `P`, `Q`, `R`, and `S` as metavariables over type schemas, where a
+type schema is a type expression that may or may not contain unbound
+type variables.  For instance, we might have
+
+    P ≡ Int
+    P ≡ α -> α
+    P ≡ ∀α. α -> α
+    P ≡ ∀α. α -> β 
+
+etc.
+
+A box type will be a type expression that contains exactly one free
+type variable.  Some examples (using OCaml's type conventions):
+
+    α Maybe
+    α List
+    (α, P) Tree    (assuming P contains no free type variables)
+    (α, α) Tree
+
+The idea is that whatever type the free type variable α might be,
+the boxed type will be a box that "contains" an object of type α.
+For instance, if `α List` is our box type, and α is the basic type
+Int, then in this context, `Int List` is the type of a boxed integer.
+
+We'll often write box types as a box containing the value of the free
+type variable.  So if our box type is `α List`, and `α == Int`, we
+would write
+
+<code><table border>Int</table></code>
+
+