XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2Fassignment7.mdwn;h=e9cf82371162e91fb718094a669a096e5809a337;hp=ebc20e064bc1ad1f7d02756ad8a015913dfaea9d;hb=9d1d3d7d480c1c808a7a9fddf39f95037196d506;hpb=a99932db08dadc468764f1dfcc32d19760b52c5a
diff git a/exercises/assignment7.mdwn b/exercises/assignment7.mdwn
index ebc20e06..e9cf8237 100644
 a/exercises/assignment7.mdwn
+++ b/exercises/assignment7.mdwn
@@ 1,180 +1,132 @@
# Assignment 6 (week 7)
+# Assignment 7
+
+There is no separate assignment 6. (There was a single big assignment for weeks 5 and 6, and
+we're going to keep the assignment numbers in synch with the weeks.)
## Evaluation order in Combinatory Logic
1. Give a term that the lazy evaluators (either [[the Haskell
evaluatorcode/ski_evaluator.hs]], or the lazy version of [[the OCaml
evaluatorcode/ski_evaluator.ml]]) do not evaluate all the way to a
normal form, i.e., that contains a redex somewhere inside of it after
+normal form, that is, that contains a redex somewhere inside of it after
it has been reduced.
2. One of the [[criteria we established for classifying reduction
strategiestopics/week3_evaluation_order]] strategies is whether they
reduce subexpressions hidden under lambdas. That is, for a term like
+reduce subterms 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 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
+would be for CL. Using the eager version of the OCaml CL evaluator (`reduce_try2`),
+prove that the evaluator does reduce terms inside of at least
+some "functional" CL terms. 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
+## Evaluation in the untyped lambda calculus: substituteandrepeat
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
+substitution in the obvious way, and keeps reducingandrepeating until
+there are no more eligible redexes. 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
+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 gluecode/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))
+Instead, we're going to give you almost the complete program, with a few gaps
+in it that you have to complete. You have to understand enough to
+add the last pieces to make the program function.
By the way, you'll see a new wrinkle on OCaml's patternmatching
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.
+You can find the skeleton code [[here/code/untyped_evaluator.ml]].
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:
+We've also prepared a much fuller version, that has userfriendly input
+and printing of results. We'll provide a link to that shortly. It
+will be easiest for you to understand that code if you've
+completed the gaps in the simplified skeleton linked above.
 # 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
strategiestopics/week3_evaluation_order]] as Q1, Q2, and Q3?
+## Evaluation in the untyped lambda calculus: environments
## 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.
+The previous strategy is nice because it corresponds so closely to the
+reduction rules we give when specifying our lambda calculus. (Including
+specifying evaluation order, which redexes it's allowed to reduce, and
+so on.) But keeping track of free and bound variables, computing fresh
+variables when needed, that's all a pain.
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
+inside of the terms, we'll keep a separate 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
+since it amounts to evaluating terms relative to an assignment
+function. The difference between the substituteandrepeat approach
above, and this approach, is one huge step towards monads.
5. First, you need to get [[the evaluation
codecode/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.
+The skeleton code for this is at the [[same link as before/code/untyped_evaluator.ml]].
+This part of the exercise is the "V2" part of that code.
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]
+## Monads
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 simpleminded 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?
+Mappables (functors), MapNables (applicative 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 unsaturated
+hole (which may have several occurrences, as in `(Î±,Î±) tree`). We can think of the box type
+as a function from a type to a type.
We'll guide you to a solution involving closures. The first step is
to allow values to carry around a specific environment with them:
+Recall that a monad requires a singleton function mid : P> P
, and a
+composition operator like >=> : (P>Q) > (Q>R) > (P>R)
.
 type value = LiteralV of literal  Closure of lambdaTerm * env
+As we said in the notes, we'll move freely back and forth between using `>=>` and using `<=<` (aka `mcomp`), which
+is just `>=>` with its arguments flipped. `<=<` has the virtue that it corresponds more
+closely to the ordinary mathematical symbol `â`. But `>=>` has the virtue
+that its types flow more naturally from left to right.
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 closuresexercises/reduction_with_closures]].
The problem is with the following line:
+Anyway, `mid` and (let's say) `<=<` have to obey the Monad Laws:
  Closure (Abstract(bound_ident, body), saved_r) > eval body (push bound_ident arg saved_r) (* FIX ME *)
+ mid <=< k = k
+ k <=< mid = k
+ j <=< (k <=< l) = (j <=< k) <=< l
What should it be in order to solve the problem?
+For example, the Identity monad has the identity function `I` for `mid`
+and ordinary function composition `â` for `<=<`. It is easy to prove
+that the laws hold for any terms `j`, `k`, and `l` whose types are
+suitable for `mid` and `<=<`:
+ mid <=< k == I â k == \p. I (k p) ~~> \p. k p ~~> k
+ k <=< mid == k â I == \p. k (I p) ~~> \p. k p ~~> k
## Monads
+ (j <=< k) <=< l == (\p. j (k p)) â l == \q. (\p. j (k p)) (l q) ~~> \q. j (k (l q))
+ j <=< (k <=< l) == j â (k â l) == j â (\p. k (l p)) == \q. j ((\p. k (l p)) q) ~~> \q. j (k (l q))
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.
+1. On a number of occasions, we've used the Option/Maybe type to make our
+conceptual world neat and tidy (for instance, think of [[our discussion
+of Kaplan's Plexytopics/week6_plexy]]). As we learned in class, there is a natural monad
+for the Option type. Using the vocabulary 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
+ type 'a option = None  Some '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.
+ (If you have trouble keeping straight what is the OCaml terminology for this and what is the Haskell terminology, don't worry, we do too.)
2. Do the same with lists. That is, given an arbitrary type
'a, let the boxed type be ['a], i.e., a list of objects of type 'a. The singleton
is `\p.[p]`, and the composition operator is
+ Now the obvious singleton for the Option monad is `\p. Some p`. Give
+(or reconstruct) either of the composition operators `>=>` or `<=<`.
+Show that your composition operator obeys the Monad Laws.
 >=> (first:P>[Q]) (second:Q>[R]) :(P>[R]) = List.flatten (List.map f (g a))
+2. Do the same with lists. That is, given an arbitrary type
+`'a`, let the boxed type be `['a]` or `'a list`, that is, lists of values of type `'a`. The `mid`
+is the singleton function `\p. [p]`, and the composition operator is:
For example:
+ let (>=>) (j : 'a > 'b list) (k : 'b > 'c list) : 'a > 'c list =
+ fun a > List.flatten (List.map k (j a))
 f p = [p, p+1]
 s q = [q*q, q+q]
 >=> f s 7 = [49, 14, 64, 16]
+ For example:
+ let j a = [a; a+1];;
+ let k b = [b*b; b+b];;
+ (j >=> k) 7 (* ==> [49; 14; 64; 16] *)