In this assignment you will create the type checker for the Fun language.
The typing rules for Fun are described in the Fun language
definition.
Type checking
Copy /u/cos320/chap4/* into a new directory
as4.
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.
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.
As usual, compile by invoking CM.make();.
You can test your code by running Compile.compile
"file".