Homework #11 Solution

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, 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 interpproduces 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>).

          
Γ ⊢ 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 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 restexpression 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")