- 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*". - Submit by running
**submit 4 <all files>**.