Instructions

  • Deadline: Friday March 1 at 11:59PM
  • Starter code: here
  • This quiz is to be completed on your own. Please do not consult with classmates. You are permitted to use the course notes and Dr Racket. Only ask questions relating to the quiz as private Piazza questions.
  • Upload a single file called code.rkt to Gradescope. Your upload should be valid Plait: be sure your upload runs in Dr Racket without errors. Use the provided starter code.
  • You should consult primarily with the course notes and course textbook while answering questions on this quiz.
  • Note: The autograder score is not your final score.
  • The quiz is graded out of 100 points in total.

Problem 1: Short answer & multiple choice [30 Points]

Problem 1a [9 Points]

Consider the following Plait AST and interpreter for a small language with let-bindings, addition, numbers, if, and Booleans:

(define-type TinyExpr
  [boolTE (b : Boolean)]
  [numTE (n : Number)]
  [varTE (v : Symbol)]
  [addTE (e1 : TinyExpr) (e2 : TinyExpr)]
  [ifTE (guard : TinyExpr) (thn : TinyExpr) (els : TinyExpr)]
  [let1TE (id : Symbol) (e1 : TinyExpr) (e2 : TinyExpr)])

; substitute e1[x |-> e2]
(subst : (TinyExpr Symbol TinyExpr -> TinyExpr))
(define (subst e1 x e2)
  (type-case TinyExpr e1
    [(varTE s) (if (symbol=? s x)
                  e2
                  (varTE s))]
    [(numTE n) (numTE n)]
    [(addTE add1 add2) (addTE (subst add1 x e2) (subst add2 x e2))]
    [(ifTE g thn els) (ifTE (subst g x e2) (subst thn x e2) (subst els x e2))]
    [(boolTE b) (boolTE b)]
    [(let1TE id assgn body)
     (if (symbol=? x id)
      (let1TE id e1 e2)              ; shadowing case
      (let1TE id (subst assgn x e2) (subst body x e2)))]
    ))

