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!