(no commit message)
[lambda.git] / exercises / _assignment6.mdwn
index d1b3696..b6a00de 100644 (file)
@@ -1,4 +1,4 @@
-~/Dropbox/Lambda/wiki/exercises/# Assignment 6 (week 7)
+# Assignment 6 (week 7)
 
 ## Evaluation order in Combinatory Logic
 
@@ -8,21 +8,181 @@ evaluator|code/ski_evaluator.ml]]) do not evaluate all the way to a
 normal form, i.e., that contains a redex somewhere inside of it after
 it has been reduced.
 
-<!-- reduce3 (FA (K, FA (I, I))) -->
-
 2. One of the [[criteria we established for classifying reduction
 strategies|topics/week3_evaluation_order]] strategies is whether they
 reduce subexpressions hidden under lambdas.  That is, for a term like
 `(\x y. x z) (\x. x)`, do we reduce to `\y.(\x.x) z` and stop, or do
 we reduce further to `\y.z`?  Explain what the corresponding question
-would be for CL. Using either the OCaml CL evaluator or the Haskell
-evaluator developed in the wiki notes, prove that the evaluator does
-reduce expressions inside of at least some "functional" CL
-expressions.  Then provide a modified evaluator that does not perform
-reductions in those positions. (Just give the modified version of your
-recursive reduction function.)
+would be for CL. Using the eager version of the OCaml CL evaluator,
+prove that the evaluator does reduce expressions inside of at least
+some "functional" CL expressions.  Then provide a modified evaluator
+that does not perform reductions in those positions. (Just give the
+modified version of your recursive reduction function.)
+
+
+## Evaluation in the untyped lambda calculus: substitution
+
+Having sketched the issues with a discussion of Combinatory Logic,
+we're going to begin to construct an evaluator for a simple language
+that includes lambda abstraction.  In this problem set, we're going to
+work through the issues twice: once with a function that does
+substitution in the obvious way.  You'll see it's somewhat
+complicated.  The complications come from the need to worry about
+variable capture.  (Seeing these complications should give you an
+inkling of why we presented the evaluation order discussion using
+Combinatory Logic, since we don't need to worry about variables in
+CL.)
+
+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_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.
+
+1. In the previous homework, you built a function that took an
+identifier and a lambda term and returned a boolean representing
+whether that identifier occured free inside of the term.  Your first
+task is to complete the `free_in` function, which has been crippled in
+the code base (look for lines that say `COMPLETE THIS LINE`).  Once
+you have your function working, you should be able to run queries such
+as this:
+
+    # free_in "x" (App (Abstract ("x", Var "x"), Var "x"));;
+    - : bool = true
+
+2. Once you get the `free_in` function working, you'll need to
+complete the `substitute` function.  Sample target:
+
+    # substitute (App (Abstract ("x", ((App (Abstract ("x", Var "x"), Var "y")))), Constant (Num 3))) "y" (Constant (Num 4));;
+    - : lambdaTerm = App (Abstract ("x", App (Abstract ("x", Var "x"), Constant (Num 4))), Constant (Num 3))
+
+By the way, you'll see a new wrinkle on OCaml's pattern-matching
+construction: `| PATTERN when x = 2 -> RESULT`.  This means that a
+match with PATTERN is only triggered if the boolean condition in the
+`when` clause evaluates to true.
+
+3. Once you have completed the previous two problems, you'll have a
+complete evaluation program. Here's a simple sanity check for when you
+get it working:
+
+    # reduce (App (Abstract ("x", Var "x"), Constant (Num 3)));;
+    - : lambdaTerm = Constant (Num 3)
+
+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?
+
+## Evaluation in the untyped calculus: environments and closures
+
+Ok, the previous strategy sucked: tracking free and bound variables,
+computing fresh variables, it's all super complicated.
+
+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 for philosophers of language and for linguists,
+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?  
+
+        term          environment
+        ------------- -------------
+        (\w.(\y.y)w)2 []
+        (\y.y)w       [w->2]
+        y             [w->2, y->w]
+
+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.  What does your evaluator code do?
+
+We'll guide you to a solution involving closures.  The first step is
+to allow values to carry around a specific environment with them:
+
+     type value = LiteralV of literal | Closure of lambdaTerm * env
+
+This will provide the extra information we need to evaluate an
+identifier all the way down to the correct final result.  Here is a
+[[modified version of the evaluator that provides all the scaffoling for
+passing around closures|exercises/reduction_with_closures]].
+The problem is with the following line:
+
+         | Closure (Abstract(bound_ident, body), saved_r) -> eval body (push bound_ident arg saved_r) (* FIX ME *)
+
+What should it be in order to solve the problem?
+
+
+## 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) -> (P->MR) [the type for
+the composition operator given here corrects a "type"-o from the class handout]
+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).  As we learned in class, 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.
+More specifically,
+
+     'a option = Nothing | Just 'a
+
+Then the obvious singleton for the Option monad is \p.Just p.  Give
+(or reconstruct) the composition operator >=> we discussed in class.
+Show your composition operator obeys the monad laws.
+
+2. Do the same with crossy lists.  That is, given an arbitrary type
+'a, let the boxed type be a list of objects of type 'a.  The singleton
+is `\p.[p]`, and the composition operator is 
+
+       >=> (first:P->[Q]) (second:Q->[R]) :(P->[R]) = fun p -> [r | q <- first p, r <- second q]
+
+Sanity check: 
+
+    f p = [x, x+1]
+    s q = [x*x, x+x]
+    >=> f s 7 = [49, 14, 64, 16]
 
-<!-- just add early no-op cases for Ka and Sab -->
+3. Do the same for zippy lists.  That is, you need to find a
+composition operator such that
 
-## Evaluation in the untyped lambda calculus
+    f p = [x, x+1]
+    s q = [x*x, x+x]
+    >=> f s 7 = [49, 64]
 
+and then prove it obeys the monad laws.