CS 3520 Homework 11

Due: Friday, December 1st, 2023 11:59pm

Difficulty:  ★★☆☆

Start with hw11_starter.rhm, which is based on infer_lambda.rhm.

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

  <Exp> = <Number>
        | <Exp> + <Exp>
        | <Exp> * <Exp>
        | <Symbol>
        | fun (<Symbol> :: <Type>): <Exp>
        | <Exp>(<Exp>)
        | []
        | cons(<Exp>, <Exp>)
        | first(<Exp>)
        | rest(<Exp>)
        | (<Exp>)
  
   <Type> = Int
          | Boolean
          | <Type> -> <Type>
          | ?
          | Listof(<Type>)
          | (<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 if.

Your solution should not add any calls to resolve, except maybe in tests, because it’s not useful outside of the one place in unify. That is, the only call to resolve that’s not in a test should be the one that’s in unify in the starting code.

Part 1 — Inferring Conditional Types

Extend the language with an if form with its usual meaning and form constrained to == 0:

  <Exp> = ....
        | if <Exp> == 0 | <Exp> | <Exp>

Also, add a run_prog function that takes a syntax object, parses it, typechecks it, and interprets it. If the parsed syntax has no type, run_prog should raise an expression including the words “no type”. Otherwise, the result from run_prog should be a syntax object: an syntax number if interp produces any number, the syntax object 'function' if interp produces a closure, or the syntax object 'list' if interp produces a list.

Examples:

  check: run_prog('if 0 == 0 | 1 | 2')
         ~is '1'
  
  check: run_prog('if 3 == 0 | 1 | 2')
         ~is '2'
  
  check: run_prog('if 2 == 0 | (fun (x :: ?): x) | (fun (x :: ?): 1 + x)')
         ~is 'function'
  
  check: run_prog('if (fun (x :: ?): x) == 0 | 1 | 2')
         ~raises "no type"
  
  check: run_prog('if 0 == 0 | (fun (x :: ?): x) | 2')
         ~raises "no type"
  
  check: run_prog('let f :: ? = (fun (x :: ?):
                                   fun (y :: ?):
                                     fun (z :: ?):
                                       if x == 0 | y | z):
                     f(1)(2)(3)')
         ~is '3'
  
  check: run_prog('let f :: ? = (fun (x :: ?):
                                   fun (y :: ?):
                                     fun (z :: ?):
                                       if x == 0
                                       | y
                                       | fun (x :: ?): z):
                     f(1)(fun (x :: Int): 2)(3)(4)')
         ~is '3'
  
  check: run_prog('let f :: ? = (fun (x :: ?):
                                   if x == 0 | x | x(1)):
                     f(1)')
         ~raises "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, []) should have type Listof(Int). Similarly, the expression cons(fun (x :: Int): x, []) should have type Listof(Int -> Int).

The expression [] 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 [] expression form to make sense (or else we’d need one [] 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:

  check: run_prog('[]')
         ~is 'list'
  
  check: run_prog('cons(1, [])')
         ~is 'list'
  check: run_prog('cons([], [])')
         ~is 'list'
  check: run_prog('cons(1, cons([], []))')
         ~raises "no type"
  
  check: run_prog('first(1)')
         ~raises  "no type"
  check: run_prog('rest(1)')
         ~raises  "no type"
  
  check: run_prog('first([])')
         ~raises  "list is empty"
  check: run_prog('rest([])')
         ~raises  "list is empty"
  
  check: run_prog('let f :: ? = (fun (x :: ?):
                                   first(x)):
                     f(cons(1, [])) + 3')
         ~is '4'
  check: run_prog('let f :: ? = (fun (x :: ?):
                                   rest(x)):
                     first(f(cons(1, cons(2, [])))) + 3')
         ~is '5'
  check: run_prog('let f :: ? = (fun (x :: ?):
                                   fun (y :: ?):
                                     cons(x, y)):
                     first(rest(f(1)(cons(2, []))))')
         ~is '2'
  
  check: run_prog('fun (x :: ?):
                     cons(x, x)')
         ~raises "no type"
  
  check: run_prog('let f :: ? = (fun (x :: ?): x):
                     cons(f(1), f([]))')
         ~raises "no type"