+++ /dev/null
-# Assignment 7
-
-There is no separate assignment 6. (There was a single big assignment for weeks 5 and 6, and
-we're going to keep the assignment numbers in synch with the weeks.)
-
-## Evaluation order in Combinatory Logic
-
-1. Give a term that the lazy evaluators (either [[the Haskell
-evaluator|code/ski_evaluator.hs]], or the lazy version of [[the OCaml
-evaluator|code/ski_evaluator.ml]]) do not evaluate all the way to a
-normal form, that is, that contains a redex somewhere inside of it after
-it has been reduced.
-
-2. One of the [[criteria we established for classifying reduction
-strategies|topics/week3_evaluation_order]] strategies is whether they
-reduce subterms hidden under lambdas. That is, for a term like
-`(\x y. x z) (\x. x)`, do we reduce to `\y.(\x.x) z` and stop, or do
-we reduce further to `\y.z`? Explain what the corresponding question
-would be for CL. Using the eager version of the OCaml CL evaluator (`reduce_try2`),
-prove that the evaluator does reduce terms inside of at least
-some "functional" CL terms. Then provide a modified evaluator
-that does not perform reductions in those positions. (Just give the
-modified version of your recursive reduction function.)
-
-
-## Evaluation in the untyped lambda calculus: substitute-and-repeat
-
-Having sketched the issues with a discussion of Combinatory Logic,
-we're going to begin to construct an evaluator for a simple language
-that includes lambda abstraction. In this problem set, we're going to
-work through the issues twice: once with a function that does
-substitution in the obvious way, and keeps reducing-and-repeating until
-there are no more eligible redexes. 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 almost the complete program, with a few gaps
-in it that you have to complete. You have to understand enough to
-add the last pieces to make the program function.
-
-You can find the skeleton code [[here|/code/untyped_evaluator.ml]].
-
-We've also prepared a much fuller version, that has user-friendly input
-and printing of results. We'll provide a link to that shortly. It
-will be easiest for you to understand that code if you've
-completed the gaps in the simplified skeleton linked above.
-
-
-## Evaluation in the untyped lambda calculus: environments
-
-The previous strategy is nice because it corresponds so closely to the
-reduction rules we give when specifying our lambda calculus. (Including
-specifying evaluation order, which redexes it's allowed to reduce, and
-so on.) But keeping track of free and bound variables, computing fresh
-variables when needed, that's all a pain.
-
-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 a separate scorecard, which we will call an "environment". This is a
-familiar strategy for philosophers of language and for linguists,
-since it amounts to evaluating terms relative to an assignment
-function. The difference between the substitute-and-repeat approach
-above, and this approach, is one huge step towards monads.
-
-The skeleton code for this is at the [[same link as before|/code/untyped_evaluator.ml]].
-This part of the exercise is the "V2" part of that code.
-
-
-## Monads
-
-Mappables (functors), MapNables (applicative 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 unsaturated
-hole (which may have several occurrences, as in `(α,α) tree`). We can think of the box type
-as a function from a type to a type.
-
-Recall that a monad requires a singleton function <code>mid : P-> <u>P</u></code>, and a
-composition operator like <code>>=> : (P-><u>Q</u>) -> (Q-><u>R</u>) -> (P-><u>R</u>)</code>.
-
-As we said in the notes, we'll move freely back and forth between using `>=>` and using `<=<` (aka `mcomp`), which
-is just `>=>` with its arguments flipped. `<=<` has the virtue that it corresponds more
-closely to the ordinary mathematical symbol `○`. But `>=>` has the virtue
-that its types flow more naturally from left to right.
-
-Anyway, `mid` and (let's say) `<=<` have to obey the Monad Laws:
-
- mid <=< k = k
- k <=< mid = k
- j <=< (k <=< l) = (j <=< k) <=< l
-
-For example, the Identity monad has the identity function `I` for `mid`
-and ordinary function composition `○` for `<=<`. It is easy to prove
-that the laws hold for any terms `j`, `k`, and `l` whose types are
-suitable for `mid` and `<=<`:
-
- mid <=< k == I ○ k == \p. I (k p) ~~> \p. k p ~~> k
- k <=< mid == k ○ I == \p. k (I p) ~~> \p. k p ~~> k
-
- (j <=< k) <=< l == (\p. j (k p)) ○ l == \q. (\p. j (k p)) (l q) ~~> \q. j (k (l q))
- j <=< (k <=< l) == j ○ (k ○ l) == j ○ (\p. k (l p)) == \q. j ((\p. k (l p)) q) ~~> \q. j (k (l q))
-
-1. On a number of occasions, we've used the Option/Maybe type to make our
-conceptual world neat and tidy (for instance, think of [[our discussion
-of Kaplan's Plexy|topics/week6_plexy]]). As we learned in class, there is a natural monad
-for the Option type. Using the vocabulary of OCaml, let's say that
-`'a option` is the type of a boxed `'a`, whatever type `'a` is.
-More specifically,
-
- type 'a option = None | Some 'a
-
- (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.)
-
- Now the obvious singleton for the Option monad is `\p. Some p`. Give
-(or reconstruct) either of the composition operators `>=>` or `<=<`.
-Show that your composition operator obeys the Monad Laws.
-
-2. Do the same with lists. That is, given an arbitrary type
-`'a`, let the boxed type be `['a]` or `'a list`, that is, lists of values of type `'a`. The `mid`
-is the singleton function `\p. [p]`, and the composition operator is:
-
- let (>=>) (j : 'a -> 'b list) (k : 'b -> 'c list) : 'a -> 'c list =
- fun a -> List.flatten (List.map k (j a))
-
- For example:
-
- let j a = [a; a+1];;
- let k b = [b*b; b+b];;
- (j >=> k) 7
- (* which OCaml evaluates to:
- - : int list = [49; 14; 64; 16]
- *)
-
- Show that these obey the Monad Laws.