Presentation by Felix Klock

Transcribed by Ryan Culpepper

Their language is based on a polymorphic lambda-calculus with explicit type annotations. Their type annotations had the form x : REF INT ! PURE (x is a reference cell holding an int, and evaluating the expression has no effect on memory) and (get x) : INT ! READ (fetching the value involves a read effect) and F : (SUBR (INT) OBS INT) ! PURE (F is a subroutine from int to int which can allocate or read memory, but the reference to F is pure) and (F 4) : INT ! OBS (applying F brings out its latent effect, OBS).

m : (poly (a b) (subr ((subr (a) _ b) [listof b]) _ [listof b]))What goes in _? We want to be able to use map on subroutines arguments with different latent effects. Need abstraction...

the old language: e::= ... | (tlambda (t) e) | (proj e t) ;; where proj projects a polymorphic value onto a type

the new language e::= ... | (plambda (x :: K) e) | (proj e t)

In the new language, plambda creates a value polymorphic in the thing named by x. K is the kind of x (type, effect, ...).

map = (plambda (t1::type t2::type f::effect)

(lambda (p::(subr (t1) f t2) l:[listof t1])

(if ((proj null? t1) l)

(proj null t2)

<lots of proj's in here>)))

They also bring back regions.

effects phi ::= (alloc rho) | (read rho) | (write rho) | pure | (maxeff phi1 phi2)

regions rho ::= x | @red | ...

map : (poly (t)They introduced notion of effect masking. Private region (private r e) if effects aren't visible from outside (Matthias says: like prompt). These could be inferred.

(subr ((subr (t1) f t2) [listof t1,r])

(maxeff f (read r) (alloc r))

[listof t2,r])

The algebra of effects is ACUI (associative, commutative, unitary, idempotent).

examples of unification on effects: Felix asks class to solve

- U[ int --(pure)--> a, b --(pure)--> int] yields {a = int, b = int}
- U[(maxeff Read Write), (maxeff a b)] yields... Peter says there are two substitutions {a = R, b = W} and {a = W, b = R}... some discussion follows.
- U[Read, (maxeff a b)] yields... gosh. Standard unification (Robinson) fails. Need ACUI-unification.

They also take out regions, but leave in plambda.

Peter asks: Is there an idea of principle type in this system? No. There are subroutines for which the most general type+effect cannot be expressed--Felix shows an example.

exp = (lambda (f)There is no principle type for f. It could have effect either pure or write. More discussion.

(lambda (g::(subr (bool) Write bool))

(if #t

g

(lambda (x) (begin (f x) (g x))))))

ACUI unification is in general NP-complete. However, the system devised here generates constraints of a certain form that can be solved in polynomial time, and always has a solution.

Users can no longer specify effects. All inferred. And now they base their system on inequivalences instead of equivalences, so they get constraints like {mu contains phi, ...} where mu is a simple unification variable, and phi can be structured. These constraints always have a solution, and in particular, they have a minimal solution that they can find.

(let ((v (build-vector 10 add1)System infers: v : [vectorof int,gamma], the whole expression has type [vectorof int,gamma2]. Since gamma does not appear in result expr, can stack-allocate v.

(f (lambda (x) (* a (+ b x))))

(vector-map f v))

Problems:

They use nondeterministic translation rules. It is perfectly legal to do everything in one region.

Quote: something like ".. Novice programmers often report that on their machines, memory is constant, not a variable." Do users have to figure out how to write programs to the memory manager? What are they trying to say?

{Matthias answers second point: Tofte influenced by Reynolds. Reynolds had been promoting call-by-name as giving stack allocation. Tofte wanted to answer, the same can be done for call-by-value.}