whoops

[lambda.git] / exercises / assignment7.mdwn

diff --git a/exercises/assignment7.mdwn b/exercises/assignment7.mdwn
index 3d21629..bd614b3 100644 (file)
--- 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.
 
 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
 
 
 ## Evaluation in the untyped lambda calculus: environments
 


@@ -61,25 +66,22 @@ 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.
 
 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
 
 
 
 ## 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.
 
 Recall that a monad requires a singleton function `mid : P-> MP`, and a
 (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".)
+composition operator like `>=> : (P-><u>Q</u>) -> (Q-><u>R</u>) -> (P-><u>R</u>)`.

 
 

-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.
 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.


@@ -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
 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
 
     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))
 
     (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
 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
+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
 
 "`'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.
 
 (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
+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))
 
 `'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:
+    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] *)