Type Checking Rules for a Simple Language

Abstract Syntax of a Simple Language

This language is similar to one in Semantic Analysis as Simplified Interpretation, but for simplicity assumes programs have only one class (called World) and all members to are assumed to be static.

program ::= "class" "World" "{" varDecl* method* "}"
method ::= varDecl "(" varDecl* ")" "{" stmt* "return" expr "}"
varDecl ::= type ID
type ::= "int" | "boolean" | "void"
stmt ::= expr | if | while | block 
if ::= "if" expr stmt "else" stmt
while ::= "while""("expr")" stmt 
block ::= "{" (stmt|varDecl)* "}"
expr ::= ID | expr "+" expr | expr "<=" expr
       | assign | call | condExpr 
assign ::= ID "=" expr
condExpr ::= expr "?" expr ":" expr
call ::= ID "(" expr* ")"

Note: this is abstract, not concrete syntax

  • some commas and semicolons are removed
  • keywords and parantheses are kept to make rules clearer
  • in the text below we do not use e.g. quotes around keywords

Remark on language:

  • method call is an expression (resulting type is return type of method)
  • assignment is an expression (resulting type is void, this will not work: x=y=z)

Notation for Type Rules

We write $expr : T$ to indicate that

  • $expr$ is well-typed inside and has resulting type $T$


Type rule for addition:

  e1 : Int, e2 : Int
     e1+e2 : Int

For <=:

  e1 : int, e2 : int
     e1<=e2 : boolean

Type derivation for

3 + 5 <= 9

is the following

  3 : Int, 5 : Int
  ---------------- , 9 : Int
    3 + 5 : Int
      (3 + 5 <= 9) : boolean

Type Rule for Function Application

We have

  • $n : \mbox{Int}$
  • ${+} : \mbox{Int} \times \mbox{Int} \to \mbox{Int}$
  • ${\le} : \mbox{Int} \times \mbox{Int} \to \mbox{boolean}$
  • $b : \mbox{boolean}$
  • $\&\& : \mbox{boolean} \times \mbox{boolean} \to \mbox{boolean}$
  • for user-defined functions, rules are given by their declaration

The general rule for operation $\mbox{Op}$ is:

  • if $f : T_1 \times \ldots \times T_n \to T$,
  • and $e_1 : T_1,\ldots, e_n : T_n$,
  • then $f(e_1,\ldots,e_n) : T$

We write this as the following application typing rule:

\frac{e_1 : T_1, \ldots, e_n : T_n,\ f : T_1 \times \ldots \times T_n \to T}
     {f(e_1,\ldots,e_n) : T}

What does it correspond to in Semantic Analysis as Simplified Interpretation?

  • checks in parameter passing, see insertArgs function

Type Rules with Environment

To know types of variables, type rules must refer to the environment.


    \Gamma \vdash e : T

means that in environment $\Gamma$, expression $e$ is type correct and has type $T$

  • $\Gamma$ is a partial function from names (of variables, operators, and methods) to types

Shorthand $\Gamma \vdash e_1:T_1,\ldots,e_n:T_n$ means $\Gamma \vdash e_i:T_i$ for $1 \le i \le n$

Variable rule with environment:

  \frac{(x,T) \in \Gamma}
       {\Gamma \vdash x : T}

Function application rule with environment:

\frac{\Gamma \vdash e_1 : T_1, \ldots, e_n : T_n,\ f : T_1 \times \ldots \times T_n \to T}
     {\Gamma \vdash f(e_1,\ldots,e_n) : T}

Type Rule for Entire Program

Given a program

  class World {
    Tg_1 xg_1;
    Tg_n xg_n;


The program is type correct if each method is type correct:

   \Gamma_0 \vdash \mbox{method1} : void, \ldots, \mbox{methodM} : void

where the initial environment $\Gamma_0$ contains:

  • types of predefined operators like $+$, $\le$, $\&\&$ and constants $true$, $false$, $0$, $1$
  • types of global variables, $xg_i : T_i$ for each global variable declaration $\mbox{Tg_i}\ x_i$
  • types of declared methods: for each method definition

   (T\, m(T_1\, x_1,\ldots,T_n\, x_n) \{s; \mbox{return}\ e\}

the environment $\Gamma_0$ contains binding

   m : T_1 \times \ldots \times T_n \to T

Type Rule for Method Bodies

Note that environment $\Gamma$ already contains the expected type that the method is supposed to have.

\frac{\Gamma \vdash m : T_1 \times \ldots \times T_n \to T,\
      \Gamma \oplus \{x_1 \mapsto T_1,\ldots, x_n \mapsto T_n\} \vdash 
         \{s; \mbox{return}\ e\} : T}
     {\Gamma \vdash (T\, m(T_1\, x_1,\ldots,T_n\, x_n) \{s; \mbox{return}\ e\}) : void}


  • $\oplus$ denotes overriding one map with another, as seen in Maps in Math
  • we give a dummy 'void' type to indicate that method is well-defined
    • the assumption of type rule checks that the return type is correct
    • later we present more elegant approach using lambda calculus

Type Rule for Method Calls

Method calls are just function applications:

\frac{\Gamma \vdash e_1 : T_1, \ldots, e_n : T_n, m : T_1 \times \ldots \times T_n \to T}
     {\Gamma \vdash m(e_1,\ldots,e_n) : T}

Type Rule for Assignment

Type Rule for If Statement

Type Rule for Conditional Expression

Type Rule for While Statement

Type Rules for Block Statement

Note that variable declarations are allowed in blocks

  • we type statements one by one
  • declarations introduce new bindings into the environment

We apply these rules (with those listed first having higher priority):

\Gamma \vdash \{\} : void

\frac{\Gamma \vdash e : T}
     {\Gamma \vdash \{\textbf{return}\ e\} : T}

\frac{\Gamma \oplus \{x \mapsto T_1\} \vdash \{ s_2 \ldots\ s_n\} : T}
     {\Gamma \vdash \{ T_1\, x; s_2\ \ldots\ s_n \} : T}

\frac{\Gamma \vdash s_1 : void,\ \Gamma \vdash \{ s_2 \ldots\ s_n\} : T}
     {\Gamma \vdash \{ s_1\ s_2\ \ldots\ s_n \} : T}

Using Rules in an Example

class World {
  boolean z;
  int u;
  int f(boolean y) {
    z = y;
    if (u > 0) {
      int z;
      z = f(u) + 3;
      return z+z;
    } else {
      return 0;


Seen notion of type rules through an example of a simple language

Advantages of rules versus semantic analyzer implementation:

  • more concise
  • precise meaning, make correctness proofs simpler
  • more declarative
    • we could execute them from top to bottom, but there are other interpretations