1 # Assignment 6 (week 7)
3 ## Evaluation order in Combinatory Logic
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.
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.)
23 ## Evaluation in the untyped lambda calculus: substitution
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.)
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.
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:
51     # free_in "x" (App (Abstract ("x", Var "x"), Var "x"));;
52     - : bool = true
54 2. Once you get the `free_in` function working, you'll need to
55 complete the `substitute` function.  Sample target:
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))
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.
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:
69     # reduce (App (Abstract ("x", Var "x"), Constant (Num 3)));;
70     - : lambdaTerm = Constant (Num 3)
72 4. What kind of evaluation strategy does this evaluator use?  In
74 evaluation strategy as given in the discussion of [[evaluation
75 strategies|topics/week3_evaluation_order]] as Q1, Q2, and Q3?
77 ## Evaluation in the untyped calculus: environments and closures
79 Ok, the previous strategy sucked: tracking free and bound variables,
80 computing fresh variables, it's all super complicated.
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.
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.
96 6. A snag: what happens when we want to replace a variable with a term
97 that itself contains a free variable?
99         term          environment
100         ------------- -------------
101         (\w.(\y.y)w)2 []
102         (\y.y)w       [w->2]
103         y             [w->2, y->w]
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?
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:
115      type value = LiteralV of literal | Closure of lambdaTerm * env
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:
123          | Closure (Abstract(bound_ident, body), saved_r) -> eval body (push bound_ident arg saved_r) (* FIX ME *)
125 What should it be in order to solve the problem?
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.
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:
141     1 >=> k = k
142     k >=> 1 = k
143     j >=> (k >=> l) = (j >=> k) >=> l
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 >=>:
150     1 >=> k == I o k == \p. I (kp) ~~> \p.kp ~~> k
151     k >=> 1 == k o I == \p. k (Ip) ~~> \p.kp ~~> k
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))
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,
163      'a option = Nothing | Just 'a
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.
169 2. Do the same with lists.  That is, given an arbitrary type
170 'a, let the boxed type be ['a], i.e., a list of objects of type 'a.  The singleton
171 is `\p.[p]`, and the composition operator is
173        >=> (first:P->[Q]) (second:Q->[R]) :(P->[R]) = List.flatten (List.map f (g a))
175 For example:
177      f p = [p, p+1]
178      s q = [q*q, q+q]
179      >=> f s 7 = [49, 14, 64, 16]