X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=exercises%2Fassignment7.mdwn;h=8dfc42d3b33bc7408b7073b4d2fc0919637ab62b;hb=cd5d55412e3ebef73b08b17584fccf36f6f18c44;hp=7ec7a4726fbb60a961e2de459039578b00c033db;hpb=caf7c722676ab5c359ca8ab78f999445453158e6;p=lambda.git diff --git a/exercises/assignment7.mdwn b/exercises/assignment7.mdwn deleted file mode 100644 index 7ec7a472..00000000 --- a/exercises/assignment7.mdwn +++ /dev/null @@ -1,137 +0,0 @@ -# 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 mid : P-> P, 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 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.