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.