Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 3

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 .

(1)

b

 0  0

Solution

 0  0

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} .

(1)

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 .

(2)

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

 0  0

Solution

 0  0

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),

(1)

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)))) .

(2)

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

 0  0

Solution

 0  0

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}) .

(1)

Every body can therefore call every member of the family, including itself. Constructing the family performs no body computations in the arbitrary computational monad. As in part (c), host lazy evaluation ties the recursive semantic environment; a monadic fixed-point operator is unnecessary.

For example, with two bodies implementing evenness and oddness, respectively, each programming closure sees both names in

ρ^{*}

. Returning the first programming closure still retains access to the second. Building each programming closure in an independently extended old semantic environment would lose this mutual recursion. For

n = 1

, the definition agrees with Fix.

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 3

a

Solution

b

Solution

c

Solution

d

Solution

 Ancestors (9)

 Discussion (0) New discussion

 Articles by others on the same topic (0)

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 3

 Discussion (0)  Subscribe (1) New discussion

 Discussion (0) New discussion