Homework 5: Effects

  • Due: Wednesday 12/07 at 11:59pm
  • Points: 30

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. Mutable lists

Assume simply-typed λNB with pairs, recursive types (μ) and references (ref, !, and :=).

In Scheme, set! corresponds roughly to :=. It also has set-car! and set-cdr!, which can be used to modify lists:

> (define l (list 1 2 3))
> (set-car! l 4)
> l
(4 2 3)
> (set-cdr! l (list 5 6))
> l
(4 5 6)
  1. Define (in simply-typed λNB with the extensions listed above) a type MutableNatList and associated functions:

      nil' : MutableNatList
     cons' : Nat  MutableNatList  MutableNatList
      car' : MutableNatList  Nat
      cdr' : MutableNatList  MutableNatList
    setcar : MutableNatList  Nat  Unit
    setcdr : MutableNatList  MutableNatList  Unit

    They should satisfy the following equations:

    car' nil'        = 0
    car' (cons' x y) = x
    cdr' nil'        = nil'
    cdr' (cons' x y) = y
    (let l = cons' x y in setcar l x'; car' l) = x'
    (let l = cons' x y in setcar l x'; cdr' l) = y
    (let l = cons' x y in setcdr l y'; car' l) = x
    (let l = cons' x y in setcdr l y'; cdr' l) = y'
    (let l = nil' in setcar l x'; l) = nil'
    (let l = nil' in setcdr l x'; l) = nil'
  2. Show how to build a circular list of zeros such that the following equations are true:

    car' zeros = 0
    cdr' zeros = zeros

2. Recursion via references

Assume simply-typed λNB with multiplication (times) and references (ref, !, and :=). Note: do not assume built-in recursion (fix) or recursive types (μ).

  1. Define a factorial function fac : NatNat. Hint: A function that calls itself is not so different from a list that contains itself as a tail (which you created in part (b) of the previous problem).

  2. Define fix : ((NatNat) NatNat) NatNat. It should be possible to use fix to define a factorial function in the usual way:

    fac ≡ fix (λf: NatNat. λn:Nat. if iszero n then succ 0 else times n (f (pred n)))

3. 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
try
  read_line f
finally
  close_file f

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

We add a syntax rule:

t ::= ...
      try t1 finally t2

The term try 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
      try
        try
          raise 0
        finally
          print "A"
      finally
        print "B"
    with λx. x

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

  • If an exception is raised while evaluating t2, then the new exception replaces the old one if any. For example,

    try
      try
        raise false
      finally
        raise true
    with λx. x

    should evaluate to true.

  1. Write typing rules for try...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 try...finally.