+++ /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.
-
-We're still writing up the (substantial) exposition of this, and will post a link
-to it here soon.
-
-## 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.
-
-We're still writing up the exposition of this, too, and will post a link
-to it here soon.
-
-
-## Monads
-
-Mappables (functors), MapNables (applicatives 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). We can think of the box type
-as a function from a type to a type. Call this type function M, and let P, Q, R, and S be schematic variables over types.
-
-Recall that a monad requires a singleton function `mid : P-> MP`, and a
-composition operator `>=> : (P->MQ) -> (Q->MR) -> (P->MR)`. The type for
-the composition operator stated here corrects a typo in the class handout.
-Also, in the handout we called `mid` `𝟭`. But now we've decided that `mid`
-is better. (Think of it as "m" plus "identity", not as the start of "midway".)
-
-We will also 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 following 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 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. Borrowing the notation 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. Just 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 objects of type `'a`. The singleton
-is `\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 (* ==> [49; 14; 64; 16] *)