Principles of programming languages (A12079W1)

a

Solution

Thread the explicit program state through the computation, using the base computational monad to sequence its effects:

result (x) s (p ▹ f) s = r_{m} (x, s), = (p s) ▹_{m} (λ (x, s^{'}) . f (x) s^{'}) .

In Haskell notation, with resultM and bindM standing for the base operations:

result :: Monad m => a -> MemT m a
result x s = resultM (x,s)

bind :: Monad m => MemT m a -> (a -> MemT m b) -> MemT m b
bind p f s = bindM (p s) (\(x,s') -> f x s')

This is the state monad transformer. The first computation's final program state, rather than its initial program state, becomes the second computation's input. The base computational monad decides whether that pair is available at all.

b

Solution

Use the three monad laws of the base computational monad. For left identity, at an arbitrary program state

s

(result (x) ▹ f) s = r_{m} (x, s) ▹_{m} (λ (y, t) . f (y) t) = f (x) s .

The last step is the base left identity law. For right identity,

(p ▹ result) s = (p s) ▹_{m} (λ (x, t) . result (x) t) = (p s) ▹_{m} (λ (x, t) . r_{m} (x, t)) = (p s) ▹_{m} r_{m} = p s .

The penultimate equality identifies the pair-destructuring function with

r_{m}

; the last uses the base right identity law.

For associativity, expand the two successive uses of sequencing and apply base associativity:

((p ▹ f) ▹ g) s = ((p s) ▹_{m} (λ (x, t) . f (x) t)) ▹_{m} (λ (y, u) . g (y) u) = (p s) ▹_{m} (λ (x, t) . (f (x) t) ▹_{m} (λ (y, u) . g (y) u)) = (p s) ▹_{m} (λ (x, t) . (f (x) ▹ g) t) = (p ▹ (λ x . f (x) ▹ g)) s .

(3)

No program state is duplicated or reset during these rearrangements: both sides pass

s

p

, its output

t

f

, and the output

u

f

g

. By function extensionality,

result (x) ▹ f = f (x), p ▹ result = p, (p ▹ f) ▹ g = p ▹ (λ x . f (x) ▹ g) .

(4)

c

Solution

Reading preserves the computer memory; writing returns the unit type value; allocating returns both the fresh memory location and the allocator's updated computer memory:

get :: Monad m => Location -> MemT m Value
get a s = resultM (contents s a,s)

put :: Monad m => Location -> Value -> MemT m ()
put a v s = resultM ((),update s a v)

new :: Monad m => MemT m Location
new s = resultM (fresh s)

These use the memory interface in ^[ref]. In particular, fresh already returns its outputs in the order required by the state monad transformer:

get (a) s put (a, v) s new s = r_{m} (contents (s, a), s), = r_{m} ((), update (s, a, v)), = r_{m} (fresh (s)) .

d

Solution

There is one undifferentiated exception, so use the two alternatives of the Haskell algebraic data type Maybe: Just x succeeds and Nothing fails. A suitable exception monad transformer is:

type ExT m a = m (Maybe a)

result :: Monad m => a -> ExT m a
result x = resultM (Just x)

bind :: Monad m => ExT m a -> (a -> ExT m b) -> ExT m b
bind p f = bindM p (\r -> case r of
  Nothing -> resultM Nothing
  Just x  -> f x)

orelse :: Monad m => ExT m a -> ExT m a -> ExT m a
orelse p q = bindM p (\r -> case r of
  Nothing -> q
  Just x  -> resultM (Just x))

failure :: Monad m => ExT m a
failure = resultM Nothing

The distinction between bindM and bind matters. The handler must inspect the failed alternative using the base computational monad; the transformed bind would propagate failure without running that inspection. The alternative computation q runs only after p returns Nothing; any effects already performed by the base computational monad remain subject to that base's semantics.

Left identity follows by selecting Just x. Right identity follows because either alternative is passed back to resultM. For associativity, base associativity exposes the first alternative: Nothing propagates through both remaining steps; Just x runs f x, with its Nothing and Just alternatives treated identically on both sides. Thus this representation also satisfies the monad laws.

ExT m A = m (Maybe A), failure orelse q = q, result (x) orelse q = result (x) .

e

Solution

The identity monad embeds a value unchanged and sequences by ordinary application:

type IdM a = a
result :: a -> IdM a
result x = x
bind :: IdM a -> (a -> IdM b) -> IdM b
bind x f = f x

All three monad laws reduce to substitution in function application. There is no additional program state, failure alternative or continuation layer:

result (x) = x, x ▹ f = f (x) .

f

Solution

Expand the two type synonyms to see what survives an exception:

ExT (MemT m) A MemT (ExT m) A = Mem \to m (Maybe A, Mem), = Mem \to m (Maybe (A, Mem)) .

In the first order, a failed computation can still produce (Nothing,s'). The exception handler therefore runs with

s^{'}

, including writes made before failure. In the second order, failure produces Nothing, with no returned computer memory. A handler defined by applying the underlying orelse pointwise runs its alternative from the original input computer memory

s

. This gives rollback of this explicit program state for the failed branch.

For example, start with a memory location holding

0

, write

1

, fail, and handle the failure by reading that memory location. The first order returns

1

; the second returns

0

. This rollback concerns the explicit computer memory only: arbitrary effects in the base computational monad are not thereby reversed.

ExT (MemT m) MemT (ExT m) : writes survive failure; : failed memory updates roll back .

A conventional programming language normally retains writes made before an exception is caught. Its mutable computer memory and exception handling therefore correspond more closely to

ExT (MemT m)

g

Solution

Fix an answer type and let the continuation return its answer inside the base computational monad:

type ContT m a = (a -> m Answer) -> m Answer

result :: Monad m => a -> ContT m a
result x k = k x

bind :: Monad m => ContT m a -> (a -> ContT m b) -> ContT m b
bind p f k = p (\x -> f x k)

The continuation monad transformer changes the continuation supplied to p: it first runs f on the produced value, then uses the original final continuation k. Base sequencing is unnecessary in these two definitions because p already accepts a continuation returning m Answer. The customary lift, if desired, is lift q k = bindM q k.

ContT m A result (x) k (p ▹ f) k = (A \to m Answer) \to m Answer, = k (x), = p (λ x . f (x) k) .

2

a

Solution

The continuation receives both the computed value and the current computer memory. Therefore return invokes it with unchanged computer memory, while sequencing installs a continuation that passes the produced value and updated computer memory to the next computation:

result :: a -> M a
result x k s = k x s

bind :: M a -> (a -> M b) -> M b
bind p f k s = p (\x s' -> f x k s') s

For left identity, expand the two definitions:

(result (x) ▹ f) k s = (λ y t . f (y) k t) x s = f (x) k s .

For right identity,

(p ▹ result) k s = p (λ x t . result (x) k t) s = p (λ x t . k x t) s = p k s .

For associativity, both groupings reduce to the same expression:

((p ▹ f) ▹ g) k s (p ▹ (λ x . f (x) ▹ g)) k s = p (λ x t . f (x) (λ y u . g (y) k u) t) s, = p (λ x t . f (x) (λ y u . g (y) k u) t) s .

(3)

By function extensionality, these establish all three monad laws:

result (x) ▹ f = f (x), p ▹ result = p, (p ▹ f) ▹ g = p ▹ (λ x . f (x) ▹ g) .

(4)

b

Solution

Apply the memory interface before invoking the supplied continuation:

get :: Location -> M Value
get a k s = k (contents s a) s

put :: Location -> Value -> M ()
put a v k s = k () (update s a v)

new :: M Location
new k s = let (a,s') = fresh s in k a s'

A read preserves computer memory; a write changes it but returns the unit type value; an allocation uses the updated computer memory returned by fresh. The continuation always receives the latest computer memory:

get (a) k s put (a, v) k s new k s = k (contents (s, a)) s, = k (()) (update (s, a, v)), = k (a) s^{'} where (a, s^{'}) = fresh (s) .

c

Solution

Capturing a continuation retains the destination, while the computer memory is supplied when that destination is eventually invoked. The required Haskell definitions are:

callcc :: (Cont a -> M a) -> M a
callcc f k s = f k k s

withc :: Cont a -> M a -> M a
withc saved p _current s = p saved s

callccPrim :: [Value] -> M Value
callccPrim [Function f] =
  callcc (\k -> f [Continuation k])

withcPrim :: [Value] -> M Value
withcPrim [Continuation k,v] = withc k (result v)

In callcc, the handler f k initially runs with the same current continuation k. If it returns normally, its result goes there. If it invokes withc with a saved continuation, the current destination is discarded. In particular,

callcc (f) k s = f (k) k s, withc (k^{'}, p) k s = p k^{'} s .

The primitive interface receives values, because the surrounding call-by-value interpreter has already evaluated its arguments. Thus the expression supplied as the second argument of withc is evaluated once, before withcPrim transfers its value. Wrapping that value with result implements precisely the remaining transfer; the primitive must not try to evaluate it a second time. Neither operation restores a saved snapshot of computer memory.

d

Solution

Keep a FIFO queue of runnable continuations in shared computer memory. Removing a continuation from its head transfers control with nil; suspending a runnable computation appends its continuation at the rear. A single scheduler group also needs a terminal continuation so that finishing the last computation cannot return through an obsolete invocation of fork.

The following is FunMem, including the shared initialization and helper definitions. run(main) starts a scheduler group; nested fork calls use that same group.

val ready = new(); ready := nil;
val stop = new();

rec append(xs,ys) =
  if xs = nil then ys else head(xs) : append(tail(xs),ys);

val enqueue(k) =
  ready := append(!ready,k:nil); nil;

val dispatch() =
  if !ready = nil then withc(!stop,nil)
  else let val k = head(!ready) in
    ready := tail(!ready); withc(k,nil);

val run(main) =
  callcc(lambda (done)
    stop := done; ready := nil;
    main(); dispatch());

val fork(f) =
  callcc(lambda (parent)
    enqueue(parent); f(); dispatch());

val yield() =
  callcc(lambda (current)
    enqueue(current); dispatch())

At fork, the parent is queued before f() starts. The child runs immediately. Its ordinary return value is ignored by sequencing into dispatch(). At yield, the current computation joins the rear, then the oldest runnable computation is removed from the front. If there was no other runnable computation, these operations select the just-captured continuation, so the caller resumes immediately with nil.

The invariant is that each suspended runnable computation has exactly one entry in ready, ordered by the time it most recently became suspended and runnable. A running computation is absent from that FIFO queue. Neither appending nor removing an entry suspends, so these operations are indivisible relative to this cooperative multitasking scheduler. Completing a child removes the child from consideration permanently; it is never enqueued by its completion wrapper.

For the paper's example, call the initial computation

P

and the forked computation

C

. The FIFO queue and writes evolve as follows:

Event	Running next	Ready queue	New list head	Fork starts child	$C$	$P$	—	Child writes and yields	$P$	$C$	$1$	Parent writes and yields	$C$	$P$	$3$	Child writes and finishes	$P$	empty	$2$	Parent writes and finishes	scheduler exits	empty	$4$

Figure 1.
FIFO continuation scheduling of the paper's two coroutines
. **Details**.

Thus the observable list, read after the scheduler group finishes, is

[4, 2, 3, 1], fork (f) and yield () resume their callers with nil .

The scheduler exit is used only when no runnable continuations remain. A main computation can place its desired final observable value in shared computer memory and read it after run returns. This wrapper also permits already-forked computations to finish if the initial computation finishes before them. Each run creates one active scheduler group; calls of run are not nested.

e

Solution

Represent a binary semaphore by a two-element list containing the addresses of its busy flag and its waiting FIFO queue. A blocked continuation belongs to the waiting FIFO queue, not the scheduler's runnable FIFO queue. These definitions extend the FunMem scheduler from the preceding part:

val semaphore() =
  let val busy = new() in
  let val waiting = new() in
    busy := false; waiting := nil; busy : waiting : nil;

val acquire(s) =
  let val busy = head(s) in
  let val waiting = head(tail(s)) in
    if !busy then
      callcc(lambda (blocked)
        waiting := append(!waiting,blocked:nil); dispatch())
    else (busy := true; nil);

val release(s) =
  let val busy = head(s) in
  let val waiting = head(tail(s)) in
    if !waiting = nil then (busy := false; nil)
    else let val next = head(!waiting) in
      waiting := tail(!waiting); enqueue(next); nil

A newly created semaphore is free. Acquiring it while free marks it busy and immediately returns nil. Acquiring it while busy captures the remainder of the caller, appends that continuation to the waiting FIFO queue, and dispatches a runnable computation. No runnable copy of the blocked caller is retained.

When a waiting caller exists, release keeps the busy flag true: the released permit is reserved for that caller. It removes exactly one waiting continuation and appends it to the scheduler's runnable FIFO queue. It does not invoke dispatch, so the releasing computation keeps running. A newcomer cannot steal the reserved permit during the interval before the released caller resumes. That caller's captured continuation resumes after acquire with nil, already possessing the permit.

free acquire: busy acquire: release with waiter: release without waiter: mark busy and continue; block outside the runnable queue; keep busy and enqueue one waiter; mark free .

These are FIFO semaphores; the question only requires selecting one waiter, so choosing the oldest is a valid stronger discipline. The updates contain no suspension except at the explicit blocking point, making them atomic relative to this cooperative multitasking scheduler. As allowed in the paper, invalid releases and executions in which every remaining computation is blocked need no error handling; the latter are deadlocks, not a way to make progress.

3

a

Solution

Use programming closures that receive evaluated arguments and return a computation in the chosen computational monad. A sufficient core of the semantic value domain is:

data Value = IntVal Integer
           | BoolVal Bool
           | Function ([Value] -> M Value)

Additional constructors may represent the other built-in values. Assume a semantic environment abstract data type with operations lookupEnv :: Env -> Ident -> Value and extend :: Env -> [(Ident,Value)] -> Env. The latter simultaneously adds the listed bindings, shadowing old bindings. Parameter names in one binding list are distinct, and calls have the expected arity.

Define programming closure construction separately; it does not run the body:

close :: Expr -> Env -> Value
close (Lambda xs body) rho =
  Function (\args -> eval body (extend rho (zip xs args)))

apply :: Value -> [Value] -> M Value
apply (Function f) args = f args

The four expression forms have the following semantic equations. Function position is evaluated first, followed by argument expressions from left to right:

eval :: Expr -> Env -> M Value

eval (Variable x) rho = result (lookupEnv rho x)

eval (Apply e es) rho =
  bind (eval e rho) (\f ->
    bind (evalArgs es rho) (\args -> apply f args))

eval e@(Lambda xs body) rho = result (close e rho)

eval (Let d body) rho =
  bind (defn d rho) (\rho' -> eval body rho')

evalArgs :: [Expr] -> Env -> M [Value]
evalArgs [] rho = result []
evalArgs (e:es) rho =
  bind (eval e rho) (\v ->
    bind (evalArgs es rho) (\vs -> result (v:vs)))

The two definition forms are:

defn :: Defn -> Env -> M Env

defn (Val x e) rho =
  bind (eval e rho) (\v -> result (extend rho [(x,v)]))

defn (Rec x e@(Lambda xs body)) rho = result rho'
  where
    rho' = extend rho [(x,v)]
    v = close e rho'

The ordinary definition evaluates its right-hand side in the old semantic environment; its own name is not yet bound there. The recursive definition creates a recursive closure in the extended semantic environment containing itself. Because the right-hand side is a lambda abstraction, constructing that programming closure does not evaluate its body. Haskell's lazy evaluation can tie this recursive data structure without requiring any extra fixed-point operation from the arbitrary computational monad.

Lexical scope is explicit: calling a programming closure extends the defining semantic environment, and its parameters shadow bindings in that semantic environment. The six requested constructs are therefore covered by

Variable, Apply, Lambda, Let, Val, Rec .

b

Solution

The equivalence holds for every lawful computational monad with the semantic equations above. In particular, effects in

e_{1}

are neither discarded nor evaluated twice. Fix an initial semantic environment

ρ

, and write

E = eval (e_{1}) ρ, ρ_{v} = extend (ρ, [(x, v)]), F (v) = eval (e_{2}) ρ_{v} .

Expanding Let and Val gives

eval (let val x = e_{1} in e_{2}) ρ = (E ▹ (λ v . result (ρ_{v}))) ▹ (λ ρ^{'} . eval (e_{2}) ρ^{'}) = E ▹ (λ v . result (ρ_{v}) ▹ (λ ρ^{'} . eval (e_{2}) ρ^{'})) = E ▹ F .

The two steps use associativity and left identity from the monad laws.

For the application, evaluating the lambda abstraction yields result c, where the programming closure

c

satisfies

apply (c, [v]) = F (v)

. The singleton argument evaluator reduces to

evalArgs ([e_{1}]) ρ = E ▹ (λ v . result ([]) ▹ (λ v s . result (v : v s))) = E ▹ (λ v . result ([v])) .

(3)

Use left identity to remove the initial result c, then associativity and left identity again:

eval ((lambda (x) e_{2}) e_{1}) ρ = (E ▹ (λ v . result ([v]))) ▹ (λ v s . apply (c, v s)) = E ▹ (λ v . result ([v]) ▹ (λ v s . apply (c, v s))) = E ▹ F .

(4)

Consequently,

eval (let val x = e_{1} in e_{2}) ρ = eval ((lambda (x) e_{2}) e_{1}) ρ for every lawful M .

(5)

The argument relies on the lambda abstraction itself being effect-free, as specified in part (a), and on using the same semantic environment for

e_{1}

on each side. No commutativity of effects is assumed. In particular, the proof applies to state monads, exceptions and continuation monads, not merely to the identity monad.

c

Solution

Add the abstract syntax tree alternative Fix Ident Expr. Its syntactic sugar expansion and the semantic equations from part (a) give

eval (Fix x e) ρ = eval (Let (Rec x e) (Variable x)) ρ = defn (Rec x e) ρ ▹ (λ ρ^{'} . result (lookupEnv (ρ^{'}, x))) = result (ρ^{*}) ▹ (λ ρ^{'} . result (lookupEnv (ρ^{'}, x))) = result (v),

where

ρ^{*} = extend (ρ, [(x, v)])

and

v = close (e, ρ^{*})

. The final step uses left identity from the monad laws and the lookup rule for the newly bound identifier.

Thus a direct evaluator equation is:

eval (Fix x e@(Lambda xs body)) rho = result v
  where
    rho' = extend rho [(x,v)]
    v = close e rho'

Equivalently, spelling out programming closure construction,

eval (Fix x (Lambda x s b)) ρ = result (v), v = Function (λa r g s . eval (b) (extend (ρ^{*}, zip (x s, a r g s)))) .

The result is a recursive closure, not the result of calling its body. Its self-binding is visible inside that body but does not extend the caller's surrounding semantic environment.

d

Solution

Add Fixes [Ident] [Expr] to the abstract syntax tree. For the stipulated nonempty, equally long lists of distinct names and lambda abstractions, define all programming closures against one common extended semantic environment:

eval (Fixes xs es) rho = result (head vs)
  where
    rho' = extend rho (zip xs vs)
    vs = map (\e -> close e rho') es

Expanding the auxiliary function, if

e_{i} = Lambda y s_{i} b_{i}

ρ^{*} v_{i} eval (Fixes [x_{1}, \dots, x_{n}] [e_{1}, \dots, e_{n}]) ρ = extend (ρ, [(x_{1}, v_{1}), \dots, (x_{n}, v_{n})]), = Function (λa r g s . eval (b_{i}) (extend (ρ^{*}, zip (y s_{i}, a r g s)))), = result (v_{1}) .