4 Types
Due date: Thursday, February 13 at 11:59PM
Upload your solutions to GradeScope here. You should upload a single file called code.rkt. Be sure to check that your uploaded solution is valid; you will receive 0 points if your solution does not run.
Your programs will be evaluated on the fraction of tests that they pass. We will show you some tests, but not all tests. You should test your code thoroughly. After the submission deadline, we will reveal the hidden tests.
Starter code: code.rkt.
4.1 Designing a typechecker for pairs and let [50 Points]
> (define-type PairLang (numE [n : Number]) (boolE [b : Boolean]) (varE [s : Symbol]) (addE [e1 : PairLang] [e2 : PairLang]) (mulE [e1 : PairLang] [e2 : PairLang]) (letE [id : Symbol] [assignment : PairLang] [body : PairLang]) (pairE [e1 : PairLang] [e2 : PairLang]) (fstE [e : PairLang]) (sndE [e : PairLang]))
We have provided you an interpreter for this language in the starter code; you should not change this interpreter. Your task is to design a typechecker for this language that:
Is sound: it rejects as ill-typed all syntactically well-formed programs that cause Racket runtime errors.
Is expressive: it accepts as well-typed all syntactically well-formed programs that do not cause Plait runtime errors.
Is efficient: your typechecker should not evaluate the program using interp or perform other expensive computations.
Create a function type-check? of type (PairLang -> Boolean) that returns true if a term is well-typed and false if it is not well-typed. You may want to use Plait error-handling features like try. Your solution will likely involve defining helper functions.
4.2 Designing a typechecker for vectors [50 Points]
Many programming languages have support for arrays (also called vectors), which are lists of a fixed length. For instance, Python supports Arrays with the following syntax:
>>> myarr = [1, 2, 3] |
>>> myarr[1] |
2 |
Unfortunately, it is easy to make Python arrays crash: for instance, we can look up an array index that is greater than the length of the array, which causes a runtime error:
>>> myarr[4] |
IndexError: list index out of range |
Let’s make a tiny language for manipulating vectors that can prevent this kind of error using a type system: we want the guarantee that all well-typed programs can have no runtime errors. (Note: In this problem, we will assume that all numbers are integers; you can ignore the case when a number happens to be something other than an integer.)
Here is the syntax for our language:
> (define-type VecLang (letV [id : Symbol] [assgn : VecLang] [body : VecLang]) (identV [id : Symbol]) (numV [n : Number]) (vecV [l : (Listof Number)]) (getvecV [e : VecLang] [n : Number]))
The semantics are as follows:
letV, identV, and numV behave as normal for let-bindings, variables, and numbers.
vecV creates a vector (fixed-length array) of numbers.
(getvecV e n) looks up the value at index n in the vector e.
4.2.1 Part 1: A definitional interpreter [10 Points]
Let’s define the set of values that VecLang programs can run to:
> (define-type VecValue (numVV [n : Number]) (vecVV [v : (Listof Number)]))
Make a function interp-vec e of type (VecLang -> VecValue) that implements the above semantics. For example,
> (define ex (letV 'x (vecV (list 1 2 3)) (getvecV (identV 'x) 1)))
> (interp-vec example-term) (numV 2)
4.2.2 Part 2: A typechecker [40 Points]
Make a function (type-check? e) of type (VecLang -> bool) that returns #t if e is well-typed and #f if it is not well-typed. Your type checker should be efficient, expressive, and sound: we will test your type checker to make sure that (1) all syntactically valid expressions that do not cause runtime errors typecheck, and (2) all syntactically valid expressions that cause runtime errors fail to typecheck. You may want to use Plait error-handling features like try. Your solution will likely involve defining helper functions.