Written: Typed

Question 1: Variants and Unions

Consider a datatype definition that introduces numeric lists as the sum of two variants: nempty and ncons. This defines a new type (nlist), and each constructor (such as ncons) creates a value of that type. As a result, however, selectors (such as nfirst) cannot statically determine whether or not they have been given the correct variant of the datatype, and must rely on a check from the run-time system.

On the Web, you read a proposal for a better design: Suppose, instead, each variant creates a new type. Then you can give a precise type for the selector (e.g., above, nfirst would take only ncons values, not nempty or nlist ones), thus turning the dynamic check into a static one, thereby increasing the effectiveness of the type system. Because this was proposed in Twitter, it's frustratingly short on details.

Can we build an effective type system out of this idea? If so, how, and if not, why not? If we can't as stated, can we turn this into something that actually works? Have you seen any languages that do something like this?

Question 2: Typing Numbers

In Java, there is no single type for numbers, and float, int, etc., are all distinct types and very few of these can be directly substituted for others. At the other extreme, in Pyret, there is a single Number type.

What are the tradeoffs between these two designs? Is there a sense in which Pyret's single type lies?

Question 3: Constraints and Errors

Consider the program:

(+ 1 (first (cons true empty)))
This program has a type error.

Generate constraints for this program. Isolate the smallest set of these constraints that, solved together, identify the type error.

Feel free to label the sub-expressions above with superscripts for use when writing and solving constraints.

Note: the rules for cons—equivalent to Pyret's link—are given in the older book, linked from the current text.

Question 4: Recursive Types

Use rec (from the book) to define a typed version of ω and hence Ω. Explain concretely how the type-checker is able to type these expressions. (If it isn't possible, explain why not.)

Submit at this link: