one more exercise
[lambda.git] / exercises / assignment7.mdwn
1 There is no separate assignment 6. (There was a single big assignment for weeks 5 and 6, and
2 we're going to keep the assignment numbers in synch with the weeks.)
3
4 [[!toc]]
5
6 ## Evaluation order in Combinatory Logic
7
8 1. Give a term that the lazy evaluators (either [[the Haskell
9 evaluator|code/ski_evaluator.hs]], or the lazy version of [[the OCaml
10 evaluator|code/ski_evaluator.ml]]) do not evaluate all the way to a
11 normal form, that is, that contains a redex somewhere inside of it after
12 it has been reduced.
13
14 2. One of the [[criteria we established for classifying reduction
15 strategies|topics/week3_evaluation_order]] strategies is whether they
16 reduce subterms hidden under lambdas.  That is, for a term like
17 `(\x y. x z) (\x. x)`, do we reduce to `\y.(\x.x) z` and stop, or do
18 we reduce further to `\y.z`?  Explain what the corresponding question
19 would be for CL. Using the eager version of the OCaml CL evaluator (`reduce_try2`),
20 prove that the evaluator does reduce terms inside of at least
21 some "functional" CL terms.  Then provide a modified evaluator
22 that does not perform reductions in those positions. (Just give the
23 modified version of your recursive reduction function.)
24
25
26 ## Evaluation in the untyped lambda calculus: substitute-and-repeat
27
28 Having sketched the issues with a discussion of Combinatory Logic,
29 we're going to begin to construct an evaluator for a simple language
30 that includes lambda abstraction.  In this problem set, we're going to
31 work through the issues twice: once with a function that does
32 substitution in the obvious way, and keeps reducing-and-repeating until
33 there are no more eligible redexes. You'll see it's somewhat
34 complicated.  The complications come from the need to worry about
35 variable capture. (Seeing these complications should give you an
36 inkling of why we presented the evaluation order discussion using
37 Combinatory Logic, since we don't need to worry about variables in
38 CL.)
39
40 We're not going to ask you to write the entire program yourself.
41 Instead, we're going to give you almost the complete program, with a few gaps
42 in it that you have to complete. You have to understand enough to
43 add the last pieces to make the program function.
44
45 You can find the skeleton code [[here|/code/untyped_evaluator.ml]].
46
47 The first place you need to add code is in the `free_in` function. You already
48 wrote such a function [[in a previous homework|assignment5#occurs_free]], so this
49 part should be easy. The intended behavior is for the function to return results
50 like this:
51
52     # free_in "x" (App (Lambda("x, Var "x"), Var "x"));;
53     - : bool = true
54
55 The second place you need to add code is in the `reduce_head_once` function. As we
56 explain in the code comments, this is similar to the `reduce_if_redex` function in the
57 combinatory logic interpreters. Three of the clauses near the end of this function are incomplete.
58
59 As we explain in the code comments, this interpreter uses an eager/call-by-value reduction
60 strategy. What are its other evaluation order properties? Does it perform beta-reduction
61 underneath lambdas? Does it perform eta-reduction?
62
63
64 ## Evaluation in the untyped lambda calculus: environments
65
66 The previous interpreter strategy is nice because it corresponds so closely to the
67 reduction rules we give when specifying our lambda calculus. (Including
68 specifying evaluation order, which redexes it's allowed to reduce, and
69 so on.) But keeping track of free and bound variables, computing fresh
70 variables when needed, that's all a pain.
71
72 Here's a better strategy. Instead of keeping all of the information
73 about which variables have been bound or are still free implicitly
74 inside of the terms, we'll keep a separate scorecard, which we will call an "environment".  This is a
75 familiar strategy for philosophers of language and for linguists,
76 since it amounts to evaluating terms relative to an assignment
77 function. The difference between the substitute-and-repeat approach
78 above, and this approach, is one huge step towards monads.
79
80 The skeleton code for this is at the [[same link as before|/code/untyped_evaluator.ml]].
81 This part of the exercise is the "VB" part of that code.
82
83 You'll see that in the `eval` function, a new kind of value `Closure (ident) (term) (env)`
84 is used. What's that about?
85
86 [[Read about Closures here.|/topics/week7_environments_and_closures]]
87
88
89 So that's what's going on with those `Closure`s. In the simple code we gave you to work with, we just made these another clause in the `term` datatype. That's really not correct. `Closure`s aren't terms. The syntax for our language doesn't have any constituents that get parsed into `Closure`s. `Closure`s are only created *during the course of evaluating terms*: specifically, when a variable gets bound to an abstract, which may itself contain variables that are locally free (not bound by the abstract itself). So really we should have two datatypes, one for terms, and another for the *results* (sometimes called "values") that terms can evaluate to. `Closure`s are results, but they aren't terms. (In later weeks, we will see more examples of results that aren't terms, but can only be generated during the course of a computation.) `App`s are terms, but not results. If we had primitive numbers or other constants in our language, they might be both terms and results. In the fuller code from which your homework is simplified, this is how the types are in fact defined. But it makes things more complicated. So to keep things simple for the homework, we just pretended like `Closure`s were a new, exotic kind of `term`.
90
91 In any case, now you know what's going on with the `Closure`s, and you should be able to complete the missing pieces of the `eval` function in the code skeleton linked above.
92
93 If you've completed all the missing parts correctly (there are six gaps for the previous stage of the homework, and two gaps for this stage), then you should be able to compile the code skeleton, and use it as described in the comments at the start of the code.
94
95
96 ## Fuller interpreter
97
98 We've also prepared [[a fuller version of the interpreter, that has user-friendly input
99 and printing of results|/topics/week7_untyped_evaluator]]. It
100 will be easiest for you to understand that code if you've
101 completed the gaps in the simplified skeleton linked above.
102
103 There's nothing you need to do with this; it's just for you to play with. If you're interested,
104 you can compare the code you completed for the previous two segments of the homework
105 to the (only moderately more complex) code in the `engine.ml` file of this fuller program.
106
107 ## Monads
108
109 Mappables (functors), MapNables (applicative functors), and Monads
110 (composables) are ways of lifting computations from unboxed types into
111 boxed types.  Here, a "boxed type" is a type function with one unsaturated
112 hole (which may have several occurrences, as in `(α,α) tree`). We can think of the box type
113 as a function from a type to a type.
114
115 Recall that a monad requires a singleton function <code>⇧ (\* mid \*) : P-> <u>P</u></code>, and a
116 composition operator like <code>&gt;=&gt; : (P-><u>Q</u>) -> (Q-><u>R</u>) -> (P-><u>R</u>)</code>.
117
118 As we said in the notes, we'll move freely back and forth between using `>=>` and using `<=<` (aka `mcomp`), which
119 is just `>=>` with its arguments flipped. `<=<` has the virtue that it corresponds more
120 closely to the ordinary mathematical symbol `○`. But `>=>` has the virtue
121 that its types flow more naturally from left to right.
122
123 Anyway, `mid`/`⇧` and (let's say) `<=<` have to obey the Monad Laws:
124
125     ⇧ <=< k == k
126     k <=< ⇧ == k 
127     j <=< (k <=< l) == (j <=< k) <=< l
128
129 For example, the Identity monad has the identity function `I` for `⇧`
130 and ordinary function composition `○` for `<=<`.  It is easy to prove
131 that the laws hold for any terms `j`, `k`, and `l` whose types are
132 suitable for `⇧` and `<=<`:
133
134     ⇧ <=< k == I ○ k == \p. I (k p) ~~> \p. k p ~~> k
135     k <=< ⇧ == k ○ I == \p. k (I p) ~~> \p. k p ~~> k
136
137     (j <=< k) <=< l == (\p. j (k p)) ○ l == \q. (\p. j (k p)) (l q) ~~> \q. j (k (l q))
138     j <=< (k <=< l) == j ○ (k ○ l) == j ○ (\p. k (l p)) == \q. j ((\p. k (l p)) q) ~~> \q. j (k (l q))
139
140 1.  On a number of occasions, we've used the Option/Maybe type to make our
141 conceptual world neat and tidy (for instance, think of [[our discussion
142 of Kaplan's Plexy|topics/week6_plexy]]).  As we learned in class, there is a natural monad
143 for the Option type. Using the vocabulary of OCaml, let's say that
144 `'a option` is the type of a boxed `'a`, whatever type `'a` is.
145 More specifically,
146
147         type 'a option = None | Some 'a
148
149     (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.)
150
151     Now the obvious singleton for the Option monad is `\p. Some p`.  Give
152 (or reconstruct) either of the composition operators `>=>` or `<=<`.
153 Show that your composition operator obeys the Monad Laws.
154
155 2.  Do the same with lists.  That is, given an arbitrary type
156 `'a`, let the boxed type be `['a]` or `'a list`, that is, lists of values of type `'a`.  The `⇧`
157 is the singleton function `\p. [p]`, and the composition operator is:
158
159         let (>=>) (j : 'a -> 'b list) (k : 'b -> 'c list) : 'a -> 'c list =
160           fun a -> List.flatten (List.map k (j a))
161
162     For example:
163
164         let j a = [a; a+1];;
165         let k b = [b*b; b+b];;
166         (j >=> k) 7
167         (* which OCaml evaluates to:
168         - : int list = [49; 14; 64; 16]
169         *)
170
171     Show that these obey the Monad Laws.