Type Rules using 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*}$

Example:

  {(x,int)} |- x : int,    {(x,int)} |- 7 : int
  ----------------------------------------------
             {(x,int)} |- (x+7) : int

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 \mapsto 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\ \mapsto\ (T_1 \times \ldots \times T_n \to T) \end{equation*}$

Example:

  class World {
    int x;
    int y;
    def inc() {
      x = x + y;
      return;
    }
  }

Initial environment G0 contains {(x,int),(y,int),(+,int x int → int)}. While type checking body in this environment, we will have

  G0 |- x : int,   G0 |- y : int,  
  G0 |- + : int x int -> int
  -------------------------------
        G0 |- x + y : int

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 Notation for Maps
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