5 Types 2

8.15

5 Types 2🔗

Instructions:

Due date: Monday, February 24 at 11:59PM
Upload your solutions to GradeScope here. You should upload a single file called code.rkt. Be sure to check that your uploaded solution is valid; you will receive 0 points if your solution does not run.
Your programs will be evaluated on the fraction of tests that they pass. We will show you some tests, but not all tests. You should test your code thoroughly. After the submission deadline, we will reveal the hidden tests.
Starter code: here.

5.1 Typechecking RecLang [30 Points]🔗

In this problem we will be typechecking the RecLang language with recursion. RecLang has the following abstract syntax, types, and values:

> (define-type RecLangT
    (numRT)
    (boolRT)
    (funRT [arg : RecLangT] [ret : RecLangT]))
> (define-type RecLang
    (varR [s : Symbol])
    (numR [n : Number])
    (addR [e1 : RecLang] [e2 : RecLang])
    (mulR [e1 : RecLang] [e2 : RecLang])
    (equalR [e1 : RecLang] [e2 : RecLang])
    (ifR [g : RecLang] [thn : RecLang] [els : RecLang])
    (lamR (arg : Symbol) [typ : RecLang] [body : RecLang])
    (appR [e : RecLang] [arg : RecLang])
    (letrecR [id : Symbol] [t : RecLangT] [assgn : RecLang] [body : RecLang])
    (letR [id : Symbol] [assgn : RecLang] [body : RecLang]))
> (define-type RecLang
    (varR [s : Symbol])
    (numR [n : Number])
    (lamR (arg : Symbol) [yp : RecLang] [body : RecLang])
    (appR [e : RecLang] [arg : RecLang]))

We have given you a definitional interpreter interp-reclang in the starter code.

Here are the typing rules for RecLang, written as inference rules:

\dfrac{~}{n : \texttt{Num}}~\text{(T-Num)} \qquad \dfrac{~}{b : \texttt{Bool}}~\text{(T-Bool)} \dfrac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau}~\text{(T-Var)} \dfrac{~}{n : \texttt{Num}}~\text{(T-Num)} \dfrac{\texttt{e1 : Num} \quad \texttt{e2 : Num}} {\texttt{(+ e1 e2)} : \texttt{Num}}~\text{(T-Add)} \dfrac{\texttt{e1 : Num} \quad \texttt{e2 : Num}} {\texttt{(* e1 e2)} : \texttt{Num}}~\text{(T-Mul)} \dfrac{\texttt{e1 : Num} \quad \texttt{e2 : Num}} {\texttt{(= e1 e2)} : \texttt{Bool}}~\text{(T-Eq)} \dfrac{\texttt{g : Bool} \quad \texttt{e1} : \tau \quad \texttt{e2} : \tau} {\texttt{(if g e1 e2)} : \tau}~\text{(T-If)} \dfrac{\Gamma, x : \tau_1 \vdash e : \tau_2} {\Gamma \vdash \lambda x : \tau_1 . ~ e : \tau_1 \rightarrow \tau_2}~\text{(T-Abs)} \dfrac{\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \qquad \Gamma \vdash e_2 : \tau_1} {\Gamma \vdash e_1 ~ e_2 : \tau_2}~\text{(T-App)} \dfrac{\Gamma \vdash e_1 : \tau \qquad \Gamma, x : \tau \vdash e_2 : \tau_2 }{\Gamma \vdash (\texttt{let}~x~e_1~e_2) : \tau_2}~\text{(T-Let)} \dfrac{\Gamma, x : \tau_1 \rightarrow \tau_2 \vdash e_1 : \tau_1 \rightarrow \tau_2 \qquad \Gamma, x : \tau_1 \rightarrow \tau_2 \vdash e_2 : \tau_3 }{\Gamma \vdash (\texttt{letrec}~x:(\tau_1 \rightarrow \tau_2)~e_1~e_2) : \tau_3}~\text{(T-LetRec)}
Figure 1: Type system for RecLang.

Implement the function type-check-letrec that returns #t if it is well-typed according to the above typing rules and #f otherwise.

5.2 Typechecking MutLang [30 Points]🔗

In this problem we will be typechecking the MutLang language with mutable state. MutLang has the following abstract syntax and types:

> (define-type MutLangT
    (numMT)
    (boolMT)
    (refMT [t : MutLangT])
    (funMT [arg : MutLangT] [ret : MutLangT]))
