CS 536 (F02) Homework 8: Type System Design

Assignment Goals

• To explore a different set of typing rules for datatypes.

We are interested in building type-safe and type-sound languages, as described in the lecture notes. Recall the typed language from homework 7 that includes numbers, booleans, conditionals, functions, and lists of numbers. Consider the typing rules for lists of numbers and a sample solution to the typechecker.

Exercises

Consider the following program (call it P):

   {let {zerofirst? {nlist -> boolean} {fun : {L : nlist} : boolean {iszero {nfirst L}}}}
      {zerofirst? nempty}} 

1. Without running the sample or your solution to homework 7, what should a type-safe/sound implementation of the language return on P and why?

2. What would (type-of (parse P)) produce (and why!) under the typing rules for lists and your solution to hwk 7 (or mine, if yours doesn't implement the given typing rules for lists)?

3. Characterize the kinds of type errors that our current typing rules require the interpreter to check at run-time. (You can give examples, but full credit requires you to explain the general class of errors that require run-time checks).

4. Assume we replaced the type nlist from homework 7 with new types nempty and ncons; this would produce the type language

      <type> ::= number
               | boolean
               | nempty
               | ncons
               | (<type> -> <type>)
   

   Design typing rules for the list primitives (nempty, ncons, nempty?, nfirst, and nrest) in this new type language. With your answer, do one of the following two questions:
   1. If you are able to write down type rules that, combined with the check-free interp, result in a sound type system, answer the following questions.
      1. Fill in types in place of the ??? in the following program:

              (rec loop (??? -> number) L
                  (bif (nempty? (L))
                       0
                       (loop ((nrest (L)))))
                (loop ((ncons (1 (nempty ())))))))
         

         (The function doesn't do anything useful. You could imagine using length instead, but it would just make your solution to the next problem much larger.)
      2. The type checker works by constructing trees of derivations, as shown in the notes. Provide a complete type derivation tree to demonstrate the validity of your annotations. Be precise; do not skip steps.
   2. If you believe you cannot give type rules that would yield a sound type system on a check-free interp, answer the following questions.
      1. Clearly explain why you cannot do this. You may use the sample program above to illustrate your claim, but you must explain the problem in general terms.
      2. Can you salvage this type system design idea? Or are runtime checks (and thus, tags) unavoidable? Be brief.

Guidelines

1. Do this assignment entirely on your own,without consulting others in the class, materials beyond lecture notes on our web page, etc.

2. You are not expected to write any code for this assignment.

3. You may write your solutions by hand, but they must be legible. If in doubt, type them up!