In this assignment, you will design and specify a type system for the Self language implemented in the previous assignment. The result of your assignment should be a set of typing judgments defining which Self programs are statically well-typed. You should use this simplified grammar for Self programs:
e ::= i an integer constant | "[" slot1 ... slotN "]" an object | "fn" "(" id1 ... idN ")" "{" e "}" a function | id a reference to a bound name | "let" id "=" e1 "in" e2 a let binding | e0 "." id "(" e1 ... eN ")" a messageslot ::= id "(" id1 ... idN ")" "{" e "}" a method slot
(This version merges statements and expressions into one syntactic form, changing the let statement into an expression in the process. It drops inheritance, since handling inheritance well is rather difficult. It also drops strings, infix and prefix operators, primitive messages, and non-method slots as being "uninteresting.")
You should define (at least) a grammar for types and two families of typing judgments of the form Gamma |- e : tau and tau1 <: tau2. (You probably will need additional grammar definitions and judgments for slots.) You should not need to modify the grammar for expressions or slots to include type declarations, but instead set up a system to infer types of expressions, i.e., to check whether proposed typing derivations are internally consistent.
Your type system should allow method slots within a single object to be mutually recursive.
Your type system need not support parametric polymorphism, but it should support subtype polymorphism.
Your main challenge is to design how to represent the type of an object, so that messages to the object and references to self within methods of the object can all be typechecked. For greater expressiveness, you may want to make the type of an object be a recursive type.
You do not need to implement your type system. (It would be hard to implement it, without adding any type declarations to the expression and slot grammars.)
For a sample program that includes at least one occurrence of each of the above syntactic constructs, including mutually recursive methods, give a typing derivation (a proof tree using your typing rules to prove that your program has some legal type).
Turn in a hard-copy of your type system and typing derivation to Todd. You may write your solution by hand, or format it electronically, or use a mix of both, as long as it is all easy to read.