程序代写代做代考 algorithm compiler Java go ocaml C c/c++ data structure Mutation

Mutation
CSI 3120 Amy Felty University of Ottawa
slides copyright 2017, 2018, 2019, 2020 Author David Walker, updated by Amy Felty permission granted to reuse these slides for non-commercial educational purposes

mutable set
immutable set
Reasoning about Mutable State is Hard
insert i s1;
f x;
member i s1
let s1 = insert i s0 in
f x;
member i s1
Is member i s1 == true? …
– When s1 is mutable, one must look at f to determine if it
modifies s1.
– Worse, one must often solve the aliasing problem.
– Worse, in a concurrent setting, one must look at every other function that any other thread may be executing to see if it modifies s1.
2

Thus far…
We have considered the (almost) purely functional subset of OCaml. – We’ve had a few side effects: printing & raising exceptions.
Two reasons for this emphasis:
– Reasoningaboutfunctionalcodeiseasier.
• Bothformalreasoning
– equationally, using the substitution model – and informal reasoning
• Datastructuresarepersistent.
– They don’t change – we build new ones and let the garbage collector
reclaim the unused old ones.
• Hence,anyinvariantyouprovetruestaystrue.
– e.g.,3isamemberofsetS.
– Toconvinceyouthatyoudon’tneedsideeffectsformanythingswhereyou
previously thought you did.
• Programmingwithbasicimmutabledatalikeints,pairs,listsiseasy.
– types do a lot of testing for you!
– do not fear recursion!
• Youcanimplementexpressive,highlyreuseablefunctionaldatastructures like polymorphic 2-3 trees or dictionaries or stacks or queues or sets with
reasonable space and time.
3

But alas…
Purely functional code can’t do everything.
– Sometimes we really want code to have some effect on the world.
– For example, the OCaml top-level loop prints out your result.
• Without that printing (a side effect), how would you know that your functions
Some algorithms or data structures need mutable state.
– Hash-tables have (essentially) constant-time access and update.
• The best functional dictionaries have either: – logarithmic access & logarithmic update – constant access & linear update
– constant update & linear access
do that in a functional setting.
– Robinson’s unification algorithm
• A critical part of the OCaml type-inference engine.
• Also used in other kinds of program analyses.
– Depth-first search, more …
However, purely mostly functional code is amazingly productive
computed the right thing?
• Don’t forget that we give up something for this:
– we can’t go back and look at previous versions of the dictionary. We can
4

OCAML MUTABLE REFERENCES

References
• New type: t ref
– Thinkofitasapointertoaboxthatholdsatvalue. – Thecontentsoftheboxcanbereadorwritten.
6

References
• New type: t ref
– Thinkofitasapointertoaboxthatholdsatvalue. – Thecontentsoftheboxcanbereadorwritten.
• To create a fresh box: ref 42
– allocatesanewbox,initializesitscontentsto42,andreturnsapointer:
42
– ifrpointstoaboxcontaining42,thenreturn42.
– ifr:tref then!r:t • To write the contents: r := 5
– updatestheboxthatrpointstosothatitcontains5. – ifr:tref thenr:=5:unit
– ref42:intref • To read the contents: !r
8

Example
let c = ref 0 in
let x = !c in (* x will be 0 *)
(c := 42;
lety=!cin (*ywillbe42.
x will still be 0! *)
…)
9

Another Example
let c = ref 0
let next() =
let v = !c in (c := v+1 ; v)
10

Another Example
let c = ref 0
let next() =
let v = !c in (c := v+1 ; v)
If e1 : unit and e2 : t then (e1 ; e2) : t
11

You can also write it like this:
let c = ref 0
let next() =
let v = !c in
let _ = c := v+1 in v
12

Another Idiom
Global Mutable Reference Mutable Reference Captured in Closure
countA
code
let c = ref 0
let next () : int = let v = !c in
(c := v+1 ; v)
let counter () = let c = ref 0 in
fun () ->
let v = !c in (c := v+1 ; v)
let countA = counter() in
let countB = counter() in
countA() ; (* 0 *)
countA() ; (* 1 *)
countB() ; (* 0 *)
countB() ; (* 1 *)
countA() ; (* 2 *)
c
3
13

