LARA

Idea of Type Rules

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