X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2Fassignment7.mdwn;h=e9cf82371162e91fb718094a669a096e5809a337;hp=22152fe3cb044c7e4bedebddaedfb5276741c563;hb=9d1d3d7d480c1c808a7a9fddf39f95037196d506;hpb=dbac2255c48ea7f08f9f7f53b2f78d4f17f56a33 diff --git a/exercises/assignment7.mdwn b/exercises/assignment7.mdwn index 22152fe3..e9cf8237 100644 --- a/exercises/assignment7.mdwn +++ b/exercises/assignment7.mdwn @@ -42,8 +42,13 @@ 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]]. + +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 @@ -61,30 +66,27 @@ 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 "V2" part of that code. ## 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 @@ -93,7 +95,7 @@ Anyway, `mid` and (let's say) `<=<` have to obey the following Monad Laws: 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 `>=>`: +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 @@ -101,30 +103,30 @@ suitable for `mid` and `>=>`: (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 `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: + For example: - let j a = [a; a+1];; - let k b = [b*b; b+b];; - (j >=> k) 7 (* ==> [49; 14; 64; 16] *) + let j a = [a; a+1];; + let k b = [b*b; b+b];; + (j >=> k) 7 (* ==> [49; 14; 64; 16] *)