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

Mutation
CSI 3120 Amy Felty University of Ottawa
slides copyright 2017, 2018 David Walker, 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 ;; let m = Cons(3,r) ;; r := m ;;
mlength m ;;
35

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
r
36

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