Task 1. Develop type-checking algorithms for the following language constructs, along the lines of the type-checking algorithm we developed in the lectures. Here is pseudo-code for typechecking `P+Q`: ```class Div ( lhs : Prog, rhs : Prog ) extends Prog def check ( env : SymbolTable, p : Prog ) : Type = { ... case Div ( l : Prog, r : Prog ) => { if ( check ( env, l ) != Int_T () || check ( env, r ) != Int_T () ) throw new Exception ( "..." ) else Int_T () } } ``` `while0 P do Q` ```class While0 ( cond : Prog, body : Prog ) extends Prog case While0 ( cond, body ) => { val t_cond = check ( env, cond ) if ( t_cond != Int_T ) throw new Exception ( "..." ) val t_body = check ( env, body ) if ( t_body != Unit_T ) throw new Exception ( "..." ) Unit_T () } ``` `repeat P until Q` ```class RepeatUntil ( body : Prog, cond : Prog ) extends Prog case RepeatUntil ( body, cond ) => { val t_body = check ( env, body ) if ( t_body != Unit_T ) throw new Exception ( "..." ) val t_cond = check ( env, cond ) if ( t_cond != Bool_T ) throw new Exception ( "..." ) Unit_T () } ``` The key insight in typechecking letrec x : t = P in Q comes from comparing the typing rules with those for let x : t = P in Q. ``` Γ ⊢ P : α Γ, x : α ⊢ Q : β -------------------------------- Γ ⊢ let x : α = P in Q : β ``` Note that the red assumption does not contain an entry for `x`, unlike here: ``` Γ, x : α ⊢ P : α Γ, x : α ⊢ Q : β ---------------------------------------- Γ ⊢ letrec x : α = P in Q : β ``` Task 2. Some languages have features like exceptions (which can be raised using a construct like `throw`), or Java's `System.exit ( ... )` that immediately aborts the calling program. Discuss how to type-check such program constructs. Answer: The trick is to realise that these constructs can have any type whatsoever as return type, since they never return. For example if `e` has type integer, then `System.exit ( ... )` has type `t` for any type `t`. This is also true for `throw`, but we must have a type of exceptions in our sets of types. Then whatever is being thrown must have be an exception. Task 3. Consider a function/procedure/method as follows: ``` def f( x : ??? ) : ??? = { return x } ``` Discuss what kind of types you would give to `f`. Answer: There are many approaches to this problem. But all involve in some form or shap a new form of type called universal type. Some programming languages write it like this: ``` def [T] f( x : T ) : T = { return x } ``` This means: for any type `T`, the procedure `f` has type ` def f( x : T ) : T = { return x }` For example `f` has type ` def f( x : Int ) : Int = { return x }` and ` def f( x : Bool ) : Bool = { return x }` A lot more could be said about this topic. If you are interested, please contact me, or read the excellent book Types and programming languages by B. Pierce -- it's in the library.