X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2F_assignment6.mdwn;h=2e4f70444aa40105471e83a71efba74b8c380be6;hp=aabcbe07b2d5bd25a082e06319b9a511d2909380;hb=73f8e125d9910c93213d357c2779cc743fa22e8b;hpb=bd471e735a942a3489670fb2c935c7577624627d diff --git a/exercises/_assignment6.mdwn b/exercises/_assignment6.mdwn index aabcbe07..2e4f7044 100644 --- a/exercises/_assignment6.mdwn +++ b/exercises/_assignment6.mdwn @@ -24,5 +24,126 @@ recursive reduction function.) -## Evaluation in the untyped lambda calculus +## Evaluation in the untyped lambda calculus: substitution +Once you grok reduction and evaluation order in Combinatory Logic, +we're going to begin to construct an evaluator for a simple language +that includes lambda abstraction. 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. 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. +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)) + +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 + +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, 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. + +## 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.