Assignment 6: Types and recursion

Parameters:

  • Due date: Wednesday Feb. 28 at 11:59PM
  • Upload your solution as a code.rkt file on Gradescope.
  • 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.
  • Starter code here: link
  • Grading: each problem is worth a certain number of points. The points given for each problem is the fraction of tests passed for that problem (i.e., if 50% of the tests are passed for a 20 point problem, 10 points are given).

Problem 1: Mutation and recursion [40 Points]

We learned in class that the simply-typed lambda calculus always terminates. This is an amazing property, but it isn’t always desirable–it limits severely the programs we can write. This is why we then introduced letrec to give us back recursion in a well-typed setting. With letrec, it is easy to make a program that runs forever, like this:

(letrec [(loopy (lambda (x) (loopy x)))]
    (loopy 10))

This begs the question: is adding letrec the only way to get recursion in the simply-typed lambda calculus? The answer to this questions is no! In fact, using only mutable references, lambdas, and let, one can make a well-typed program that runs forever! Here is an example in Plait that is equivalent to the one above, but makes use of mutable references instead of letrec:

(let [(f (box (lambda (x) x)))]
    (let [(loopy (lambda (x) ((unbox f) x)))]
      (begin
        (set-box! f loopy)
        ((unbox f) 10))))

We recommend you carefully walk through this example to understand it.

In this exercise, you will be implementing a letrec interpreter using mutable state. We have given you substantial starter code for this problem. You will use the following grammar:

(define-type Type
  [TNum]
  [TFun (arg : Type) (ret : Type)])

(define-type Exp
  [letrecE (s : Symbol) (t : Type) (e : Exp) (body : Exp)]
  [numE (n : Number)]
  [varE (s : Symbol)]
  [locE (n : Number)]
  [lamE (arg : Symbol) (t : Type) (body : Exp)]
  [appE (e1 : Exp) (e2 : Exp)])

Exp includes a variant locE which contains a heap location n. Note that the grammar does not include box, unbox, or setbox; the only way to introduce a location will be through letrecE.

You will make use a mutable heap that maps heap locations (numbers) to expressions:

(define-type-alias MutableHeap (Boxof (Hashof Number Exp)))
(define mt-heap (box (hash empty))) ;; "empty environment"

(define (lookup (h : MutableHeap) (n : Number))
  (type-case (Optionof Exp) (hash-ref (unbox h) n)
             [(none) (error 'type-error "unrecognized symbol")]
             [(some v) v]))

(extend : (MutableHeap Number Exp -> Void))
(define (extend old-env new-name value)
  (set-box! old-env (hash-set (unbox old-env) new-name value)))

Additionally, your solution should make use of the following function for generating a fresh heap address when needed:

(define counter (box 0))
(define (fresh-loc!)
  (begin
    (set-box! counter (+ (unbox counter) 1))
    (unbox counter)))

Problem 1. Implement a function interp of type (MutableHeap Exp -> Exp) that interprets letrec programs. Your solution should not make use of any mutation except through the provided extend and fresh-loc! function.

If you have implemented your solution correctly, the following program will run forever:

(interp mt-heap (letrecE 'f (TFun (TNum) (TNum)) (lamE 'x (TFun (TNum) (TNum)) (appE (varE 'f) (varE 'x))) (appE (varE 'f) (numE 10))))

Note: This is most likely the trickiest problem we’ve asked you to do so far – it will be challenging and take some time.

Problem 2: Type-safe vectors [60 Points]

Plait supports vectors, but there is a problem: it’s very easy to make Plait’s vectors crash. Consider the following code:

; create a vector of length 10 initialized with all zeros
> (define my-vec (make-vector 10 0))
; looking up entry 4 in my vector
> (vector-ref my-vec 4)
- Number
0
> (vector-ref my-vec 11)
- Number
. . vector-ref: index is out of range
  index: 11
  valid range: [0, 9]
  vector: '#(0 0 0 0 0 0 0 0 0 0)

Uh oh! We tried to look up an index that was out of range of the vector and caused a runtime error.

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 VExpr
  [let1E (x : Symbol) (assgn : VExpr) (body : VExpr)]
  [vvecE (v : (Vectorof Number))]
  [vnumE (n : Number)]
  [getvecE (e : VExpr) (index : Number)]
  [vvarE (s : Symbol)])

The semantics are as follows:

  • let1E behaves as normal for let.
  • vvecE v is a value that contains a vector v
  • vnumE n is a value that contains a number n
  • getvecE e index (1) evaluates e to a vvecE v and fails with a 'runtime error otherwise; (2) looks up index index in v and returns vnumE v, failing with a 'runtime error if the index is invalid.
  • vvarE s is an identifier

Problem 2a: Make a function interpv e of type VExpr -> VExpr that implements the above semantics.

Problem 2b: Make 5 test/exn tests that cause your interpreter to “go wrong” and have a runtime error.

Problem 2c: Make a function type-of of type TEnv VExpr -> VType such that any well-typed program does not cause the 'runtime errors in your solution for interpv. Your type-of function should raise a 'type-error if it encountered an ill-typed program.