exercises/_assignment6.mdwn

   1 # Assignment 6 (week 7)
   2
   3 ## Evaluation order in Combinatory Logic
   4
   5 1. Give a term that the lazy evaluators (either [[the Haskell
   6 evaluator|code/ski_evaluator.hs]], or the lazy version of [[the OCaml
   7 evaluator|code/ski_evaluator.ml]]) do not evaluate all the way to a
   8 normal form, i.e., that contains a redex somewhere inside of it after
   9 it has been reduced.
  10
  11 2. One of the [[criteria we established for classifying reduction
  12 strategies|topics/week3_evaluation_order]] strategies is whether they
  13 reduce subexpressions hidden under lambdas.  That is, for a term like
  14 `(\x y. x z) (\x. x)`, do we reduce to `\y.(\x.x) z` and stop, or do
  15 we reduce further to `\y.z`?  Explain what the corresponding question
  16 would be for CL. Using the eager version of the OCaml CL evaluator,
  17 prove that the evaluator does reduce expressions inside of at least
  18 some "functional" CL expressions.  Then provide a modified evaluator
  19 that does not perform reductions in those positions. (Just give the
  20 modified version of your recursive reduction function.)
  21
  22
  23 ## Evaluation in the untyped lambda calculus: substitution
  24
  25 Having sketched the issues with a discussion of Combinatory Logic,
  26 we're going to begin to construct an evaluator for a simple language
  27 that includes lambda abstraction.  In this problem set, we're going to
  28 work through the issues twice: once with a function that does
  29 substitution in the obvious way.  You'll see it's somewhat
  30 complicated.  The complications come from the need to worry about
  31 variable capture.  (Seeing these complications should give you an
  32 inkling of why we presented the evaluation order discussion using
  33 Combinatory Logic, since we don't need to worry about variables in
  34 CL.)
  35
  36 We're not going to ask you to write the entire program yourself.
  37 Instead, we're going to give you [[the complete program, minus a few
  38 little bits of glue|code/reduction_with_substitution.ml]].  What you
  39 need to do is understand how it all fits together.  When you do,
  40 you'll understand how to add the last little bits to make functioning
  41 program.
  42
  43 1. In the previous homework, you built a function that took an
  44 identifier and a lambda term and returned a boolean representing
  45 whether that identifier occured free inside of the term.  Your first
  46 task is to complete the `free_in` function, which has been crippled in
  47 the code base (look for lines that say `COMPLETE THIS LINE`).  Once
  48 you have your function working, you should be able to run queries such
  49 as this:
  50
  51     # free_in "x" (App (Abstract ("x", Var "x"), Var "x"));;
  52     - : bool = true
  53
  54 2. Once you get the `free_in` function working, you'll need to
  55 complete the `substitute` function.  Sample target:
  56
  57     # substitute (App (Abstract ("x", ((App (Abstract ("x", Var "x"), Var "y")))), Constant (Num 3))) "y" (Constant (Num 4));;
  58     - : lambdaTerm = App (Abstract ("x", App (Abstract ("x", Var "x"), Constant (Num 4))), Constant (Num 3))
  59
  60 By the way, you'll see a new wrinkle on OCaml's pattern-matching
  61 construction: `| PATTERN when x = 2 -> RESULT`.  This means that a
  62 match with PATTERN is only triggered if the boolean condition in the
  63 `when` clause evaluates to true.
  64
  65 3. Once you have completed the previous two problems, you'll have a
  66 complete evaluation program. Here's a simple sanity check for when you
  67 get it working:
  68
  69     # reduce (App (Abstract ("x", Var "x"), Constant (Num 3)));;
  70     - : lambdaTerm = Constant (Num 3)
  71
  72 4. What kind of evaluation strategy does this evaluator use?  In
  73 particular, what are the answers to the three questions about
  74 evaluation strategy as given in the discussion of [[evaluation
  75 strategies|topics/week3_evaluation_order]] as Q1, Q2, and Q3?
  76
  77 ## Evaluation in the untyped calculus: environments and closures
  78
  79 Ok, the previous strategy sucked: tracking free and bound variables,
  80 computing fresh variables, it's all super complicated.
  81
  82 Here's a better strategy. Instead of keeping all of the information
  83 about which variables have been bound or are still free implicitly
  84 inside of the terms, we'll keep score.  This will require us to carry
  85 around a scorecard, which we will call an "environment".  This is a
  86 familiar strategy for philosophers of language and for linguists,
  87 since it amounts to evaluating expressions relative to an assignment
  88 function.  The difference between the assignment function approach
  89 above, and this approach, is one huge step towards monads.
  90
  91 5. First, you need to get [[the evaluation
  92 code|code/reduction_with_environments.ml]]  working.  Look in the
  93 code for places where you see "not yet implemented", and get enough of
  94 those places working that you can use the code to evaluate terms.
  95
  96 6. A snag: what happens when we want to replace a variable with a term
  97 that itself contains a free variable?
  98
  99         term          environment
 100         ------------- -------------
 101         (\w.(\y.y)w)2 []
 102         (\y.y)w       [w->2]
 103         y             [w->2, y->w]
 104
 105 In the first step, we bind `w` to the argument `2`.  In the second
 106 step, we bind `y` to the argument `w`.  In the third step, we would
 107 like to replace `y` with whatever its current value is according to
 108 our scorecard.  On the simple-minded view, we would replace it with
 109 `w`.  But that's not the right result, because `w` itself has been
 110 mapped onto 2.  What does your evaluator code do?
 111
 112 We'll guide you to a solution involving closures.  The first step is
 113 to allow values to carry around a specific environment with them:
 114
 115      type value = LiteralV of literal | Closure of lambdaTerm * env
 116
 117 This will provide the extra information we need to evaluate an
 118 identifier all the way down to the correct final result.  Here is a
 119 [[modified version of the evaluator that provides all the scaffoling for
 120 passing around closures|exercises/reduction_with_closures]].
 121 The problem is with the following line:
 122
 123          | Closure (Abstract(bound_ident, body), saved_r) -> eval body (push bound_ident arg saved_r) (* FIX ME *)
 124
 125 What should it be in order to solve the problem?
 126
 127
 128 ## Monads
 129
 130 Mappables (functors), MapNables (applicatives functors), and Monads
 131 (composables) are ways of lifting computations from unboxed types into
 132 boxed types.  Here, a "boxed type" is a type function with one missing
 133 piece, which we can think of as a function from a type to a type.
 134 Call this type function M, and let P, Q, R, and S be variables over types.
 135
 136 Recall that a monad requires a singleton function 1:P-> MP, and a
 137 composition operator >=>: (P->MQ) -> (Q->MR) -> (P->MR) [the type for
 138 the composition operator given here corrects a "type"-o from the class handout]
 139 that obey the following laws:
 140
 141     1 >=> k = k
 142     k >=> 1 = k
 143     j >=> (k >=> l) = (j >=> k) >=> l
 144
 145 For instance, the identity monad has the identity function I for 1
 146 and ordinary function composition (o) for >=>.  It is easy to prove
 147 that the laws hold for any expressions j, k, and l whose types are
 148 suitable for 1 and >=>:
 149
 150     1 >=> k == I o k == \p. I (kp) ~~> \p.kp ~~> k
 151     k >=> 1 == k o I == \p. k (Ip) ~~> \p.kp ~~> k
 152
 153     (j >=> k) >=> l == (\p.j(kp)) o l == \q.(\p.j(kp))(lq) ~~> \q.j(k(lq))
 154     j >=> (k >=> l) == j o (k o l) == j o \p.k(lp) == \q.j(\p.k(lp)q) ~~> \q.j(k(lq))
 155
 156 1. On a number of occasions, we've used the Option type to make our
 157 conceptual world neat and tidy (for instance, think of the discussion
 158 of Kaplan's Plexy).  As we learned in class, there is a natural monad
 159 for the Option type.  Borrowing the notation of OCaml, let's say that
 160 "`'a option`" is the type of a boxed `'a`, whatever type `'a` is.
 161 More specifically,
 162
 163      'a option = Nothing | Just 'a
 164
 165 Then the obvious singleton for the Option monad is \p.Just p.  Give
 166 (or reconstruct) the composition operator >=> we discussed in class.
 167 Show your composition operator obeys the monad laws.
 168
 169 2. Do the same with crossy lists.  That is, given an arbitrary type
 170 'a, let the boxed type be a list of objects of type 'a.  The singleton
 171 is `\p.[p]`, and the composition operator is
 172
 173        >=> (first:P->[Q]) (second:Q->[R]) :(P->[R]) = fun p -> [r | q <- first p, r <- second q]
 174
 175 Sanity check:
 176
 177      f p = [x, x+1]
 178      s q = [x*x, x+x]
 179      >=> f s 7 = [49, 14, 64, 16]
 180
 181 3. Do the same for zippy lists.  That is, you need to find a
 182 composition operator such that
 183
 184      f p = [x, x+1]
 185      s q = [x*x, x+x]
 186      >=> f s 7 = [49, 64]
 187
 188 and then prove it obeys the monad laws.