week9
[lambda.git] / week9.mdwn
1 [[!toc]]
2
3 The seminar is now going to begin talking about more **imperatival** or **effect**-like elements in programming languages. The only effect-like element we've encountered so far is the possibility of divergence, in languages that permit fixed point combinators and so have the full power of recursion. What it means for something to be effect-like, and why this counts as an example of such, will emerge.
4
5 Other effect-like elements in a language include: printing (recall the [[damn]] example at the start of term), continuations (also foreshadowed in the [[damn]] example) and exceptions, and **mutation**. This last notion is our first topic.
6
7
8 ## Mutation##
9
10 What is mutation? It's helpful to build up to this in a series of fragments. For pedagogical purposes, we'll be using a made-up language that's syntactically similar to, but not quite the same as, OCaml.
11
12 This should seem entirely familiar:
13
14         [A] let x be 1 + 2 in
15                   let y be 10 in
16                         (x + y, x + 20)       ==> (13, 23)
17
18 Recall from earlier discussions that the following two forms are equivalent:
19
20         [B] let x be EXPRESSION in
21                   BODY
22
23                 (lambda (x) -> BODY) (EXPRESSION)
24
25 In fragment [A], we bound the variables `x` and `y` to `int`s. We can also bind variables to function values, as here:
26
27         [C] let f be (lambda (x, y) -> x + y + 1) in
28                   (f (10, 2), f (20, 2))
29                                                                   ==> (13, 23)
30
31 If the expression that evaluates to a function value has a free variable in it, like `y` in the next fragment, it's interpreted as bound to whatever value `y` has in the surrounding lexical context:
32
33         [D] let y be 3 in
34                   let f be (lambda (x) -> x + y) in
35                         (f (10), f (20))
36                                                                   ==> (13, 23)
37
38 Other choices about how to interpret free variables are also possible (you can read about "lexical scope" versus "dynamic scope"), but what we do here is the norm in functional programming languages, and seems to be easiest for programmers to reason about.
39
40 In our next fragement, we re-use a variable that had been bound to another value in a wider context:
41
42         [E] let x be 4 in
43                   let x be 3 in
44                         (x + 10, x + 20)      ==> (13, 23)
45
46 As you can see, the narrowest assignment is what's effective. This is just like in predicate logic: consider `(exists x. Fx and (exists x. Gx))`. The computer-science terminology to describe this is that the narrower assignment of `x` to the value 3 **shadows** the wider assignment to 4.
47
48 I call attention to this because you might casually describe it as "changing the value that x is assigned to." What we'll go on to see is a more exotic phenomenon that merits that description better.
49
50 Sometimes the shadowing is merely temporary, as here:
51
52         [F] let y be 2 in
53                   let f be (lambda (x) ->
54                         let y be 3 in
55                           ; here the most local assignment to y applies
56                           x + y
57                   ) in
58                         ; here the assignment of 3 to y has expired
59                         (f (10), y, f (20))   ==> (13, 2, 23)
60
61 OK, now we're ready for our main event, **mutable variables.** We'll introduce new syntax to express an operation where we're not shadowing a wider assignment, but *changing* the original assignemnt:
62
63         [G] let y be 2 in
64                   let f be (lambda (x) ->
65                         change y to 3 then
66                           x + y
67                   ) in
68                         ; here the change in what value y was assigned *sticks*
69                         ; we updated y's value, instead of introducing a new y
70                         (f (10), y, f (19))   ==> (13, 3, 23)
71
72 In languages that have native syntax for this, there are two styles in which it can be expressed. The *implicit style* is exemplified in fragment [G] above, and also in languages like C:
73
74         {
75                 int x = 1;    // this is like "let x be 1 in ..."
76                 x = 2;        // this is like "change x to 2 then ..."
77                 return x + 1; // this is like "x + 1"
78         }
79
80 A different possibility is the *explicit style* for handling mutation. Here we explicitly create and refer to new "reference cells" to hold our values. When we change a variable's value, the variable stays associated with the same reference cell, but that reference cell's contents get modified. The same thing happens in the semantic machinery underlying implicit-style mutable variables, but there it's implicit. The reference cells aren't themselves explicitly referred to in the object language. In explicit-style mutation, they are. OCaml has explicit-style mutation. It looks like this:
81
82           let xcell = ref 1         (* this creates a new reference cell *)
83                         in let () = xcell := 2  (* this changes the contents of that cell to 2; the return value of doing so is () *)
84                                                                     (* other return values could also be reasonable: such as the old value of xcell, the new value, an arbitrary int, and so on *)
85                         in !xcell + 1;;                 (* the !xcell operation "dereferences" the cell---it retrieves the value it contains *)
86
87 When we're dealing with mutable variables (or any other kind of effect), order now matters. For example, it would make a big difference whether I evaluated "let z = !xcell" before or after evaluating "xcell := !xcell + 1". Before this point, order never mattered except with respect to sometimes avoiding divergence.
88
89 OCaml does not however guarantee what order expressions will be evaluated in arbitrary contexts. For example, in the following fragment, you cannot rely on `expression_a` being evaluated before `expression_b` before `expression_c`:
90
91         let triple = (expression_a, expression_b, expression_c)
92
93 OCaml does however guarantee that different let-expressions are evaluated in the order they lexically appear. So in the following fragment, `expression_a` *will* be evaluated before `expression_b` and that before `expression_c`:
94
95         let a = expression_a
96                 in let b = expression_b
97                         in expression_c
98
99 Scheme does the same---if you use Scheme's `let*`, but not if you use its `let`. I agree this is annoying.
100
101 If `expression_a` and `expression_b` evaluate to (), for instance if they're something like `xcell := !xcell + 1`, that can also be expressed in OCaml as:
102
103         let () = expression_a
104                 in let () = expression_b
105                         in expression_c
106
107 And OCaml has a syntactic shorthand for this form, namely to use semi-colons:
108
109         expression_a; expression_b; expression_c
110
111 This is not the same role that semi-colons play in list expressions, like `[1; 2; 3]`. For parsing purposes, these semi-colon'ed complexes sometimes need to be enclosed in parentheses or a `begin ... end` construction:
112
113         (expression_a; expression_b; expression_c)
114
115         begin expression_a; expression_b; expression_c end
116
117 Scheme has a construction similar to the latter:
118
119         (begin (expression_a) (expression_b) (expression_c))
120
121 Though often in Scheme, the `(begin ...)` is implicit and doesn't need to be explicitly inserted, as here:
122
123         (lambda (x) (expression_a) (expression_b) (expression_c))
124
125
126 ##Referential opacity##
127
128 In addition to order-sensitivity, when you're dealing with mutable variables you also give up a property that computer scientists call "referential transparency." It's not obvious whether they mean exactly the same by that as philosophers and linguists do, or only something approximately the same. What they do mean is a kind of substitution principle, illustrated here:
129
130         let x = 1
131                 in (x, x)
132
133 should evaluate the same as:
134
135         let x = 1
136                 in (x, 1)
137
138 or:
139
140         (1, 1)
141
142 Notice, however, that these don't evaluate the same:
143
144         let xcell = ref 1
145                 in xcell := 2; !xcell
146         (* evaluates to 2 *)
147
148         (ref 1) := 2; !(ref 1)
149         (* evaluates to 1 *)
150
151
152 NOTES NEED TO BE CLEANED UP FROM THIS POINT ONWARD...
153
154 ##Aliasing##
155
156     [H] ; *** aliasing ***
157         let y be 2 in
158           let x be y in
159             let w alias y in
160               (y, x, w)           ==> (2, 2, 2)
161
162     [I] ; mutation plus aliasing
163         let y be 2 in
164           let x be y in
165             let w alias y in
166               change y to 3 then
167                 (y, x, w)         ==> (3, 2, 3)
168
169     [J] let f be (lambda (y) -> BODY) in  ; a
170           ... f (EXPRESSION) ...
171
172         (lambda (y) -> BODY) EXPRESSION
173
174         let y be EXPRESSION in            ; b
175           ... BODY ...
176
177     [K] ; *** passing "by reference" ***
178         let f be (lambda (alias w) ->     ; ?
179           BODY
180         ) in
181           ... f (y) ...
182
183         let w alias y in                  ; d
184           ... BODY ...
185
186     [L] let f be (lambda (alias w) ->
187           change w to 2 then
188             w + 2
189         ) in
190           let y be 1 in
191             let z be f (y) in
192               ; y is now 2, not 1
193               (z, y)              ==> (4, 2)
194
195     [M] ; hyper-evaluativity
196         let h be 1 in
197           let p be 1 in
198             let f be (lambda (alias x, alias y) ->
199               ; contrast here: "let z be x + y + 1"
200               change y to y + 1 then
201                 let z be x + y in
202                   change y to y - 1 then
203                     z
204             ) in
205               (f (h, p), f (h, h))
206                                   ==> (3, 4)
207
208     Notice: h, p have same value (1), but f (h, p) and f (h, h) differ
209
210
211 Different grades of mutation involvement...
212
213 Five grades of mutation involvement
214
215     0. Purely functional languages
216     1. Passing by reference
217        need primitive hyper-evaluative predicates for it to make a difference
218     2. mutable variables
219     3. mutable values
220         - numerically distinct but indiscernible values
221         - two equality predicates
222         - examples: closures with currently-indiscernible but numerically distinct
223           environments, mutable lists
224     4. "references" as first-class values
225         - x not the same as !x, explicit deref operation
226         - can not only be assigned and passed as arguments, also returned (and manipulated?)
227         - can be compared for qualitative equality
228     5. structured references
229         (a) if `a` and `b` are mutable variables that uncoordinatedly refer to numerically the same value
230             then mutating `b` won't affect `a` or its value
231         (b) if however their value has a mutable field `f`, then mutating `b.f` does
232             affect their shared value; will see a difference in what `a.f` now evaluates to
233
234
235
236 loops instead of recursion
237
238
239
240 ## Side-effects and mutation ##
241
242 1.      What difference imperativity makes
243 2.      Side-effects in a purely functional setting, via monads
244 3.      [Phil/ling application]Semantics for DPL, using state monad
245         Groenendijk, Stokhof, and Veltman, "Coreference and modality"
246         in Shalom Lappin, ed. Handbook of Contemporary Semantic Theory (Blackwell, 1996)
247 4.      Passing by reference
248 5.      [Phil/ling application] Fine and Pryor on "coordinated contents" (see, e.g., [Hyper-Evaluativity](http://www.jimpryor.net/research/papers/Hyper-Evaluativity.txt))
249