Quiz 2: Types

Instructions:

Due Date: Monday, Nov. 4, 11:59PM EST
You must complete this quiz on your own. Do not consult with others. You are encouraged to use the course notes (posted on this webpage) as your main resource when solving these quiz questions.
All quiz solutions are uploaded to gradescope. There will be two submissions
1. A code upload for the programming assignment. Upload two files: a file called toplang.rkt and a file called reconstruction.rkt.
2. A file upload where you upload your written solutions. This can be a PDF, photos of paper, etc.
Quiz-related questions will not be answered on Piazza or during office hours. Logistics-related questions (like “how do I turn in the quiz?”) are OK.

Starter code:

reconstruction.rkt

toplang.rkt

Question 1 [20 Points]

State whether each of the following is true or false. If it is false, provide a brief explanation for why. Upload your solutions as written solutions.

Types are collections of values.
Types in programming languages only serve to help the CPU understand the underlying data being used.
In the implementation of STLC, the type checker interprets the expressions to determine their types.
All type checkers always prevent all possible runtime errors.
Ω can be typed in the simply-typed λ-calculus.
Static typechecking determines the types of values at runtime.
The assembly language used for MicroASM programs can directly represent both numbers and Booleans.
In System F, self-application can be typed, which is not possible in the simply-typed lambda calculus.
The following is a well-typed program in System F: $((\Lambda X . \lambda x : X . 20) [\texttt{tnum}])~30$
The following is a well-typed program in System F: $\Lambda X . \lambda x : X . (x~10)$

Question 2: Type Reconstruction [10 Points]

Type reconstruction is the process of finding a type that makes an untyped program well-typed. For each of the following lambda terms, add a type annotation that makes it typed in the simply-typed lambda calculus, or state that no such type is possible to write. Your answers should all be written using the syntax of the simply-typed lambda calculus from this interpreter. The starter code provides you with the necessary structs for defining your answers.

Example: for the prompt $\lambda x . 10$, you answer should be (elam "x" (tnum) (enum 10)).

Provide your answer by filling in the corresponding definitions in the provided template; if there is no valid type, define your answer to be the false constant #f. We will grade your answer by checking if it typechecks using the typechecker provided in the interpreter. Name the terms term-1 to term-5.

$\lambda x. (x~20)$
$\lambda x . (x~(\lambda y.10))$
$\lambda x . (x~((\lambda y . y)~x))$
$((\lambda x . x)~(\lambda y . y))$
$((\lambda x . x~(\lambda z . 30))~(\lambda y . y~20))$

Question 3: Derivation Trees [10 Points]

For each of the derivation trees for the call-by-value lambda calculus in the following file, state whether they are valid or invalid. If they are invalid, briefly explain why. 2 points per problem. Upload your solutions as written solutions.

quiz trees

Question 4 [60 Points]: A Typed Recursive Language

We’ve seen that programs in the simply-typed $\lambda$-calculus always terminate because it’s impossible to type recursive functions. One way to allow recursion with simple types, however, is to define named functions at the top level of the program instead of using unnamed $\lambda$ expressions. Define a program as a list of functions combined with a “main” expression, which is evaluated with all of the top-level functions in scope:

(struct program (funs main))

A function is value that includes the name of the function, the name of its single parameter, the type of its parameter, the return type, and the body expression. The only other kind of value is a number.

(struct tnum ())
(struct tfun (in out))
(define type/c (or/c tnum? tfun?))

(struct vnum (n))
(struct vfun (name param param-ty ret-ty body))
(define val/c (or/c vnum? vfun?))

The expression language supports simple arithmetic over integers (enum, eadd, and emul), let bindings (elet and eident), and function application (eapp). To allow base cases for the recursive functions, a simple conditional expression is also supported (eif0), which tests if a number is 0.

(struct enum (n))
(struct eadd (e1 e2))
(struct emul (e1 e2))
(struct eif0 (guard thn els))
(struct elet (id assgn body))
(struct eident (id))
(struct eapp (e1 e2))
(define expr/c (or/c enum? eadd? emul? eif0? elet? eident? eapp?))

Notice that top-level functions are the only kind of functions supported—there is no elam expression.

As an example, this language is expressive enough to implement the factorial function. The following program evaluates to (vnum 6):

(program
 (list
  (vfun "fact" "n" (tnum) (tnum)
        (eif0 (eident "n")
              (enum 1)
              (emul (eident "n") (eapp (eident "fact") (eadd (enum -1) (eident "n")))))))
 (eapp (eident "fact") (enum 3)))

Part A: An Interpreter

You will first need to implement an interpreter for this language, which takes in a program and returns a value.

(define/contract (interp prog)
  (-> program? val/c)
  (error "implement me"))

The interpreter must implement the following semantics:

enum, eadd, emul, elet, eident, and eapp behave like we have seen before.
(eif0 guard thn els) first evaluates guard to (vnum n). (It’s a runtime error if guard is not a vnum.) If n is zero, the result is the result of evaluating thn. If n is not zero, the result is the result of evaluating els.
The main expression is allowed to use the name of any function in the program’s funs field. For example, if there is a (vfun "foo" ...), then main could contain (eapp (eident "foo") (enum 5)), which applies foo to 5.
The body of a function is allowed to refer to its own name. For example, the body of (vfun "foo" ...) could contain (eapp (eident "foo") (enum 5)), which is a recursive call applying itself to 5.
The body of a function is not allowed to refer to the name of any other functions besides itself.
In the body of a function, a parameter with the same name as the function itself shadows the function, and a let binding with the same name as the function itself or its parameter shadows the function or parameter.
In the main expression, a let binding with the same name as a top-level function shadows that function.
Call (raise-runtime-error reason) whenever a runtime error occurs. (The reason string doesn’t matter, it’s just to help you debug.)
You can assume that we will only run your interpreter on programs that terminate and evaluate to a number, although intermediate subexpressions may evaluate to functions.

Part B: A Type Checker

Lastly, you will need to implement a type checker for this language. The function type-check? takes a program and returns a boolean: #t if the program type checks or #f if there is a type error.

Like we have seen before, it may be helpful to define a helper function type-of that returns the type of a term, or if the term cannot be typed, raises a type error exception by calling (raise-type-error reason). (The exact message or reason string doesn’t matter, it’s just to help you debug.)

(define/contract (type-check? prog)
  (-> program? boolean?)
  (with-handlers ([exn:fail:type? (lambda _ #f)])
    (error "implement me")))

The type checker must reject all programs that would cause a runtime error. It should also avoid rejecting any programs that would not cause a runtime error, except that, for eif0, it should should require that both thn and els have the same type. The type checker may not call the interpreter.

The type checker also needs to make sure that every top-level function is defined and used correctly. The body of each function should be checked in a typing environment that contains the type of the function itself (using param-ty and ret-ty), and the type of the function parameter (using param-ty). The body must have the same type as ret-ty.

We will evaluate your typechecker based on the fraction of soundness and expressivity tests that it passes.