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?
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?
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.
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: