Due Tuesday, 25 February, 6am
The purpose of this homework problem is to appreciate type soundness and the limitations of a type system (for language implementors and developers).
Delivery Deliver your solutions in a folder called 7 in your github repo:
soundness.md as specified in the programming task below.
xinterpret as specified in the testing task below.
ITests/ as specified in the testing task below.
Other/, which contains the solutions to the programming tasks.
A type soundness theorem permits the removal of all run-time checks from an interpreter or moving them into the standard prelude (base environment).
The language XPAL is TPAL with the restriction that right-hand sides of let declarations must be either fun* expressions or literal integer constants.
Programming Task 1 Modify your interpreter for SFVExpr (from
it type checks the given programs before it interprets them;
You may re-use the solution to 6 —
it must report a type error if the type-checker fails and stop;
if type checking succeeds, the interpreter strips the types from the XPAL program;
it finally runs the programs stripped of types on the modified interpreter function from 5 —
Simple Mutable Objects.
Note As in 6 —
Task 2 Explain why a type soundness theorem does not hold for TPAL running on the modified interpreter. You may provide a general analysis and/or work through an example. Restrict yourself to at most half a page.
Place the explanation in soundness.md.
When you are all done you have six primitive operations in the standard prelude: +, *, ^, @, !, and =.
Testing Task Write the test harness xinterpret for your modified interpreter.
Create ten tests for xinterpret. Place them in ITests/. A test consists of two files: N-in.json and N-out.json for N in [0 .. 9].
I used s and t as meta-variables here instead of using s twice because English and mathematics is not as explicit about scope as programming languages in general.
a JSON string for a type error: "type error: s";
s is one of the type-error messages from 6 —
a JSON integer;
the JSON string "closure" when the result is a programmer-defined function or a primitive operation;
the JSON string "cell" when the result is a cell value; or
a JSON string for a run-time error: "run-time error: t".
Recall JSON: Simplicity and Complexity.