029a7798c182c8c0125848c9f6e70089a4baec77
1 # Assignment 7
3 There is no separate assignment 6. (There was a single big assignment for weeks 5 and 6, and
4 we're going to keep the assignment numbers in synch with the weeks.)
6 ## Evaluation order in Combinatory Logic
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.
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.)
26 ## Evaluation in the untyped lambda calculus: substitute-and-repeat
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.)
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.
45 You can find the skeleton code [[here|/code/untyped_evaluator.ml]].
47 We've also prepared a much fuller version, that has user-friendly input
48 and printing of results. We'll provide a link to that shortly. It
49 will be easiest for you to understand that code if you've
50 completed the gaps in the simplified skeleton linked above.
53 ## Evaluation in the untyped lambda calculus: environments
55 The previous strategy is nice because it corresponds so closely to the
56 reduction rules we give when specifying our lambda calculus. (Including
57 specifying evaluation order, which redexes it's allowed to reduce, and
58 so on.) But keeping track of free and bound variables, computing fresh
59 variables when needed, that's all a pain.
61 Here's a better strategy. Instead of keeping all of the information
62 about which variables have been bound or are still free implicitly
63 inside of the terms, we'll keep a separate scorecard, which we will call an "environment".  This is a
64 familiar strategy for philosophers of language and for linguists,
65 since it amounts to evaluating terms relative to an assignment
66 function. The difference between the substitute-and-repeat approach
67 above, and this approach, is one huge step towards monads.
69 The skeleton code for this is at the [[same link as before|/code/untyped_evaluator.ml]].
70 This part of the exercise is the "V2" part of that code.
75 Mappables (functors), MapNables (applicative functors), and Monads
76 (composables) are ways of lifting computations from unboxed types into
77 boxed types.  Here, a "boxed type" is a type function with one unsaturated
78 hole (which may have several occurrences, as in `(α,α) tree`). We can think of the box type
79 as a function from a type to a type.
81 Recall that a monad requires a singleton function <code>⇧ (\* mid \*) : P-> <u>P</u></code>, and a
82 composition operator like <code>&gt;=&gt; : (P-><u>Q</u>) -> (Q-><u>R</u>) -> (P-><u>R</u>)</code>.
84 As we said in the notes, we'll move freely back and forth between using `>=>` and using `<=<` (aka `mcomp`), which
85 is just `>=>` with its arguments flipped. `<=<` has the virtue that it corresponds more
86 closely to the ordinary mathematical symbol `○`. But `>=>` has the virtue
87 that its types flow more naturally from left to right.
89 Anyway, `mid`/`⇧` and (let's say) `<=<` have to obey the Monad Laws:
91     ⇧ <=< k == k
92     k <=< ⇧ == k
93     j <=< (k <=< l) == (j <=< k) <=< l
95 For example, the Identity monad has the identity function `I` for `⇧`
96 and ordinary function composition `○` for `<=<`.  It is easy to prove
97 that the laws hold for any terms `j`, `k`, and `l` whose types are
98 suitable for `⇧` and `<=<`:
100     ⇧ <=< k == I ○ k == \p. I (k p) ~~> \p. k p ~~> k
101     k <=< ⇧ == k ○ I == \p. k (I p) ~~> \p. k p ~~> k
103     (j <=< k) <=< l == (\p. j (k p)) ○ l == \q. (\p. j (k p)) (l q) ~~> \q. j (k (l q))
104     j <=< (k <=< l) == j ○ (k ○ l) == j ○ (\p. k (l p)) == \q. j ((\p. k (l p)) q) ~~> \q. j (k (l q))
106 1.  On a number of occasions, we've used the Option/Maybe type to make our
107 conceptual world neat and tidy (for instance, think of [[our discussion
108 of Kaplan's Plexy|topics/week6_plexy]]).  As we learned in class, there is a natural monad
109 for the Option type. Using the vocabulary of OCaml, let's say that
110 `'a option` is the type of a boxed `'a`, whatever type `'a` is.
111 More specifically,
113         type 'a option = None | Some 'a
115     (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.)
117     Now the obvious singleton for the Option monad is `\p. Some p`.  Give
118 (or reconstruct) either of the composition operators `>=>` or `<=<`.
119 Show that your composition operator obeys the Monad Laws.
121 2.  Do the same with lists.  That is, given an arbitrary type
122 `'a`, let the boxed type be `['a]` or `'a list`, that is, lists of values of type `'a`.  The `⇧`
123 is the singleton function `\p. [p]`, and the composition operator is:
125         let (>=>) (j : 'a -> 'b list) (k : 'b -> 'c list) : 'a -> 'c list =
126           fun a -> List.flatten (List.map k (j a))
128     For example:
130         let j a = [a; a+1];;
131         let k b = [b*b; b+b];;
132         (j >=> k) 7
133         (* which OCaml evaluates to:
134         - : int list = [49; 14; 64; 16]
135         *)
137     Show that these obey the Monad Laws.