Homework 8: Control
- Due: 04/29 at 11:55pm
- Points: 15 (each question 5 points)
Please prepare your solutions as a PDF file (scanned handwriting is okay, but no .doc or .docx, please). Submit your PDF file in Sakai.
Some languages have a
finally keyword with which the programmer can write code that will always be evaluated, whether an exception occurs or not. A typical use-case would be closing a file:
let f = open_file "file.txt" in protect read_line f finally close_file f
read_line raises an exception, the file
f still gets closed.x
We add a syntax rule:
t ::= ... protect t1 finally t2
protect t1 finally t2 evaluates
t1evaluates to a value
t2is evaluated for its side-effects, and then the value of the whole term is
If an exception is raised while evaluating
t2is evaluated for its side-effects, and the exception propagates up.
try protect protect raise 0 finally print "A" finally print "B" with λx. x
A, then print
B, then evaluate to
Write typing rules for
t2is evaluated for its side-effects only, it should have type
Write evaluation rules (including any new syntax rules for
Fas needed) for
finally. If you make any non-obvious choices, please explain them briefly.
2. Exception types
The book defines a type
Texn for exceptions; in this exercise, we’ll extend the type system and typing rules to allow exceptions to be of any type, and to distinguish between terms that can raise exceptions and terms that can’t.
We define new syntax for a set of types that a term may raise; it can either be empty or a singleton (we won’t allow a single term to raise more than one type of exception):
R ::= ∅ T
The syntax for types is extended so that function types indicate whether the function, when applied, can raise an exception, and if so, of what type:
T ::= Nat Bool T → (T raises R)
Typing judgements are now of the form
Γ ⊢ t : T raises R
Γ is defined as before (that is, the types of variables can’t be modified with
Γ ⊢ t : Nat raises ∅ t is a Nat and can't raise Γ ⊢ t : Nat raises Bool t is a Nat and can raise a Bool Γ ⊢ t : Nat→Nat raises Bool t is a Nat→Nat when evaluated, it can raise a Bool when applied, it can't raise Γ ⊢ t : Nat→(Nat raises Bool) t is a Nat→Nat when evaluated, it can't raise when applied, it can raise a Bool
What should the typing judgements for the following terms be?
⊢ 0 : _____ raises _____ ⊢ if x then raise 0 else false : _____ raises _____ ⊢ λx:Bool. x : _____ raises _____ ⊢ λx:Bool. if x then raise 0 else false : _____ raises _____ ⊢ if x then raise 0 else λx:Bool. x : _____ raises _____
The typing rules for variables, abstractions, and applications are:
――――――― x:T ∈ Γ Γ ⊢ x:T Γ, x:T1 ⊢ t2 : T2 raises R2 ―――――――――――――――――――――――――――――――――― Γ ⊢ λx:T1. t2 : T1→(T2 raises R2) Γ ⊢ t1 : T11→(T12 raises R12) raises R1 Γ ⊢ t2 : T11 raises R2 ――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――― Γ ⊢ t1 t2 : T12 raises (R12 ∪ R1 ∪ R2)
where the union operator
∪behaves as usual; however, if the union results in more than one type, the typing derivation fails because an
Rcan have at most one type.
Write the typing rules for
try(the final version on page 175).
In class, we wrote semantics for
collect t, which evaluates to a list of the values of all branches of the computation
t. Suppose we also wanted
find t1 else t2, which evaluates to the value of the first branch of
t2 if there is none. For example:
find 0 else false = 0 find (amb [1, 2, 3]) else false = 1 find (amb ) else false = false find (amb [10, 20, 30] + amb [1, 2, 3]) else false = 11
find t1 else t2in terms of
amb. Don’t worry about the possibility of nontermination.
find t1 else t2 ≡ _____
Now consider that some branches of the computation may never terminate. If the first branch terminates but some other branch does not terminate, we still want
findto find the first branch. That is,
find (amb [0, Ω]) else false = 0 find (amb [Ω, 0]) else false diverges
Write evaluation rules for