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