Imperative loops
(* print n .. 0 *)
let count_down (n:int) =
for i = n downto 0 do print_int i; print_newline()
done
(* print 0 .. n *)
let count_up (n:int) =
for i = 0 to n do print_int i; print_newline()
done
(* sum of 0 .. n *)
let sum (n:int) =
let s = ref 0 in let current = ref n in while !current > 0 do
s := !s + !current;
current := !current – 1 done;
!s

Imperative loops?
(* print n .. 0 *)
let count_down (n:int) = for i = n downto 0 do
print_int i;
print_newline()
done
(* for i=n downto 0 do f i *)
let rec for_down (n : int)
(f : int -> unit) : unit =
if n >= 0 then
(f n; for_down (n-1) f)
else ()
let count_down (n:int) = for_down n (fun i ->
print_int i;
print_newline() )

Aliasing
let c = ref 0 ;; let x = c ;;
x := 42 ;;
!c ;;
c
0
16

Aliasing
let c = ref 0 ;; let x = c ;;
x := 42 ;;
!c ;;
c x
0
17

Aliasing
let c = ref 0 ;; let x = c ;;
x := 42 ;;
!c ;;
c x
42
18

REFS AND MODULES

Types and References
Concrete, first-order type tells you a lot about a data structure:
• int
• int ref
• int * int
• int * (int ref)
• … etc
==> immutable
==> mutable
==> immutable
==> 1st component immutable, 2nd mutable
What about higher-order types?
• int -> int ==> the function can’t be changed
==> what happens when we run it?
What about abstract types?
• stack, queue? stack * queue?

Functional Stacks
module type STACK = sig
type ‘a stack
val empty : unit -> ‘a stack
val push : ‘a -> ‘a stack -> ‘a stack
val pop : ‘a stack -> ‘a stack val top : ‘a stack -> ‘a option
…
end
21

Functional Stacks
module type STACK = sig
type ‘a stack
val empty : unit -> ‘a stack
val push : ‘a -> ‘a stack -> ‘a stack val pop : ‘a stack -> ‘a stack
val top : ‘a stack -> ‘a option …
end
A functional interface takes in arguments, analyzes them, and produces new results
22

Imperative Stacks
module type IMP_STACK = sig
type ‘a stack
val empty : unit -> ‘a stack
val push : ‘a -> ‘a stack -> unit
…
end
23

Imperative Stacks
module type IMP_STACK = sig
type ‘a stack
val empty : unit -> ‘a stack
val push : ‘a -> ‘a stack -> unit
…
end
When you see “unit” as the return type, you know the function is being executed for its side effects. (Like void in C/C++/Java.)
24

Imperative Stacks
module type IMP_STACK = sig
type ‘a stack
val empty : unit -> ‘a stack
val push : ‘a -> ‘a stack -> unit
val pop : ‘a stack -> ‘a option end
Unfortunately, we can’t always tell from the type that there are side- effects going on. It’s a good idea to document them explicitly if the user can perceive them.
25

Imperative Stacks
module type IMP_STACK = sig
end
type ‘a stack
val empty : unit -> ‘a stack
val push : ‘a -> ‘a stack -> unit
val pop : ‘a stack -> ‘a option Look for these opportunities
This is a terrific way to use references in ML.
Unfortunately, we can’t always tell from the type that there are side- effects going on. It’s a good idea to document them explicitly if the user can perceive them.
Sometimes, one uses references inside a module but the data structures have functional (persistent) semantics
27

Imperative Stacks
module ImpStack : IMP_STACK = struct
type ‘a stack = (‘a list) ref
let empty() : ‘a stack = ref []
let push (x:’a) (s:’a stack) : unit = s := x::(!s)
let pop (s:’a stack) : ‘a option = match !s with
| [] -> None
| h::t -> (s := t ; Some h)
end
28

Imperative Stacks
module ImpStack : IMP_STACK = struct
type ‘a stack = (‘a list) ref let empty() : ‘a stack = ref []
end
let push (x:’a) (s:’a stack) : unit =
s := x::(!s)
let pop (s:’a stack) : ‘a op
t | h::t -> (s := t ; Some h)
i
o
n
ut
match !s with | [] -> None
Note: We don’t have to
make everything mutable. The list is an immutable data structure stored in a
sin
g
le
m
able cell.
=
29

Fully Mutable Lists
type ‘a mlist =
Nil | Cons of ‘a * (‘a mlist ref)
let ml = Cons(1, ref (Cons(2, ref (Cons(3, ref Nil)))))
ml
123
cons ref cons ref cons ref
30

Fully Mutable Lists
type ‘a mlist =
Nil | Cons of ‘a * (‘a mlist ref)
let ml = Cons(1, ref (Cons(2, ref (Cons(3, ref Nil)))))
let ml2 = Cons(7, ref Nil)
ml
123
cons ref cons ref cons ref
ml2
7
31

Fully Mutable Lists
type ‘a mlist =
Nil | Cons of ‘a * (‘a mlist ref)
let rec fudge(l:’a mlist)
(m:’a mlist) : unit =
match l with
| Nil -> ()
| Cons(h,t) -> t := m ; ()
fudge ml ml2
ml
123
cons ref cons ref cons ref
ml2
7
32

Fully Mutable Lists
type ‘a mlist =
Nil | Cons of ‘a * (‘a mlist ref)
let rec fudge(l:’a mlist)
(m:’a mlist) : unit =
match l with
| Nil -> ()
| Cons(h,t) -> t := m ; ()
fudge ml ml2
ml
ml2
cons ref
cons ref cons ref 23
7
1
33

Fully Mutable Lists
type ‘a mlist =
Nil | Cons of ‘a * (‘a mlist ref)
let rec mlength(m:’a mlist) : int = match m with
| Nil -> 0
| Cons(h,t) -> 1 + mlength(!t)
ml
pictorial convention:
cons ref cons ref cons ref
123 ml
123
34

Fraught with Peril
type ‘a mlist =
Nil | Cons of ‘a * (‘a mlist ref)
let rec mlength(m:’a mlist) : int = match m with
| Nil -> 0
| Cons(h,t) -> 1 + length(!t)
let r = ref Nil in let m = Cons(3,r) in (r := m ;
mlength m)
35

Mutable Append Example:
let rec mappend xs ys = match xs with
| Nil -> ()
| Cons(h,t) ->
(match !t with
| Nil -> t := ys
| Cons(_,_) as m -> mappend m ys) ;;
let x = Cons(1,ref (Cons (2, ref (Cons (3, ref Nil))))) ;; let y = Cons(4,ref (Cons (5, ref (Cons (6, ref Nil))))) ;; mappend x y ;;
123 456
40

Two types:
Add mutability judiciously
type ‘a very_mutable_list = Nil
| Cons of ‘a * (‘a very_mutable_list ref)
type ‘a less_mutable_list = ‘a list ref
The first makes cyclic lists possible, the second doesn’t
– the second preemptively avoids certain kinds of errors. – often called a correct-by-construction design
49

Is it possible to avoid all state? Yes! (in single-threaded programs)
– Pass in old values to functions; return new values from functions … but this isn’t necessarily the most efficient thing to do
Consider the difference between our functional stacks and our imperative ones:
– fnl_push : ‘a -> ‘a stack -> ‘a stack – imp_push : ‘a -> ‘a stack -> unit
50

SUMMARY

Summary: How/when to use state?
• A complicated question!
• In general, try to write the functional version first.
– e.g.,prototype
– don’thavetoworryaboutsharingandupdates
– reasoningiseasy(thesubstitutionmodelisvalid!)
• Sometimes you find you can’t afford it for efficiency reasons. – example: routing tables need to be fast in a switch
– constanttimelookup,update(hash-table)
• When using state, try to encapsulate it behind an interface. – trytoreducethenumberoferrorconditionsaclientcansee
• correct-by-constructiondesign
– moduleimplementermustthinkexplicitlyaboutsharingandinvariants – writethesedown,writeassertionstotestthem
– ifencapsulatedinamodule,thesetestscanbelocalized
– mostofyourcodeshouldstillbefunctional
52

Summary
Mutable data structures can lead to efficiency improvements.
– e.g., Hash tables, memoization, depth-first search
But they are much harder to get right, so don’t jump the gun
– updating in one place may have an effect on other places.
– writing and enforcing invariants becomes more important.
• why more important? because the types do less …
– cycles in data (other than functions) can’t happen until we
introduce refs.
• must write operations much more carefully to avoid looping • more cases to deal with and the compiler doesn’t help you!
– we haven’t even gotten to the multi-threaded part. So use refs when you must, but try hard to avoid it.
53

Related Posts