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$

Examples:

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:

$\begin{equation*} \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} \end{equation*}$

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.

Notation

$\begin{equation*} \Gamma \vdash e : T \end{equation*}$

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:

$\begin{equation*} \frac{(x,T) \in \Gamma} {\Gamma \vdash x : T} \end{equation*}$

Function application rule with environment:

$\begin{equation*} \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} \end{equation*}$

Type Rule for Entire Program

Given a program

  class World {
    Tg_1 xg_1;
    ...
    Tg_n xg_n;

    method1
    ...    
    methodM
  }

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

$\begin{equation*} \Gamma_0 \vdash \mbox{method1} : void, \ldots, \mbox{methodM} : void \end{equation*}$

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

$\begin{equation*} (T\, m(T_1\, x_1,\ldots,T_n\, x_n) \{s; \mbox{return}\ e\} \end{equation*}$

the environment $\Gamma_0$ contains binding

$\begin{equation*} m : T_1 \times \ldots \times T_n \to T \end{equation*}$

Type Rule for Method Bodies

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

$\begin{equation*} \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} \end{equation*}$

Here

$\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:

$\begin{equation*} \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} \end{equation*}$

Type Rule for Assignment

$\begin{equation*} \frac{?} {\Gamma \vdash (x=e) : void} \end{equation*}$

Answer:

Type Rule for If Statement

$\begin{equation*} \frac{?} {\Gamma \vdash (\mbox{if}(e)\ s_1\ \mbox{else}\ s_2) : void} \end{equation*}$

Answer:

Type Rule for Conditional Expression

$\begin{equation*} \frac{?} {\Gamma \vdash (e\ ?\ s_1\ :\ s_2) : T} \end{equation*}$

Answer:

Type Rule for While Statement

$\begin{equation*} \frac{?} {\Gamma \vdash (\mbox{while}(e)\ s) : void} \end{equation*}$

Answer:

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):

$\begin{equation*} \Gamma \vdash \{\} : void \end{equation*}$

$\begin{equation*} \frac{\Gamma \vdash e : T} {\Gamma \vdash \{\textbf{return}\ e\} : T} \end{equation*}$

$\begin{equation*} \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} \end{equation*}$

$\begin{equation*} \frac{\Gamma \vdash s_1 : void,\ \Gamma \vdash \{ s_2 \ldots\ s_n\} : T} {\Gamma \vdash \{ s_1\ s_2\ \ldots\ s_n \} : T} \end{equation*}$

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;
    }
  }
}

Remarks

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