Tutorial Week 7 (Solutions) |

- 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 : β
This is also true
for
def f( x : ??? ) : ??? = { return x }Discuss what kind of types you would give to `f` .
def [T] f( x : T ) : T = { return x } This means: for any
type def f( x : T ) : T = { return x } For example 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. |