Assignment 4: Type Extensions

CS 242: Programming Languages Assignments Course Policies Guides Final Project
Assignment 4: Type Extensions

Now that you’ve got some interpeter experience under your belt, it’s time to take your language to the next level. In this
assignment, you will implement an interpreter for the exciting simply typed lambda calculus, or (a name of my
own invention). Specifically you will extend our previous language with algebraic data types, pattern matching and
polymorphic/existential types.
Setup
Setup is same as always—copy the assignment folder out of our folder on Rice.
On the Rice machines:
cp -r /afs/ir/class/cs242/assignments/assign4 assign4
On your local machine:
scp -r <SUNetID@rice.stanford.edu:/afs/ir/class/cs242/assignments/assign4 assign4
Requirements
You must implement the translation, typechecking, and interpretation stages of the interpreter. You wll turn in these
files:
translator.ml
typechecker.ml
interpreter.ml
There are no written portions to this assignment.
Submitting
Then upload the files in your copy of assign4 to Rice. To submit, navigate to the assignment root and execute:
python /afs/ir/class/cs242/bin/submit.py 4
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
Language specification
Adding algebraic datatypes, pattern matching, and first-order type logic to our language introduces a substantial level
of complexity in both the language and its implementation. A common technique for mitigating complexity in
language implementation is to use intermediate representations (IRs), or mini-languages internal to the interpreter. For
our language , we have the top-level language defined by what the programmer will write as well an IR for our
typechecker and interpreter.
First, we will examine the grammar for our new language. Specifically, we have added new types:
and the corresponding terms necessary to implement those types. These are precisely
λ→!
λ→
λ→!
, , ,
the same formulations as we discussed in class. Additionally, this language introduces pattern matching, a restricted
version of the match clause you’ve used in OCaml.
As a refresher from lecture, “injects” the term as the left or right side of the sum type , depending on what
is. and are similar to and except that they operate on types, and not terms. That means maps
a variable name to a type and not a term . expects a type as an argument for some .
, , and are intimately related. is always used with the type . states that
there exists a type that looks like the type . This essentially allows us to define abstract interfaces. , “packs” a
concrete implementation of some type into some existential type . allows us to retrieve the concrete
implementation.
As mentioned, all of the rules for algebraic data types and first order type logic mirror the semantics discussed in class,
so refer back to those notes for more details. The pattern matching mechanism is novel, however, as this is the first
time we will give it a formal treatment. Here’s a few examples using patterns in this language:
τ ::=
t ::=
ρ ::=
⊕ ::=
d ::=
(X)

(τ , ) 1 τ2
(τ , ) 1 τ2
(τ , ) 1 τ2
(X, τ)
(X, τ)
(x)
(n)
(⊕, t , ) 1 t2
(x, τ, t)
(t , ) 1 t2
(t , ) 1 t2
(t, d)
(t, d, τ)
(X, t)
(t, τ)
(τ , t, ) 1 τ2
(ρ, t , ) 1 t2
(t, (ρ , ), ( , )) 1 t1 ρ2 t2

(x, τ)
(ρ, x, τ)
(ρ , ) 1 ρ2
(X, x)






X

τ1 → τ2
τ1 ∗ τ2
τ1 + τ2
∀X. τ
∃X. τ
x
n
t1 ⊕ t2
(x : τ) . t
t1 t2
(t , ) 1 t2
t. d
t = d τ
X . t
t [τ]
{τ1
, t} τ2
ρ = t1 t2
t { ρ1 ↪ t1
∣ ρ2 ↪ t2 }
--
x : τ
ρ x : τ
(ρ , ) 1 ρ2
{X, x}
+
−
∗
/
L
R
variable
integer
function
product
sum
forall
exists
variable
integer
binary operation
function
application
tuple
projection
injection
type function
type application
type abstraction
let
match
wildcard
variable binding
alias
tuple
type unpack
addition
subtraction
multiplication
division
t τ d

τ t τ

