Assignment 4:
Effects: Control and Storage
15-312: Principles of Programming Languages (Fall 2023)
This assignment will familiarize you with effects that are widely present in programming language.
Effects, or side effects are umbrella terms used to describe any computational phenomenon that is
not fully captured in the return value of an expression. Common examples of effects includes control
effects, present in its full form as continuations, and storage evaluation pertaining to mutation in
some form of storage.
We will consider to extensions to the rich expression language that we have developed.
The first extension, called KPCF, introduces the explicit manipulation of continuations. For ease
and concision of specification and implementation, we will use KPCFv, a presentation of KPCF
that uses a modal separation to distinguish values and computations. Code you write in KPCF will
be elaborated to KPCFv.
The second extension, called MA, adds constructs for storage effects. Again, we will work with a
modally-separated presentation, for meta-theoretic and implementation purposes. This will help
us to distinguish expression and commands. The latter are “instructions” that operates on the
Make sure to start early and to understand the statics and dynamics of the new languages. There
will be plenty of code to write, so don’t delay!
Submission
As usual, please submit the written part of this homework as a PDF file to Gradescope. To submit
the implementation part, submit a zipfile to Gradescope. To create the zipfile, use the Makefile
supplied in the handout. It will ensure that all the relevant files are handed in.
Reference Implementation
As always, we have included the solution to this assignment as a binary heap image. You can load it
into SML/NJ by passing in the @SMLload flag. Your solutions should behave just like ours.
Typ τ ::= cont( τ ) τ cont cont[tau]
unit unit unit
prod( τ1 ; τ2 ) τ1 × τ2 tau1 * tau2
void void void
sum( τ1 ; τ2 ) τ1 + τ2 tau1 + tau2
parr( τ1 ; τ2 ) τ1 ⇀ τ2 tau1 -> tau2
nat nat nat
α, β, . . . α, β, . . . A , B , . . .
Exp e ::= x x x
let( e1 ; x . e2 ) letx be e1 in e2 let x = e1 in e2
letcc[ τ ](x . e ) letccx in e letcc[tau] x in e
throw[ τ ]( e ; e1 ) throw e1 to e throw[tau](e, e1)
triv ⟨⟩ <>
pair( e1 ; e2 ) ⟨e1, e2⟩
split( e ; x1, x2 . e
′ ) split e asx1 ⊗ x2 in e′ split e is x1, x2 in e’
abort[ τ ]( e ) abort( e ) case[tau] e {}
in[ l ][ τ1 ; τ2 ]( e ) l · e L[tau1, tau2].e
in[ r ][ τ1 ; τ2 ]( e ) r · e R[tau1, tau2].e
case( e ; x1 . e1 ; x2 . e2 ) case e {l · x1 ↪→ e1 | r · x2 ↪→ e2} case e { L.x1 => e1 | R.x2 => e2 }
fun[ τ1 ; τ2 ]( f . x . e ) fun f(x:τ1 ):τ2 is e fun f (x : tau1): tau2 is e
λ[ τ ](x . e ) λ (x : τ ) e fn (x : tau) => e
ap( e ; e1 ) e( e1 ) e e1
s( e ) s( e ) s(e)
ifz( e ; e0 ; x . e1 ) ifz( e ; e0 ; x . e1 ) ifz e { z => e0 | s(x)=> e1 }
Figure 1.1: KPCF Grammar
In this section, we will work with KPCF, an extension of PCF with continuations. To simplify the
specification and implementation, though, we will consider KPCFv, a presentation of KPCF that
uses a modal separation to distinguish values and computations. You will be able to write code
in KPCF directly, though, which will be elaborated to KPCFv. There is no conceptual difference
between continuations in KPCFv and KPCF.
We give the grammar of KPCF in Figure 1.1.
Rather than give a statics and dynamics for KPCF, we will first elaborate to KPCFv, which we
will henceforth define.
First, we define the syntax of KPCFv in Figure 1.2. As described, we draw a syntactic distinction
between values v and computations e; this leads us to include a few new constructs:
• Expression ret( v ) treats a value as a trivial computation.
• Type comp( τ ) describes computations of type τ .
• Value comp( e ) suspends a computation.
• Expression bind( v ; x . e ) evaluates a suspended computation v, binding the resulting value
to x in e.
We also include internal forms (i.e., forms which cannot be written by programmers), such as stacks
k, reified stacks cont( k ), and evaluation states s.
Observe that the types for KPCFv contain type variables. This will allow you to write down
expressions in an upcoming subsection that do not depend on the choice of any concrete type. To
account for type variables, an KPCFv term is type-checked under a context ∆ of type variables.
For the sake of simplicity, in this assignment we will fix our typing context ∆ to be
∆0 ≜ α, β, γ, δ
and omit the ∆ from judgments. In the code, the four type variables are A , B , C , and D .
1.3 Elaboration
As mentioned, we elaborate KPCF expressions (easier for humans to write code in) to KPCFv
expressions (easier to specify and implement). We give a few cases of the translation e here,
assuming the trivial translation τ :
let( e1 ; x . e2 ) = bind( comp( e1 ) ; x . e2 )
letcc[ τ ](x . e ) = letcc[ τ ](x . e )
throw[ τ ]( e ; e1 ) = bind( comp( e ) ; xe . bind( comp( e1 ) ; xe1 . throw[ τ ](xe ; xe1 ) ) )
triv = ret( triv )
pair( e1 ; e2 ) = bind( comp( e1 ) ; xe1 . bind( comp( e2 ) ; xe2 . ret( pair(xe1 ; xe2 ) ) ) )
split( e ; x1, x2 . e′ ) = bind( comp( e ) ; xe . split(xe ; x1, x2 . e′ ) )
The remaining cases are similar and may be found in kpcf/elaborator/elaborator.sml . Ob-
serve that KPCFv requires us to sequentialize the dynamics such that the code now guarantees a
particular evaluation order.
Typ τ ::= comp( τ ) τ comp computation
cont( τ ) τ cont continuation
unit unit unit
prod( τ1 ; τ2 ) τ1 × τ2 product
void void void
sum( τ1 ; τ2 ) τ1 + τ2 sum
parr( τ1 ; τ2 ) τ1 ⇀ τ2 partial function
nat nat natural number
α, β, . . . α, β, . . . type variable
Stack k ::= ϵ empty stack
k ; x . e stack frame
Value v ::= x x variable
comp( e ) comp( e ) suspended computation
cont( k ) cont( k ) reified stack
triv ⟨⟩ unit value
pair( v1 ; v2 ) ⟨v1, v2⟩ pair value
in[ l ][ τ1 ; τ2 ]( v ) l · v left injection
in[ r ][ τ1 ; τ2 ]( v ) r · v right injection
fun[ τ1 ; τ2 ]( f . x . e ) fun f(x:τ1 ):τ2 is e recursive function
λ[ τ ](x . e ) λ (x : τ ) e non-recursive function
s( v ) s( v ) successor
Exp e ::= ret( v ) ret(v) trivial computation
bind( v ; x . e ) bind x← v in e sequential evaluation
letcc[ τ ](x . e ) letccx in e bind current continuation
throw[ τ ]( v ; v1 ) throw v1 to v throw to a continuation
split( v ; x1, x2 . e
′ ) split v asx1 ⊗ x2 in e′ pair split
abort[ τ ]( v ) abort( v ) nullary case analysis
case( v ; x1 . e1 ; x2 . e2 ) case v {l · x1 ↪→ e1 | r · x2 ↪→ e2} binary case analysis
ap( v ; v1 ) v( v1 ) function application
ifz( v ; e0 ; x . e1 ) ifz( v ; e0 ; x . e1 ) zero test
State s ::= k ▷ e evaluating e for stack k
k ◁ v returning v to stack k
Figure 1.2: KPCFv Grammar
1.4 Statics
We will have a typing judgments for each of our syntactic forms.
k ÷ τ stack k accepts a value of type τ
Γ ⊢ v : τ value v has type τ
Γ ⊢ e ∼·· τ expression e may evaluate to a value of τ
s ok state s is well-formed
x : τ ⊢ e ∼·· τ ′ k ÷ τ ′
k ; x . e ÷ τ
Notice that typing for e does not carry a context Γ with it. This is not a shorthand or a mistake:
since we evaluate only closed terms, x should be the only free variable in e. Be sure to implement
this correctly.
Γ, x : τ ⊢ x : τ
Γ ⊢ e ∼·· τ
Γ ⊢ comp( e ) : τ comp
Γ ⊢ cont( k ) : τ cont
Γ ⊢ triv : unit
Γ ⊢ v1 : τ1 Γ ⊢ v2 : τ2
Γ ⊢ pair( v1 ; v2 ) : τ1 × τ2
Γ ⊢ v : τ1
Γ ⊢ in[ l ][ τ1 ; τ2 ]( v ) : τ1 + τ2
Γ ⊢ v : τ2
Γ ⊢ in[ r ][ τ1 ; τ2 ]( v ) : τ1 + τ2
Γ, f : τ1 ⇀ τ2, x : τ1 ⊢ e ∼·· τ2
Γ ⊢ fun[ τ1 ; τ2 ]( f . x . e ) : τ1 ⇀ τ2
Γ, x : τ1 ⊢ e ∼·· τ2
Γ ⊢ λ[ τ1 ](x . e ) : τ1 ⇀ τ2
Γ ⊢ z : nat
Γ ⊢ v : nat
Γ ⊢ s( v ) : nat
Γ ⊢ e ∼·· τ
Γ ⊢ ret( v ) ∼·· τ
Γ ⊢ v : τ1 comp Γ, x : τ1 ⊢ e ∼·· τ2
Γ ⊢ bind( v ; x . e ) ∼·· τ2
Γ, x : τ cont ⊢ e ∼·· τ
Γ ⊢ letcc[ τ ](x . e ) ∼·· τ
Γ ⊢ v : τ cont Γ ⊢ v1 : τ
Γ ⊢ throw[ ρ ]( v ; v1 ) ∼·· ρ
Γ ⊢ v : τ1 × τ2 Γ, x1 : τ1, x2 : τ2 ⊢ e ∼·· τ
Γ ⊢ split( v ; x1, x2 . e ) ∼·· τ
Γ ⊢ v : void
Γ ⊢ abort[ τ ]( v ) ∼·· τ
Γ ⊢ v : τ1 + τ2 Γ, x1 : τ1 ⊢ e1 ∼·· τ Γ, x2 : τ2 ⊢ e2 ∼·· τ
Γ ⊢ case( v ; x1 . e1 ; x2 . e2 ) ∼·· τ
Γ ⊢ v : τ1 ⇀ τ2 Γ ⊢ v1 : τ1
Γ ⊢ ap( v ; v1 ) ∼·· τ2
Γ ⊢ v : nat Γ ⊢ e0 ∼·· τ Γ, x : nat ⊢ e1 ∼·· τ
Γ ⊢ ifz( v ; e0 ; x . e1 ) ∼·· τ
Notice that ret(v) is the only way to elevate a value into a computation.
k ÷ τ · ⊢ v : τ
k ÷ τ · ⊢ e ∼·· τ
Task 1.1 (20 pts). Implement the statics for KPCFv in kpcf/language/statics.sml according
to kpcf/language/statics.sig .
Remark. The functions inferTypeValue and inferTypeExp infer (synthesize) a type. However,
the function checkStack takes in a type and checks that the stack can accept values of that type.
If an erroneous situation is encountered, you should raise TypeError as usual.
1.5 Dynamics
Evaluating a KPCFv term using K Machines starts in the initial state ϵ ▷ e. The evaluation
terminates when it reaches a final state specified by the dynamics after taking a number of transition
steps. The following judgments are involved in describing the dynamics using K machines:
s 7−−→ s evaluation state taking a step
s final evaluation state is final
k ▷ ret( v ) 7−−→ k ◁ v k ▷ bind( comp( e ) ; x . e′ ) 7−−→ k ; x . e′ ▷ e
k ▷ letcc[ τ ](x . e ) 7−−→ k ▷ {cont( k )/x}e k ▷ throw[ τ ]( cont( k′ ) ; v ) 7−−→ k′ ◁ v
k ▷ split( ⟨v1, v2⟩ ; x1, x2 . e ) 7−−→ k ▷ {v1, v2/x1, x2}e
k ▷ case( l · v ; x . e1 ; x2 . e2 ) 7−−→ k ▷ {v/x1}e1
k ▷ case( r · v ; x1 . e1 ; x2 . e2 ) 7−−→ k ▷ {v/x2}e2
k ▷ ap( fun[ τ1 ; τ2 ]( f . x . e ) ; v1 ) 7−−→ k ▷ {fun[ τ1 ; τ2 ]( f . x . e ), v1/f, x}e
k ▷ ap(λ[ τ ](x . e ) ; v1 ) 7−−→ k ▷ {v1/x}e
k ▷ ifz( z ; e0 ; x . e1 ) 7−−→ k ▷ e0 k ▷ ifz( s( v ) ; e0 ; x . e1 ) 7−−→ k ▷ {v/x}e1
ϵ ◁ v final k ; x . e ◁ v 7−−→ k ▷ {v/x}e
In the dynamics, ret(v) is the only expression that causes the state to change from evaluation
mode to return mode. Also, bind( comp( e ) ; x . e′ ) is the only expression that causes a new stack
frame to be generated.
Notice how simple defining dynamics are: you only need to take care for the elimination forms.
Introduction forms are naturally taken care of through modal separation. You will also notice how
modal separation dramatically simplifies your dynamics implementation.
1.5.1 The K Machine
Before we implement the K machine, let’s run some small KPCFv examples on paper.
Consider the following expression e:
h ≜ λ[ nat→ nat ]( f . bind( comp( ap( f ; z ) ) ; x . bind( comp( ap( f ; x ) ) ; y . ret( s( y ) ) ) ) )
g[k] ≜ λ[ nat ](n . ifz(n ; ret( 10 ) ; n′ . throw[ nat ]( k ; n′ ) ) )
e ≜ letcc[ nat ]( k . ap(h ; g[k] ) )
It calls higher-order function h on function g, which conditionally returns numeral 10 or throws to
the top-level continuation.
We can evaluate e on the empty stack ϵ as follows:
ϵ ▷ letcc[ nat ]( k . ap(h ; g[k] ) )
7−−→ ϵ ▷ ap(h ; g[cont( ϵ )] )
7−−→ ϵ ▷ bind( comp( ap( g[cont( ϵ )] ; z ) ) ; x . bind( comp( ap( g[cont( ϵ )] ; x ) ) ; y . ret( s( y ) ) ) )
7−−→ k1 ▷ ap( g[cont( ϵ )] ; z )
7−−→ k1 ▷ ifz( z ; ret( 10 ) ; n′ . throw[ nat ]( cont( ϵ ) ; n′ ) )
7−−→ k1 ▷ ret( 10 )
7−−→ k1 ◁ 10
7−−→ ϵ ▷ bind( comp( ap( g[cont( ϵ )] ; 10 ) ) ; y . ret( s( y ) ) )
7−−→ ϵ ; y . ret( s( y ) ) ▷ ap( g[cont( ϵ )] ; 10 )
7−−→ ϵ ; y . ret( s( y ) ) ▷ ifz( 10 ; ret( 10 ) ; n′ . throw[ nat ]( cont( ϵ ) ; n′ ) )
7−−→ ϵ ; y . ret( s( y ) ) ▷ throw[ nat ]( cont( ϵ ) ; 9 )
7−−→ ϵ ◁ 9
where we abbreviate:
k1 = ϵ ; x . bind( comp( ap( g[cont( ϵ )] ; x ) ) ; y . ret( s( y ) ) )
Observe that ϵ ◁ 9 final, so e evaluates to 9.
Task 1.2 (10 pts). Consider the following expression e:
Lem[τ ] ≜ letcc[ τ + τ cont ]( k . bind( comp( letcc[ τ ]( k′ . throw[ τ ]( k ; r · k′ ) ) ) ; x . ret( l · x ) ) )
e ≜ bind( comp(Lem[nat] ) ; y . case( y ; n . ret(n ) ; k . throw[ nat ]( k ; 312 ) ) )
Evaluate ϵ ▷ e until it reaches a final state.
1.5.2 Implementing the K Machine
Task 1.3 (20 pts). Implement the structure Dynamics in the file kpcf/language/dynamics.sml .
Testing A REPL is available through InterpreterKPCF.repl () , in which you can directly
input KPCF expressions and see the type and the value it evaluates to. Remember your input has
to be a modal separated expression, otherwise the parser will reject your input outright. Here is
an example interaction with the interpreter:
– InterpreterKPCF.repl ();
Statics: term has type Nat
->fn (a : A) => fn (b : B) =>
Statics: term has type (Arrow (A, (Arrow (B, (Prod (A, B))))))
(Lam ((a17 , A) . (Ret (Lam ((b19 , B) . (Bind ((Comp (Ret a17)),
(tuple_e1_21 . (Bind ((Comp (Ret b19)), (tuple_e2_23 . (Ret
(Tuple (tuple_e1_21 , tuple_e2_23))))))))))))))
->letcc[unit] k in throw[unit](k, <>);
Statics: term has type Unit
A Testing harness can be accessed through TestHarness.runalltests true. It evaluates files
listed in tests/tests.sml. These test files also serves as a syntax guide.
1.6 A Continuation of Logic
Earlier in the semester, we observed that types correspond to logical propositions. We considered
a language with a type system corresponding to constructive propositional logic. Now, we explore
this correspondence in the presence of continuations, which we may interpret as refutations. Then,
the continuation type corresponds to classical negation. We recall the earlier correspondence,
extending it with continuations:
Connective Proposition φ Type φ
trivial truth ⊤ unit
conjunction φ1 ∧ φ2 φ1 × φ2
trivial falsehood ⊥ void
disjunction φ1 ∨ φ2 φ1 + φ2
implication φ1 ⊃ φ2 φ1 → φ2
negation ¬φ cont(φ )
This correspondence doesn’t quite hold in KPCF, since divergence results in an inconsistent proof
system. For example, the value
fun[ unit ; void ]( f . x . f(x) ) : unit→ void
would prove the proposition ⊤ ⊃ ⊥, which should not be the case. Therefore, we consider a subset
of KPCF in which all expressions terminate in this subsection, using τ1 → τ2 instead of τ1 ⇀ τ2.
For the tasks in this subsection, you may not use recursive functions.
You should write the following proofs using the concrete syntax of KPCF, available in the table in
Section 1.1; we will elaborate your code to KPCFv for typechecking, so you may interpret ⊢ e : τ
in KPCF as ⊢ e ∼·· τ in KPCFv. Feel free to draw inspiration from sample proofs in kpcf/tests/ .
To test your answers, you can use the function InterpreterKPCF.checkFile .
Task 1.4 (10 pts). To refute A ∨ B, you need to refute both A and B. In kpcf/refute.kpcf ,
exhibit an expression e such that:
⊢ e : cont(α )× cont(β )→ cont(α+ β )
Behavior specification: Let k be the continuation which e( ⟨k1, k2⟩ ) evaluates to. Then, throwing
l · v to k throws v to k1, and throwing r · v to k throws v to k2.
The use of continuation blurs the difference between constructive negations A ⊃ ⊥ and refutations
of A. Constructively, a value of α→ void affirms the nonexistence of values of type α, since there is
no value of type void. However, in (terminating) KPCFv, it’s possible to come up with a function
of type α→ void provided with a continuation of α:
λ ( k : α cont )λ (x : α ) throw[ void ]( k ; x ) : α cont→ (α→ void)
The continuation serves as an escape hatch for the function, saving the term from having to produce
a value of type void. This corresponds to the tautology ¬A ⊃ (A ⊃ ⊥).
Task 1.5 (10 pts). Show that the converse also holds. In kpcf/nothrow.kpcf , exhibit an expres-
sion e such that:
⊢ e : (α→ void )→ cont(α )
Behavior specification: Let k be the continuation which e( f ) evaluates to. Hypothetically, throwing
v to k would evaluate abort[α ]( v′ ), for some v′.
Task 1.6 (10 pts). Now consider the proposition (A ⊃ B) ⊃ (B ∨ ¬A). The law of excluded
middle (LEM), A∨¬A, is directly derivable from this proposition if we substitute A for B. In fact,
(A ⊃ B) ⊃ (B ∨ ¬A) is equivalent to A ∨ ¬A.
In kpcf/derivable.kpcf , exhibit an expression e of type:
⊢ e : (α→ β)→ (β + cont(α ))
Behavior specification: Suppose v is the result of evaluating e( f ) on stack k. If v = r · k′ for some
continuation k′, then throwing some v′ to k′ throws l · f( v′ ) to k.
In the lecture, we have observed it’s possible to prove the law of excluded middle (LEM) by
exhibiting a term of type τ + cont( τ ):
letcc[ τ + cont( τ ) ]( r . bind( comp( letcc[ τ1 ]( r
′ . throw (r · r′) to r ) ) ; x . l · x ) )
Task 1.7 (10 pts). Another proposition that is equivalent to LEM is known as Peirce’s law. Al-
though it’s equivalent to LEM, it does not involve negation in the formula. In kpcf/peirce.kpcf ,
exhibit an expression e of the following type that corresponds to Peirce’s law.
⊢ e : ((α→ β)→ α)→ α
Behavior specification: When applied to some function f , it returns a value of type α.
Hint: Consider how f may behave: it either returns a value of α, or it activates its argument with
a value of α. Either way, f knows a proof of α.
2 Twice Upon the MA
In the previous section we have seen a language that manipulates the control flow. The modal
separated language separates values, which does not step, from expressions, which steps and there-
fore induce a notion of control flow. This separation enables us to reify the control flow with a
stack machine, then further reify the stack as a value, enabling programs to directly program their
control flow.
In this section we will deploy the idea of modal separation once more for storage effects. Imperative
languages are known for their ability to allocate, store and mutate contents in some storage, identi-
fied colloquially by variables, but here precisely as assignables. Observe that the result of a program
is sensitive to the order of storage effects, prompting us to consider a modal separated language
between expressions, which are effect-free computations, and commands, which engenders, among
possibly others, storage effects.
In this section we will consider storage effects in two flavours: the free assignables and the scoped
assignables. The scoped assignables are assignables whose existence are tied to a scope, i.e. tied
to command they are declared in. They model the idea of a “local assignable” commonly found
in imperative languages. In contrast, free assignables are assignables that, once allocated, exists
independent of their scope of declaration. They model the idea of “heap allocation” commonly
found in languages.
In this assignment, you will explore both setups. We will start with modernized algo with free
assignables. You will implement type checking and dynamics for this calculus, then implement a
few commonly found syntax extensions for this language. You will then explore scoped assignables,
presented with an explicit control stack, borrowing ideas from KPCF. You will see that it is possible
to further extend the language to support another commonly found non-local transfer of control,
namely the exit command.
Typ τ ::= · · · · · · everything else
τ cmd τ cmd command types
Exp e ::= · · · · · · everything else
cmd(m ) cmdm encapsulated commands
Cmd m ::= ret( e ) ret e return
bnd( e ; x . m ) bndx← e ;m bind command
dcl[ τ ]( e ; a . m ) dcl a := e inm declare new assignable
get[ a ] @ a get variable
set[ a ]( e ) a := e set variable
Figure 2.1: MA Grammar
2.1 MA with free assignables
The (reduced) syntax chart for MA with free assignables is presented in Figure 2.1. The syntax
chart as presented focuses on the introduction of commands.
The language MA with free-assignable has two program syntax sort: that of expressions and that
of commands. The top-level user program will be a command.
On the expression level, expressions for sums, products, (recursive) functions, booleans and recur-
sive types are all available and standard. They are evaluated eagerly. It additionally supports
encapsulated commands (i.e. expressions containing “unevaluated” commands). This provides the
language the ability to “stage” commands in the expression layer so that they can be effected down
the line. Unlike KPCFv, values of expressions are part of expressions, as the modality distinguishes
between commands and expressions, not values and non-values (within expressions).
On the command layer, in addition to commands arising from the modal distinction, three addi-
tional commands are present: dcl[ τ ]( e ; a . m ) declares the assignable a and make it available
within m. It is important to understand that assignables themselves are in a different syntactic
then variables, in particular the command m is under an assignable binder, in other words, a is not
a variable within m. The command get[ a ] and a := e reads from the assignable a and assigns to
it with expression e respectively.
“Runtime” incarnations of commands are machines of syntax ν Σ {m ∥ µ }, where m is executing
command, Σ is the signature for already-allocated free assignables, and µ is memory mapping
assignables to expressions. The empty memory is denoted with ∅ (so is the empty signature).
Entries in the memory is syntactically delimited with the symbol “⊗”
µ ::= ∅ | µ⊗ a ↪→ ea
For example, the following memory µ0 maps assignable a to z and b to true
µ0 ≜ a ↪→ z⊗ b ↪→ true
Statics Similar to KPCFv, we will have two judgments in our static semantics: one for expres-
sions Γ ⊢Σ e : τ and one for commands Γ ⊢Σ m ∼·· τ . Both typing judgments are indexed by
the signature of assignable, mapping the name of the assignable to the type of its (expression)
The expression typing judgment states that expression e has type τ under the signature Σ. For the
expression forms that we have warmed up to, the signature is simply threaded through. To typed
encapsulated commands, one simply that encapsulated command is well-typed as a command of
type τ , which we will explain shortly after.
Γ ⊢Σ e : τ
Γ ⊢Σ m ∼·· τ
Γ ⊢Σ cmd(m ) : τ cmd
The command typing judgment states that command m, when executed under signature Σ, (if
terminates) produces a value of type τ .
Γ ⊢Σ m ∼·· τ .
Γ ⊢Σ e : τ
Γ ⊢Σ ret( e ) ∼·· τ
Γ ⊢Σ e : τ ′ cmd Γ, x : τ ′ ⊢Σ m ∼·· τ
Γ ⊢Σ bnd( e ; x . m ) ∼·· τ
Γ ⊢Σ,a~τ get[ a ] ∼·· τ
Γ ⊢Σ,a~τ e : τ
Γ ⊢Σ,a~τ set[ a ]( e ) ∼·· unit
Γ ⊢Σ,a~τ m ∼·· τ ′ Γ ⊢Σ e : τ
Γ ⊢Σ dcl[ τ ]( e ; a . m ) ∼·· τ ′
By executing a command under signature Σ, we meant the command is executed along with a
memory µ that adheres to Σ, i.e. all assignables in Σ are allocated and contains properly typed
contents. This intuition is captured in the following “machine” typing judgment.
⊢Σ ν Σ {m ∥ µ } ok
⊢Σ m ∼·· τ ∀a∈Σ( ⊢Σ µ(a) : Σ(a))
ν Σ {m ∥ µ } ok
The rules state that a machine is well-behaving if the command is well-typed under the signature of
the currently allocated assignables, and that for every entry a of the memory µ, the content of the
cell µ(a) is well-typed, again under the current signature Σ, with type specified by the signature
Dynamics When provided with user program m, the machine executes with the initial state
ν ∅ {m ∥ ∅ }, i.e. with an empty signature and memory. The final state of the machine consists of
single ret(e) where e val, regardless of the status of Σ and µ. For the machine to be final, not only
all commands are processed, the expression must also have reached a value.
ν Σ {m ∥ µ } initial ν Σ {m ∥ µ } final
ν ∅ {m ∥ ∅ } initial
ν Σ { ret(e) ∥ µ } final
Execution of the machine are defined case-by-case for each command. Commands that work on
expressions, such as ret(e) and a := e, must first evaluate their expression fully.
ν Σ {m ∥ µ } 7−−→ ν Σ′ {m′ ∥ µ′ }
ν Σ { ret( e ) ∥ µ } 7−−→ ν Σ { ret( e′ ) ∥ µ }
ν Σ {m ∥ µ } 7−−→ ν Σ {m′ ∥ µ′ }
ν Σ { bnd( cmd(m ) ; x . m1 ) ∥ µ } 7−−→ ν Σ { bnd( cmd(m′ ) ; x . m1 ) ∥ µ′ }
ν Σ { bnd( cmd( ret( e ) ) ; x . m1 ) ∥ µ } 7−−→ ν Σ { {e/x}m1 ∥ µ }
ν Σ { bnd( e ; x . m′′ ) ∥ µ } 7−−→ ν Σ { bnd( e′ ; x . m′′ ) ∥ µ }
ν Σ, a ~ τ { get[ a ] ∥ µ⊗ a ↪→ e } 7−−→ ν Σ, a ~ τ { ret( e ) ∥ µ⊗ a ↪→ e }
ν Σ, a ~ τ { set[ a ]( e ) ∥ µ } 7−−→ ν Σ, a ~ τ { set[ a ]( e′ ) ∥ µ }
ν Σ, a ~ τ { set[ a ]( e ) ∥ µ⊗ a ↪→ e′ } 7−−→ ν Σ, a ~ τ { ret( ⟨⟩ ) ∥ µ⊗ a ↪→ e }
ν Σ { dcl[ τ ]( e ; a . m ) ∥ µ } 7−−→ ν Σ { dcl[ τ ]( e′ ; a . m ) ∥ µ }
ν Σ { dcl[ τ ]( e ; a . m ) ∥ µ } 7−−→ ν Σ, a ~ τ {m ∥ µ⊗ a ↪→ e }
One notable command is that of dcl a := e in m. This commands after evaluating the principal
expression to a value, allocates a new assignable in the signature and memory. Once allocated,
the assignable exists “permanently”, even when the encapsulated command returns. This allows
references to the allocated assignable to escape it’s intended scope, setting the assignable free.
Implementation In this part you will complete a partial implementation of the language. We
have provided type checker and stepping for expressions. You will need to implement the statics
and dynamics of the language
Task 2.1 (20 pts). Implement the typechecker for MA with free assignables in the structure
StaticsMA in ma/statics_ma.sml according to ma/statics_ma.sig . In particular we have
implemented the statics for expressions, so you only need to implement that of commands.
Programming in plain MA quickly becomes unwieldy. To ease the pain, the implementation pro-
vides the following syntactical conveniences:
• ifm (m ) then {m1} else {m2}: Conditional command, which executesm for bool and branch.
• while (m ){m1}: Loop command, which executes m1 until test in m fails.
• m1 ;m2: Sequencing command, which execute m1 and m2 sequentially.
• ignore (m ): “ignore” command, which runs the command and throws away the result.
Typing judgments for these short-hands are provided as follows. The loop command has type unit
because it is possible that the loop body never executes.
Γ ⊢Σ m ∼·· bool Γ ⊢Σ m1 ∼·· τ Γ ⊢Σ m2 ∼·· τ
Γ ⊢Σ ifm (m ) then {m1} else {m2} ∼·· τ
Γ ⊢Σ m ∼·· bool Γ ⊢Σ m1 ∼·· unit
Γ ⊢Σ while (m ){m1} ∼·· unit
Γ ⊢Σ m1 ∼·· unit Γ ⊢Σ m2 ∼·· τ
Γ ⊢Σ m1 ;m2 ∼·· τ
Γ ⊢Σ m ∼·· τ
Γ ⊢Σ ignore (m ) ∼·· unit
Task 2.2 (20 pts). Desugar these syntax conveniences into commands of our language in
ma/parser/desugar.sml according to ma/parser/desugar.sig . Implement the command dy-
namics for MA with free assignables in the structure DynamicsMA in ma/dynamics_ma.sml .
The parser will use your version of Desugar to parse the concrete syntax, so you will not be able
to run MA code until you have implemented the desugaring functions.
To help you program in MA, we provide some other syntactic sugars, which are explained in
Appendix A. Concrete syntax is also explained in Appendix A. We also provide you a set of test
cases in ma/tests/basic and ma/tests/large .
Task 2.3 (10 pts). Implement the following functions in MA using concrete syntax. Your solution
shouldn’t be recursive and should use MA features.
1. In ma/tests/tasks/collatz.ma , implement collatz : nat -> cmd[nat] such that collatz n
returns the number of steps it takes to reach 1 when starting from n and repeatedly applying
the following rule: if n is even, divide it by 2. If n is odd, multiply it by 3 and add 1. For
example, collatz 27 should return 111.1
2. In ma/tests/tasks/gcd.ma , implement gcd : nat -> nat -> cmd[nat + unit] such
that gcd m n returns the greatest common divisor of m and n when defined. Great-
est common divisor of 0 and 0 is undefined and should return right of unit. For example,
gcd 4 6 should return 2 injected to the left.
You might recall similar implementation of those functions in language like C as 2.2.
int collatz(int n) {
int count = 0;
while (n != 1) {
if (n % 2 == 0) {
n = n / 2;
n = 3 * n + 1;
count = count + 1;
return count;
int gcd(int m, int n) {
if (m == 0 && n == 0) {
while (n != 0) {
int r = m % n;
Figure 2.2: collatz and gcd in C
Testing As usual, you can test your code using InterpreterMA . We provide a set of test cases
for collatz and gcd in ma/tests/test.ma . For example:
– InterpreterMA.repl ();
->ret (1);
->local a := 1 in { set a := 2 , get a };
https://en.wikipedia.org/wiki/Collatz_conjecture
https://en.wikipedia.org/wiki/Collatz_conjecture
– InterpreterMA.evalFile “large/sum.ma”;
(Num 10000)
val it = () : unit
2.2 MA with scoped assignables
Alternative to assignables being free, they can be alternatively be scoped. The existence of a scoped
assignable is tied to the “block” that the assignable is declared in. The assignable is created when
we enter the scope, and it is de-allocated when we exit it. The number of assignables allocated at
a time increases as we drill down into sub-commands, and decreases when we come back up.
Therefore, it is a common design to tie the scoped assignable to the control stack, as exemplified by
the C-family languages. Scoped assignables are colloquially referred to as stack-allocated assignable
for this reason. In principle, the assignables do not have to be allocated literally “on the stack”, as
in occupying control stack spaces.
In this exercise, we will examine this common design choice, by first taking inspiration from KPCF
and make explicit the control stack of MA with scoped assignables. We will see how this design
presents us intricate proofs of safety. We will then extend the language with a new command
that resembles a throw expression, performing a non-local transfer of control. However, this new
command must respect the scoped assignable allocation scheme, which leads to an interesting
Typ τ ::= · · · · · · everything else
Exp e ::= · · · · · · everything else
Cmd m ::= · · · · · · everything else
Stack k ::= ϵ ϵ empty stack
k ; bnd( − ;x . m ) k ; bnd( − ;x . m ) sequenced command
k ; dcl[ a ] k ; dcl[ a ] allocation frame
Mach M ::= ν Σ { k ▷ m ∥ µ } ν Σ { k ▷ m ∥ µ } machine evaluates
ν Σ { k ◁ e ∥ µ } ν Σ { k ◁ e ∥ µ } m