3.17 Type Checking
Complete this assignment with Team Three.
You must submit this in an archive named "wtypec.zip". This archive must contain a folder named "wtypec". This folder must contain all the files specified below. You must attach "wtypec.zip" to an email whose subject is "BYU - Fall 2011 - CS 330 - wtypec" and whose message body contains the name of everyone on your team (each on a separate line.) You must send this email to jay@cs.byu.edu before 5pm (Provo time) on 11/22. Ensure that what you are satisfied with what you submit, because only your chronologically first submission will be graded. Ensure that you follow these instructions exactly, since submissions that do not meet these requirements (i.e. do not have the correct format) will receive no credit, despite the time and energy you put into the assignment. Please see Turn In Policy for more information.
You must submit this in a file named "wtypec.pdf".
3.17.1 Variant Types
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.
3.17.2 Lazy Type Checking
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.
3.17.3 Application
In 850 words or less, describe if and how your knowledge of type checking will help you in your future programming practice. Good answers might discuss how this concept can be applied in interesting programming environments or how knowledge of its subtleties clarifies or improves existing practices, techniques, tools, etc.