CS 3520 Homework 11

Due: Tuesday, November 24th, 2020 11:59pm

Difficulty:  ★★☆☆

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

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

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

Only the interp part of the language is implemented, so far. The typecheck part is incomplete (there are ....s), 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:

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

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 (run-prog `{if0 2 {lambda {[x : ?]} x} {lambda {[x : ?]} {+ 1 x}}})
        `function)
  (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>).

A list is somewhat like a pair that you added to the language in HW 10, 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 : ?]} {rest x}}]}
                     {+ {first {f {cons 1 {cons 2 empty}}}} 3}})
        `5)
  (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")