# 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 t
```_{1} finally t_{2}

The term `protect t`

evaluates _{1} finally t_{2}`t`

:_{1}

If

`t`

evaluates to a value_{1}`v`

, then_{1}`t`

is evaluated for its side-effects, and then the value of the whole term is_{2}`v`

._{1}If an exception is raised while evaluating

`t`

, then_{1}`t`

is evaluated for its side-effects, and the exception propagates up._{2}

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`

.

Write typing rules for

`protect`

/`finally`

. Because`t`

is evaluated for its side-effects only, it should have type_{2}`Unit`

.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 `T`

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._{e}_{x}_{n}

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
```

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:T`

_{1}⊢ t_{2}: T_{2}raises R_{2}―――――――――――――――――――――――――――――――――― Γ ⊢ λx:T_{1}. t_{2}: T_{1}→(T_{2}raises R_{2}) Γ ⊢ t_{1}: T_{1}_{1}→(T_{1}_{2}raises R_{1}_{2}) raises R_{1}Γ ⊢ t_{2}: T_{1}_{1}raises R_{2}――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――― Γ ⊢ t_{1}t_{2}: T_{1}_{2}raises (R_{1}_{2}∪ R_{1}∪ R_{2})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 t`

, which evaluates to the value of the _{1} else t_{2}*first* branch of `t`

, or _{1}`t`

if there is none. For example:_{2}

```
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
```

Define

`find t`

in terms of_{1}else t_{2}`amb`

. Don’t worry about the possibility of nontermination.`find t`

_{1}else t_{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`

.