Assignment 3: Lambda Interpreter

CS 242: Programming Languages Assignments Course Policies Guides Final Project
Assignment 3: Lambda Interpreter

In this assignment, you will implement an interpreter for a variant of the simply typed lambda calculus or as
presented in class. This will help you become more familiar with the OCaml programming language as well as the
process of writing functional interpreters for small languages, a common feature of language experimentation.
Setup
OCaml guide: OCaml setup
After setting up OCaml on your environment, copy the assignment folder.
On the Rice machines:
cp -r /afs/ir/class/cs242/assignments/assign3 assign3
On your local machine:
scp -r <SUNetID@myth.stanford.edu:/afs/ir/class/cs242/assignments/assign3 assign3
Requirements
You must implement the typechecking and interpretation stages of the interpreter. You will turn in these files:
ast.ml
typecheck.ml
interpreter.ml
You will also solve written problems in Part 4. You will submit a file solutions.pdf with your solutions.
Submitting
Then upload the files in your copy of assign3 to Rice. To submit, navigate to the assignment root and execute:
python /afs/ir/class/cs242/bin/submit.py 3
Note: We are grading tests that do not result in an error using exact text matching, and will not fix submissions
that have extra print statements or the like. It is your responsibility to test before submitting
In order to verify that your assignment was submitted, execute
ls /afs/ir/class/cs242/submissions/assign3/$USER
You should see the timestamps of your submissions.
Prelude: Modules
To understand the starter code, you will need to have a passing familiarity with one last OCaml concept: modules. For
our purposes, modules provide basically just a namespace, or a way to separate out one function from another. Here’s
λ→
an example:
module Counter = struct
type t = int
let make () : t = 0
let incr (counter : t) : t = counter + 1
let value (counter : t) : int = counter
end
let ctr : Counter.t = Counter.make ()
let ctr : Counter.t = Counter.incr ctr
print_int (Counter.value ctr)
A common convention in OCaml is that a module has a type t that represents the type associated with the module.
For example, in our starter code, we have a Term.t that represents what a term is in the code, and a Type.t for types.
In an OCaml project, each file implicitly defines a new module, where the module’s name is the same as the file’s. For
example, if I defined a file foo.ml that contained:
let do_something () = print_string "Hello"
Then from a file bar.ml in the same directory, I can run:
let () = Foo.do_something ()
You don’t need requires/imports or anything, that happens implicitly. Lastly, within our source directory, for each
.ml file we have a corresponding .mli file, where the i means “interface.” These define the type signature of the
function contained in the file (just like a .h file in C). You do not need to modify these files. We will talk more about
modules in class next week.
Language specification
You will be implementing , the simply typed lambda calculus (with a few twists). The language syntax is shown
below. The first two columns are abstract and concrete syntax, and the third column is the English name.
Grammar
Statics
λ→
τ ::=
t ::=
⊕ ::=

(τ , ) 1 τ2
(x)
(n)
(⊕, t , ) 1 t2
(x, τ, t )
′
(t , ) 1 t2





