15-150 Fall 2014
Lecture 8
Stephen Brookes
Parallelism
The recursive calls in
Merge(Msort t1, Msort t2)
can be evaluated in parallel
Sequential evaluation would take the sum
of the runtimes of the two calls
Parallel evaluation would take the max
The span is the runtime, assuming an
unlimited number of parallel processors
Let SMsort(d) be the span for Msort(T)
when T is a balanced tree of depth d
Span of Ins
fun Ins (x, Empty) = Node(Empty, x, Empty)
| Ins (x, Node(t1, y, t2)) =
case compare(x, y) of
GREATER => Node(t1, y, Ins(x, t2))
|
_
=> Node(Ins(x, t1), y, t2)
(no parallelism!)
For a balanced tree of depth d>0,
SIns(d) = c + SIns(d-1)
SIns(d) is O(d)
Span of SplitAt
fun SplitAt(y, Empty) = (Empty, Empty)
| SplitAt(y, Node(t1, x, t2)) =
case compare(x, y) of
GREATER => let val (l1, r1) = SplitAt(y, t1) in (l1, Node(r1, x, t2)) end
| _
=> let val (l2, r2) = SplitAt(y, t2) in (Node(t1, x, l2), r2) end;
(no parallelism!)
For a balanced tree of depth d>0,
SSplitAt(d) = k + SSplitAt(d-1)
SSplitAt(d) is O(d)
Span of Merge
independent
fun Merge (Empty, t2) = t2!
| Merge (Node(l1,x,r1), t2) = !
let val (l2, r2) = SplitAt(x, t2) in Node(Merge(l1, l2), x, Merge(r1, r2)) end
For balanced trees of same depth d>0,
assuming that the trees got by splitting
have the same depth (d-1) and are balanced
SMerge(d) = SSplitAt(d) + max(SMerge(d-1), SMerge(d-1))
= SSplitAt(d) + SMerge(d-1)
= O(d) + SMerge(d-1)
SMerge(d) is O(d2)
Span of Msort
fun Msort Empty = Empty!
independent
| Msort (Node(t1, x, t2)) = !
Ins (x, Merge(Msort t1, Msort t2))
For a balanced tree of depth d
SMsort(d) = max(SMsort(d-1), SMsort(d-1))
+ SMerge(d) + SIns(2d)
= SMsort(d-1) +
2
O(d )
SMsort(d) is O(d3)
losing balance
Msort can produce badly balanced trees
42
42
42
42 42
Msort
42
42
42
42
42
42
42
42
42
Really?
The balance assumptions are not realistic!
But we could design a rebalancing function...
fun Msort Empty = Empty!
| Msort (Node(t1, x, t2)) = !
Rebalance(Ins (x, Merge(Msort t1, Msort t2)))
Or implement an abstract type
of balanced trees with Ins and Merge
functions that preserve balance
15-150 Fall 2014
Lecture 8
Stephen Brookes
Type checking
Polymorphism
Type inference
type benefits
... a static check provides a runtime guarantee
If e has type t,
e evaluates to a value of type t
assuming
termination
If d declares x of type t,
d binds x to a value of type t
static property
runtime guarantee
e has type t
if e =>* v then v : t
d declares x : t
if d =>* [x : v] then v : t
advantages
Type analysis is easy, static, cheap
and yields a runtime guarantee
A type error indicates a bug,
would be
expensive
to keep checking
at runtime
detected and prevented without running code
An unexpected type may also indicate a bug!
Values of a given type have predictable form
We can choose patterns, operations, etc
that are appropriate for that type
Specifications and correctness proofs
can also use knowledge about types
More succinct, simpler specs and proofs
Referential transparency
for types
The type of an expression depends on the
types of its sub-expressions
... hence, the type of an expression
depends ultimately on
the types of its free variables
x + x has type int if x has type int
x + x has type real if x has type real
type analysis
can be done statically, at parse time
There are syntax-directed rules
for figuring out when e has type t
e is well-typed, with type t,
if and only if provable from these rules
We say e has type t
or write e : t
possibly with
assumptions like
x:int and y:int
Typing rules
There are static (syntax-directed) rules for
e has type t
d declares x1 : t1 xk : tk
p fits type t and binds x1 : t1 xk : tk
under appropriate assumptions
about the free variables of e and d
Arithmetic rules
numerals have type int
e + e has type int
1
if e1 and e2 have type int
Similarly for e
* e2 and e1 - e2
static property
21 + 21 has type int
runtime behavior
21 + 21 =>* 42 : int
Boolean rules
true and false have type bool
e andalso e has type bool
1
if e1 and e2 have type bool
< e2 has type bool
if e1 and e2 have type int
1
similarly for
e1 orelse e2
similarly for
e1 = e2
e1 > e 2
static property
runtime behavior
(3+4 < 1+7) : bool
(3+4 < 1+7) =>* true : bool
Conditional rules
(one for each type t)
if e then e
else e2 has type t
if e has type bool and e1, e2 have type t
1
test must be a boolean,
both branches must have the same type
static property
if x<y then x else y has type int
if x:int and y:int
runtime behavior
if x<y then x else =>* 4:int
if x:4 and y:5
Tuple rules
(for all types t1 and t2)
(e , e ) has type t
1
1 * t2
if e1 has type t1 and e2 has type t2
static property
runtime behavior
(x+2, y) has type int * bool
when x:int and y:bool
(x+2, y) =>* (4, true) : int * bool
when x:2 and y:true
Similarly for (e1, ..., ek) when k>0
Also ( ) has type unit
List rules
[e , ..., e ] has type t list
1
if for each i, ei has type t
e ::e
(for each type t)
all items in a list
must have the same type
has type t list
if e1 has type t and e2 has type t list
1
e @e
has type t list
if e1 and e2 have type t list
1
[1<2, 3<4] has type bool list
[1<2, 3<4] =>* [true, true] : bool list
Functions
fn x => e has type t
-> t2
if, assuming x : t1, e has type t2
1
the type of a
function expression
ensures type-safe
applicative behavior
when applied
to an argument of type t1
the result (if it terminates)
will be a value of type t2
fn x => if x=0 then 1 else f(x-1)
has type int -> int if f : int -> int
and is a value of type int -> int,
if f is bound to a value of type int -> int
Application
e
e2 has type t2
if e1 has type t1 -> t2 and e2 has type t1
1
when a function of type t1 -> t2
gets applied to
an argument of type t1
the result (if application terminates)
will be a value of type t2
argument e2 must have
correct type for function e1
(fn x => if x=0 then 1 else f(x-1)) 5
has type int if f : int -> int
evaluates to
46 : int
if f : fn y => y+42
Declarations
val x = e declares x : t
if e has type t
+ scope rules
for combining
declarations
val x = 42 declares x : int
and when executed, binds x to 42 : int
val f = fn x => x + 1 declares f : int -> int
and when executed, binds f to (fn x => x+1) : int -> int
Declarations
fun f x = e declares f : t
-> t2
if, assuming x : t1 and f : t1 -> t2, e has type t2
1
assuming that
and
f is applied to
recursive calls to f in e
an argument of type t1
have type t1 -> t2
the result of
application
will have type t2
!
fun f x = if x=0 then 1 else f(x-1)
declares f : int -> int
binds f to a function value of type int -> int
let expressions
let d in e end has type t
if d declares x1 : t1, ..., xk : tk
and, in the scope of these bindings
e has type t
let val x = 21 in x + x end has type int
and evaluates to 42 : int
let
fun f x = if x=0 then 1 else f(x-1)
in
f 42
end
has type int
and evaluates to 1 : int
Patterns
when p fits type t
42 fits t iff t is int
x fits t always
(p , p ) fits t iff
_ fits t always
t is t1*t2, p1 fits t1, p2 fits t2
p ::p
what bindings?
none
none
x:t
combined
combined
fits t iff
t is t1 list, p1 fits t1, p2 fits t1 list
1
clausal function
expressions
fn p
=> e1 | ... | pk => ek has type t1 -> t2
if for each i, pi fits t1, with type bindings for
which ei has type t2
1
each clause pi => ei must have same type t1 -> t2
- each pi must fit type t1
- each ei must have type t2
fn 0 => 0 | n => f(n - 1) has type int -> int
if f has type int -> int
clausal fun declarations
fun f p
= e1 | ... | f pk = ek declares f : t1 -> t2
iff for i = 1 to k,
pi fits t1, with type bindings for which,
assuming f : t1 -> t2, ei has type t2
1
each clause pi => ei must have same type t1 -> t2
assuming recursive calls to f in ei have this type
fun f 0 = 0 | f n = f (n - 1)
declares f : int -> int
and binds f to a value of type int -> int
Polymorphic types
ML has type variables
a, b, c
A type with type variables is polymorphic
a list -> a list
A polymorphic type has instances
!
int list -> int list
real list -> real list
(int * real) list -> (int * real) list
substitute
a type
for each type variable
... instances of a list -> a list
split
fun split [ ] = ([ ], [ ])
| split [x] = ([x], [ ])
| split (x::y::L) =
let val (A,B) = split L in (x::A, y::B) end
declares
split : int list -> int list * int list
also (more generally!) declares
split : a list -> a list * a list
(the most general type is polymorphic)
sorting
Assuming split : int list -> int list * int list
merge : int list * int list -> int list
fun msort [ ] = [ ]
| msort [x] = [x]
| msort L = let
val (A,B) = split L
in
merge (msort A, msort B)
end
declares msort : int list -> int list
sorting
Assuming split : a list -> a list * a list
merge : int list * int list -> int list
fun msort [ ] = [ ]
| msort L = let
val (A,B) = split L
in
merge(msort A, msort B)
end
declares msort : a list -> int list
... theres a bug in the code!
