Assignment 4: Types

Instructions:

  • Due date: Friday Oct 18, 11:59PM EST
  • Use the following code template: here
  • Upload a code.rkt solution to Gradescope. It will give you a score, but this is not your final score; some of the test cases will be kept private. You should test all your code thoroughly.
  • 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: Programming with types [20 Points]

Download the implementation of the simply-typed lambda calculus from here and load it into your Racket environment to answer the following questions. All answers to these questions should be lambda calculus abstract syntax. We will test your answers by using the type-of function in the provided implementation.

  1. Give three different lambda terms of type (tnum -> tnum) -> (tnum -> tnum). Provide your answer by defining term-1, term-2, and term-3 in your solution.
  2. Give 3 different lambda terms that are not well-typed. Provide your answer by defining term-4, term-5, and term-6 in your solution.
  3. Suppose we add a type tunit to our language, which is a type that contains only the value (eunit) (i.e., all terms of type tunit must evaluate to the value (eunit)). Give 3 different functions of type tunit -> tnum. Label these functions term-7, term-8, and term-9. Do you notice any pattern about the behavior of functions with this type? Define a term pattern that contains your answer as a string.
  4. Give 3 syntactically inequivalent functions of type tunit -> tunit, and label them term-10, term-11, and term-12. Are there any observationally inequivalent functions in this language of type tunit -> tunit? Define a term are-there? with a string containing yes or no.

Problem 2: Designing a typechecker for pairs and let [80 Points]

Recall the small language of pairs from Quiz 1, which has the following syntax including pairs and let expressions:

;;; type expr =
;;;   | add of expr * expr
;;;   | mul of expr * expr
;;;   | num of number
;;;   | bool of bool
;;;   | let of string * expr * expr
;;;   | ident of string
;;;   | epair of expr * expr 
;;;   | efst of expr 
;;;   | esnd of expr
(struct eadd (e1 e2) #:transparent)
(struct emul (e1 e2) #:transparent)
(struct enum (n) #:transparent)
(struct ebool (n) #:transparent)
(struct elet (id binding body) #:transparent)
(struct eident (id) #:transparent)
(struct epair (e1 e2) #:transparent)
(struct efst (e) #:transparent)
(struct esnd (e) #:transparent)

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:

  1. Is sound: it rejects as ill-typed all syntactically well-formed programs that cause Racket runtime errors.
  2. Is expressive: it accepts as well-typed all syntactically well-formed programs that do not cause Racket runtime errors.
  3. Is efficient: your typechecker should not evaluate the program using interp or perform other expensive computations.

Create a function type-check? of type expr -> bool that returns true if a term is well-typed and false if it is not well-typed. You should not change the syntax of the expressions.