topics/_week7_monads.mdwn

   1 <!-- λ Λ ∀ ≡ α β ρ ω Ω -->
   2
   3 Monads
   4 ======
   5
   6 The [[tradition in the functional programming
   7 literature|https://wiki.haskell.org/Monad_tutorials_timeline]] is to
   8 introduce monads using a metaphor: monads are spacesuits, monads are
   9 monsters, monads are burritos.  We're part of the backlash that
  10 prefers to say that monads are monads.
  11
  12 The closest we will come to metaphorical talk is to suggest that
  13 monadic types place objects inside of *boxes*, and that monads wrap
  14 and unwrap boxes to expose or enclose the objects inside of them.  In
  15 any case, the emphasis will be on starting with the abstract structure
  16 of monads, followed by instances of monads from the philosophical and
  17 linguistics literature.
  18
  19 ### Boxes: type expressions with one free type variable
  20
  21 Recall that we've been using lower-case Greek letters
  22 <code>&alpha;, &beta;, &gamma;, ...</code> to represent types.  We'll
  23 use `P`, `Q`, `R`, and `S` as metavariables over type schemas, where a
  24 type schema is a type expression that may or may not contain unbound
  25 type variables.  For instance, we might have
  26
  27     P ≡ Int
  28     P ≡ α -> α
  29     P ≡ ∀α. α -> α
  30     P ≡ ∀α. α -> β
  31
  32 etc.
  33
  34 A box type will be a type expression that contains exactly one free
  35 type variable.  Some examples (using OCaml's type conventions):
  36
  37     α Maybe
  38     α List
  39     (α, P) Tree    (assuming P contains no free type variables)
  40     (α, α) Tree
  41
  42 The idea is that whatever type the free type variable α might be,
  43 the boxed type will be a box that "contains" an object of type α.
  44 For instance, if `α List` is our box type, and α is the basic type
  45 Int, then in this context, `Int List` is the type of a boxed integer.
  46
  47 We'll often write box types as a box containing the value of the free
  48 type variable.  So if our box type is `α List`, and `α == Int`, we
  49 would write
  50
  51 <table border=2px><td>Int</td></table>
  52
  53 for the type of a boxed Int.
  54
  55 At the most general level, we'll talk about *Kleisli arrows*:
  56
  57 P -> <table border=2px><td>Q</td></table>
  58
  59 A Kleisli arrow is the type of a function from objects of type P to
  60 objects of type box Q, for some choice of type expressions P and Q.
  61 For instance, the following are arrows:
  62
  63 Int -> <table border=2px><td>Bool</td></table>
  64
  65 Int List -> <table border=2px><td>Int List</td></table>
  66
  67 Note that the left-hand schema can itself be a boxed type.  That is,
  68 if `α List` is our box type, we can write the second arrow as
  69
  70 <table border=2px><td>Int</td></table>
  71 ->
  72 <table border=2px><td><table
  73 border=2px><td>Int</td></table></td></table>
  74