CS 225: Programming Languages UVM, Spring 2018
Written Portion (25 Points)
Consider the language of arithmetic expressions, described in the book in chapters 3 and 8, as well as at the end of this assignment in the section titled “Reference: Arithmetic Expressions”.
Also consider the following expression definitions:
e1 :=0 e2 :=F e3 :=predT e4 :=iszero(pred0) e5 :=ifTthen(succ0)else0 e6 :=ifTthenFelse0
Problem 1 (15 Points)
For each of the expressions ei, either:
(1) Identify a type τ such that ei : τ and give the full typing derivation of ei : τ OR
(2) Write “untypeable” if there is no τ such that ei : τ
Problem 2 (10 Points)
Recall the definitions of unsafe and safe expressions:
Definition 1. An expression e is unsafe if and only if there exists some e′ such that: (1) e −→∗ e′, (2) e′ is
not a value, and (3) there does not exist any e′′ such that e′ −→ e′′. Definition 2. An expression e is safe if and only if it is not unsafe.
Write an expression e such that e is safe, but where e is not typeable, that is, there does not exist any τ such that e : τ.
Programming Portion (75 Points)
Follow the directions posted on the course website for installing OCaml and required packages.
Download hw3.zip from the course webpage and extract it to a folder on your machine. Ensure that you are able to run the following commands from the directory without error:
> make > make hw3
Running make should print out a log of compiling various OCaml files. Running make hw3 should run a bunch of tests, and report that 5 passed, 0 failed, and 15 are still “todo”. In order for the merlin plugin to work, you must first run make.
Your assignment is to complete the definitions of free_vars and infer to handle the following extensions to the simply typed lambda calculus: (1) the empty type, (2) the unit type, (3) the sum type, and (4) the product type. These extensions are described in the book in Chapter 11, and are also included for reference at the end of this assignment in the section titled “Reference: Extended Simply Typed Lambda Calculus”.
Look in the assignment file for raise TODO expressions and replace them with your solution. To help you, the corresponding mathematics for each of these definitions are shown in comments.
At the end of hw3.ml is a test suite which will test your functions on a few test cases. Feel free to add your own tests. Just because you pass the provided tests doesn’t guarantee your solution is correct.
CS 225: Programming Languages
UVM, Spring 2018
Reference: Arithmetic Expressions
Syntax for simple arithmetic expressions, types and values:
Small-step semantics:
e ::= T | F | if e then e else e
| 0|succe|prede|iszeroe
τ ::= bool | nat nv ::= 0 | succ nv
v ::= T | F | nv
e −→ e
ifTthene2 elsee3 −→e2 e1 −→ e′1
ife1 thene2 elsee3 −→ife′1 thene2 elsee3 e −→ e′
ifFthene2 elsee3 −→e3
e −→ e′
succe−→succe′ pred0−→0
iszero (succ nv) −→ F
pred (succ nv) −→ nv
pred e −→ pred e′
e −→ e′
Type system:
T:bool
F:bool
e1 :bool e2 :τ e2 :τ
ife1 thene2 elsee3 :τ 0:nat
e : nat iszero e : bool
e:nat succe:nat
e:nat prede:nat
iszero 0 −→ T iszero e −→ iszero e′
e:τ
CS 225: Programming Languages
UVM, Spring 2018
Reference: Extended Simply Typed Lambda Calculus
Syntax for extended simply typed lambda calculus expressions, types and values:
e ::= T | F | if(e){e}{e} | x|λx:τ.e|e1 e2 | absurd(e) as τ |•
- | inl(e) as τ | inr(e) as τ | case(e){x.e}{x.e}
- | ⟨e, e⟩ | projl(e) | projr(e)τ ::= bool | τ ⇒ τ | empty | unit | τ + τ | τ × τ Free variables metafunction:
Type system:
Γ ⊢ T : bool x:τ1,Γ⊢e:τ2
Γ⊢e2 :τ Γ⊢e:empty
Γ⊢absurd(e):τ Γ ⊢ e : τ2
x:τ ∈Γ Γ ⊢ x : τ
Γ⊢•:unit
FV ∈ exp → P(var) FV(T) := {}
FV(F) := {}
FV(if(e1){e2}{e3}) := FV(e1) ∪ FV(e2) ∪ FV(e3) FV(x) := {x}
FV(λx : τ.e) := FV(e) \ {x} FV(e1 e2) := FV(e1) ∪ FV(e2)
FV(absurd(e) as τ) := FV(e) FV(•) := {}
FV(inl(e) as τ) := FV(e)
FV(inr(e) as τ) := FV(e)
FV(case(e1){x2.e2}{x3.e3}) := FV(e1) ∪ (FV(e2) \ {x2}) ∪ (FV(e3) \ {x3})
FV(⟨e1, e2⟩) := FV(e1) ∪ FV(e2) FV(projl(e)) := FV(e) FV(projr(e)) := FV(e)
Γ⊢e:τ
Γ⊢e1 :bool Γ⊢e2 :τ
Γ ⊢ F : bool Γ ⊢ if(e1){e2}{e3} : τ
Γ⊢e1 :(τ1 ⇒τ2) Γ⊢e2 :τ1 Γ⊢(e1 e2):τ2
Γ⊢(λx:τ1.e):(τ1 ⇒τ2)
Γ ⊢ e : τ1
Γ ⊢ inl(e) as (τ1 + τ2) : (τ1 + τ2) Γ⊢e1 :(τ2 +τ3) x2 :τ2,Γ⊢e2 :τ
Γ ⊢ inr(e) as (τ1 + τ2) : (τ1 + τ2)
x3 :τ3,Γ⊢e3 :τ Γ⊢e1 :τ1 Γ⊢e2 :τ2
Γ ⊢ case(e1){x2.e2}{x3.e3} : τ
Γ⊢e:(τ1 ×τ2) Γ ⊢ projl(e) : τ1
Γ ⊢ ⟨e1, e2⟩ : (τ1 × τ2) Γ⊢e:(τ1 ×τ2)
Γ ⊢ projr(e) : τ2