cs-4400-sp26

hw4: Type Checking

Instructions:

Due date: Thursday, Feb 12 (11:59pm)
Upload your solutions to GradeScope. 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: hw4-starter.rkt

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 the PairLang language (syntax given above) 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 PairLang programs that cause Racket runtime errors when interpreted.
Is expressive: it accepts as well-typed all PairLang programs that do not cause Plait runtime errors when interpreted.
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 #t if a term is well-typed and #f if it is not well-typed. Your solution will likely involve defining helper functions.

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 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 of 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.

Part 1: A definitional interpreter [10 points]

Here is 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-dev ex)
(numV 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 typechecker should be efficient, expressive, and sound: we will test your typechecker to make sure that (1) all 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.