# 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 (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). 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 like `>=> : (P->__Q__) -> (Q->__R__) -> (P->__R__)`.
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 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/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 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] *)