The University of COMP3259: Principles of Programming Languages
Tutorial 7
Yaozhu Sun Instructor
Copyright By PowCoder代写 加微信 powcoder
12 April 2022
Table of Contents
1 Introduction
2 A Language with Recursive Functions
3 A Stack Machine
1 Introduction
This tutorial aims at providing students with experience in writing interpreters and type checkers with first-class functions and recursion. In addition, we will introduce a stack machine for evaluating expressions.
2 A Language with Recursive Functions
We now continue to improve SNH by supporting recursive definitions. For example, you may want to write a Fibonacci function as follows:
var fib = function(x: Int) { if (x == 0) 0;
else if (x == 1) 1;
else fib(x-1) + fib(x-2)
}; fib(10)
Recall that the code for evaluating non-recursive variable declarations is:
evaluate (Decl x e body) env =
let newEnv = (x, evaluate e env) : env in evaluate body newEnv
The declared variable x itself is not in the environment so it cannot be used in e. We can add support for recursion in SNH with the help of recursion in Haskell. By using a circular program, the change to variable declarations is minimal:
evaluate (Decl x e body) env =
— when evaluating `e`, use `newEnv` instead of `env` let newEnv = (x, evaluate e newEnv) : env
in evaluate body newEnv
Similarly, when type checking a variable declaration, we don’t know the type of x that may be recursively used in e:
tcheck (Decl x e body) env = do t <- tcheck e env
tcheck body ((x, t) : env)
Unfortunately, the same trick doesn’t apply here because it leads to an endless loop. To remedy this, one simple way is to give extra information to the type checker. Therefore, we slightly alter the syntax of variable declarations, that is, we require that every variable needs to be explicitly typed. For example, fib now becomes:
var fib: Int -> Int = function(x: Int) { if (x == 0) 0;
else if (x == 1) 1;
else fib(x-1) + fib(x-2)
}; fib(10)
Here we specify the type of fib as Int -> Int. It may seem tedious to write types for non-recursive declarations, but it makes type checking recursive functions much easier.
How are variable declararions type checked then? The answer is that we assume the variable to have the specified type and then check if the definition is consistent with this assumption. In the case of fib, we assume it to have type Int -> Int in the typing environment, and then call tcheck e. Since the result is indeed Int -> Int, it type checks.
Question 1. Finish type checking Decl in the file TypeCheck.hs.
Now you can recompile SNH and test if it can type check and evaluate recursive functions.
3 A Stack Machine
One disadvantage of our previous implementation of evaluation is that we make the control flow implicit. In other words, we are utilizing the semantics of the host language (Haskell) to help define the semantics of our object language (SNH). Take the evaluation
of addition for example:
evaluate (Add a b) = evaluate a + evaluate b
From the above code, we don’t know which operand (a or b) is evaluated first. This is all controlled by Haskell. Of course, the order doesn’t matter to addition (we get the same result either from left to right or from right to left). But for If expressions:
evaluate (If a b c) =
let BoolV test = evaluate a
in if test then evaluate b else evaluate c
The semantics of If in SNH tells us that either b or c is evaluated but not both. Here we are utilizing the semantics of if in Haskell to help guarantee that. But what if the Haskell compiler has a bug and evaluates both branches of if whatever the condition is? Then we are in trouble.
That’s our motivation to use a stack machine to make the control flow explicit. Java is one example of the real-world programming languages that use a stack machine for execution. The standard model is that we compile Java source code to Java bytecode, which is then interpreted by the Java virtual machine (JVM). One benefit of bytecode is that it is portable to any architecture as long as the JVM is available.
Here we introduce a different stack machine from Java called K. A state s of the K machine consists of a control stack k, which records the work remaining to be done after an instruction is executed, and a closed expression e. States are in either of the two forms:
1. An evaluation state of form k ≻ e, which corresponds to the evaluation of a closed expression e on a control stack k.
2. A return state of form k ≺ v (we use v to imply that v must be a value), which returns a value v that has been computed.
The control stack represents the context of evaluation. It records the “current location” of evaluation, where the value of the current expression is returned. A control stack k may contain control frames f as well as evaluation environments ∆:
k ::= ε | k ▷ f | k ▶ ∆
Formally speaking, a stack is either empty (ε), or a stack k plus a control frame f (k▷f),
or a stack k plus an evaluation environment ∆ (k ▶ ∆). A frames f is defined as follows:
f ::= u(−)
| o(−, e2) | o(v1, −)
| call(−, e2) | call(v1, −) | decl(x, −, e)
| if(−, e1, e2)
unary operations binary operations function calls variable declarations conditionals
A hole (denoted as −) in the top frame is intended to hold the value returned by eval- uating the current expression. It corresponds to the location in an expression where evaluation can take place. By placing a hole in an expression, we effectively specify which part to evaluate first.
We often need to get the most recent evaluation environment of a stack. This operation is denoted by ∆(k) and is recursively defined by:
∆(ε) = · ∆(k ▷ f) = ∆(k)
∆(k ▶ ∆′) = ∆′ The main judgment defining the stack machine is:
It means that state s makes a transition to state s′ in one step. An initial state of the stack machine has the form ε ≻ e, and a final state has the form ε ≺ v. To establish a relation with big-step operational semantics taught in the lectures and tutorials, we have: if·⊢e−→v,then
ε ≻ e −→ · · · −→ ε ≺ v
We begin with the rule for literals. To evaluate a literal n, we simply return it: k ≻ n −→ k ≺ n
Next, we consider the rules for unary expressions:
k ≻ u(e) −→ k ▷ u(−) ≻ e k ▷ u(−) ≺ v −→ k ≺ u(v)
To evaluate u(e), we push the frame u(−) onto the stack to record the pending unary operation and evaluate e; when a value v is returned, we calculate the result of u(v).
The rules are similar for binary expressions:
k ≻ o(e1,e2) −→ k ▷ o(−,e2) ≻ e1 k▷o(−,e2)≺v1 −→k▷o(v1,−)≻e2 k ▷ o(v1,−) ≺ v2 −→ k ≺ o(v1,v2)
To evaluate o(e1, e2), we first push the frame o(−, e2) to the stack and evaluate e1. When v1 is returned, we pop the top frame and push a new frame o(v1,−) to the stack. After e2 is evaluated, we return the result of o(v1 , v2 ). This accounts for the left-to-right evaluation order of binary expressions.
Then it comes to the rules for conditionals:
k ≻if(e1,e2,e3) −→ k ▷if(−,e2,e3) ≻ e1 k ▷if(−,e2,e3) ≺true−→ k ≻ e2
k ▷if(−,e2,e3) ≺false−→ k ≻ e3
To evaluate conditionals, we first push the frame if(−, e2, e3) to the stack and evaluate e1. If true is returned, we evaluate e2; otherwise, we evaluate e3. Note that we don’t need the help of Haskell’s if expressions, we gain the control by ourselves!
The rule for functions is as simple as that for literals:
k ≻ function(x){e} −→ k ≺ (function(x){e}, ∆(k))
We pack the most recent environment ∆(k) together with the function definition to form
a closure.
Now let’s consider the rules for function calls:
k ≻ call(e1, e2) −→ k ▷ call(−, e2) ≻ e1
k ▷call(−,e2) ≺ v1 −→ k ▷call(v1,−) ≻ e2
k ▷ call((function(x){e}, ∆), −) ≺ v2 −→ k ▶ (∆, x = v2) ≻ e
Just like our previous implementation of function calls, we first evaluate e1 and then e2. The result of evaluating e1 must be a closure. We then push the environment (∆, x = v2) to the stack and continue to evaluate the body e.
The rules for variable declarations are as follows:
k ≻decl(x,e1,e2) −→ k ▷decl(x,−,e2) ≻ e1
k ▷decl(x,−,e2) ≺ v1 −→ k ▶ (∆(k),x = v1) ≻ e2
We first push a new frame decl(x, −, e2) to the stack and evaluate the bound expression e1. Then we pop the top frame and push the environment (∆(k),x = v1) to the stack, and evaluate e2.
Finally, we have the rule for variables:
k ≻ x −→ k ≺ ∆(k)(x)
To evaluate x, we get the most recent environment ∆(k) from the stack and fetch the
value from it.
The last rule is just to repeatedly pop environments:
k ▶ ∆ ≺ v −→ k ≺ v
It takes quite a lot of time to write down all the rules! These rules will make much more sense when you try to evaluate a expression by yourself. I encourage you to do that with pen and paper before writing any code. As an example, below shows the evaluation derivation of (function(x){x + 1})(3):
−→ ε ▷ call(−, 3)
−→ ε ▷ call(−, 3)
−→ ε ▷ call((function(x){x + 1}, ·), −)
−→ ε ▷ call((function(x){x + 1}, ·), −)
−→ ε▶x=3▷+(−,1)
−→ ε▶x=3▷+(−,1)
−→ ε▶x=3▷+(3,−)
−→ ε▶x=3▷+(3,−)
≻ call(function(x){x + 1}, 3) ≻ function(x){x + 1}
≺ (function(x){x + 1}, ·)
Question 2. Write the evaluation derivation for the following expression:
var bar = 4;
var foo = function(x) { x + bar };
var bar = 8;
Now let’s turn to the implementation. To start off, we first consider the data structure for frames:
data Frame = F Op
| FBin BinaryOp (Either Value Exp)
| FIf Exp Exp
| FCall1 ()
| FCall2 ()
| FDecl ()
— TODO: Give a proper type for both kinds — of call frames
— TODO: Give a proper type for decl frames
Question 3. Replace () with proper types for call and decl frames in Interp.hs.
For the sake of convenience, we tactically make environments part of frames. That’s why we have the FEnv constructor in Frame. Then a stack is just a list of frames:
type Stack = [Frame]
States of our stack machine are represented as follows:
data State = Eval Stack Exp
| Return Stack Value
Operation ∆(k) is just a simple recursive function:
getEnv :: Stack -> Env
getEnv [] = []
getEnv (FEnv env : k) = env
getEnv (_ : k) = getEnv k
The soul of our stack machine is the step function, which specifies how one state makes a transition to another:
step :: State -> State
Question 4. Implement the step function in Interp.hs according to the rules that we
have elaborated above.
To run the stack machine, we just repeats step until it reaches the final state:
execute’ :: Exp -> Value
execute’ e = go (Eval [] e)
where go :: State -> Value go (Return [] v) = v
go s = go (step s)
Question 5. Does the K machine support recursive definitions? If so, show the evalua-
tion derivation of fib(2); if not, modify the implementation to support recursion.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com