--------------------------------------------------
Imperative programming in SML
Lecture 2
12 Nov 2002
Tom Murphy VII
--------------------------------------------------
Assignment 5 Info
- minor changes
- fact example
- > isn't in MinML
- parser tips
- assuming type-checked input
--------------------------------------------------
Outline
- References
- Memoization
- Memoized Streams
- Benign Effects
- Proofs about Imperative Programs (?)
- Value Restriction
--------------------------------------------------
Re-introduction to references
(* REVIEW. *)
References are:
A type
'a ref
... representing references holding
values of type 'a.
A constructor
ref : 'a -> 'a ref
...
Functions
! : 'a ref -> 'a
... fetching the contents of a reference
:= : 'a ref * 'a -> unit
... updating the contents of a reference
--------------------------------------------------
Memoization: Suspensions
(* REVIEW. *)
signature SUSPENSION =
sig
type 'a susp
val delay : (unit -> 'a) -> 'a susp
val force : 'a susp -> 'a
end
(* simpler version *)
structure MemoSusp :> SUSPENSION =
struct
type 'a susp = (unit -> 'a) * 'a option ref
fun delay f = (f, ref NONE)
fun force (f, memo as ref NONE) =
let val res = f ()
in
memo := SOME res;
res
end
| force (_, ref (SOME m)) = m
end
We implemented these such that the first force
would do the computation, but later forces would
simply return the memoized result.
--------------------------------------------------
Memoized streams ("lazy lists")
Using memoized suspensions, we can create
memoized streams. The definition is the same, we
just use MemoSusp instead of Suspension?
structure MS = MemoSusp
datatype 'a front =
Cons of 'a * 'a stream
| Nil
withtype 'a stream = 'a front MS.susp
--------------------------------------------------
Memoized streams
Memoized streams act just like memoized
suspensions. The first time they are forced,
potentially expensive computation is carried out.
Later forces are free.
Here are some standard definitions:
fun fib 0 = 1
| fib 1 = 1
| fib n = fib (n - 1) + fib (n - 2)
fun count n () = Cons(n, MS.delay (count (n+1)))
val ints = MS.delay (count 0)
(* map for streams *)
fun smap' f s () =
case MS.force s of
Nil => Nil
| Cons(a, ss) => Cons(f a, smap f ss)
and smap f s = MS.delay (smap' f s)
(* take n elements from a stream *)
fun stake 0 s = nil
| stake n s =
case MS.force s of
Nil => nil
| Cons(a, ss) => a :: stake (n - 1) ss
--------------------------------------------------
Memoized streams
fun loudfib n =
let in
print ("Called fib " ^
Int.toString n ^ "\n");
fib n
end
(* stream of fibonacci numbers *)
val fibs = smap loudfib ints
(* slow *)
val fib33 = stake 33 fibs
(* instantaneous *)
val fib33' = stake 33 fibs
(* only computes 1 new fibonacci number *)
val fib34 = stake 34 fibs
--------------------------------------------------
Sometimes, Two Wrongs Make a Right
We've seen (and will see later) that imperative
programming usually makes your program hard to
reason about.
Paradoxically, however, using imperative
features to memoize other imperative features can
lead to a *more* functional program!
--------------------------------------------------
Example: Memoized keyboard input stream.
fun genkeys () =
case TextIO.input1 TextIO.stdIn of
NONE => Nil
| SOME c => Cons(c, MS.delay genkeys)
val keys = MS.delay genkeys
(* waits for input ... *)
val first_ten = stake 10 keys
(* returns the same keystrokes! *)
val again = stake 10 keys
--------------------------------------------------
Standard Table-based Memoization
Sometimes we're not just memoizing a single
suspended computation, but a single function
over a range of possible inputs.
For instance, the way we wrote fibonacci
before was really bad. We re-compute a lot
of intermediate values.
--------------------------------------------------
Table-based Memoization: Fibonacci
(* fib n
calculate fibonacci(n) for n >= 0 *)
fun fib 0 = 1
| fib 1 = 1
| fib n = fib (n - 1) + fib (n - 2)
fib 4 calls...
fib 3, which calls...
fib 2, which calls...
fib 0
fib 1
fib 2, which calls...
fib 0
fib 1
Lots of redundant computation!
--------------------------------------------------
Table-based Memoization: Fibonacci
local
val fiba = Array.array(500, NONE)
val _ = Array.update(fiba, 0, SOME 1)
val _ = Array.update(fiba, 1, SOME 1)
in
(* fib n
calculate fibonacci of n,
for 0 <= n < 500 *)
fun fib n =
case Array.sub(fiba, n) of
SOME x => x
| NONE =>
let val r =
fib (n - 1) + fib (n - 2)
in
Array.update(fiba, n, SOME r);
r
end
end
--------------------------------------------------
Table-based Memoization
Most of this code doesn't have to do with
fibonacci.
Can we abstract it into a general
function-memoizer?
(This will be tricky, watch out.)
Morally, such a function should take an
(int -> 'a) function, and return an
(int -> 'a) function that's memoized.
What's the problem with this setup?
--------------------------------------------------
Table-based Memoization
Problem:
fun fact 0 = 1
| fact n = n * fact (n - 1)
^^^^
The factorial function calls itself directly.
(NOT through the table.)
What can we do?
--------------------------------------------------
Generalized Table-based Memoization
Suppose we wrote factorial like this:
fun fact f 0 = 1
| fact f n = n * f (n - 1)
^^^
We pass in the function f that it should use
for its "recursive" calls.
Now factorial isn't recursive!!
Our memoizer will pass in a memoized version
of factorial for the recursive calls.
What's the type of fact?
What will be the type of our memoizer?
--------------------------------------------------
Generalized Table-based Memoization
(* ((int -> 'a) -> int -> 'a) -> int -> 'a *)
fun tablize f =
let
val memo = Array.array(500, NONE)
fun mf x =
case Array.sub(memo, x) of
SOME r => r
| NONE =>
let val r = f mf x (* !! *)
in
Array.update(memo, x, SOME r);
r
end
in
mf
end
--------------------------------------------------
Other Benign Effects: MTF Lists
As we see, it's possible to use imperative
constructs to implement persistent data structures
more efficiently. These are called "benign effects".
Move to front ("MTF") lists are a simple data
structure for quick access to unordered data. The
basic idea is to move an item to the head of the list
any time it is used. Though this won't improve our
worst-case running time, it tends to help in
real-world situations where some data are looked up
more frequently than others. (Or simply when there
is good locality of access.)
--------------------------------------------------
Move-to-front Lists
signature BUNCH =
sig
type 'a bunch
val insert : 'a bunch -> 'a -> 'a bunch
val lookup : ('a * 'b -> bool) -> 'a bunch ->
'b -> 'a option
end
structure MTF :> BUNCH =
struct
type 'a bunch = 'a list ref
fun insert (ref l) x = ref (x :: l)
fun lookup eq (b as ref l) x =
let
fun look _ nil = NONE
| look l (h::t) = if eq (h, x) then
(b := h :: (rev l @ t);
SOME h)
else look (h::l) t
in look nil l
end
end
... why do we have to copy in insert?
--------------------------------------------------
Benign Effects, continued
Other examples:
- Splay Trees
- Union-Find path compression
--------------------------------------------------
Proving Things
- Proving things about imperative programs much
harder than functional programs
- Have to reason about *effect* of expression
as well as *value*
- Must be careful when replicating / deleting
code
--------------------------------------------------
Proving Things
- Transformation:
an imperative function from int -> int
becomes a functional function from
int * state -> int * state
- This makes it easier to reason about
the programs, but makes the programs
much uglier.
- "Purely Functional" languages like Haskell
build this in. ("Monads")
--------------------------------------------------
Value Restriction
- val x = nil @ nil
stdIn:79.1-79.19 Warning: type vars not generalized because of
value restriction are instantiated to dummy types (X1,X2,...)
val x = [] : ?.X1 list
What is this nonsense?
Now we can finally understand what this is for.
--------------------------------------------------
Value Restriction
val bindings in SML can be polymorphic:
(this is called "let-polymorphism")
val x : 'a list = nil
... but only if the expression is
a syntactic value.
Examples of values:
Datatype constructors (applied to values),
functions, tuples of values.
OK:
val z = (0, nil, [fn x => x])
NOT OK:
val z = (0 + 1, nil)
--------------------------------------------------
Value Restriction
But why?
Suppose we allowed expressions.
val r = ref nil
.. now r has type 'a list ref.
val _ = r := [1000]
.. r still has type 'a list ref!
(* yikes!! *)
val f = (hd (!r)) : unit -> unit
.. ok, we choose 'a = unit -> unit
val _ = f ()
--------------------------------------------------
Value Restriction
This causes the language to be unsafe!
The value restriction fixes the problem.
Why does the problem occur?
Let-polymorphism is justified by substitution.
let val x = nil
in
... 0 :: x ...
... true :: x ...
end
Can be thought of as shorthand for:
... 0 :: nil ...
... true :: nil ...
--------------------------------------------------
Value Restriction
What happens if we do this with ref?
let val r = ref nil
in
r := [1000];
(hd (!r))()
end
becomes
(ref nil) := [1000];
(hd (!(ref nil))) ()
This program is TYPE SAFE,
but not the same program as before!
Replicating an expression with effect
(creation of a reference cell) may change the
program by duplicating that effect.
Because let doesn't replicate the behavior of
the program under substitution, we can't use
substitution as a justification for polymorphism.
--------------------------------------------------
Value Restriction: Demo
--------------------------------------------------
Welcome to the end of the slide show.
--------------------------------------------------
--------------------------------------------------
val r = ref nil;
val r = magic r : 'a list ref;
val _ = r := [1000];
val x = (hd (!r)) ();
--------------------------------------------------