• Homework
• Resources

Homework #8: Typechecking lists

Out: Friday, March 17th, Due: Monday, March 27th, 4:30pm

Administrative

The language for this homework is:

#lang plait

In this homework you will start with Typed infered Language with lists, functions, numbers, and booleans (a typed toy language, partially extended to support lists). This is the same as as tifae from class, with

• New variants Lst and Cons added to the abstract syntax (and parser updated to generate those)
• Updated the value type FAE-Value
• Updated the type syntax TE
• Updated the type representing FAE types Type
• Added stubs to the the typechecker function typecheck
• Added stubs to the evaluator interp
• Added stub to unify!

Typechecking and Evaluating Lists

Update the following to get typechecking and evaluating lists working.

• The typechecker function typecheck
• The evaluator interp
• Any auxilary functions needed by these functions. You can also create new auxilary functions if needed. Note that some functions may need updating, even if no stubs were added to get them compiling.

;; lists of numbers
(test (run `{list 1 2})
      (ListV (list (NumV 1) (NumV 2))))
(test/type `{list 1 2} (ListT (NumT)))

;; lists of booleans
(test (run `{list false true})
      (ListV (list (BoolV #f) (BoolV #t))))

;; 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))))

;; 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)))

Cons

Add a builtin Cons to FAE. This should have a similar type signature to plait’s cons (and indeed will most likely use cons in its implementation).

You can simplify your implementation of interp for Cons by assuming the code being evaluated passes the typechecker.

Your code should pass (at least) these tests:

;; cons to empty list
(test (run `{cons 1 {list}}) (ListV (list (NumV 1))))
(test/type `{cons 1 {list}} (ListT (NumT)))

;; cons to non-empty list
(test (run `{cons 1 {list 2}}) (ListV (list (NumV 1) (NumV 2))))
(test/type `{cons 1 {list 2}} (ListT (NumT)))

;; infer type of cons
(test/type `{lam {x : ?} {cons x {list 1}}} (ArrowT (NumT) (ListT (NumT)))) ;; inferen

;; report error for cyclic type
(test/notype `{lam {x : ?} {cons x x}})

Finally

Define minutes-spent as the number of minutes you spent on your homework.