One important real-world type system issue we haven't dealt with in this course is overloading. Many programmers, either in fits of linguistic passion, or in moments of turbid thinking, or simply out of ignorance, confuse this feature for many others, most often polymorphism (of either kind).
Overloading is really the assignment of one name to many different operators. Which operator gets used depends on the types of the arguments; some process selects the actual operator and invokes it on those values. The different operators may have nothing in common; each one may be implemented in a manner entirely distinct from the others. Think of overloading as a syntactic add-on to an otherwise traditional language of the sorts we have studied in this course.
We will study overloading in a language for graphical animation, based on a typed extension to the iota calculus from the first exam. We've kept the language fairly dumb to reduce your work (see the implementation note at the bottom). The language's grammar is as follows:
<L> := <num> | <id> | (<L> + <L>) | (<L> * <L>) | (fun (<id> : <T>) <L>) | (<L> (<L>)) | now | (< <L> <L> >) | (ellipse <L> <L> <L>) | (rectangle <L> <L>) | (after <L> draw <L>)with the type language
T := time | dim ;; we will refer to this as a dimension | <dim, dim> ;; we will refer to this as a position | <T> -> <T>Notice that there is no numeric type! Every number is either a time or a dimension, depending on how it is used.
This language has two overloaded operations:
This poses a problem to a static type checker. There is no
uniform type that the type checker can assign to these
primitives. Its best bet is to rewrite the program into one
that makes the type evident at each primitive application; for
Your task is to design a type checker that translates the names of all overloaded primitives into their disambiguated implementation names. (Think of the type checker as conveying this information, by rewriting, to the interpreter/compiler, so the latter won't have to figure this out again.) This kind of rewriter is called a type elaborator. Rather than implement it, you must present it as a set of judgements. (Yes, those again.) Though judgements were initially presented as a peculiar way of writing if-then rules, you have since seen judgements take on more functionality. In the polymorphism section, the judgements computed sets of constraints (and, in fact, did no type checking!). In the section on Java types, the judgements elaborated the program to annotate field and some method lookups with their compile-time types. This latter kind of elaboration is very similar to what you will want to do, except yours is much simpler.
One tricky problem: what if the entire expression is, say,
Tips: You may find it easier to first write down a
type system that ignores the overloading and elaboration,
rather than tackle it all at once. Beware that
Please do individual work on this assignment, so you fully understand the related language design issues. You must turn in three things:
Turn in your text on paper. Unless your handwriting is extremely legible, please print your submission. Your responses are due by 11:59pm on 2000-12-06.
Terminology: People sometimes refer to overloading as ad hoc polymorphism. The operative term here is the ``ad hoc'' part there is no rhyme or reason to these operations sharing the same name, other than clashing convention, perceived convenience or programmer caprice. Most programming languages people would not call this a form of polymorphism at all to avoid muddying the waters.
Literacy Note: Overloading is a type issue,
and many languages resolve it in a static type system. ML,
for instance, overloads
Opinion: Overloading is not inherently evil.
As the paragraph above illustrates, most languages internally
have some limited form of overloading. Giving
unrestricted use of this to programmers, however, doesn't seem
too smart. The good examples I've seen seem to all involve
math (e.g., overloading
Implementation Note: Don't worry, you don't
need to implement anything. You could imagine the drawing
language described here being beneath the surface of a tool
Macromedia Flash, especially if