Tutorial Week 7 (Solutions)
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.