# Introduction

In this assignment you will add type-inference for lists to the unification based interpreter from lecture12. The type inference should be based on the following type rule, which says that list elements can be any type, but they all have to be the same type (just like in plait).

\begin{equation} \frac{\Gamma \vdash e_1 : T\quad \Gamma \vdash e_2 : T\quad \Gamma \vdash e_3:T \;\dots\; \Gamma \vdash e_k : T}{\Gamma \vdash (\mathtt{list}\; e_1 \;e_2 \,\dots\, e_k) : (\mathrm{List} \; T)} \end{equation}

Start by downloading the skeleton interpreter This is the same as ti-interp.rkt from class, with change described in the next section.

# Changes from Lecture 12

A new variant has been added to the `Type`

type, and to the
corresponding `TE`

type representing abstract syntax for types. The
function `parse-type`

for mapping between them was also updated. A
`....`

stub was added to `unify!`

, that you will have to fill in in
the next step.

```
(define-type TE
[numTE]
[boolTE]
[arrowTE (arg : TE) (result : TE)]
[listTE (element : TE)] ;; New
[guessTE])
(define-type Type
[numT]
[boolT]
[arrowT (arg : Type) (result : Type)]
[listT (element : Type)] ;; New
[varT (id : Number) (val : (Boxof (Optionof Type)))])
```

The abstract syntax has been updated to include a `listE`

variant. A
stub has been added to `interp`

, that you will fill in below.

```
(define-type Exp
[numE (n : Number)]
[boolE (b : Boolean)]
[notE (expr : Exp)]
[plusE (lhs : Exp) (rhs : Exp)]
[minusE (lhs : Exp) (rhs : Exp)]
[timesE (lhs : Exp) (rhs : Exp)]
[listE (elements : (Listof Exp))] ;; New
[if0E (test-expr : Exp) (then-expr : Exp) (else-expr : Exp)]
[recE (name : Symbol) (ty : TE) (rhs-expr : Exp) (body-expr : Exp)]
[idE (name : Symbol)]
[lamE (param : Symbol) (argty : TE) (body : Exp)]
[appE (lam-expr : Exp) (arg-expr : Exp)])
```

A new variant has been added to the `Value`

type to return lists.

```
(define-type Value
[numV (n : Number)]
[boolV (b : Boolean)]
[listV (elements : (Listof Value))]
[closureV (param : Symbol)
(body : Exp)
(env : ValueEnv)])
```

# Question 1: update `unify!`

Update the given skeleton for `unify!`

to handle list types. Follow
the pattern for `arrowT`

, and make sure your updated function passes
the following functions.

```
(module+ test
(test (unify! (listT (boolT)) (listT (boolT)) 'test) (void))
(test/exn (unify! (listT (boolT)) (listT (numT)) 'test) "no type")
(test/exn (unify! (boolT) (listT (numT)) 'test) "no type")
(test/exn (unify! (listT (numT)) (boolT) 'test) "no type"))
```

# Question 2: evaluating lists

Update the given skeleton for `interp`

to evaluate lists.
Your solution should pass (at least) the following tests

```
(module+ test
(test (run `{list 1 2}) (listV (list (numV 1) (numV 2))))
(test (run `{list false true false}) (listV (list (boolV #f) (boolV #t) (boolV #f)))))
```

# Question 3: typechecking lists

Replace the stub in `typecheck`

to enable typechecking of lists. Your solution should
pass (at least) the following tests

```
(module+ test
;; lists of numbers
(test/type `{list 1 2} (listT (numT)))
;; report error for mixed types
(test/notype `{list 1 true})
;; infer type of list
(test/type `{lam {x : num} {list x}} (arrowT (numT) (listT (numT))))
;; functions taking list parameters
(test/type `{lam {x : {listof num}} x}
(arrowT (listT (numT)) (listT (numT))))
;; report error for mixed inferred types
(test/notype `{lam {x : num} {list true x}})
;; infer type of function parameter from list element
(test/type `{lam {x : ?} {list x 1}} (arrowT (numT) (listT (numT))))
;; complain about cyclic type (Y-combinator) inside list
(test/notype `{lam {x : ?} {list {x x}}})
;; infer type of list from function application
(test/type `{{lam {x : ?} {list x}} 2} (listT (numT)))
)
```

# Tests

Referring to the grading grading rubric for guidance, add any needed tests for your solution.

As always, make sure you have complete test coverage.