You must complete this assignment with Team 3.
This problem is extremely open-ended. It reflects the kind of question you may need to answer if you ever design a language.
Consider our typing rules for datatypes. A datatype declaration defines
a new type (such as nlist), and each constructor (eg, cons) creates a
value of that type. As a result, however, selectors (such as first)
cannot statically determine whether or not they have been given the
correct variant (there are two variants of lists, for instance) of the
datatype, and must rely on a check from the run-time system.
Your boss, who thinks he has a better idea of how to design a type system (your colleagues always do, and so do your students) thinks you’ve made a poor decision. He says that if you instead create a new type for each variant, you can give a very precise type for the selector thus turning the dynamic check into a static one, thereby increasing the effectiveness of the type system. (You ask him what to do about the new type declared in the datatype declaration: should the programmer no longer declare it? Should they declare two or three new types when defining lists? He hasn't of course thought this issue out in that much depth—that's your problem—so he just murmurs and asks you to do at least a little work in return for the brainwave he's just handed you.)
Write at most a page (of reasonably-sized text) exploring this question. Can we build an effective type system out of this idea? If so, how, and if not, why not? If so, why hasn’t someone already done this? If not, can we turn this germ of an idea into something that actually works? Have you seen any languages that do something like this? Solutions to this problem which are much shorter than one page are certainly acceptable so long as they get the point across.
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.
Consider the following typed expression:
{fun {f : B1 } : B2
{fun {x : B3 } : B4
{fun {y : B5 } : B6
{cons x {f {f y}}}}}}
We have left the types unspecified (Bn) to be filled in by the type inference
process. Derive type constraints from the above program. Then solve these
constraints. From these solutions, fill in the values of the boxes. Be sure to
show all the steps specified by the algorithms (i.e., writing the answer based
on intuition or knowledge is insufficient). You should use type variables where
necessary. To save writing, you can annotate each expression with an
appropriate type variable, and present the rest of the algorithm in terms of
these type variables alone (to avoid having to copy the corresponding
expressions). If you do this, be sure to annotate every sub-expression with a
type variable. Be sure the annotations are clearly readable!
Consider the type judgments discussed in the textbook. These rules are for an eager language. Consider the lazy version of the language instead. Pay special attention to the typing rules for
For each one, provide a new rule or, if you believe the existing rule does not change, explain why not. (If you believe neither rule changes, you can answer both parts together.) If you believe any other type judgments should change, mention those as well.