We're not going to ask you to write the entire program yourself.
Instead, we're going to give you [[the complete program, minus a few
-little bits of glue|code/reduction_with_reduction.ml]]. What you need to do is
+little bits of glue|code/reduction_with_substitution.ml]]. What you need to do is
understand how it all fits together. When you do, you'll understand
how to add the last little bits to make functioning program.
# reduce (App (Abstract ("x", Var "x"), Constant (Num 3)));;
- : lambdaTerm = Constant (Num 3)
-What kind of evaluation strategy does this evaluator use? In
+4. What kind of evaluation strategy does this evaluator use? In
particular, what are the answers to the three questions about
evaluation strategy as given in the discussion of [[evaluation
strategies|topics/week3_evaluation_order]] as Q1, Q2, and Q3?
Ok, the previous strategy sucked: tracking free and bound variables,
computing fresh variables, it's all super complicated.
-Here's a better strategy.
-
+Here's a better strategy. Instead of keeping all of the information
+about which variables have been bound or are still free implicitly
+inside of the terms, we'll keep score. This will require us to carry
+around a scorecard, which we will call an "environment". This is a
+familiar strategy, since it amounts to evaluating expressions relative
+to an assignment function. The difference between the assignment
+function approach above, and this approach, is one huge step towards
+monads.
+
+5. First, you need to get [[the evaluation
+code|code/reduction_with_environments.ml]] working. Look in the
+code for places where you see "not yet implemented", and get enough of
+those places working that you can use the code to evaluate terms.
+
+6. A snag: what happens when we want to replace a variable with a term
+that itself contains a free variable?
+
+<pre>
+term environment
+------------- -------------
+(\w.(\y.y)w)2 []
+(\y.y)w [w->2]
+y [w->2, y->w]
+</pre>
+
+In the first step, we bind `w` to the argument `2`. In the second
+step, we bind `y` to the argument `w`. In the third step, we would
+like to replace `y` with whatever its current value is according to
+our scorecard. On the simple-minded view, we would replace it with
+`w`. But that's not the right result, because `w` itself has been
+mapped onto 2.
+
+## Monads
+
+Mappables (functors), MapNables (applicatives functors), and Monads
+(composables) are ways of lifting computations from unboxed types into
+boxed types. Here, a "boxed type" is a type function with one missing
+piece, which we can think of as a function from a type to a type.
+Call this type function M, and let P, Q, R, and S be variables over types.
+
+Recall that a monad requires a singleton function 1:P-> MP, and a
+composition operator >=>: (P->MQ) -> (Q->MR) -> (R->MS) that obey the
+following laws:
+
+ 1 >=> k = k
+ k >=> 1 = k
+ j >=> (k >=> l) = (j >=> k) >=> l
+
+For instance, the identity monad has the identity function I for 1
+and ordinary function composition (o) for >=>. It is easy to prove
+that the laws hold for any expressions j, k, and l whose types are
+suitable for 1 and >=>:
+
+ 1 >=> k == I o k == \p. I (kp) ~~> \p.kp ~~> k
+ k >=> 1 == k o I == \p. k (Ip) ~~> \p.kp ~~> k
+
+ (j >=> k) >=> l == (\p.j(kp)) o l == \q.(\p.j(kp))(lq) ~~> \q.j(k(lq))
+ j >=> (k >=> l) == j o (k o l) == j o \p.k(lp) == \q.j(\p.k(lp)q) ~~> \q.j(k(lq))
+
+1. On a number of occasions, we've used the Option type to make our
+conceptual world neat and tidy (for instance, think of the discussion
+of Kaplan's Plexy). It turns out that there is a natural monad for
+the Option type. Borrowing the notation of OCaml, let's say that "`'a
+option`" is the type of a boxed `'a`, whatever type `'a` is. Then the
+obvious singleton for the Option monad is \p.Just p. What is the
+composition operator >=> for the Option monad? Show your answer is
+correct by proving that it obeys the monad laws.