From 1cb2ced803dc9958388bc7a868489d768afe5021 Mon Sep 17 00:00:00 2001
From: Jim Pryor
Date: Thu, 25 Nov 2010 11:22:28 -0500
Subject: [PATCH] calculator improvements
Signed-off-by: Jim Pryor
---
advanced_topics.mdwn | 1 +
advanced_topics/calculator_improvements.mdwn | 292 +++++++++++++++++++++++++++
2 files changed, 293 insertions(+)
create mode 100644 advanced_topics/calculator_improvements.mdwn
diff --git a/advanced_topics.mdwn b/advanced_topics.mdwn
index 3f82880b..6fff3e51 100644
--- a/advanced_topics.mdwn
+++ b/advanced_topics.mdwn
@@ -1,2 +1,3 @@
##[[Version 4 lists]]##
##[[Monads in Category Theory]]##
+##[[Calculator Improvements]]##
diff --git a/advanced_topics/calculator_improvements.mdwn b/advanced_topics/calculator_improvements.mdwn
new file mode 100644
index 00000000..013b9a61
--- /dev/null
+++ b/advanced_topics/calculator_improvements.mdwn
@@ -0,0 +1,292 @@
+[[!toc]]
+
+We're going to make gradual improvements to the calculator we developed in [week7](/reader_monad_for_variable_binding).
+
+##Original Calculator##
+
+In a real programming application, one would usually start with a string that needs to be parsed and interpreted, such as:
+
+ let x = 1 in let y = x + 2 in x * y
+
+The parsing phase converts this to an "abstract syntax tree" (AST), which in this case might be:
+
+ Let ('x', Constant 1,
+ Let ('y', Addition (Variable 'x', Constant 2),
+ Multiplication (Variable 'x', Variable 'y')))
+
+Then the interpreter (or "evaluator") would convert that AST into an "expressed value": in this case, to the integer 3. We're not concerning ourselves with the parsing phase here, so we're just thinking about how to interpret expressions that are already in AST form.
+
+The language we had in week 7 looked like this:
+
+ type term = Constant of int
+ | Multiplication of (term * term)
+ | Addition of (term * term)
+ | Variable of char
+ | Let of (char * term * term);;
+
+and the evaluation function looked like this:
+
+ let rec eval (t : term) (e: (char * int) list) = match t with
+ Constant x -> x
+ | Multiplication (t1,t2) -> (eval t1 e) * (eval t2 e)
+ | Addition (t1,t2) -> (eval t1 e) + (eval t2 e)
+ | Variable c ->
+ (* lookup the value of c in the current environment
+ This will fail if c isn't assigned anything by e *)
+ List.assoc c e
+ | Let (c,t1,t2) ->
+ (* evaluate t2 in a new environment where c has been associated
+ with the result of evaluating t1 in the current environment *)
+ eval t2 ((c, eval t1 e) :: e);;
+
+
+##Adding Booleans##
+
+Let's tweak this a bit.
+
+First, let's abstract away from the assumption that our terms always evaluate to `int`s. Let's suppose they evaluate to a more general type, which might have an `int` payload, or might have, for example, a `bool` payload.
+
+ type expressed_value = Int of int | Bool of bool;;
+
+We'll add one boolean predicate, `Iszero`, and an `If...` construction.
+
+We won't try here to catch any type errors, such as attempts to add a `bool` to an `int`, or attempts to check whether a `bool` iszero. Neither will we try here to monadize anything: these will be implementations of a calculator with all the plumbing exposed. What we will do is add more and more features to the calculator.
+
+We'll switch over to using variable `g` for assignment functions, which is a convention many of you seem familiar with. As we mentioned a few times in week 9, for some purposes it's easier to implement environment or assignment functions as functions from `char`s to `int`s (or whatever variables are bound to), rather than as lists as pairs. However, we'll stick with this implementation for now. We will however abstract out the type that the variables are bound to. For now, we'll suppose that they're bound to the same types that terms can express.
+
+ type bound_value = expressed_value;;
+ type assignment = (char * bound_value) list;;
+
+Here's where we should be now:
+
+ type term = Constant of int
+ | Multiplication of (term * term)
+ | Addition of (term * term)
+ | Variable of char
+ | Let of (char * term * term)
+ | Iszero of term
+ | If of (term * term * term);;
+
+ let rec eval (t : term) (g: assignment) = match t with
+ Constant x -> Int x
+ | Multiplication (t1, t2) ->
+ (* we don't handle cases where the subterms don't evaluate to Ints *)
+ let Int value1 = eval t1 g
+ in let Int value2 = eval t2 g
+ (* Multiplication (t1, t2) should evaluate to an Int *)
+ in Int (value1 * value2)
+ | Addition (t1, t2) ->
+ let Int value1 = eval t1 g
+ in let Int value2 = eval t2 g
+ in Int (value1 + value2)
+ | Variable c ->
+ (* we don't handle cases where g doesn't bind c to any value *)
+ List.assoc c g
+ | Let (c, t1, t2) ->
+ (* evaluate t2 under a new assignment where c has been bound to
+ the result of evaluating t1 under the current assignment *)
+ let value1 = eval t1 g
+ in let g' = (c, value1) :: g
+ in eval t2 g'
+ | Iszero t1 ->
+ (* we don't handle cases where t1 doesn't evaluate to an Int *)
+ let Int value1 = eval t1 g
+ (* Iszero t1 should evaluate to a Bool *)
+ in Bool (value1 = 0)
+ | If (t1, t2, t3) ->
+ (* we don't handle cases where t1 doesn't evaluate to a boolean *)
+ let Bool value1 = eval t1 g
+ in if value1 then eval t2 g
+ else eval t3 g;;
+
+
+##Adding Function Values##
+
+Now we want to add function values to our language, so that we can interpret (the abstract syntax trees of) expressions like this:
+
+ let x = 1 in let f = lambda y -> y + x in apply f 2
+
+What changes do we need to handle this?
+
+We can begin with our language:
+
+ type term = Constant of int
+ | Multiplication of (term * term)
+ | Addition of (term * term)
+ | Variable of char
+ | Let of (char * term * term)
+ | Iszero of term
+ | If of (term * term * term)
+ | Lambda of (char * term)
+ | Apply of (term * term);;
+
+Next, we need to expand our stock of `expressed_value`s to include function values as well. How should we think of these? We've several times mentioned the issue of how to handle free variables in a function's body, like the `x` in `lambda y -> y + x`. We'll follow the usual functional programming standard for these (known as "lexical scoping"), which keeps track of what value `x` has in the function expression's lexical environment. That shouldn't get shadowed by any different value `x` may have when the function value is later applied. So:
+
+ let x = 1 in let f = lambda y -> y + x in let x = 2 in apply f 2
+
+should evaluate to `3` not to `4`. To handle this, the function values we construct need to keep track of the present values of all free variables in the function's body. The combination of the function's body and the values of its free variables is called a "function closure." We'll implement these closures in a straightforward though inefficient way: we'll just stash away a copy of the assignment in effect when the function value is being constructed. Our function values also need to keep track of which of their variables are to be bound to the arguments they get applied to. All together, then, we need three pieces of information: which variables are to be bound to arguments, what the function's body is, and something that keeps track of the right values for the free variables in the function body. We'll pack this all together into an additional variant for our `expressed_value` type:
+
+ type expressed_value = Int of int | Bool of bool | Closure of char * term * assignment;;
+
+We'd like to define `bound_value`s and `assignment`s just as before:
+
+ type bound_value = expressed_value;;
+ type assignment = (char * bound_value) list;;
+
+However, note that we have a recursive relation between these types: `expressed_value` is defined partly in terms of `assignment`, which is defined partly in terms of `bound_value`, which is equivalent to `expressed_value`. In OCaml one has to define such types using the following form:
+
+ type expressed_value = Int of int | Bool of bool | Closure of char * term * assignment
+ and bound_value = expressed_value
+ and assignment = (char * bound_value) list;;
+
+Now our evaluation function needs two further clauses to interpret the two new expression forms `Lambda(...)` and `Apply(...)`:
+
+ let rec eval (t : term) (g: assignment) = match t with
+ ...
+ | Lambda(c, t1) -> Closure (c, t1, g)
+ | Apply(t1, t2) ->
+ let value2 = eval t2 g
+ (* we don't handle cases where t1 doesn't evaluate to a function value *)
+ in let Closure (arg_var, body, savedg) = eval t1 g
+ (* evaluate body under savedg, except with arg_var bound to value2 *)
+ in let savedg' = (arg_var, value2) :: savedg
+ in eval body savedg';;
+
+
+##Adding Recursive Functions##
+
+There are different ways to include recursion in our calculator. First, let's imagine our language expanded like this:
+
+ let x = 1 in letrec f = lambda y -> if iszero y then x else y * f (y - 1) in f 3
+
+where the AST would be:
+
+ Let('x', Constant 1,
+ Letrec ('f',
+ Lambda ('y',
+ If (Iszero (Variable 'y'),
+ Variable 'x',
+ Multiplication (Variable 'y',
+ Apply (Variable 'f',
+ Addition (Variable 'y', Constant (-1)))))),
+ Apply (Variable 'f', Constant 3)))
+
+Here is the expanded definition for our language type:
+
+ type term = Constant of int
+ | Multiplication of (term * term)
+ | Addition of (term * term)
+ | Variable of char
+ | Let of (char * term * term)
+ | Iszero of term
+ | If of (term * term * term)
+ | Lambda of (char * term)
+ | Apply of (term * term)
+ | Letrec of (char * term * term);;
+
+Now consider what we'll need to do when evaluating a term like `Letrec ('f', Lambda (...), t2)`. The subterm `Lambda (...)` will evaluate to something of the form `Closure ('y', body, savedg)`, where `f` may occur free in `body`. What we'll want to do is to ensure that when `body` is applied, it's applied using not the assignment `savedg` but a modified assignment `savedg'` which binds `f` to this very function value. That is, we want to bind `f` not to:
+
+ Closure ('y', body, savedg)
+
+but instead to:
+
+ let orig_closure = Closure ('y', body, savedg)
+ in let savedg' = ('f', orig_closure) :: savedg
+ in let new_closure = Closure ('y', body, savedg')
+ in new_closure
+
+Except, this isn't quite right. It's almost what we want, but not exactly. Can you see the flaw?
+
+The flaw is this: inside `new_closure`, what is `f` bound to? It's bound by `savedg'` to `orig_closure`, which in turn leaves `f` free (or bound to whatever existing value it had according to `savedg`). This isn't what we want. It'll break if we need to make recursive calls to `f` which go more than two levels deep.
+
+What we really want is for `f` to be bound to `new_closure`, something like this:
+
+ let rec new_closure = Closure ('y', body, ('f', new_closure) :: savedg)
+ in new_closure
+
+And as a matter of fact, OCaml *does* permit us to recursively define cyclical lists in this way. So a minimal change to our evaluation function would suffice:
+
+ let rec eval (t : term) (g: assignment) = match t with
+ ...
+ | Letrec (c, t1, t2) ->
+ (* we don't handle cases where t1 doesn't evaluate to a function value *)
+ let Closure (arg_var, body, savedg) = eval t1 g
+ in let rec new_closure = Closure (arg_var, body, (c, new_closure) :: savedg)
+ in let g' = (c, new_closure) :: g
+ in eval t2 g';;
+
+However, this is a somewhat exotic ability in a programming language, so it would be good to work out how to interpret `Letrec(...)` forms without relying on it.
+
+If we implemented assignments as functions rather than as lists of pairs, the corresponding move would be less exotic. In that case, our `Let(...)` and `Letrec(...)` clauses would look something like this:
+
+
+ | Let (c, t1, t2) ->
+ let value1 = eval t1 g
+ in let g' = fun var -> if var = c then value1 else g var
+ in eval t2 g'
+ ...
+ | Letrec (c, t1, t2) ->
+ let Closure (arg_var, body, savedg) = eval t1 g
+ in let rec savedg' = fun var -> if var = c then Closure (arg_var, body, savedg') else savedg var
+ in let g' = fun var -> if var = c then Closure (arg_var, body, savedg') else g var
+ in eval t2 g';;
+
+and this is just a run-of-the-mill use of recursive functions. However, for this exercise we'll continue using lists of pairs, and work out how to interpret `Letrec(...)` forms using them.
+
+The way we'll do this is that, when we bind a value to a variable, we'll keep track of whether the term was bound via `let` or `letrec`. We'll rely on that to interpret pairs of terms like these differently:
+
+ Let ('f',
+ Constant 1,
+ Let ('f', Lambda ('y', Variable 'f')),
+ ...)
+
+ Let ('f',
+ Constant 1,
+ Letrec ('f', Lambda ('y', Variable 'f')),
+ ...)
+
+In the first case, an application of `f` to any argument should evaluate to `Int 1`; in the second case, it should evaluate to the same function closure that `f` evaluates to. We'll keep track of which way a variable was bound by expanding our `bound_value` type:
+
+ type expressed_value = Int of int | Bool of bool | Closure of char * term * assignment
+ and bound_value = Nonrecursive of expressed_value |
+ Recursive_Closure of char * char * term * assignment
+ and assignment = (char * bound_value) list;;
+
+
+Since we're not permitting ourselves OCaml's ability to recursively define cyclical lists, we're not going to be able to update the saved assignment in a closure when that closure is recursively bound to a variable. Instead, we'll just make a note of what variable `f` is supposed to be the recursively bound one---by binding it not to `Nonrecursive (Closure (arg_var, body, savedg))` but rather to `Recursive_Closure ('f', arg_var, body, savedg)`. We'll do the work to make the saved assignment recursive in the right way *later*, when we *evaluate* `f`. The result will look like this:
+
+ let rec eval (t : term) (g: assignment) = match t with
+ ...
+ | Variable c -> (
+ (* we don't handle cases where g doesn't bind c to any value *)
+ match List.assoc c g with
+ | Nonrecursive value -> value
+ | Recursive_Closure (self_var, arg_var, body, savedg) as rec_closure ->
+ (* we update savedg to bind self_var to rec_closure here *)
+ let savedg' = (self_var, rec_closure) :: savedg
+ in Closure (arg_var, body, savedg')
+ )
+ | Let (c, t1, t2) ->
+ (* evaluate t2 under a new assignment where c has been bound to
+ the result of evaluating t1 under the current assignment *)
+ let value1 = eval t1 g
+ (* we have to wrap value1 in Nonrecursive *)
+ in let g' = (c, Nonrecursive value1) :: g
+ in eval t2 g'
+ ...
+ | Lambda(c, t1) -> Closure (c, t1, g)
+ | Apply(t1, t2) ->
+ let value2 = eval t2 g
+ (* we don't handle cases where t1 doesn't evaluate to a function value *)
+ in let Closure (arg_var, body, savedg) = eval t1 g
+ (* evaluate body under savedg, except with arg_var bound to Nonrecursive value2 *)
+ in let savedg' = (arg_var, Nonrecursive value2) :: savedg
+ in eval body savedg'
+ | Letrec (c, t1, t2) ->
+ (* we don't handle cases where t1 doesn't evaluate to a function value *)
+ let Closure (arg_var, body, savedg) = eval t1 g
+ (* evaluate t2 under a new assignment where c has been recursively bound to that function value *)
+ in let g' = (c, Recursive_Closure(c, arg_var, body, savedg)) :: g
+ in eval t2 g';;
+
+
--
2.11.0