* Practical advice for working with OCaml and/or Haskell (will be posted someday)
* [[Kaplan on Plexy|topics/week6_plexy]] and the Maybe type
* Untyped lambda evaluator ([[in browser|code/lambda_evaluator]]) ([[for home|topics/week7_untyped_evaluator]])
+ * [[Ramble on Monads and Modules|topics/week8_monads_and_modules]]
+ * [[Installing and Using the Juli8 Libraries|/juli8]]
+ * [[Programming with mutable state|/topics/week9_mutable_state]]
* Order, "static versus dynamic"
* [[Reduction Strategies and Normal Forms in the Lambda Calculus|topics/week3_evaluation_order]]
* [[Unit and its usefulness|topics/week3 unit]]
* Combinatory evaluator ([[for home|topics/week7_combinatory_evaluator]])
+ * [[Programming with mutable state|/topics/week9_mutable_state]]
* The Untyped Lambda Calculus
* Monads
* [[Introducing Monads|topics/week7_introducing_monads]]
* [[Safe division with monads|topics/week8_safe_division_with_monads]]
-
+ * [[Reader Monad|/topics/week8_reader_monad]]
+ * [[Ramble on Monads and Modules|topics/week8_monads_and_modules]]
+ * [[Using the OCaml Monad library|/topics/week9_using_the_monad_library]]
+ * [[Programming with mutable state|/topics/week9_mutable_state]]
+ * [[A State Monad Tutorial|/topics/week9_state_monad_tutorial]]
+ * [[Using multiple monads together|/topics/week9_monad_transformers]]
## Topics by week ##
Week 8:
* [[Safe division with monads|topics/week8_safe_division_with_monads]]
+* [[Reader Monad|/topics/week8_reader_monad]]
+* [[Ramble on Monads and Modules|topics/week8_monads_and_modules]]
+
+Week 9:
+
+* [[Installing and Using the Juli8 Libraries|/juli8]]
+* [[Using the OCaml Monad library|/topics/week9_using_the_monad_library]]
+* [[Programming with mutable state|/topics/week9_mutable_state]]
+* [[A State Monad Tutorial|/topics/week9_state_monad_tutorial]]
+* [[Using multiple monads together|/topics/week9_monad_transformers]]
+* [[Homework for weeks 8-9|/exercises/assignment8-9]]
+
+Week 10:
+* Groenendijk, Stokhof, and Veltman, "[[Coreference and Modality|/readings/coreference-and-modality.pdf]]" (1996)
--- /dev/null
+[[!toc]]
+
+## 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.
+
+ ANSWER
+
+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.)
+
+ ANSWER
+
+
+## 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]].
+
+The first place you need to add code is in the `free_in` function. You already
+wrote such a function [[in a previous homework|exercises/assignment5-6#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?
+
+COMPLETED CODE (for this problem and next) IS AVAILABLE [[HERE|/code/untyped_evaluator_complete.ml]].
+
+
+## Evaluation in the untyped lambda calculus: environments
+
+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
+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 "VB" part of that code.
+
+COMPLETED CODE IS AVAILABLE [[HERE|/code/untyped_evaluator_complete.ml]] (same link as above).
+
+
+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. (In later weeks, we will see more examples of results that aren't terms, but can only be generated during the course of a computation.) `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|/topics/week7_untyped_evaluator]]. 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 (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 <code>⇧ (\* mid \*) : P-> <u>P</u></code>, and a
+composition operator like <code>>=> : (P-><u>Q</u>) -> (Q-><u>R</u>) -> (P-><u>R</u>)</code>.
+
+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:
+
+ ⇧ <=< k == k
+ k <=< ⇧ == k
+ j <=< (k <=< l) == (j <=< k) <=< l
+
+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 `⇧` and `<=<`:
+
+ ⇧ <=< 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/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.
+
+ ANSWER
+
+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:
+
+ 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.
+
+ ANSWER
--- /dev/null
+This is the assignment for weeks 8-9, on Reader and State monads.
+
+<!--
+1. When discussing safe division, we worked with operators like `map2 (+)` which just did their ordinary thing, only now lifted up into working on "boxed" or monadic values. Also there was a special division operator, which interacted with the new possibilities presented by the Option/Maybe monad. Instead of this special division operator and the Option monad, show us how to write expressions in the Reader monad with special `getx` operators. That is, instead of representing computations like `(2+3)/0/1`, now you will represent computations like `(2+x)+1`. To keep things simple, suppose that your language only allows three variables `x`, `y`, and `z`, and you can represent the `env` as a triple of `int`s. For this problem you don't need to demonstrate how to implement binding expressions like `let x = 3 in ...`. You just need to compute the value of possibly open expressions, relative to a supplied `env` that gives values for `x` and `y` and `z`.
+
+2. Okay, now what changes do you need to make to add in expressions like `let x = 3 in ...`
+-->
+
+
+1. Jacobson's reader monad only allows for establishing a single binding
+relationship at a time. It requires considerable cleverness to deploy
+her combinators in a way that establishes multiple binding
+relationships, as in
+
+ John_x thinks Mary_y said he_x likes her_y.
+
+ See her 1999 paper for details. Essentially, she ends up layering several
+Reader monads over each other.
+
+ Here is [[code for the arithmetic tree Chris presented in week 8|code/arith1.ml]]. It computes
+`\n. (+ 1 (* (/ 6 n) 4))`. Your task is to modify it to compute
+`\n m. (+ 1 (* (/ 6 n) m))`. You will need to modify five lines.
+The first one is the type of a boxed int. Instead of `type num = int
+-> int`, you'll need
+
+ type num = int -> int -> int
+
+ The second and third are the definitions of `mid` and `map2`. The fourth
+is the one that encodes the variable `n`, the line that begins `(Leaf
+(Num (fun n -> ...`. The fifth line you need to modify is the one
+that replaces "4" with "m". When you have these lines modified,
+you should be able to execute the following expression:
+
+ # match eval t2 with Leaf (Num f) -> f 2 4;;
+ - : int = 13
+
+2. Based on [[the evaluator code from assignment 7|/exercises/assignment7/#index3h2]], and what you've learned about the Reader monad,
+enhance the arithmetic tree code to handle an arbitrary set of free variables. Don't use Juli8 libraries for this; just do it by hand.
+Return to the original code (that is, before the modifications required by the previous problem).
+
+ Start like this:
+
+ type env = string -> int
+ type num = env -> int
+ let my_env = fun var -> match var with "x" -> 2 | "y" -> 4 | _ -> 0;;
+
+ When you have it working, try
+
+ # match eval t2 with Leaf (Num f) -> f my_env;;
+ - : int = 13
+
+ For this problem you don't need to demonstrate how to implement binding expressions like `let x = 3 in ...`. You just need to compute the value of possibly open expressions, relative to the supplied `env`.
+
+3. Okay, now what changes do you need to make to add in expressions like `let x = 3 in ...`
+
+4. Add in the Option/Maybe monad. Start here:
+
+ type num = env -> int option
+
+ Show that your code handles division by zero gracefully.
+
+5. Consider the following code which uses the Juli8 libraries for OCaml.
+
+ module S = Monad.State(struct type store = int end);;
+ let xx = S.(mid 1 >>= fun x -> put 20 >> modify succ >> get >>= fun y -> mid [x;y]) in
+ S.run xx 0
+
+ Recall that `xx >> yy` is short for `xx >>= fun _ -> yy`. The equivalent Haskell code is:
+
+ import Control.Monad.State
+ let { xx :: State Int [Int];
+ xx = return 1 >>= \x -> put 20 >> modify succ >> get >>= \y -> return [x,y] } in
+ runState xx 0
+
+ Or:
+
+ import Control.Monad.State
+ let { xx :: State Int [Int];
+ xx = do { x <- return 1;
+ put 20;
+ modify succ;
+ y <- get;
+ return [x,y] } } in
+ runState xx 0
+
+ Don't try running the code yet. Instead, get yourself into a position to predict what it will do, by reading the past few discussions about the State monad. After you've made a prediction, then run the code and see if you got it right.
+
+6. Here's another one:
+
+ (* start with module S = ... as before *)
+ let yy = S.(let xx = modify succ >> get in
+ xx >>= fun x1 -> xx >>= fun x2 -> xx >>= fun x3 -> mid [x1;x2;x3]) in
+ S.run yy 0
+
+ The equivalent Haskell code is:
+
+ import Control.Monad.State
+ let { xx :: State Int Int;
+ xx = modify succ >> get;
+ yy = xx >>= \x1 -> xx >>= \x2 -> xx >>= \x3 -> return [x1,x2,x3] } in
+ runState yy 0
+
+ What is your prediction? What did OCaml or Haskell actually evaluate this to?
+
+7. Suppose you're trying to use the State monad to keep a running tally of how often certain arithmetic operations have been used in computing a complex expression. You've come upon the design plan of using the same State monad module `S` from the previous problems, and defining a function like this:
+
+ let counting_plus xx yy = S.(tick >> map2 (+) xx yy)
+
+ How should you define the operation `tick` to make this work? The intended behavior is that after running:
+
+ let zz = counting_plus (S.mid 1) (counting_plus (S.mid 2) (S.mid 3)) in
+ S.run zz 0
+
+ you should get a payload of `6` (`1+(2+3)`) and a final `store` of `2` (because `+` was used twice).
+
+8. Instead of the design in the previous problem, suppose you had instead chosen to do things this way:
+
+ let counting_plus xx yy = S.(map2 (+) xx yy >>= tock)
+
+ How should you define the operation `tock` to make this work, with the same behavior as before?
+
+ <!-- How would you expand your strategy, if you also wanted to be safe from division by zero? This is a deep question. How should you combine two monads into a single system? If you don't arrive at working code, you can still discuss the issues and design choices. -->
+
+9. Here is how to create a monadic stack of a Reader monad transformer wrapped around an underlying Option monad:
+
+ module O = Monad.Option (* not really necessary *)
+ module R = Monad.Reader(struct type env = (* whatever *) end)
+ module RO = R.T(O) (* wrap R's Transformer around O *)
+
+ You can inspect the types that result by saying `#show RO.result` (in OCaml version >= 4.02), or by running:
+
+ let env0 = (* some appropriate env, depending on how you defined R *) in
+ let xx = RO.(mid 1) in RO.run xx env0
+
+ and inspecting the type of the result. In Haskell:
+
+ import Control.Monad.Reader
+ -- substitute your own choices for the type Env and value env0
+ let { xx :: ReaderT Env Maybe Int; xx = return 1 } in runReaderT xx env0
+
+ Okay, here are some questions about various monad transformers. Use OCaml or Haskell to help you answer them. Which combined monad has the type of an optional list (that is, either `None` or `Some [...]`): an Option transformer wrapped around an underlying List monad, or a List transformer wrapped around an underlying Option monad? Which combined monad has the type of a function from `store`s to a pair `('a list, store)`: a List transformer wrapped around an underlying State monad or a State transformer wrapped around an underlying List monad?
+
+The last two problems are non-monadic.
+
+10. This is a question about native mutation mechanisms in languages that have them, like OCaml or Scheme. What an expression like this:
+
+ let cell = ref 0 in
+ let incr c = (let old = !cell in let () = cell := old + 1 in ()) in
+ (incr cell, !cell, incr cell, incr cell)
+
+ will evaluate to will be `((), n, (), ())` for some number `n` between `0` and `3`. But what number is sensitive to the details of OCaml's evaluation strategy for evaluating tuple expressions. How can you avoid that dependence? That is, how can you rewrite such code to force it that the values in the 4-tuple have been evaluated left-to-right? Show us a strategy that works no matter what the expressions in the tuple are, not just these particular ones. (But you can assume that the expressions all terminate.)
+
+11. In the evaluator code for [[Week 7 homework|/exercises/assignment7]], we left the `LetRec` portions unimplemented. How might we implement these for the second, `env`-using interpreter? One strategy would be to interpret expressions like:
+
+ letrec f = \x. BODY in
+ TERM
+
+ as though they really read:
+
+ let f = FIX (\f x. BODY) in
+ TERM
+
+ for some fixed-point combinator `FIX`. And that would work, supposing you use some fixed point combinator like the "primed" ones we showed you earlier that work with eager/call-by-value evaluation strategies. But for this problem, we want you to approach the task a different way.
+
+ Begin by deleting all the `module VA = ...` code that implements the substitute-and-repeat interpreter. Next, change the type of `env` to be an `(identifier * bound) list`. Add a line after the definition of that type that says `and bound = Plain of result | Recursive of identifier * identifier * term * env`. The idea here is that some variables will be bound to ordinary `result`s, and others will be bound to special structures we've made to keep track of the recursive definitions. These special structures are akin to the `Closure of identifier * term * env` we already added to the `term` (or really more properly `result`) datatype. For `Closure`s, the single `identifier` is the bound variable, the `term` is the body of the lambda abstract, and the `env` is the environment that is in place when some variable is bound to this lambda abstract. Those same parameters make up the last three arguments of our `Recursive` structure. The first argument in the `Recursive` structure is to hold the variable that our `letrec` construction binds to the lambda abstract. That is, in:
+
+ letrec f = \x. BODY in
+ TERM
+
+ both of the variables `f` and `x` need to be interpreted specially when we evaluate `BODY`, and this is how we keep track of which variable is `f`.
+
+ Just making those changes will require you to change some other parts of the interpreter to make it still work. Before trying to do anything further with `letrec`, try finding what parts of the code need to be changed to accommodate these modifications to our types. See if you can get the interpreter working again as well as it was before.
+
+ OK, once you've done that, then add an extra line:
+
+ | LetRec of identifier * term * term
+
+ to the definition of the `term` datatype. (For `letrec IDENT1 = TERM1 in TERM2`. You can assume that `TERM1` is always a `Lambda` term.) Now what will you need to add to the `eval` function to get it to interpret these terms properly? This will take some thought, and a good understanding of how the other clauses in the `eval` function are working.
+
+ Here's a conceptual question: why did we point you in the direction of complicating the type that environments associate variables with, rather than just adding a new clause to the `result` type, as we did with Closures?
> Small bug fix to Juli8 on Mon 6 April.
-> Topics: [[Using the OCaml Monad library|/topics/week9_using_the_monad_library]]; [[Programming with mutable state|/topics/week9_mutable_state]]; [[A State Monad Tutorial|/topics/week9_state_monad_tutorial]]; Using multiple monads together; [[Homework for weeks 8-9|/exercises/assignment8-9]]
+> Topics: [[Using the OCaml Monad library|/topics/week9_using_the_monad_library]]; [[Programming with mutable state|/topics/week9_mutable_state]]; [[A State Monad Tutorial|/topics/week9_state_monad_tutorial]]; [[Using multiple monads together|/topics/week9_monad_transformers]]; [[Homework for weeks 8-9|/exercises/assignment8-9]]
> Reading for Week 10: Groenendijk, Stokhof, and Veltman, "[[Coreference and Modality|/readings/coreference-and-modality.pdf]]" (1996)
- : int LO.result = None
On the other hand, when Option is on the inside, as in LO, failures (which we represent by `mzero`s from the Option monad, here `hoist Monad.Option.mzero`, not the List monad's own `mzero`) abort the whole computation.
+
+This is fun. Notice the difference it makes whether the second `++` is native to the outer `Monad.List`, or whether it's the inner `Monad.List`'s `++` hoisted into the outer wrapper:
+
+ # module LL = Monad.List.T(Monad.List);;
+
+ # LL.(run((++) (mid 1) (mid 2) >>= fun i -> (++) (mid i) (mid (10*i)) ));;
+ - : int LL.result = \[[1; 10; 2; 20]]
+ # LL.(run((++) (mid 1) (mid 2) >>= fun i -> hoist L.((++) (mid i) (mid (10*i)) )));;
+ - : int LL.result = [[1; 2]; [1; 20]; [10; 2]; [10; 20]]
-->
<!--
Exception: Failure "bye".
-->
-This is fun. Notice the difference it makes whether the second `++` is native to the outer `Monad.List`, or whether it's the inner `Monad.List`'s `++` hoisted into the outer wrapper:
-
- # module LL = Monad.List.T(Monad.List);;
-
- # LL.(run((++) (mid 1) (mid 2) >>= fun i -> (++) (mid i) (mid (10*i)) ));;
- - : int LL.result = \[[1; 10; 2; 20]]
- # LL.(run((++) (mid 1) (mid 2) >>= fun i -> hoist L.((++) (mid i) (mid (10*i)) )));;
- - : int LL.result = [[1; 2]; [1; 20]; [10; 2]; [10; 20]]
-
Further Reading