CS 6510 Homework 10

Due: Tuesday, April 11th, 2017 11:59pm

Inferring List Types

Start with hw10-starter.rkt, which is based on infer-lambda.rkt.

The language implemented by hw10-starter.rkt adds empty, cons, first, and rest expressions to the language, and a listof type constructor:

  <Expr> = <Num>
         | {+ <Expr> <Expr>}
         | {* <Expr> <Expr>}
         | <Sym>
         | {lambda {[<Sym> : <Type>]} <Expr>}
         | {<Expr> <Expr>}
         | empty
         | {cons <Expr> <Expr>}
         | {first <Expr>}
         | {rest <Expr>}
  
   <Type> = num
          | bool
          | (<Type> -> <Type>)
          | ?
          | (listof <Type>)

Only the interp part of the language is implemented, so far. The typecheck part is incomplete, and your job is to complete it. Your typecheck must ensure that an expression with a type never triggers a “not a list” or “not a number” error from interp, although an expression with a type may still trigger a “list is empty” error.

The listof type constructor takes another type for the elements of a list. For example, the expression {cons 1 empty} should have type (listof num). Similarly, the expression {cons {fun {x : num} x} empty} should have type (listof (num -> num)).

The expression empty can have type (listof <Type>) for any <Type>. Similarly, cons should work on arguments of type <Type> and (listof <Type>) for any <Type>, while first and rest work on an argument of type (listof <Type>).

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.

Add a run-prog function that takes an S-expression, parses it, typechecks it, and interprets it. If the parsed S-expression has no type, run-prog should raise a “no type” exception. Otherwise, the result from run-prog should be an S-xpression: an S-expression number if interp produces any number, the S-expression `function if interp produces a closure, or the S-expression `list if interp produces a list.

Examples:

  (test (run-prog '1)
        '1)
  
  (test (run-prog `empty)
        `list)
  
  (test (run-prog '{cons 1 empty})
        `list)
  (test (run-prog '{cons empty empty})
        `list)
  (test/exn (run-prog '{cons 1 {cons empty empty}})
            "no type")
  
  (test/exn (run-prog '{first 1})
            "no type")
  (test/exn (run-prog '{rest 1})
            "no type")
  
  (test/exn (run-prog '{first empty})
            "list is empty")
  (test/exn (run-prog '{rest empty})
            "list is empty")
  
  (test (run-prog '{let {[f : ?
                            {lambda {[x : ?]} {first x}}]}
                     {+ {f {cons 1 empty}} 3}})
        '4)
  (test (run-prog '{let {[f : ?
                            {lambda {[x : ?]}
                              {lambda {[y : ?]}
                                {cons x y}}}]}
                     {first {rest {{f 1} {cons 2 empty}}}}})
        '2)
  
  (test/exn (run-prog '{lambda {[x : ?]}
                         {cons x x}})
            "no type")
  
  (test/exn (run-prog '{let {[f : ? {lambda {[x : ?]} x}]}
                         {cons {f 1} {f empty}}})
            "no type")