Assignment 8: Types
Part A
Here are some written questions on typing.

For each of these expressions, either construct a typing proof in TFb, or show exactly why they cannot typecheck (i.e. no derivation tree could ever be built; don’t just informally describe it, use the formal system rules).
a.
(If True Then 0 Else False)
b.
(If True Then (Fun x:Int > x + 1) Else (Fun x:Int > x)) 0
c.
(Fun x:(Bool > Int) > x False)(Fun x:Bool > 4)

Of the following pairs of types, is the left type a subtype of the right type, a supertype, or neither? Justify your answer by showing the proofs in the subtype proof system of the book; if neither holds describe why in words. Pay close attention to the rules, it is easy for intuitions to fail on these examples. Just build a proof tree based on the rules and you know you are correct.
a.
{ x : Int; y : { z : Bool } }
and{ x : Int; y : {}; w : Int }
,b.
{ x : Int } > { }
and{ } > { x : Int }
c.
{ } > { }
and{ } > { x : Int }

Type the following program in STFbR (note this program is not showing the type declarations on
r1/r2
, you need to find types to fill in there such that the program is typeable):Function n:Int > Function r1:{...} > Function r2:{...}> {x = r1.x + 1; y = (If n = 0 Then r1.y  1 Else r2.y +1); z = r2.z + 2}
Part B
Write a type checker for TFbSRX. The language was described in lecture and is in section 6.4 of the book. The TFbSRX/
directory of the FbDK contains the relevant parser and OCaml data type, all you have to do is fill in the file tfbsrxtype.ml with a correct implemention of the typecheck function there. Note that you don’t have to write an interpreter, only the typechecker.
 The file tfbsrx_examples.ml contains quite a few examples for you to test the typechecker with.
 The AST for the language, in file TFbSRX/tfbsrxast.ml, is slightly different from the one at the top of Section 6.4 in the textbook, it is a bit simpler.
 As with the other languages in the FbDK you can use our reference implementations. Type
./reference/TFbSRX/toplevel.exe
(or thewsl
version if you have been using that) to load the type checker intoutop
. The above filetfbsrx_examples.ml
then contains information on how you can invoke the typechecker in testing  either#use
that file or copy/paste in the lines at the top.  Notice that
Raise ..
evaluates to “arbitrary tau” in the rule in the book. As we mentioned in lecture, this is usually handled by introducing an “anything type *”  a type that is equal to every other type in the system. A new typeTBottom
has been added to the type fbtype for this purpose. 
Type checking exceptions can be somewhat tricky; especially their interactions with other expressions and type rules. You need to consider each rule carefully.
For example:
 (Function x:Int > x = 1) (Raise #Exn@Bool False) : Bool Because by function rule  (Function x:Int > x = 1) : Int > Bool and by exception rule  (Raise #Exn@Bool False) : Bottom (arbitrary tau) And because Int and Bottom can be equated, by application rule we have  (Function x:Int > x = 1) (Raise #Exn@Bool False) : Bool `
Submission
For Part A, the upload is as for the other written assignments. For Part B, upload (only) your file tfbsrxtype.ml
which will (hopefully) contain your fully functioning type checker.