# BEST代写-线上编程学术专家

Best代写-最专业靠谱代写IT | CS | 留学生作业 | 编程代写Java | Python |C/C++ | PHP | Matlab | Assignment Project Homework代写

# 这是一篇来自美国的关于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
finally
close_ file f
If the read_ _line raises an exception, the file f still gets closed.
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 