Quiz 4

Instructions:

Due Date: Monday, Dec. 9, 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 three files: quiz4-problem2.rkt, quiz4-problem3.rkt, quiz4-problem4.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?” or “the autograder does not terminate or errors”) are OK.

Starter code:

Question 1 [60 Points]: True/False, Short Answer, Multiple Choice

Upload a PDF to Gradescope containing your answers to these problems.

Part A [30 Points]: Concept Checks

For each of the following problems clearly state your answer. For true-false questions, if your answer is false, briefly explain why.

The lambda calculus program $((\lambda x . (\lambda x . x)) ~ (\lambda z . z))$ evaluates to $(\lambda z . z)$.
How many unique programs (i.e., has observationally inequivalent behavior) in System F are there of type $\forall X . X \rightarrow (X \rightarrow X)$?
How many distinct programs (i.e., has observationally inequivalent behavior) in System F are there of type $\forall X . \forall Y. Y \rightarrow (X \rightarrow X)$?
A compiler translates a program in one programming language into a program in another programming language while preserving its semantics.

The following program is in tail form:

(define (foo x)
  (if x
   (foo x)
   (foo (foo x))))

The only valid Church-encoding of Booleans is to associate true with $\lambda x. \lambda y . x$ and false with $\lambda x . \lambda y . y$.
In untyped lambda calculus (lambda, variable, application), two terms are extensionally equal only if both of them either terminate or diverge.
You can typecheck the $\Omega$ term in System-F.
The type checker for the simply-typed lambda calculus can eliminate all runtime errors.
The simply-typed lambda calculus with mutable state is a terminating language.
Any recursive function can be rewritten in tail-style using continuations.
The following program terminates in untyped lambda calculus with call-by-name semantics: $(\lambda x . (\lambda x . x))~\Omega$
In which languages can you type a self application:
a. None
b. Untyped Lambda Calculus
c. STLC
d. System F
e. STLC and System F
f. Untyped Lambda Calculus and System F
g. All of the above
You can implement the following control features using continuations (choose all that apply):
a. Exceptions
b. Early function return
c. Loops and breaks
d. Non-determinism
Which of the following untyped lambda calculus programs terminate (choose all that apply):
a. $(λx.x)(λx.x)$
b. $(\lambda x . x x)(\lambda x . x x)$
c. $(\lambda x . x x x)(\lambda x . x x x)$

Part B [30 Points]: Short Answer

Provide a brief (at most 1 paragraph) answer to the following questions:

What is lexical scope and why is it an important property to have in a programming language?
What does it mean for a typechecker to be “efficient,” and why is that important?
What are some advantages of programming in a language with a type system?
Briefly summarize your favorite programming language’s approach to polymorphism. What features does it offer to achieve polymorphic behavior? What are the design tradeoffs, when compared with the approach we saw with System-F?
What is the difference between intensional and extensional equivalence? Why is it important that we distinguish these two kinds of equality of programs?

Question 2: Typechecking Named Exceptions [50 Points]

Recall the named exception problem from Assignment 6. We provide a solution for this in the starter code.

Implement a typechecker type-check? for this programming language. We will evaluate your typechecker on the usual two metrics: expressivity and soundness. This language differs in a few ways from the one you saw in class:

We have provided you with the types you should use:

(struct tnum () #:transparent)
(struct tfun (arg body exns) #:transparent
#:guard (struct-guard/c (recursive-contract type/c)
                        (recursive-contract type/c)
                        set?))

Function types will be annotated by exns, which is a set of possible exceptions that a function can raise when called.

There are some additional type annotations in the abstract syntax tree that we have provided for you. In particular, eraise is now annotated with a type so that it can be used in a well-typed way inside of expressions.

For example, the following expression should be well-typed:

> (type-check? (etry 
                 (eadd (eraise 1 (tnum)) (enum 10)) 
                 1 
                 (enum 20)))
#t

Your type checker should eliminate as many runtime errors as possible while remaining efficient (i.e., your typechecker should not evaluate the program). We will evaluate your solution on the usual metrics of expressivity and soundness.

Question 3 [20 Points]: Find the Typechecker Errors

Consider the implementation of a typechecker for a language with mutable state in the provided starter code.

First, identify any possible errors in this typechecker and explain them in the mistake definition. You should clearly indicate whether or not the errors result in a soundness or expressivity issue. Then, provide 3 example programs that exercise the errors you identify.

Hint: In addition to looking at the code, you should write your own test cases to look for the errors. You can include those test cases in your final solution.

Question 4 [20 Points]: Find the Interpreter Errors

Consider the implementation of continuation-passing interpreter for a language with exceptions in the provided starter code.

Hint: In addition to looking at the code, you should write your own test cases to look for the errors. You can include those test cases in your final solution.