CS 5510 Homework 10

Due: Thursday, November 17th, 2011 10:45am

Inferring List Types

Start with tifae-t.rkt.

Add empty, cons, first, and rest expressions to the language, using abstract-syntax expression constructors mt, cns, fst and rst. Also add a listofTE type-expression constructor, a listofT type constructor, cnsV value constructor, and (mtV) value.

The listofT type constructor takes another type for the elements of a list. For example, the expression (whose concrete syntax is) {cons 1 empty} has type (listofT (numT)). Similarly, the expression (whose concrete syntax is) {cons {fun {x : num} x} empty} has type (listofT (arrowT (numT) (numT))).

The expression empty can have type (listof T) for any T. Similarly, cons should work on a T and a (listof T) for any T, while first and rest work on a (listof T).

A list is somewhat like a pair that you added to the language in HW 9, but it is treated differently by the type system. Note that type inference is needed for a plain empty expression form to make sense (or else we'd need one empty for every type of list element). Type-inferring and checking a first or rest expression will be similar to the application case, in that you'll need to invent a type variable to stand for the list element's type.

Some tests:

(test (unify! (typecheck (fun 'x (guessTE)
                              (cns (num 10) (rst (id 'x))))
                         (mtEnv))
              (arrowT (listofT (numT)) (listofT (numT)))
              (num -1))
      (values))

(test (unify! (typecheck (app (fst (cns (fun 'x (guessTE) (id 'x)) 
                                        (mt)))
                              (fun 'y (numTE) (id 'y)))
                         (mtEnv))
              (arrowT (numT) (numT))
              (num -1))
      (values))

(test/exn (typecheck (cns (fun 'x (guessTE) (id 'x)) 
                          (cns (num 5)
                               (mt)))
                     (mtEnv))
          "no type")