> (define-type MutLang
    (varE [id : Symbol])
    (lamE [arg : Symbol] [typ : MutLangT] [body : MutLang])
    (appE [e1 : MutLang] [e2 : MutLang])
    (numE [n : Number])
    (addE [e1 : MutLang] [e2 : MutLang])
    (ifE [g : MutLang] [thn : MutLang] [els : MutLang])
    (equalE [e1 : MutLang] [e2 : MutLang])
    (mulE [e1 : MutLang] [e2 : MutLang])
    (boolE [b : Boolean])
    (locE [l : Number])
    (unboxE [e : MutLang])
    (boxE [e : MutLang])
    (setE [b : MutLang] [v : MutLang]))

Here is the type system for MutLang:

\dfrac{~}{n : \texttt{Num}}~\text{(T-Num)} \qquad \dfrac{~}{b : \texttt{Bool}}~\text{(T-Bool)} \dfrac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau}~\text{(T-Var)} \dfrac{~}{n : \texttt{Num}}~\text{(T-Num)} \dfrac{\texttt{e1 : Num} \quad \texttt{e2 : Num}} {\texttt{(+ e1 e2)} : \texttt{Num}}~\text{(T-Add)} \dfrac{\texttt{e1 : Num} \quad \texttt{e2 : Num}} {\texttt{(* e1 e2)} : \texttt{Num}}~\text{(T-Mul)} \dfrac{\texttt{e1 : Num} \quad \texttt{e2 : Num}} {\texttt{(= e1 e2)} : \texttt{Bool}}~\text{(T-Eq)} \dfrac{\texttt{g : Bool} \quad \texttt{e1} : \tau \quad \texttt{e2} : \tau} {\texttt{(if g e1 e2)} : \tau}~\text{(T-If)} \dfrac{\Gamma, x : \tau_1 \vdash e : \tau_2} {\Gamma \vdash \lambda x : \tau_1 . ~ e : \tau_1 \rightarrow \tau_2}~\text{(T-Abs)} \dfrac{\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \qquad \Gamma \vdash e_2 : \tau_1} {\Gamma \vdash e_1 ~ e_2 : \tau_2}~\text{(T-App)} \dfrac{\Gamma \vdash e : \texttt{Ref}~\tau} {\Gamma \vdash (\texttt{unbox}~e : \tau)}~\text{(T-Unbox)} \dfrac{\Gamma \vdash e : \tau} {\Gamma \vdash (\texttt{box}~e : \texttt{Ref}~\tau)}~\text{(T-Box)} \dfrac{\Gamma \vdash e_1 : \texttt{Ref}~\tau \qquad \Gamma \vdash e_2 : \tau} {\Gamma \vdash (\texttt{set-box!}~e_1~e_2 : \texttt{Num})}~\text{(T-SetBox)}
Figure 2: Type system for MutLang.

We have provided you with a definitional interpreter for MutLang that gives the semantics of this language. To understand the types for the new terms box, set-box!, and unbox, you may need to inspect this interpreter. Note that there is no typing rule for locE; this means that, if a program has a locE syntax in it, it is considered not well-typed.

Implement the function type-check-mutlang that returns #t if it is well-typed according to the above typing rules and #f otherwise.

5.3 Compiling RecLang to MutLang [40 Points]🔗

Notice that MutLang doesn’t have letrec, so it doesn’t seem initially that it is possible to write recursive MutLang programs. However, it is possible to do so by carefully using references using a technique called backpatching. For example, consider the following Plait program:

(let ([my-fun (box (lambda (x) (+ x 1)))])
  (let ([loopy (lambda (x) ((unbox my-fun) x))])
    (let ([_ (set-box! my-fun loopy)])
      (loopy 10))))

The above program runs forever even though it only uses let and lambda! Why? Let’s step through it one line at a time using a relation \rho, e \rightarrow \rho{}’, e{}’ where \rho is a heap that maps addresses to values:

{},

(let ([my-fun (box (lambda (x) (+ x 1)))])

(let ([loopy (lambda (x) ((unbox my-fun) x))])

(let ([_ (set-box! my-fun loopy)])

(loopy 10))))

--evaluate box -->

{0x0 -> (lambda (x) (+ x 1))},

(let ([my-fun 0x0])

(let ([loopy (lambda (x) ((unbox my-fun) x))])

(let ([_ (set-box! my-fun loopy)])

(loopy 10))))

--substitute my-fun -->

{0x0 -> (lambda (x) (+ x 1))},

(let ([loopy (lambda (x) ((unbox 0x0) x))])

(let ([_ (set-box! 0x0 loopy)])

(loopy 10)))

-- substitute loopy -->

{0x0 -> (lambda (x) (+ x 1))},

(let ([_ (set-box! 0x0 (lambda (x) ((unbox 0x0) x)))])

((lambda (x) ((unbox 0x0) x)) 10))

-- evaluate set-box! -->