X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2Fassignment7.mdwn;h=f0213aa28ba3f9708a725a2202d87c125b536954;hp=22152fe3cb044c7e4bedebddaedfb5276741c563;hb=c51047cd5851147777c81822d00b1dd6e35988d5;hpb=dbac2255c48ea7f08f9f7f53b2f78d4f17f56a33 diff --git a/exercises/assignment7.mdwn b/exercises/assignment7.mdwn index 22152fe3..f0213aa2 100644 --- a/exercises/assignment7.mdwn +++ b/exercises/assignment7.mdwn @@ -1,8 +1,8 @@ -# 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.) +[[!toc]] + ## Evaluation order in Combinatory Logic 1. Give a term that the lazy evaluators (either [[the Haskell @@ -42,12 +42,28 @@ 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. +You can find the skeleton code [[here|/code/untyped_evaluator.ml]]. + +The first place you need to add code is in the `free_in` function. You already +wrote such a function [[in a previous homework|assignment5#occurs_free]], so this +part should be easy. The intended behavior is for the function to return results +like this: + + # free_in "x" (App (Lambda("x, Var "x"), Var "x"));; + - : bool = true + +The second place you need to add code is in the `reduce_head_once` function. As we +explain in the code comments, this is similar to the `reduce_if_redex` function in the +combinatory logic interpreters. Three of the clauses near the end of this function are incomplete. + +As we explain in the code comments, this interpreter uses an eager/call-by-value reduction +strategy. What are its other evaluation order properties? Does it perform beta-reduction +underneath lambdas? Does it perform eta-reduction? + ## Evaluation in the untyped lambda calculus: environments -The previous strategy is nice because it corresponds so closely to the +The previous interpreter 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 @@ -61,70 +77,95 @@ 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. +The skeleton code for this is at the [[same link as before|/code/untyped_evaluator.ml]]. +This part of the exercise is the "VB" part of that code. + +You'll see that in the `eval` function, a new kind of value `Closure (ident) (term) (env)` +is used. What's that about? + +[[Read about Closures here.|/topics/week7_environments_and_closures]] +So that's what's going on with those `Closure`s. In the simple code we gave you to work with, we just made these another clause in the `term` datatype. That's really not correct. `Closure`s aren't terms. The syntax for our language doesn't have any constituents that get parsed into `Closure`s. `Closure`s are only created *during the course of evaluating terms*: specifically, when a variable gets bound to an abstract, which may itself contain variables that are locally free (not bound by the abstract itself). So really we should have two datatypes, one for terms, and another for the *results* (sometimes called "values") that terms can evaluate to. `Closure`s are results, but they aren't terms. `App`s are terms, but not results. If we had primitive numbers or other constants in our language, they might be both terms and results. In the fuller code from which your homework is simplified, this is how the types are in fact defined. But it makes things more complicated. So to keep things simple for the homework, we just pretended like `Closure`s were a new, exotic kind of `term`. + +In any case, now you know what's going on with the `Closure`s, and you should be able to complete the missing pieces of the `eval` function in the code skeleton linked above. + +If you've completed all the missing parts correctly (there are six gaps for the previous stage of the homework, and two gaps for this stage), then you should be able to compile the code skeleton, and use it as described in the comments at the start of the code. + + +## Fuller interpreter + +We've also prepared a fuller version of the interpreter, 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. + +There's nothing you need to do with this; it's just for you to play with. If you're interested, +you can compare the code you completed for the previous two segments of the homework +to the (only moderately more complex) code in the `engine.ml` file of this fuller program. + ## Monads -Mappables (functors), MapNables (applicatives functors), and 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. +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-> 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` 1. But now we've decided that `mid` -is better. (Think of it as "m" plus "identity", not as the start of "midway".) +Recall that a monad requires a singleton function `â§ (\* mid \*) : P-> P`, and a +composition operator like `>=> : (P->Q) -> (Q->R) -> (P->R)`. -We will also move freely back and forth between using `>=>` and using `<=<` (aka `mcomp`), which +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: +Anyway, `mid`/`â§` and (let's say) `<=<` have to obey the Monad Laws: - mid <=< k = k - k <=< mid = k - j <=< (k <=< l) = (j <=< k) <=< l + â§ <=< k == k + k <=< â§ == k + j <=< (k <=< l) == (j <=< k) <=< l -For example, the Identity monad has the identity function `I` for `mid` +For example, the Identity monad has the identity function `I` for `â§` 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 `>=>`: +suitable for `â§` 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 + â§ <=< k == I â k == \p. I (k p) ~~> \p. k p ~~> k + k <=< â§ == 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 +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. Borrowing the notation of OCaml, let's say that -"`'a option`" is the type of a boxed `'a`, whatever type `'a` is. +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.) + (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 + 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: +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 `â§` +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: + 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] + *) - let j a = [a; a+1];; - let k b = [b*b; b+b];; - (j >=> k) 7 (* ==> [49; 14; 64; 16] *) + Show that these obey the Monad Laws.