X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week9.mdwn;h=2b80483989efca1fd91845b1a022eee173b2ee36;hp=145833d54ffe6ba2d3c369ab1975fbfc4a7cce3c;hb=40b5ff7bf5c1f0fe0843ca938af8ced1ec5c9976;hpb=b9707741b7a76175e4870be85a7b7147f237c584 diff --git a/week9.mdwn b/week9.mdwn index 145833d5..2b804839 100644 --- a/week9.mdwn +++ b/week9.mdwn @@ -100,7 +100,9 @@ Scheme is similar. There are various sorts of reference cells available in Schem (set-box! ycell 3) (+ x (unbox ycell))) -When dealing with explicit-style mutation, there's a difference between the types and values of `ycell` and `!ycell` (or `(unbox ycell)`). The former has the type `int ref`: the variable `ycell` is assigned a reference cell that contains an `int`. The latter has the type `int`, and has whatever value is now stored in the relevant reference cell. In an implicit-style framework though, we only have the resources to refer to the contents of the relevant reference cell. `y` in fragment [G] or the C snippet above has the type `int`, and only ever evaluates to `int` values. +(C has explicit-style mutable variables, too, which it calls *pointers*. But simple variables in C are already mutable, in the implicit style.) + +When dealing with explicit-style mutation, there's a difference between the types and values of `ycell` and `!ycell` (or in Scheme, `(unbox ycell)`). The former has the type `int ref`: the variable `ycell` is assigned a reference cell that contains an `int`. The latter has the type `int`, and has whatever value is now stored in the relevant reference cell. In an implicit-style framework though, we only have the resources to refer to the contents of the relevant reference cell. `y` in fragment [G] or the C snippet above has the type `int`, and only ever evaluates to `int` values. ##Controlling order## @@ -236,6 +238,14 @@ The core idea to referential transparency is that when the same value is supplie Notice that the two invocations of `f 1` yield different results, even though the same value is being supplied as an argument to the same function. +Similarly, functions like these: + + let f cell = !cell;; + + let g cell = cell := !cell + 1; !cell;; + +may return different results each time they're invoked, even if they're always supplied one and the same reference cell as argument. + Computer scientists also associate referential transparency with a kind of substitution principle, illustrated here: let x = 1 @@ -281,7 +291,34 @@ Now we're going to relativize our interpretations not only to the assignment fun > \[[expression]]g s = (value, s') -With that kind of framework, we can interpret `newref`, `deref`, and `setref` as follows. +For expressions we already know how to interpret, expect `s'` to just be `s`. +An exception is complex expressions like `let var = expr1 in expr2`. Part of +interpreting this will be to interpret the sub-expression `expr1`, and we have +to allow that in doing that, the store may have already been updated. We want +to use that possibly updated store when interpreting `expr2`. Like this: + + let rec eval expression g s = + match expression with + ... + | Let (c, expr1, expr2) -> + let (value, s') = eval expr1 g s + (* s' may be different from s *) + (* now we evaluate expr2 in a new environment where c has been associated + with the result of evaluating expr1 in the current environment *) + eval expr2 ((c, value) :: g) s' + ... + +Similarly: + + ... + | Addition (expr1, expr2) -> + let (value1, s') = eval expr1 g s + in let (value2, s'') = eval expr2 g s' + in (value1 + value2, s'') + ... + +Let's consider how to interpet our new syntactic forms `newref`, `deref`, and `setref`: + 1. \[[newref starting_val]] should allocate a new reference cell in the store and insert `starting_val` into that cell. It should return some "key" or "index" or "pointer" to the newly created reference cell, so that we can do things like: @@ -297,7 +334,7 @@ With that kind of framework, we can interpret `newref`, `deref`, and `setref` as let rec eval expression g s = match expression with ... - | Newref expr -> + | Newref (expr) -> let (starting_val, s') = eval expr g s (* note that s' may be different from s, if expr itself contained any mutation operations *) (* now we want to retrieve the next free index in s' *) @@ -308,12 +345,12 @@ With that kind of framework, we can interpret `newref`, `deref`, and `setref` as in (Index new_index, s'') ... -2. When `expr` evaluates to a `store_index`, then `deref expr` should evaluate to whatever value is at that index in the current store. (If `expr` evaluates to a value of another type, `deref expr` is undefined.) In this operation, we don't change the store at all; we're just reading from it. So we'll return the same store back unchanged. +2. When `expr` evaluates to a `store_index`, then `deref expr` should evaluate to whatever value is at that index in the current store. (If `expr` evaluates to a value of another type, `deref expr` is undefined.) In this operation, we don't change the store at all; we're just reading from it. So we'll return the same store back unchanged (assuming it wasn't changed during the evaluation of `expr`). let rec eval expression g s = match expression with ... - | Deref expr -> + | Deref (expr) -> let (Index n, s') = eval expr g s (* note that s' may be different from s, if expr itself contained any mutation operations *) in (List.nth s' n, s') @@ -324,9 +361,9 @@ With that kind of framework, we can interpret `newref`, `deref`, and `setref` as let rec eval expression g s = match expression with ... - | Setref expr1 expr2 + | Setref (expr1, expr2) -> let (Index n, s') = eval expr1 g s - (* note that s' may be different from s, if expr itself contained any mutation operations *) + (* note that s' may be different from s, if expr1 itself contained any mutation operations *) in let (new_value, s'') = eval expr2 g s' (* now we create a list which is just like s'' except it has new_value in index n *) in let rec replace_nth lst m = @@ -339,6 +376,9 @@ With that kind of framework, we can interpret `newref`, `deref`, and `setref` as ... + + + ##How to implement implicit-style mutable variables## With implicit-style mutation, we don't have new syntactic forms like `newref` and `deref`. Instead, we just treat ordinary variables as being mutable. You could if you wanted to have some variables be mutable and others not; perhaps the first sort are written in Greek and the second in Latin. But we will suppose all variables in our language are mutable. @@ -349,7 +389,7 @@ This brings up an interesting conceptual distinction. Formerly, we'd naturally t To handle implicit-style mutation, we'll need to re-implement the way we interpret expressions like `x` and `let x = expr1 in expr2`. We will also have just one new syntactic form, `change x to expr1 then expr2`. -Here's how to implement these. We'll suppose that our assignment function is list of pairs, as in [week6](/reader_monad_for_variable_binding). +Here's how to implement these. We'll suppose that our assignment function is list of pairs, as in [week7](/reader_monad_for_variable_binding). let rec eval expression g s = match expression with @@ -360,7 +400,7 @@ Here's how to implement these. We'll suppose that our assignment function is lis in let value = List.nth s index in (value, s) - | Let (c : char) expr1 expr2 -> + | Let ((c : char), expr1, expr2) -> let (starting_val, s') = eval expr1 g s (* get next free index in s' *) in let new_index = List.length s' @@ -369,7 +409,7 @@ Here's how to implement these. We'll suppose that our assignment function is lis (* evaluate expr2 using a new assignment function and store *) in eval expr2 ((c, new_index) :: g) s'' - | Change (c : char) expr1 expr2 -> + | Change ((c : char), expr1, expr2) -> let (new_value, s') = eval expr1 g s (* lookup which index is associated with Var c *) in let index = List.assoc c g @@ -515,6 +555,9 @@ To get the whole process started, the complex computation so defined will need t Notice: h, p have same value (1), but f (h, p) and f (h, h) differ +Fine and Pryor on "coordinated contents" (see, e.g., [Hyper-Evaluativity](http://www.jimpryor.net/research/papers/Hyper-Evaluativity.txt)) + + ##Five grades of mutation involvement## -- FIXME -- @@ -578,7 +621,29 @@ To get the whole process started, the complex computation so defined will need t We use the `None`/`Some factorial` option type here just as a way to ensure that the contents of `fact_cell` are of the same type both at the start and the end of the block. +##Offsite Reading## + +* [[!wikipedia Declarative programming]] +* [[!wikipedia Functional programming]] +* [[!wikipedia Purely functional]] +* [[!wikipedia Side effect (computer science) desc="Side effects"]] +* [[!wikipedia Referential transparency (computer science)]] +* [[!wikipedia Imperative programming]] +* [[!wikipedia Reference (computer science) desc="References"]] +* [[!wikipedia Pointer (computing) desc="Pointers"]] +* [Pointers in OCaml](http://caml.inria.fr/resources/doc/guides/pointers.html) +