τ1 → τ2
x
n
t1 ⊕ t2
(x : τ) . t
′
t1 t2
+
−
∗
/
integer
function
variable
integer
binary operation
function
application
addition
subtraction
multiplication
division
(T-Var) (T-Int) (T-Lam)
x : τ ∈ Γ
Γ ⊢ x : τ (n) :
Γ, x : τ ⊢ t : 1 τ2
Γ ⊢ ( (x : τ1
) . t) : τ1 → τ2
(T-App) (T-Binop)
Γ ⊢ t : → Γ ⊢ : 1 τ1 τ2 t2 τ1
Γ ⊢ (t ) : 1 t2 τ2
Γ ⊢ t1
: Γ ⊢ t2
:
Γ ⊢ t1 ⊕ t2
:
Dynamics
Code overview
Before you start writing the interpreter, read through the code for the interpreter using the arithmetic language
defined in class: link. It will help you understand many of the concepts in this assignment.
Now, take a moment to familiarize yourself with all of the starter code provided. The flow of the interpreter is:
1. Raw source code enters as a string at the toplevel main.ml .
2. The source string is tokenized (lexed) into tokens in lexer.mll .
3. The tokens are parsed in parser.mly into an abstract syntax tree (AST) defined in ast.mli .
4. The AST is typechecked in typecheck.ml .
5. The AST is interpreted to produce a final result in interpreter.ml .
Each set of .ml and .mli files represent a module, with the .mli as the interface and .ml as the implementation.
For example, typecheck.mli provides the interface to the typechecker, whereas main.ml has no corresponding
interface as no other functions call the main.
Part 1: Substitution
An essential part of the lambda calculus is properly dealing with scope, binding and shadowing. This will be primarily
addressed through your implementation of variable substitution. Specifically, you will implement the following
function in ast.ml :
val substitute : Var.t - Term.t - Term.t - Term.t
This is approximate translation of substitute x t' t . The substitute function substitutes every nonshadowed instance of x (i.e. every x that is a free variable) in t with t' . Here are a few examples of substitutions:
Part 2: Typechecker
The next step is to validate that a given term is well-typed according to the statics provided above. Your goal is to
implement the typecheck function in typechecker.ml . It adheres to the following signature:
val typecheck : Term.t - (Type.t, string) Result.t
The typecheck function takes in a Term and returns a Result.t , a sum type that is either Ok(the_type) if the term
typechecks or Error(the_error) if it does not.
(D-Int) (D-Lam) (n) ( (x : τ) . t)
(D-App ) (D-App ) (D-App )
t1 ↦ t
′
1
(t1 t2 ) ↦ (t )
′
1
t2
1
t1 t2 ↦ t
′
2
(t1 t2 ) ↦ (t1 t )
′
2
2
t2
(( (x : τ) . t1 ) t2 ) ↦ [x → t2 ] t1
3
(D-Binop ) (D-Binop )
t1 ↦ t
′
1
t1 ⊕ t2 ↦ t1
′ ⊕ t2
1
t1 t2 ↦ t
′
2
t1 ⊕ t2 ↦ t1 ⊕ t
′
2
2
(D-Div) (D-Binop )
t1 / (0) (n1) ⊕ (n2) ↦ (n1 ⊕ n2)
3
[x → t ] t =
′
[x → 2] (1 + x)
[x → 2] (( (x : ) . x) x)
[x → 2] (( (y : ) . y + x) x)
= 1 + 2
= ( (x : ) . x) 2
= ( (y : ) . y + 2) 2
Again, your implementation of typecheck should mirror exactly the semantics described by the typing rules in the
language specification. You will need to carry around a typing context, a mapping from variables to types. This can be
concretely implemented using a String.Map.t , described further in code_examples.ml .
Here’s a few examples:
Part 3:Interpreter
Once you have verified that a term is well-typed, the last step is to write an interpreter in interpreter.ml that
attempts to reduce the term to a value. Your interpreter operates on small-step semantics as is given in the language
specification–that is, your core interpreter routine will reduce the term one baby step at a time. Specifically, you will
implement trystep :
type outcome =
| Step of Term.t
| Val
| Err of string
val trystep : Term.t - outcome
The trystep function attempts to take a single step on a well-typed term t strictly following the dynamics above. If
t is value then the outcome is Val . If t successfully stepped, then the outcome is Step t' where . If t is in
an error state (a divide by zero in this language), then an Err outcome should be returned.
Here’s a few examples:
trystep(Term.Int(3)) = Val (* 3 val *)
let lam = Term.Lam("x", Type.Int, Term.Int(3)) in
trystep(Term.App(lam, Term.Int(2))) = Step(Term.Int(3)) (* (fn (x : int) . 3) 2 |- 3 *)
trystep(Term.Binop(Term.Add, Term.Binop(Term.Add, Term.Int(1), Term.Int(3)), Term.Int(7)))
= Step(Term.Binop(Term.Add, Term.Int(4), Term.Int(7)))
(* (1 + 3) + 7 |- 4 + 7 *)
trystep(Term.Binop(Term.Div, Term.Int(3), Term.Int(0))) = Err("div by 0")
Part 4: Language extensions
This is the written portion of the assignment. Always eager to Move Fast and Break Things™, Will has submitted two
new potential extensions to the language above. For each extension, he wrote down the proposed statics and dynamics.
Unfortunately, only one of these extensions is type safe–the other violates at least one of progress and preservation.
Your task is to identify which extension violates these theorems and provide a counterexample, then for the other
extension provide a proof of both progress and preservation for the given rules.
First, recall from lecture the definitions of progress and preservation.
Progress: if , then either or there exists an such that .
Preservation: if and then .
The first extension adds let statements to the language, just like in OCaml:
For example, this would allow us to write:
typecheck(Term.Int(3)) = Ok(Type.Int) (* 3 : int *)
typecheck(Term.App(Term.Int(3), Term.Int(3))) = Error("something informative")
typecheck(Term.Lam("x", Type.Int, Term.Int(3))) = Ok(Type.Fn(Type.Int, Type.Int)) (* (fn (x : int) . 3) : int - in
t ↦ t
′
t : τ t t
′ t ↦ t
′
t : τ t ↦ t
′ t : τ
′
(T-Let) (D-Let)
Γ, x : τ1 ⊢ t2 : τ2
Γ ⊢ ( x : τ1 = t1 t2 ) : τ2 x : τ = t1 t2 ↦ [x → t1 ] t2
x : = 3 x + 2
The second extension adds a recursor ( rec ) to the language. A recursor is like a for loop (or more accurately a “fold”)
that runs an expression from 0 to :
Here’s a few examples of using a recursor:
If you know LaTeX, we strongly recommend that you use LaTeX to write your proofs. We have provided you a file
tex/solution.tex in which you may write your solutions. You may, however, use a word processor or handwrite your
solutions—we simply require that your submission be a PDF and legible.
Testing
To build the interpreter, run make . This will create an executable, main.native .
Running run_tests.py will run the test suite over all the files in the tests directory and compare them to our
solution.
python3 run_tests.py
Note that the tests are just a representative sample of the tests we will run your code on.
To test an individual file, you can use main.native to invoke the interpreter manually, e.g.
./main.native tests/function.lam1
For each of the functions you have to implement, we have provided a few additional unit tests inside of an
inline_tests function in each file. Uncomment the line that says:
let () = inline_tests ()
And then execute ./main.native to run those tests. If it does not fail with an assertion error, you have passed those
tests.
One last thing: we have provided you with a number of useful code examples in code_examples.ml that demonstrate
libraries/features you will find useful on the assignment that we may not have covered in-depth in class. Read through
that file before starting the assignment. It also generates a binary code_examples.native that you can modify and run.
n
(T-Rec)
Γ ⊢ t : Γ ⊢ t0
: τ Γ, x : , y : τ ⊢ t1
: τ
Γ ⊢ (t0
; x. y. t1
)(t) : τ
(D-Rec ) (D-Rec )
t ↦ t
′
(t ; x. y. )(t) ↦ ( ; x. y. )( ) 0
t1
t0
t1
t
′ 1
(t0
; x. y. t1
)((0)) ↦ t0
2
(D-Rec )
n ≠ 0
(t ; x. y. )((n)) ↦ [x → (n), y → ( ; x. y. )((n − 1))] 0 t1 t0 t1 t1
3
(0; x. y. x + y)(n)
(1; x. y. x ∗ y)(n)
= 0 + 1 + … + n
= 1 ∗ 1 ∗ 2 ∗ … ∗ n