; interpret expressions
(interp : (TinyExpr -> TinyExpr))
(define (interp e)
  (type-case TinyExpr e
    [(varTE s) (error 'runtime "unrecognized symbol")]
    [(numTE n) (numTE n)]
    [(boolTE b) (boolTE b)]
    [(addTE e1 e2) (numTE (+ (numTE-n (interp e1)) (numTE-n (interp e2))))]
    [(ifTE g thn els)
     (if (boolTE-b (interp g))
         (interp thn)
         (interp els))]
    [(let1TE x e1 e2)
     (interp (subst e2 x (interp e1)))]))

We design the following type-system for this language:

\[\dfrac{\texttt{Γ}(x) = \texttt{τ}}{\texttt{Γ ⊢ x : τ}}(\text{T-var})\] \[\dfrac{}{\texttt{Γ ⊢ num : Number}}(\text{T-Num}) \quad\quad \dfrac{}{\texttt{Γ ⊢ true : Bool}}(\text{T-true}) \quad\quad \dfrac{}{\texttt{Γ ⊢ false : Bool}}(\text{T-false}) \quad\quad\] \[\dfrac{\texttt{Γ ⊢ e1 : Bool} \quad\quad \texttt{Γ ⊢ e2 : τ} \quad\quad \texttt{Γ ⊢ e3 : τ}} {\texttt{Γ ⊢ (if e1 e2 e3) : τ}}(\text{T-If})\] \[\dfrac{\texttt{Γ ⊢ e1 : Number} \quad\quad \texttt{Γ ⊢ e2 : Number}} {\texttt{Γ ⊢ (+ e1 e2) : Number}}~\text{(T-Add)}\] \[\dfrac{\texttt{Γ ⊢ e1} : \texttt{τ1} \quad \quad \texttt{Γ} ∪ \texttt{\{x ↦ τ1\}} \vdash \texttt{e2} : \texttt{τ2} } {\texttt{Γ ⊢ (let (x : τ1 e1) e2) : τ2}}(\text{T-Let})\]

For each of the following derivation trees, state whether the tree is valid or invalid according to the typing rules above. 3 points of credit are given for each correctly marked answer. Some rule names are omitted for space; this does not invalidate the typing rule.

  1. \[\dfrac{\dfrac{}{\texttt{\{\} ⊢ 1 : Number}}~\text{(T-Num)} \quad\quad \dfrac{}{\texttt{\{\} ⊢ 2 : Number}}~\text{(T-Num)}} {\texttt{\{\} ⊢ (+ 1 2) : Number}}~\text{(T-Add)}\]
  2. \[\dfrac{\dfrac{}{\{\} ⊢ \texttt{true : Bool}} \quad \dfrac{}{\{\} ⊢ \texttt{10 : Number}} \quad \dfrac{}{\{\} ⊢ \texttt{false : Bool}} }{\{\} ⊢ \texttt{(if true 10 false) : Number}}~\text{(T-If)}\]
  3. \[\dfrac{\dfrac{}{\texttt{\{\} ⊢ x : Bool}}}{\texttt{\{\} ⊢ (let (x : Bool true) x) : Bool}}~\text{(T-Let)}\]

Problem 1b [6 Points]

Continuing with the TinyExpr language above, define a term called problem-1b of type TinyExpr that is not well-typed and does not cause the interpreter to have a runtime error.

No partial credit will be given on this problem.

Problem 1c [5 Points]

Suppose you are using the following alternative type-system for TinyExpr, where all of the rules are the same except for T-Let which is now the following:

\[\dfrac{ \texttt{Γ} ∪ \{\texttt{x ↦ τ}\} \vdash \texttt{e2} : \texttt{τ2} } {\texttt{Γ ⊢ (let (x : τ e1) e2) : τ2}}(\text{T-Let})\]

Define a term problem-1c of type TinyExpr that is well-typed according to these new rules, but that causes a run-time error in the above interpreter.

No partial credit will be given on this problem.

Problem 1d [10 Points, 2.5 Points each]

Mark each of the following as true or false (no partial credit):

  1. Adding functions to our TinyExpr grammar is a change to the host semantics.
  2. The fact that TinyExpr numbers can be floating point, integer-valued, or rational-valued is an example of host semantics.
  3. All type checkers always prevent all possible runtime errors.
  4. $\Omega$ can be typed in the simply-typed $\lambda$-calculus.

Problem 2: Designing a type-system [70 Points]

In this problem, we will be designing an interpreter and type-checker for an imperative language. Imperative languages look different than the kinds of programming languages we’ve been working with so far: their syntax consists of expressions and statements. Examples of imperative languages include Python and Java. Here is the abstract syntax for our tiny imperative language:

(define-type ImpExp
  [varE (v : Symbol)]
  [numE (n : Number)]
  [boolE (b : Boolean)]
  [ifE (g : ImpExp) (thn : ImpExp) (els : ImpExp)]
  [addE (e1 : ImpExp) (e2 : ImpExp)])

(define-type ImpStatement
  [seqS (s1 : ImpStatement) (s2 : ImpStatement)]
  [assignS (var : Symbol) (assignment : ImpExp)])

(define-type ImpProgram
  [prog (p : ImpStatement) (ret : ImpExp)])

(define-type Value
  [VBool (b : Boolean)]
  [VNum (n : Number)])

For example, the following ImpProgram:

(prog
  (seqS
    (assignS 'x (numE 2))
    (assignS 'x (addE (varE 'x) (numE 10))))
  (varE 'x))

can be translated syntactically into the equivalent Python program.

x = 2
x = x + 10
x

Note: 5 points of your score (out of the 70 for Problem 2) will be style. Your solution should make use of type-case instead of cond, should contain type annotations for all functions, should have a comment describing the purpose of each function, and should have at least 2 test cases for each defined function. We will deduct 1 point from your style score for each missing component.

Problem 2a: An imperative interpreter, part 1 [15 Points]

In this problem, you will implement an interpreter interp-e of type (Env ImpExp -> Value) that evaluates ImpExps. The type Env is a mutable environment; a basic interface to manipulate environments is given for you in the starter code. Additionally we have given you two functions value->int and value->bool that extracts the Numbers and Bools bound in an expression of type Value, respectively.

ImpExp consists of variable references (varE), number constants (numE), Boolean constants (boolE), if-expressions ifE, and addition addE. The semantics of these expressions is identical to that of the languages we have seen in class.

  • ifE g thn els should raise a 'runtime error if g does not evaluate to a VBool.
  • addE e1 e2 should raise a 'runtime error if either of its arguments do not evaluate to VNum.
  • varE s should raise a 'runtime error if s is not found in Env.

Example:

>(interp-e 
  (box (hash (list (pair 'x (VNum 5)))))
  (addE (varE 'x) (numE 10)))
(VNum 15)

We will evaluate your solution based on the fraction of tests that pass.

Problem 2b: An imperative interpreter, part 2 [15 Points]

In this problem, you will implement an interpreter interp-p of type (ImpProgram -> Value) that evaluates ImpPrograms. You will likely need a helper function.

  • The semantics of an ImpStatement consists of the following semantics:
    • seqS s1 s2 evalautes s1 and then evaluates s2 in sequence.
    • assignS var assignment assigns variable var equal to the result of evaluating assignment. If var is already assigned, then it is updated to be the new result.
  • The semantics of an ImpProgram, which will have the form (prog p ret), is to (1) run p to get an environment containing assignments to variables, and (2) return the result of running ret in the environment obtained from (1).

Example:

>(interp-p (prog (seqS
                  (assignS 'x (numE 5))
                  (assignS 'x (addE (varE 'x) (numE 10))))
            (varE 'x))) 
(VNum 15)

We will evaluate your solution based on the fraction of tests that pass.

Problem 2c: An imperative typechecker [35 Points]

Now, we will make a type-checker for our imperative language so that well-typed programs do not raise 'runtime errors. We will use the following Type datatype:

(define-type Type
  [TNum]
  [TBool])

Make a function type-of-p p of type (ImpProgram -> Type) that gives the type of the returned value from the program and raises a 'type-error if p would cause a runtime error for the interpreter in Part 2a.

Example:

> (type-of-p (prog (assignS 'x (numE 10)) (varE 'x)))
(TNum)

> (type-of-p (prog (assignS 'x (numE 10)) (varE 'y)))
; raises 'type-error

We will evaluate your solution based on the total fraction of tests that pass from two categories of tests:

  1. Tests that check that any program that can raise a 'runtime error for the interpreter in Part 2a raise 'type-errors when type-checked.

  2. Tests that check that valid programs (i.e., programs that do not cause runtime errors) do not raise 'type-errors.

    Note: Just like we’ve seen in class, your solution should raise a type error for programs where ifE would return different types for the two branches, i.e. (ifE (boolE #t) (numE 10) (boolE #f)) should cause a 'type-error. In all other cases, if running the program in the interpreter does not cause a 'runtime erorr, then your type-checker should not raise a 'type-error.