CS 5510 Homework 10

Due: Friday, November 10th, 2017 11:59pm

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 will be to complete it. First, however, you’ll add if0.

Part 1 — Inferring Conditional Types

Extend the language with an if0 form with its usual meaning:

  <Expr> = ...
         | {if0 <Expr> <Expr> <Expr>}

Also, 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-expression: 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 '{if0 0 1 2})
        '1)
  (test (run-prog '{if0 2 1 0})
        '0)
  (test/exn (run-prog '{if0 {lambda {[x : ?]} x} 1 2})
            "no type")
  (test/exn (run-prog '{if0 0 {lambda {[x : ?]} x} 2})
            "no type")
  (test (run-prog '{let {[f : ?
                            {lambda {[x : ?]}
                             {lambda {[y : ?]}
                              {lambda {[z : ?]}
                               {if0 x y z}}}}]}
                    {{{f 1} 2} 3}})
        '3)
  (test (run-prog '{let {[f : ?
                            {lambda {[x : ?]}
                             {lambda {[y : ?]}
                              {lambda {[z : ?]}
                               {if0 x y {lambda ([x : ?]) z}}}}}]}
                    {{{{f 1} {lambda {[x : num]} 2}} 3} 4}})
        '3)
  (test/exn (run-prog '{let {[f : ?
                                {lambda {[x : ?]}
                                 {if0 x x {x 1}}}]}
                        {f 1}})
            "no type")

Part 2 — Inferring List Types

Complete typecheck for lists. 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>).

   Γ empty : (listof τ)   
Γ e1 : τ     Γ e2 : (listof τ)
Γ (cons e1 e2) : (listof τ)
                  
   
Γ e : (listof τ)
Γ (first e) : τ
   
Γ e : (listof τ)
Γ (rest e) : (listof τ)

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.

Examples:

  (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")

Last update: Wednesday, November 1st, 2017
mflatt@cs.utah.edu