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.

1. Finally

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

If the read_line raises an exception, the file f still gets closed.x

We add a syntax rule:

t ::= ...
      protect t1 finally t2

The term protect t1 finally t2 evaluates t1:

• If t1 evaluates to a value v1, then t2 is evaluated for its side-effects, and then the value of the whole term is v1.

• If an exception is raised while evaluating t1, then t2 is evaluated for its side-effects, and the exception propagates up.

For example,

try
  protect
    protect
      raise 0
    finally print "A"
  finally print "B"
with λx. x

should print A, then print B, then evaluate to 0.

1. Write typing rules for protect/finally. Because t2 is evaluated for its side-effects only, it should have type Unit.

2. Write evaluation rules (including any new syntax rules for E and F as needed) for protect/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

where Γ is defined as before (that is, the types of variables can’t be modified with raises).

For example:

Γ ⊢ 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

1. 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 _____

2. 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 R can have at most one type.

   Write the typing rules for raise and try (the final version on page 175).

3. Nondeterminism

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 t1, or 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

1. Define find t1 else t2 in terms of amb. Don’t worry about the possibility of nontermination.

   find t1 else t2 ≡ _____

2. 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 find to find the first branch. That is,

   find (amb [0, Ω]) else false = 0
   find (amb [Ω, 0]) else false   diverges

   Write evaluation rules for find.