Programming Assignment 4: Type Checker

Type checking

1. Copy /u/cos320/chap4/* into a new directory as4.
2. If you have your own working copy of fun.lex and fun.grm from assignments 2 and 3 you may use them for this assignment.  If you don't have working versions, then use the ones we provide.
3. Your main job is to edit the file typecheck.sml to implement the functions tc_exp, tc_sub and tc_join.  The typing rules for the Fun language are described in the Fun language definition.  You need to implement these rules.  The main catch is that these rules are declarative.  In other words, they are nondeterministic and do not directly specify an algorithm for type checking.  You need to implement a (deterministic) algorithm for type checking that is sound and complete with respect to the nondeterministic rules  Your algorithm will be sound if whenever it says a program type checks, there exists some typing derivation in the nondeterministic, declarative type system for the program.  Your algorithm will be complete if whenever there exists some typing derivation, your algorithm will find the typing derivation and say the program in question type checks.
   
   The first part of defining the type checking algorithm is defining the subtyping function tc_sub.  When you call tc_sub t1 t2, the function should return true if t1 is a subtype of t2 and return false otherwise.  The subtyping rules in the Fun language definition are nondeterministic and cannot be implemented directly primarily because of the reflexivity rule.  The transitivity rule says:
   
   t1 < t2      t2 < t3                                   
   -------------------  (transitivity)      
           t1 < t3                                   
   
   If we were trying to read this rule bottom-up like a function then it would say t1 is a subtype of t3 if we can magically conjure up some type t2 such that t1 is a subtype of t2 and t2 is a subtype of t3.  Fortunately, if restructure our other subtyping rules a little bit to make sure that overall our subtype in relation is transitive, we don't really need to implement the transitivity rule directly.  In particular, this means it will be necessary to combine the rules for tuples and check all of the conditions for subtyping on tuples at once.
   
   The second part of defining the type checking algorithm requires that you define the function tc_join.  When you call tc_join t1 t2 it should return a third type t3 such that t1 is a subtype of t3 and t2 is also a subtype of t3.  In addition, you should return the "least" type t3 you can.  For example,
   
   tc_join (<int,bool>) (<int>) = <int>
   
   Even though <> is a supertype of both <int,bool> and <int>, it is also a supertype of <int>.  Therefore, the tc_join function should return <int> not <>.  <int> is the least super type of both <int,bool> and <int> and therefore it is a "join."  Hint:  there is a substantial twist when implementing the tc_join function for function types.  Feel free to implement a second, mutually recursive helper function in this case.
   
   The last part of the algorithm involves implementing the type checking algorithm for expressions themselves.  This algorithm will invoke tc_sub and tc_join when necessary.  Notice that in the declarative rules there is a troublesome rule called subsumption:
   
   G |-- e : t     t < t'
   -------------------
   G |-- e : t'
   
   Implementing this rule directly in the function tc_exp is problematic because if we try to read this rule as a function bottom-up in which the arguments to the function are the context G, the expression e and the type t' then we will somehow have to "guess" what type t to recursively invoke tc_exp with.  Moreover, the subsumption rule can always be used.  A stupid type checker might try to check subsumption over and over again and go into an infinite loop.
   
   Instead, what we will do is call tc_exp ctxt e and expect it either to fail (and call function tc_err) or to succeed and return the least type t that e can possibly have in the context ctxt.  The only places that we will use subtyping in our algorithm is when we absolutely have to (or else type checking will fail).  For instance, one place that we might need to use subtyping is when we have a function call f (e).  If f has type t1 -> t2 and e has type t1' then our type checker should succeed if t1' is a subtype of t1.
    
4. As usual, compile by invoking CM.make();.
5. You can test your code by running Compile.compile "file".
6. Submit by running submit 4 <all files>.