8 Type Checking and Interpretation🔗
8.1 Introduction🔗
In past assignments you’ve written an interpreter for Paret and a type-checker for Typed Paret. Now you’re going to combine the two into an interpreter for Typed Paret.
8.2 Exam Mode🔗
For this homework, you are expected to do the work entirely on your own: you may consult with the course staff only for essential information (clarification of typos/errors, names of library functions, etc.: if in doubt you can always ask). In other words, you will do this in “exam mode”. Though some parts will be more challenging than others, we do believe you can do all the problems in this assignment.
8.3 Assignment🔗
As in
Interpreter, we have provided the
parse and
desugar functions for you.
You will be re-implementing
interp and
type-of, with the same general requirements. So you should be able to copy-and-paste the vast majority of your code. The difficulty of this assignment is in making these functions work together correctly. Also, this assignment uses
Typed Paret, the same language as in
Type Checker (well, not
exactly the same; see the Additional Notes section.), but you wrote your interpreter for Paret, so you will need to extend your interpreter.
In your final implementation, the evaluation pipeline will work like this:
The input S-Exp is parsed into an Expr+ with the provided parse function.
The Expr+ is passed through desugar, to create a desugared Expr.
The desugared Expr is type-checked by passing it through type-of. The result of type-of is the Type of the given Expr. We just confirm that it has a type; if it does not, we signal a type error. Otherwise:
The desugared Expr is passed to interp to produce a final value.
In order to simplify things, and keep you on the right track, we’ve split this assignment into 3 phases.
8.3.1 Phase 1 : Updating interp🔗
In the first phase, you will modify your work on the
Interpreter assignment to interpret the
syntax of Typed Paret, but with the same, “untyped”
semantics of the interpreter. Thus, some expressions (
let and
lambda expressions, specifically) passed to your interpreter will now have type annotations, but you will
ignore the annotations.
Of course, you will still have safety checks, just as before. For example, if a program tries to add a number and a string,
interp should still throw an error because those types don’t make sense for that operation. But you will not try to simulate all the checks that the type-checker does. Thus,
interp should not immediately throw an error when applying a function with a
Num-annotated formal parameter to a string. (If that function then tries to add its input to a number,
then interp would have to throw an error.) For more context on what safety checks are and to understand exactly what “untyped”
semantics means, read sections 17.1 and 17.2 of
Programming and Programming Languages.
Additionally, for reasons that will become clear in phase 3, all errors produced by your interp function must now come from the provided raise-interp-error function.
8.3.2 Phase 2 : Updating type-of🔗
In the second phase, you will modify your work on
Type Checker to be compatible with this assignment. This one should be much simpler than phase 1: you need to make your
type-of function compatible with the altered
let syntax, and should remove the cases that are now handled by
desugar.
Additionally, like in phase 1, all errors produced by your type-of function must now come from the provided raise-type-error function.
8.3.3 Phase 3 : Putting them together🔗
Finally, you will combine interp and type-of in one file, as described in the evaluation pipeline. After doing so, many of your interp errors will now be caught in type-of, so you should remove all unnecessary error-handling code from your interp function.
Take care though: type-of can’t catch every error!
Additionally, combining them as described in the evaluation pipeline will slightly change the semantics of the language. Remember to update your tests accordingly.
8.3.4 Write-up🔗
By introducing a type-checker, you’ve eliminated the need for certain runtime checks and error handling in your interp function. We’d like you to reflect on this modification in a short write-up. Please answer the following questions with a paragraph each:
Which runtime errors are now caught by the initial type-check? Which runtime errors must still be handled by interp?
How has the addition of type-checking changed the semantics of our overall language? Write three programs that run just fine on your interpreter from Phase 1, but are no longer valid because they fail the type checker in Phase 3.
How does adding type-checking affect how long it takes to interpret a program (ignore the time to type-check)? What kinds of programs might take less “wall clock’’ running time, what kinds might stay the same, and what kinds might take more?
8.3.5 Additional notes🔗
Here are some more points to keep in mind.
First: Let expressions in this assignment have a slightly different syntax than they did in type-checker. They now require a type annotation on the variable binding, like this:
| #lang racket |
| (eval `(let (x 4 : Num) (+ x x))) |
In
Type Checker we could omit this annotation because we could determine the type of the actual parameter by calling
type-of recursively. We
could still omit the annotation, but it would require complicating our evaluation pipeline. Why? (Hint:
Type Checker didn’t have a desugaring step.)
Second: There are now two kinds of environments you need to work with. Env is for tracking variable bindings in interp, and TEnv is for tracking variable types in type-of. Don’t get them confused!
8.3.6 Errors🔗
To raise an error found in type-of, you should call the raise-type-error function with a helpful message, like so:
| #lang racket |
| (raise-type-error "can't add numbers to strings") |
Similarly, to raise an error found in interp, you should call the raise-interp-error function.
Both kinds of errors can (and should) be explicitly tested for in your tests file, using the test-raises-type-error? and test-raises-interp-error? constructions.
8.4 Testing🔗
You will be writing separate test files for each phase, so you can get feedback as you go. You can copy-and-paste most of your tests from
Interpreter for testing phases 1 and 3, and similarly you can copy-and-paste most of your tests from
Type Checker for testing phase 2.
But remember:
Phase 1 adds new functionality to the interpreter that you must add new tests for.
You will need to add type annotations to the let expressions in your tests to avoid parser errors.
Phase 3 removes some functionality from the interpreter, so some of your tests will have to be changed to account for that.
You should only be testing against the eval and type-check functions.
8.5 Grammar🔗
The modified grammar of Typed Paret is as follows:
<expr> ::= <num> |
| <string> |
| true |
| false |
| (+ <expr> <expr>) |
| (++ <expr> <expr>) |
| (num= <expr> <expr>) |
| (str= <expr> <expr>) |
| (if <expr> <expr> <expr>) |
| (and <expr> <expr>) |
| (or <expr> <expr>) |
| <id> |
| (<expr> <expr>) |
| (lam (<id> : <type>) <expr>) |
| (let (<id> <expr> : <type>) <expr>) |
| (first <expr>) |
| (rest <expr>) |
| (is-empty <expr>) |
| (empty : <type>) |
| (link <expr> <expr>) |
|
<type> ::= Num |
| Str |
| Bool |
| (List <type>) |
| (<type> -> <type>) |
8.5.1 Abstract Syntax🔗
The
Value type is the same as in
Interpreter, but is repeated here for convenience. The
Expr type is almost identical to the one in
Type Checker, but
let expressions now include a type.
| #lang racket |
| (define-type Type |
| (t-num) |
| (t-bool) |
| (t-str) |
| (t-fun [arg-type : Type] [return-type : Type]) |
| (t-list [elem-type : Type])) |
| |
| (define-type Value |
| (v-num [value : Number]) |
| (v-bool [value : Boolean]) |
| (v-str [value : String]) |
| (v-fun [param : Symbol] |
| [body : Expr] |
| [env : Env]) |
| (v-list [vals : (Listof Value)])) |
| |
| (define-type Expr+ |
| (e-num [value : Number]) |
| (e-bool [value : Boolean]) |
| (e-str [value : String]) |
| (e-op [op : Operator] |
| [left : Expr] |
| [right : Expr]) |
| (e-un-op [op : UnaryOperator] |
| [expr : Expr]) |
| (e-if [cond : Expr] |
| [consq : Expr] |
| [altern : Expr]) |
| (e-lam [param : Symbol] |
| [arg-type : Type] |
| [body : Expr]) |
| (e-app [func : Expr] |
| [arg : Expr]) |
| (e-var [name : Symbol]) |
| (sugar-and [left : Expr] |
| [right : Expr]) |
| (sugar-or [left : Expr] |
| [right : Expr]) |
| (sugar-let [var : Symbol] |
| [value : Expr] |
| [type : Type] |
| [body : Expr]) |
| (e-empty [elem-type : Type])) |
| |
| (define-type Operator |
| (op-plus) |
| (op-append) |
| (op-num-eq) |
| (op-str-eq) |
| (op-link)) |
| |
| (define-type UnaryOperator |
| (op-first) |
| (op-rest) |
| (op-is-empty)) |
8.6 Starter Code🔗
GitHub Classroom
8.7 What To Hand In🔗
You will submit your work for each phase separately.
For phase 1, you will submit updated-interp.rkt to the “Code” drop on Gradescope, and you will submit updated-interp-tests.rkt to the “Tests” drop on Gradescope.
For phase 2, you will submit updated-tcheck.rkt to the “Code” drop on Gradescope, and you will submit updated-tcheck-tests.rkt to the “Tests” drop on Gradescope.
For phase 3, you will submit tynterp.rkt to the “Code” drop on Gradescope, and you will submit tynterp-tests.rkt to the “Tests” drop on Gradescope.
For the write-up, you will submit your answers to the “Write-up” drop on Gradescope.
You can update your submissions as many times as you want before the deadline.