►Principles of Programming Languages
▼Assignments
•7 — Type Sound Interpretation
7.7.0.3
    ← prev  up  next → 

7 — Type Sound Interpretation

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.

Do read Make in case you need us to build your executables.

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 5 — Simple Mutable Objects) to run programs without run-time checks, except those necessitated by the soundness theorem (v3) in 12 — The Truth (which holds for XPAL).

Wrap your modified interpreter into a "main" function/method that proceeds as follows:

  • it type checks the given programs before it interprets them;

    You may re-use the solution to 6 — Type Checking.

  • 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 — Type Checking, parse infix primop uses into function calls.

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.

Task 3 Add @, !, and = to the standard prelude for XPAL (base environment). Use “cheap polymorphism” to type check these functions. (See 13 — Poly Types.)

The external syntax for cell types, PType, is extended with the clause [PType, "cell"],

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.

An input file in ITests contains a single JSON XPAL expression. An output file is one of:

  • a JSON string for a type error: "type error: s";

    s is one of the type-error messages from 6 — Type Checking.

  • 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".

    t is one of the type-error messages from 4 — Interpreting Functions & 5 — Simple Mutable Objects. The formulation of error messages of 5 supersede those of 4 as specified.

Recall JSON: Simplicity and Complexity.

    ← prev  up  next →