Assignment 7

The following assignment is due Thursday 4/3 by 8:00 PM. You'll need to submit one crate on Gradescope called assign7.

In this assignment, we're finishing up the workshop assignment from lecture. The following is a specification of the linearly typed lambda calculus.

Linear Typed Lambda Calculus (LTLC)

Syntax

Surface-level syntax:
<expr> ::= <var>
         | ( lambda <var> <type> <expr> )
         | ( <expr> <expr> )
<type> ::= EMPTY | ( FUN <type> <type> )
Mathematical syntax:
\begin{align*} e &::= x \ | \ \lambda x^T. e \ | \ e e \\ T &::= \bot \ | \ T \multimap T \end{align*}

Type System

\[ \frac {} {x : A \vdash x : A} \qquad \frac {\Gamma, x : B, y : C, \Delta \vdash M : A} {\Gamma, y : C, x : B, \Delta \vdash M : A} \] \[ \frac {\Gamma, x : A \vdash M : B} {\Gamma \vdash \lambda x^A . M : A \multimap B} \qquad \frac {\Gamma \vdash M : A \multimap B \qquad \Delta \vdash N : A} {\Gamma, \Delta \vdash M N : B} \]

Semantics

\[ \frac {} {\lambda x . e \Downarrow \lambda x . e} \qquad \frac { e_1 \Downarrow \lambda x . e \qquad e_2 \Downarrow v_2 \qquad e[v_2 / x] \Downarrow v } {e_1 e_2 \Downarrow v} \]

The Task

You should fill in the todo!() items in the given starter code. This includes:

filling in some of the parser (it's rewritten in this assignment using a Peekable iterator)
implementing type checking (basically what we did in lecture)
implementing substitution and evaluation (what we didn't get to in lecture). The only requirement is that your implementation of substitution cannot use clone (because of linearity!)