exercises/assignment7.mdwn

   1 # Assignment 7
   2
   3 There is no separate assignment 6. (There was a single big assignment for weeks 5 and 6, and
   4 we're going to keep the assignment numbers in synch with the weeks.)
   5
   6 ## Evaluation order in Combinatory Logic
   7
   8 1. Give a term that the lazy evaluators (either [[the Haskell
   9 evaluator|code/ski_evaluator.hs]], or the lazy version of [[the OCaml
  10 evaluator|code/ski_evaluator.ml]]) do not evaluate all the way to a
  11 normal form, that is, that contains a redex somewhere inside of it after
  12 it has been reduced.
  13
  14 2. One of the [[criteria we established for classifying reduction
  15 strategies|topics/week3_evaluation_order]] strategies is whether they
  16 reduce subterms hidden under lambdas.  That is, for a term like
  17 `(\x y. x z) (\x. x)`, do we reduce to `\y.(\x.x) z` and stop, or do
  18 we reduce further to `\y.z`?  Explain what the corresponding question
  19 would be for CL. Using the eager version of the OCaml CL evaluator (`reduce_try2`),
  20 prove that the evaluator does reduce terms inside of at least
  21 some "functional" CL terms.  Then provide a modified evaluator
  22 that does not perform reductions in those positions. (Just give the
  23 modified version of your recursive reduction function.)
  24
  25
  26 ## Evaluation in the untyped lambda calculus: substitute-and-repeat
  27
  28 Having sketched the issues with a discussion of Combinatory Logic,
  29 we're going to begin to construct an evaluator for a simple language
  30 that includes lambda abstraction.  In this problem set, we're going to
  31 work through the issues twice: once with a function that does
  32 substitution in the obvious way, and keeps reducing-and-repeating until
  33 there are no more eligible redexes. You'll see it's somewhat
  34 complicated.  The complications come from the need to worry about
  35 variable capture. (Seeing these complications should give you an
  36 inkling of why we presented the evaluation order discussion using
  37 Combinatory Logic, since we don't need to worry about variables in
  38 CL.)
  39
  40 We're not going to ask you to write the entire program yourself.
  41 Instead, we're going to give you almost the complete program, with a few gaps
  42 in it that you have to complete. You have to understand enough to
  43 add the last pieces to make the program function.
  44
  45 We're still writing up the (substantial) exposition of this, and will post a link
  46 to it here soon.
  47
  48 ## Evaluation in the untyped lambda calculus: environments
  49
  50 The previous strategy is nice because it corresponds so closely to the
  51 reduction rules we give when specifying our lambda calculus. (Including
  52 specifying evaluation order, which redexes it's allowed to reduce, and
  53 so on.) But keeping track of free and bound variables, computing fresh
  54 variables when needed, that's all a pain.
  55
  56 Here's a better strategy. Instead of keeping all of the information
  57 about which variables have been bound or are still free implicitly
  58 inside of the terms, we'll keep a separate scorecard, which we will call an "environment".  This is a
  59 familiar strategy for philosophers of language and for linguists,
  60 since it amounts to evaluating terms relative to an assignment
  61 function. The difference between the substitute-and-repeat approach
  62 above, and this approach, is one huge step towards monads.
  63
  64 We're still writing up the exposition of this, too, and will post a link
  65 to it here soon.
  66
  67
  68 ## Monads
  69
  70 Mappables (functors), MapNables (applicatives functors), and Monads
  71 (composables) are ways of lifting computations from unboxed types into
  72 boxed types.  Here, a "boxed type" is a type function with one unsaturated
  73 hole (which may have several occurrences). We can think of the box type
  74 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.
  75
  76 Recall that a monad requires a singleton function `mid : P-> MP`, and a
  77 composition operator `>=> : (P->MQ) -> (Q->MR) -> (P->MR)`. The type for
  78 the composition operator stated here corrects a typo in the class handout.
  79 Also, in the handout we called `mid` `𝟭`. But now we've decided that `mid`
  80 is better. (Think of it as "m" plus "identity", not as the start of "midway".)
  81
  82 We will also move freely back and forth between using `>=>` and using `<=<` (aka `mcomp`), which
  83 is just `>=>` with its arguments flipped. `<=<` has the virtue that it corresponds more
  84 closely to the ordinary mathematical symbol `○`. But `>=>` has the virtue
  85 that its types flow more naturally from left to right.
  86
  87 Anyway, `mid` and (let's say) `<=<` have to obey the following Monad Laws:
  88
  89     mid <=< k = k
  90     k <=< mid = k
  91     j <=< (k <=< l) = (j <=< k) <=< l
  92
  93 For example, the Identity monad has the identity function `I` for `mid`
  94 and ordinary function composition `○` for `<=<`.  It is easy to prove
  95 that the laws hold for any terms `j`, `k`, and `l` whose types are
  96 suitable for `mid` and `>=>`:
  97
  98     mid <=< k == I ○ k == \p. I (k p) ~~> \p. k p ~~> k
  99     k <=< mid == k ○ I == \p. k (I p) ~~> \p. k p ~~> k
 100
 101     (j <=< k) <=< l == (\p. j (k p)) ○ l == \q. (\p. j (k p)) (l q) ~~> \q. j (k (l q))
 102     j <=< (k <=< l) == j ○ (k ○ l) == j ○ (\p. k (l p)) == \q. j ((\p. k (l p)) q) ~~> \q. j (k (l q))
 103
 104 1.  On a number of occasions, we've used the Option type to make our
 105 conceptual world neat and tidy (for instance, think of [[our discussion
 106 of Kaplan's Plexy|topics/week6_plexy]]).  As we learned in class, there is a natural monad
 107 for the Option type.  Borrowing the notation of OCaml, let's say that
 108 "`'a option`" is the type of a boxed `'a`, whatever type `'a` is.
 109 More specifically,
 110
 111         type 'a option = None | Some 'a
 112
 113 (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.)
 114
 115 Now the obvious singleton for the Option monad is `\p. Some p`.  Give
 116 (or reconstruct) either of the composition operators `>=>` or `<=<`.
 117 Show that your composition operator obeys the Monad Laws.
 118
 119 2.   Do the same with lists.  That is, given an arbitrary type
 120 `'a`, let the boxed type be `['a]` or `'a list`, that is, lists of objects of type `'a`.  The singleton
 121 is `\p. [p]`, and the composition operator is:
 122
 123         let (>=>) (j : 'a -> 'b list) (k : 'b -> 'c list) : 'a -> 'c list =
 124           fun a -> List.flatten (List.map k (j a))
 125
 126 For example:
 127
 128      let j a = [a; a+1];;
 129      let k b = [b*b; b+b];;
 130      (j >=> k) 7 (* ==> [49; 14; 64; 16] *)