X τ
τ1 τ2
( x : = 2 1 + x) ⟹ 3
( (a : , b : ) c : ∗ = (1, 2) a + b + c. L) ⟹ 4
( ( (1, 2) = L ( ∗ ) + ) { (a : , b : ) ↪ a + b ∣ c : ↪ c }) ⟹ 3
If we wanted to, we could stop here and define a full statics and semantics for the language above. However, we need
not to, since we can translate some parts of the language into other. Specifically, we will eliminate pattern matching in
a translation pass. For example, we could define the following translation of a tuple match (where means “translates
to”):
To formalize this translation, we will first define a grammar for a new IR:
This IR has three differences from the top-level:
1. Patterns are removed entirely.
2. TUnpack has moved from Pattern to Term .
3. Match has been replaced by Case .
In terms of the code, the first grammar corresponds to the Lang module in ast.ml , whereas the second corresponds
to the IR module.
Part 1: Translator
Your first job is to implement the translation function in translator.ml :
val translate : Lang.Term.t - IR.Term.t
⇝
(a : , b : ) c : (, ) = (1, 2) a + b ⇝
( (a : ) . ( (b : ) . ( (c : ∗ ) . a + b) (1, 2)) (1, 2). R) (1, 2). L
τ ::=
t ::=
⊕ ::=
d ::=
(X)

(τ , ) 1 τ2
(τ , ) 1 τ2
(τ , ) 1 τ2
(X, τ)
(X, τ)
(x)
(n)
(⊕, t , ) 1 t2
(x, τ, t)
(t , ) 1 t2
(t , ) 1 t2
(t, d)
(t, d, τ)
(t, (x , ), ( , )) 1 t1 x2 t2
(X, t)
(t, τ)
(τ , t, ) 1 τ2
(X, x, t , ) 1
t2






X

τ1 → τ2
τ1 ∗ τ2
τ1 + τ2
∀X. τ
∃X. τ
x
n
t1 ⊕ t2
(x : τ) . t
t1 t2
(t , ) 1 t2
t. d
t = d τ
t { x1 ↪ t1
∣ x2 ↪ t2 }
X . t
t [τ]
{τ1
, t} τ2
{X, x} = t1 t2
+
−
∗
/
L
R
variable
integer
function
product
sum
forall
exists
variable
integer
binary operation
function
application
tuple
projection
injection
case
type function
type application
type abstraction
type open
addition
subtraction
multiplication
division
This function takes a term of the top-level language Lang.Term.t and converts it into an IR.Term.t . It cannot fail, so
we do not return a Result.t .
The translation is largely trivial for most of the language as the only major difference is the Lang.Term.Let and
Lang.Term.Match cases. We have implemented all of the trivial cases as well the Match case for you.
We can formalize the Let and Match translations by defining a series of translation rules:
Look at Match for an example of implementing one of these translation rules. After implementing these rules, you will
have a complete pipeline to move from source code to your IR.
Note: if we wanted to formally verify our translation rules, we could define a dynamics for both the toplevel Lang
and the IR , and then prove that for all that if in Lang and then implies that
.
Part 2: Typechecker
Your next task is to implement a typechecker for the IR. Because we decided to translate before typechecking, this will
reduce the complexity of the typechecker (although this will obscure type errors–it’s a tricky business to match a type
error on generated code back to the original source).
The format of the typechecker is the mostly same as the previous assignment, but now the type system is more
complex. The statics are:
(Tr-let ) (Tr-let )
t2 ⇝ t
′
2
-- = t1 t2 ⇝ t
′
2
1
t1 ⇝ t1
′ t2 ⇝ t
′
2
x : τ = t ⇝ ( (x : τ) . ) 1 t2 t
′
2
t
′
1
2
(Tr-let ) (Tr-let )
t1 ⇝ t1
′ ρ = t1 t2 ⇝ t
′
ρ x : τ = t ⇝ ( (x : τ) . ) 1 t2 t
′ t
′
1
3
( ρ1 = t1
. L ρ2 = t1
. R t2
) ⇝ t
′
(ρ1
, ρ2
) = t1 t2 ⇝ t
′ 4
(Tr-let )
t1 ⇝ t1
′ t2 ⇝ t
′
2
{X, x} = t1 t2 ⇝ {X, x} = t
′ 1
t
′
2
5
(Tr-match)
t ⇝ t
′ ρ1 = x1 t1 ⇝ t1
′ ρn = x2 t2 ⇝ t
′
2
t { ρ1 ↪ t1
∣ ρ2 ↪ t2 } ⇝ t { ↪ ∣ ↪ }
′ x1 t
′
1 x2 t
′
2
t : τ tL ⇒ t
′
L
tL ⇝ tIR tIR ⇒ t
′
IR
tL
′ ⇝ t
′
IR
(T-var) (T-n) (T-fn) Γ, x : τ ⊢ x : τ (n) :
Γ, x : τ ⊢ t : 1 τ2
Γ ⊢ ( (x : τ1
) . t) : τ1 → τ2
(T-app) (T-tuple)
Γ ⊢ t : → Γ ⊢ : 1 τ1 τ2 t2 τ1
Γ ⊢ (t ) : 1 t2 τ2
Γ ⊢ t : Γ ⊢ : 1 τ1 t2 τ2
Γ ⊢ (t1
, t2
) : τ1 ∗ τ2
(T-project-L) (T-project-R)
Γ ⊢ t : τ1 × τ2
Γ ⊢ t. L : τ1
Γ ⊢ t : τ1 × τ2
Γ ⊢ t. R : τ2
(T-inject-L) (T-inject-R)
Γ ⊢ t : τ1
Γ ⊢ t = L τ1 + τ2
: τ1 + τ2
Γ ⊢ t : τ2
Γ ⊢ t = R τ1 + τ2
: τ1 + τ2
(T-case)
Γ ⊢ t : τ1 + τ2 Γ, x1
: τ1 ⊢ t1
: τ Γ, x2
: τ2 ⊢ t2
: τ
Γ ⊢ t { x1 ↪ t1
∣ x2 ↪ t2 } : τ
(T-tfn) (T-tapp) (T-pack)
Γ, X ⊢ t : τ
Γ ⊢ X . t : ∀X. τ
Γ ⊢ t : ∀X. τ1
Γ ⊢ t [τ ] : [X → ] 2 τ2 τ1
Γ ⊢ t : [X → τ ] 1 τ2
Γ ⊢ {τ , t} ∃X. : ∃X. 1 τ2 τ2
(T-unpack)
Γ ⊢ t : ∃X. Γ, X, x : ⊢ : 1 τ1 τ1
t2 τ2
Γ ⊢ {X, x} = t : 1
t2 τ2
There are two major additions: sum/product types and polymorphic/existential types. Typechecking the former is
straightforwardly derived from the rules like from the previous assignment, but the latter introduces a new concept:
type variables. Now, your typing context keeps track of two things:
1. Mappings from term variables to types, notated by . This is as before used for when term variables are
introduced by lambdas, or here also case expressions.
2. Existence of type variables, notated by . Type variables do not map to anything, the context just tracks
when a type variable is in scope (to catch type expressions that use an undefined type variable).
Concretely, you will implement the following function:
val typecheck_term : String.Set.t - Type.t String.Map.t - Term.t - Type.t
Where typecheck_term type_env env t returns the type of t if it exists. Note that instead of using a Result.t , this
time you can use a simpler approach: whenever a type error occurs, you should raises a TypeError exception, e.g.
raise (TypError "Does not typecheck") , with the appropriate error message. Otherwise, assume that when you call
typecheck_term recursively you get back a valid type.
Here, env is the same mapping from variables to types as in the previous assignment, but we have added tenv which
is a set of type variables. Type variables do not map to anything (they do not themselves have types), but instead just
provide the context that a type variable is in scope during typechecking of an expression.
We have provided you a function typecheck_type : String.Set.t - Type.t - Type.t . Whenever you’re typechecking a
term that contains a type specified by the user, for example the type annotation on a function or an injection, you will
need to check that the provided type does not use unbound type variables. For example, the following expression
should not typecheck because is unbound:
Lastly, during typechecking, there will be points where you will want to compare the equality of two types. Do not use
the equals operator (e.g. tau1 = tau2 ) as that would be incorrect! Use the Type.aequiv function that compares two
types for equality up to renaming of bound variables, or check them for alpha-equivalence. For example, the types
and should be considered equal, however the = operator will return false because the variable names are
different. Type.aequiv has the signature Type.t - Type.t - bool .
Note: Technically, it’s possible for match statements to introduce variables that are already free variables in the
expression, which is not legal. However, for the sake of this assignment, assume that match statements will always
use fresh variables. That is, variables introduced in cases will not be found elsewhere in the expression.
Part 3:Interpeter
Lastly, you must implement the interpreter. At this point, all of the terms relating to type abstraction
(polymorphic/existential types) have trivial dynamics, since we’ve already verified our required type properties in the
typechecker. Most of the legwork is in supporting algebraic data types. The dynamics are as follows:
Γ, x : τ ⊢ e : τ
Γ, X ⊢ e : τ
Y
X . (x : Y) . x
∀X. X ∀Y. Y
As in the previous assignment, you will implement these dynamics in the trystep function in interpreter.ml :
val trystep : Term.t - outcome
The dynamics for Int and Var as well as the dynamics for the polymorphic/existential cases are done for you.
Testing
To build the interpreter, run make . This will create an executable, main.byte . This creates OCaml bytecode that needs
to passed to ocamlrun to execute. We’ve provided two scripts user.sh and solution.sh for main.byte and
solution.byte respectively.
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 user.sh to invoke the interpreter manually, e.g.
./user.sh tests/exists1.lam2
(V-n) (V-fn) (D-app ) (D-app ) (n) ( (x : τ ) . e) 1
t1 ↦ t
′
1
(t ) ↦ ( ) 1 t2 t
′
1
t2
1
t1 t2 ↦ t
′
2
(t ) ↦ ( ) 1 t2 t1 t
′
2
2
(D-app ) (D-binop ) (D-binop )
t 2
(( (x : τ) . t ) ) ↦ [x → ] 1 t2 t2 t1
3
t1 ↦ t
′
1
t1 ⊕ t2 ↦ t1
′ ⊕ t2
1
t1 t2 ↦ t
′
2
t1 ⊕ t2 ↦ t1 ⊕ t
′
2
2
(D-div) (D-binop )
t / (0) 1 (n ) ⊕ ( ) ↦ ( ⊕ ) 1 n2 n1 n2
3
(D-tuple ) (D-tuple ) (D-tuple )
t1 ↦ t
′
1
(t , ) ↦ ( , ) 1
t2
t
′
1
t2
1
t1 t2 ↦ t
′
2
(t , ) ↦ ( , ) 1
t2
t1
t
′
2
2
t 1
t2
(t , ) 1
t2
3
(D-project ) (D-project ) (D-project )
t ↦ t
′
t. d ↦ t . d
′ 1
(t , ) 1
t2
(t1
, t2
). L ↦ t1
2
(t , ) 1
t2
(t1
, t2
). R ↦ t2
3
(D-inject ) (D-inject )
t ↦ t
′
t = d τ ↦ t = d τ
′ 1
t
t = d τ
2
(D-case )
t ↦ t
′
t { x1 ↪ t1
∣ x2 ↪ t2 } ↦ t { ↪ ∣ ↪ }
′ x1
t1 x2
t2
1
(D-case )
t
t = L τ { x ↪ ∣ ↪ } ↦ [ → t] 1 t1 x2 t2 x1 t1
2
(D-case )
t
t = R τ { x ↪ ∣ ↪ } ↦ [ → t] 1 t1 x2 t2 x2 t2
3
(D-tfn) (D-tapp) (D-pack) X . t ↦ t t [τ] ↦ t {τ , t} ↦ t 1 τ2
(D-unpack)
{X, x} = t ↦ [x → ] 1
t2
t1
t2
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 ./user.sh to run those tests. If it does not fail with an assertion error, you have passed those tests.