Complete this assignment with the same team you worked with for Continuations (Written). You and your partner must each understand the answers to all the problems, so don't just split up the work.
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
nempty) 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 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
- function definition
- function application
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.
Turn in your answer to each problem in a separate text or PDF file.