15–312: Principles of Programming Languages
Midterm Examination
March 9, 2017
• There are 14 pages in this examination, comprising 3 questions worth a total of 90 points.
• You may refer to your personal notes and to Practical Foundations of Programming Languages,
but not to any other person or source.
• You may use your laptop or tablet as long as you only refer to the aformentioned sources and
disable WiFi and other network connections at all times.
• You have 80 minutes to complete this examination.
• Please answer all questions in the space provided with the question.
• There are three scratch sheets at the end for your use.
Full Name:
Andrew ID:
Question: Type Safety Algebra Binary Total
Points: 30 30 30 90
15–312 Midterm 1 of 14 March 9, 2017
Question 1 [30]: System T++
After spending hours implementing the dynamics of T, Jan is frustrated with the performance
of his interpreter. He notices that running the function mod2 defined below takes about 4n
steps when applied to the numeral n. The reason is that the recursor in mod2 is evaluated n+1
flip , λ (x : nat) recx {z ↪→ s(z) | s(n) with y ↪→ z}
mod2 , λ (x : nat) recx {z ↪→ z | s(n) with y ↪→ flip(y)}
To improve the evaluation speed of T, Jan comes up with a new recursor that is supposed to
be twice as fast as the standard recursor. The resulting language is System T++: T extended
with Jan’s recursor.
Exp e ::= . . .
| jrec{e0;x.y.e1}(e) jrec e {z ↪→ e0 | s(s(x)) with y ↪→ e1} Jan’s recursor
Jan’s recursor is defined by the following extension of the statics and dynamics.
Γ ` e : nat Γ ` e0 : τ Γ, x : nat, y : τ ` e1 : τ
Γ ` jrec{e0;x.y.e1}(e) : τ
jrec{e0;x.y.e1}(e) 7−→ jrec{e0;x.y.e1}(e′)
jrec{e0;x.y.e1}(z) 7−→ e0
s(s(e)) val
jrec{e0;x.y.e1}(s(s(e))) 7−→ [e, jrec{e0;x.y.e1}(e)/x, y]e1
When Jan presents his idea at the weekly PLunch meeting, Bob is repelled by the name of the
new language. He also points out that System T++ is not even type safe.
(a) 10 points Show that System T++ is not type safe. Hint : Provide an example and show
that it violates the progress theorem or the preservation theorem.
(Question continues on the next page)
15–312 Midterm 2 of 14 March 9, 2017
(b) Even though, Bob does not believe in the future of System T++, he proposes a change
to Jan’s recursor that will make the language type safe. Bob’s version of System T++ is
defined by adding the following recursor to T.
Exp e ::= . . .
| brec{e0; e1;x.y.e2}(e) brec e {z ↪→ e0 | s(z) ↪→ e1 | s(s(x)) with y ↪→ e2} Bob’s recursor
The dynamics of Bob’s recursor is given by the following rules.
brec{e0; e1;x.y.e2}(e) 7−→ brec{e0; e1;x.y.e2}(e′)
brec{e0; e1;x.y.e2}(z) 7−→ e0
brec{e0; e1;x.y.e2}(s(z)) 7−→ e1
s(s(e)) val
brec{e0; e1;x.y.e2}(s(s(e))) 7−→ [e, brec{e0; e1;x.y.e2}(e)/x, y]e2
i. 5 points Define the statics of Bob’s recursor so that the new System T++ is type
ii. 5 points Re-implement the function mod2 exclusively using Bob’s recursor. (You are
not allowed to use the standard recursor of T in your code.)
(Question continues on next page.)
15–312 Midterm 3 of 14 March 9, 2017
iii. 10 points Prove the progress theorem for Bob’s System T++. You only have to
consider the case in which e is the recursor brec{e0; e1;x.y.e2}(e).
Theorem 1.1 (Progress). If e : τ , then either e val or e 7−→ e′ for some e′.
Hint: Recall that the proof proceeds by induction on the type derivation. You have
to consider the case in which Γ ` brec{e0; e1;x.y.e2}(e) : τ is derived by the type rule
you defined in Part i. You can use the following canonical forms lemma.
Lemma 1.2. If e : nat and e val then either
• e is z or
• e is s(e′) for an e′ such that e′ : nat and e′ val.
Hint 2: Do a case distinction on e.
15–312 Midterm 4 of 14 March 9, 2017
Question 2 [30]: Type Algebra
Two types σ and τ are isomorphic, written σ ∼= τ , iff there are two functions f : σ → τ and
g : τ → σ that are mutually inverse. In this question you are to exhibit such pairs of functions
as evidence that two types are isomorphic in T enriched with product and sum types.
Important: You must exhibit an inverse pair, but you do not have to prove that they are
(a) Exhibit the mutually inverse functions that witness each of the following isomorphisms:
i. 4 points 1× τ ∼= τ :
ii. 4 points 0 + τ ∼= τ :
(Question continues on next page.)
15–312 Midterm 5 of 14 March 9, 2017
iii. 4 points ρ× (σ + τ) ∼= (ρ× σ) + (ρ× τ):
iv. 4 points (σ1 + σ2)→ τ ∼= (σ1 → τ)× (σ2 → τ):
(Question continues on next page.)
15–312 Midterm 6 of 14 March 9, 2017
(b) In the following questions, you are to use the preceding isomorphisms. In addition, you
can use the following isomorphisms.
1. Commutativity and associativity of product and sum up to isomorphism. (For exam-
ple, σ × τ ∼= τ × σ.)
2. Each type constructor respects isomorphism in the sense that if σ1 ∼= σ2, then σ1×τ ∼=
σ2 × τ , and so on.
3. σ → (τ1 × τ2) ∼= (σ → τ1)× (σ → τ2)
4. 1→ τ ∼= τ
If applicable, state clearly which isomorphisms you apply in your reasoning by citing the
question number or the number of the previous enumeration.
Note: You are able to reason about these isomorphisms without defining new functions.
i. 4 points Recall that the type 2 is defined to be 1 + 1. Show that 2× τ ∼= τ + τ :
ii. 4 points Define τ2 to be τ × τ . Show that τ2 ∼= 2→ τ :
iii. 4 points Recall that τ opt is defined as 1 + τ . Show that (τ opt)
2 ∼= τ2 + 2× τ + 1.
(In other words, show that τ opt ∼=
τ2 + 2× τ + 1!)
(Question continues on next page.)
15–312 Midterm 7 of 14 March 9, 2017
iv. 2 points Explain in one English sentence the meaning of the preceding isomorphism.
Your answer should have the form “A pair of optional values of type τ is . . . .”
15–312 Midterm 8 of 14 March 9, 2017
Question 3 [30]: Binary Natural Numbers
The formulation of natural numbers in T uses a unary representation. In this question you are
to explore a binary representation of natural numbers based on the following idea: a natural
number is either 0, twice another natural number, 2 × n, or one more than twice a natural
number, 2 × n + 1. (Quick quiz: how is 1 to be written using this formulation of natural
Here is the statics of the type of natural numbers in binary.
Γ ` z : bin
Γ ` e : bin
Γ ` tw(e) : bin
Γ ` e : bin
Γ ` twpo(e) : bin
Γ ` e : bin Γ ` e0 : τ Γ, x : τ ` e1 : τ Γ, x : τ ` e2 : τ
Γ ` binrec{τ}(e; e0;x.e1;x.e2) : τ
The introductory forms are for zero, twice a number, and one more than twice a number. The
elimination form, correspondingly, has three cases.
Here is the (lazy) dynamics for the binary formulation of natural numbers:
z val tw(e) val twpo(e) val
binrec{τ}(e; e0;x.e1;x.e2) 7−→ binrec{τ}(e′; e0;x.e1;x.e2)
binrec{τ}(z; e0;x.e1;x.e2) 7−→ e0
binrec{τ}(tw(e); e0;x.e1;x.e2) 7−→ [binrec{τ}(e; e0;x.e1;x.e2)/x]e1
binrec{τ}(twpo(e); e0;x.e1;x.e2) 7−→ [binrec{τ}(e; e0;x.e1;x.e2)/x]e2
Defining the successor function on the binary natural numbers requires an idea similar to that
used to define the predecessor function on the unary natural numbers. The successor of 0 is
easily defined outright. The successor of 2× n+ 1 is is twice the successor of n, which we are
given by induction. But how can we compute the successor of 2× n given only n+ 1?
As with the predecessor in the unary case, the trick is to compute more: given n, compute the
pair 〈n, n+ 1〉. The desired successor is the second component, but having the first component
is helpful exactly in the awkard case just mentioned.
(Question continues on next page.)
15–312 Midterm 9 of 14 March 9, 2017
(a) i. 4 points The binary numeral n of type bin for the natural number n is given in
terms of z, tw(−) and twpo(−) amounting to the binary expansion of n. Define the
two numerals 10 and 14.
ii. 10 points Define the function succ′ : bin → (bin× bin) such that succ′(n) evalu-
ates to 〈n, n+ 1〉.
iii. 5 points Define succ : bin→ bin in terms of succ′ such that succ(n) evaluates to
(Question continues on next page.)
15–312 Midterm 10 of 14 March 9, 2017
(b) The binary numerals admit a Church representation in System F similar to that for the
unary numerals. Recall that the unary Church representation of nat is the polymorphic
type ∀(t.t→ (t→ t)→ t), which expresses the type of the iterator for each number n. The
Church representation of bin is given by the polymorphic type
∀(t.t→ (t→ t)→ (t→ t)→ t).
i. 6 points Define the introductory forms z, tw(e), and twpo(e) as elements of the
preceding polymorphic type.
• twpo(e):
ii. 5 points Define the recursor binrec{τ}(e; e0;x.e1;x.e2) in terms of the binary Church
representation.
15–312 Midterm 11 of 14 March 9, 2017
Scratch Work:
15–312 Midterm 12 of 14 March 9, 2017
Scratch Work:
15–312 Midterm 13 of 14 March 9, 2017
Scratch Work:
15–312 Midterm 14 of 14 March 9, 2017