Assignment 5: More Types

Instructions:

  • Due date: Fri. Nov 1, 11:59PM EST
  • Upload your solutions to gradescope as problem-1.rkt, problem-2.rkt, and a PDF containing your derivation trees called trees.pdf.
  • Ask questions on Piazza or during office hours.
  • Perform all the work for this project by yourself. You may discuss with your classmates, but you must write your own code and solve your own exercises.

Problem 1: Typesafe Vectors [40 Points]

Starter code here

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:

(struct elet (id assgn body) #:transparent
  #:guard (struct-guard/c string? eveclang? eveclang?))
(struct eident (id) #:transparent
  #:guard (struct-guard/c string?))
(struct evec (l) #:transparent
  #:guard (struct-guard/c (listof integer?)))
(struct enum (n) #:transparent
  #:guard (struct-guard/c integer?))
(struct egetvec (e idx) #:transparent
  #:guard (struct-guard/c eveclang? integer?))

The semantics are as follows:

  • elet behaves as normal for let.
  • (evec v) is a value where v is a list of numbers (not enum expressions, just numbers; see the contract above).
  • (enum n) is a value that contains a number, which is assumed to be an integer
  • (egetvec e idx) (1) evaluates e to a (evec l) and fails with a runtime error otherwise (by calling the Racket error function); (2) looks up index idx in v, failing with a runtime error if the index is invalid.
  • (eident id) is an identifier

Part a: Make a function interp e of type expr -> expr that implements the above semantics. For example,

> (define example-term
    (elet "x" (evec (list 1 2 3))
        (egetvec (eident "x") 1)))
> (interp example-term)
(enum 2)

Part b: Make a function type-check? e of type expr -> 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. For example,

> (define example-term-2
  (elet "x" (evec (list 1 2 3))
        (egetvec (eident "x") 10)))
> (type-check? example-term-2)
#f

Problem 2: Dynamic Safety for Pairs [50 Points]

Starter code here

On this assignment you extend the dynamic safety compiler from lecture to handle pairs.

Our micro assembly language is slightly different from the lecture for this assignment, and has the following abstract syntax (see the source code for the predicates invoked by the contracts):

;;; set register[reg] = heap[addr]
(struct Aload (reg addr) #:transparent
  #:guard (struct-guard/c valid-reg? valid-heap-loc?))
;;; store register[reg] into heap[addr]
(struct Astore (reg addr) #:transparent
  #:guard (struct-guard/c valid-reg? valid-heap-loc?))
;;; set register[reg] = value
(struct Asetreg (reg value) #:transparent
  #:guard (struct-guard/c valid-reg? integer?))
;;; trap: gives a runtime error if register[0] != v
(struct Atrap (v) #:transparent
  #:guard (struct-guard/c integer?))
;;; set register[0] = register[1] + register[2]
(struct Aadd () #:transparent)
;;; set register[reg] = heap[register[addr]]
(struct Adynamicload (reg addr) #:transparent
  #:guard (struct-guard/c valid-reg? valid-heap-loc?))
;;; set register[0] = register[1] * register[2]
(struct Amul () #:transparent)
;;; terminate
(struct Ahalt () #:transparent)

We have given you an interpreter for MicroASM in the starter code. Your goal in this assignment is to compile the following abstract syntax into MicroASM:

(struct elet (id assgn body) #:transparent
  #:guard (struct-guard/c string? calc? calc?))
(struct eident (id) #:transparent
  #:guard (struct-guard/c string?))
(struct efst (e) #:transparent
  #:guard (struct-guard/c calc?))
(struct esnd (e) #:transparent
  #:guard (struct-guard/c calc?))
(struct epair (e1 e2) #:transparent
  #:guard (struct-guard/c calc? calc?))
(struct enum (n) #:transparent
  #:guard (struct-guard/c number?))

We have provided helper functions for running your compiler.

You should fill in the function calc->asm with your code. Your implementation should emit Atrap instructions when needed to prevent illegal operations from being performed (for instance, calling efst or esnd on a non-pair). We will only test your solution on programs that evaluate to numbers. Here are some examples:

> (compile-and-run (efst (epair (enum 10) (enum 20))))
10
> (compile-and-run (efst (enum 10)))
. error trap exception

Be sure to test your solution thoroughly. This problem is quite a bit trickier than prior programming assignments. Here are some hints:

  • Test thoroughly: you should have at least 10 test cases for this problem.
  • Use the stepper we saw in class to slowly run assembly programs. You will find it helpful to draw the heap as the program is run.
  • You will have to come up with a way of storing pairs on the heap. Think about what information you needs to know to implement efst and esnd; you will need to be creative about how you represent pairs.

Problem 3: Typing Derivations [10 Points]

Recall the type derivation rules for the simply-typed $\lambda$-calculus from Lecture 11 and Lecture 12. Draw typing derivation trees for the following terms, starting with an empty typing context (meaning $\Gamma$ is initially {}):

  1. $(\lambda x : \texttt{num} . x) ~ 10$
  2. $\lambda x : (\texttt{num -> num}) . (x~10)$
  3. $\lambda x : \texttt{num} . (\lambda x : \texttt{(num -> num)} .~x)$
  4. $\lambda x : \texttt{num} . (\lambda y : \texttt{num} . ~ x)$

Upload your trees as a separate PDF. These trees are all quite small.