Please read Chapters 20 and 21 in your textbook.
Please do the following problems
Using the fullisorec checker, WITHOUT the ``fix'' keyword or side-effects, implement a plus function that works on actual nats, not on church numerals. You will need to roll your own Y combinator. Put your result in file myfix.f. Demonstrate that it works adding 2 and 3.
NB: The textbook (page 273) gives the wrong definition of fix:
it will cause nontermination. (Furthermore it assumes equi-recursive
types. Your code needs to work with iso-recursive types.)
You need to use the call-by-value
version on page 65 and add iso-recursion.
A major part of this question is figuring out how
to handle these aspects.
Prove the type soundness of recursive types using SASyLF.
Start with the skeleton file homework11.slf.SKEL.
Add subtyping using S-Amber and prove soundness.
A separate skeleton file homework11-sub.slf.SKEL should be
used for that. You will want to use your solution to the main proof
to start this proof.
In Homework #10 (see the solution), we showed how objects could be
modeled to take the self object as a parameter.
Recursive types can be used to give valid types to the
SetCounter class in our answer to
Question 4.3 of Homework #9 (object.f).
Do that. Leave your answer in an updated object.f in this
homework directory.
(You will need to use the everything checker because you need
subtyping, recursive types and references.)
However, you will be unable to add types to get the
InstrSetCounter class to type check. Look at the book's
S-AMBER rule and explain why the ``obvious'' typing for the
InstrSetCounter class does not check. Is the type error
necessary? That is, can you come up with an example which will break
type soundness if this type error were not checked? Explain.