Task 1. Develop type-checking algorithms for the following language constructs, along the lines of the type-checking algorithm we developed in the lectures.

  • P/Q
  • while0 P do Q. This is like conventional while except that the loop terminates when P hits 0.
  • repeat P until Q
  • letrec x : t = P in Q. This is like let except that let can occur in P.

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.

Task 3. Consider a function/procedure/method as follows: 

 def f( x : ??? ) : ??? = { return x }
Discuss what kind of types you could give to f, replacing the ???, and how type-checking would have to be adapted to type-check such code.

Task 4. In the lectures you heard that type checking catches variables that are used before they are declared. Convince yourself that this is true by trying to construct a counterexample, ie. try and construct a program (in the toy language we used in Friday's lecture) that uses a variable before it is declared (or that is not declared at all).