这是一篇来自美国的关于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)
> (set-cdr! l (list 5 6))
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 ‘
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))
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
read_ _line f
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,
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,
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