Design 1

We ask you to consider an alternate design for the type rules of datatype. This is a design exercise, so it is intentionally open-ended. If at any point you are unsure about assumptions or consequences, talk to us! Assume that you are given the type language type :== number | boolean | (<type> * ... * <type> -> <type>) | <tid> where tids are type identifiers, reflecting new types introduced by datatype. This type system mirrors the programming language <L> :== <num> | <id> | (fun (<id> : <type> ... <id> : <type>) <L>) | (<L> (<L> ... <L>)) | (<L> + <L>) | (if <L> <L> <L>) | true | false | (zero? (<L>)) | (<L> and <L>) | (<L> or <L>) | (rec <id> <type> <id> <L> <L>) | (datatype <type> [<id> (<id> <type>) ... (<id> <type>)] [<id> (<id> <type>) ... (<id> <type>)] <L>) with semantics as described in the lectures. (Note that we have extended functions to have arity greater than one, and correspondingly extended function application.) Assume that all type, variant and field names are unique. Semantically, recall that each of the selectors of a datatype had to perform a safety check on the value to ensure it was of the right variant before attempting to extract a field. (This is to flag incorrect programs such as (first empty) in Scheme.) Question: Can we build these checks into the type system? If we could, then there would be no need to tag values or to perform safety checks at runtime. Programs would consume less space and run faster! Idea: Each variant of a datatype subscribes a new type in the type system. Each constructor now returns a value of the type corresponding to its variant. Selectors only accept values of their variant's type. The type-checker can thus ensure that selectors are never mis-applied to the wrong variant. Changes to the type system must preserve type soundness. Since we have removed checks from the evaluator, the type rules can no longer rely on them. Exercises Write down the type rules for this language. Indicate all the constructs whose type rules changed. If you are able to write down type rules that, combined with the check-free runtime, result in a sound type system, answer the following questions. Fill in types in place of the two instances of ??? in the following program: (datatype nlist ; declare the two variants: [nempty] [ncons (first number) (rest ???)] ; body expression: (rec loop (??? -> number) L (if (nempty? (L)) 0 (loop ((rest (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.) The type checker works by constructing trees of derivations, as explained in class. Provide a complete type derivation tree to demonstrate the validity of your annotations. Be precise; do not skip steps. If you believe you cannot give type rules that would yield a sound type system on a check-free runtime, answer the following questions. 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. Can you salvage this type system design idea? Or are runtime checks (and thus, tags) unavoidable? Be brief. Turn all solutions in on paper. You may hand-write type judgements if your writing is extremely legible. All other text must be printed. Your solutions are due by 2am on 2000-10-28. Restrictions For this assignment: Do not discuss the problem or solution with others. If you want to discuss your ideas, please do so with the course staff. It really is important that you develop an intuition for such questions on your own. We will not accept late submissions. This homework leads directly to subsequent classroom material, so this restriction is both a carrot and a stick: a stick because we will probably discuss the solution in class, and a carrot because without an intuitive feel for this problem, the subsequent lectures won't make as much sense.