LARA

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