# 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:

https://www.captain-teach.org/brown-cs173/assignments/