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 }
  

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.