Homework 5: Effects的编程代写

1. Mutable lists

Assume simply-typed λNB with pairs, recursive types( μ ) and references( ref，! ,and := ).
In Scheme, set! corresponds roughlyto := .It also has set-car! and set-cdr! , which can be use modify lists:
> (define l (list 1 2 3))
> (set-car! l 4)
>l
(423)
> (set-cdr! l (list 5 6))
>l
(456)
a. Define (in simply-typed λNB with the extensions listed above) a type MutableNatList and associate 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 ‘
=Θ
car’ (cons’ X y) = x
cdr’ nil ‘
= nil’
cdr’
(cons’xy) =y
(letl=cons’xyinsetcarlx’;car’l)=x’
(letl=cons’Xyinsetcarlx’;cdr’l)=y
(letl=cons’Xyinsetcdrly’;car’l)=X
(letl=cons’Xyinsetcdrly’;cdr’l)=y’
b. Show how to build a circular list of zeros such that the following equations are true:
car’ zeros =Θ
cdr’ zeros = zeros

2. Recursion via references

Assume simply-typed λNB with multiplication ( times ) and references( ref ，! , and := ).

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

b. Define fix : ((Nat→Nat) →Nat→Nat) →Nat →Nat . It should be possible to use fix to defi
a factorial function in the usual way:
fac三fix (λf: Nat -→Nat. λn:Nat. if iszero n then succ 0 else times n (f (pred n))
3. Finally
Some languages havea 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 termis 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.

a. Write typing rules for try… finally . Because t2 is evaluated for its side-effects only, it should h type Unit .

b. Write evaluation rules (including any new syntax rules for E and F as needed) for try… finally