# Type rule

(Redirected from Type rules)

In type theory, a type rule is an inference rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is well typed and what type expressions have. A prototypical example of the use of type rules is in defining type inference in the simply typed lambda calculus, which is the internal language of Cartesian closed categories.

## Notation

An expression $e$ of type $\tau$ is written as $e\!:\!\tau$. The typing environment is written as $\Gamma$. The notation for inference is the usual one for sequents and inference rules, and has the following general form

$\frac{\Gamma_1 \vdash e_1\!:\!\tau_1 \quad \cdots \quad \Gamma_n \vdash e_n\!:\!\tau_n}{\Gamma \vdash e\!:\!\tau}$

The sequents above the line are the premises that must be fulfilled for the rule to be applied, yielding the conclusion: the sequents below the line. This can be read as: if expression $e_i$ has type $\tau_i$ in environment $\Gamma_i$, for all $i=1..n$, then the expression $e$ will have an environment $\Gamma$ and type $\tau$.

For example, a simple language to perform arithmetic calculations on real numbers may have the following rules

$\frac{\Gamma \vdash e_1\!:\!real \quad \Gamma \vdash e_2\!:\!real}{\Gamma \vdash e_1+e_2\!:\!real} \qquad \frac{\Gamma \vdash e_1\!:\!integer \quad \Gamma \vdash e_2 : integer}{\Gamma \vdash e_1+e_2\!:\!integer} \qquad \cdots$

A type rule may have no premises, and usually the line is omitted in these cases. A type rule may also change an environment by adding new variables to a previous environment; for example, a declaration may have the following type rule, where a new variable $id$, with type $\tau'$, is added to $\Gamma$:

$\frac{\Gamma \vdash e'\!:\!\tau' \quad \Gamma, id\!:\!\tau' \vdash e\!:\!\tau}{\Gamma \vdash \text{let id = } e' \text{ in } e \text{ end} :\!\tau}$

Here the syntax of the let expression is that of Standard ML. Thus type rules can be used to derive the types of composed expressions, much like in natural deduction.