# Type rule

Jump to: navigation, search

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 ${\displaystyle e}$ of type ${\displaystyle \tau }$ is written as ${\displaystyle e\!:\!\tau }$. The typing environment is written as ${\displaystyle \Gamma }$. The notation for inference is the usual one for sequents and inference rules, and has the following general form

${\displaystyle {\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 ${\displaystyle e_{i}}$ has type ${\displaystyle \tau _{i}}$ in environment ${\displaystyle \Gamma _{i}}$, for all ${\displaystyle i=1..n}$, then the expression ${\displaystyle e}$ will have an environment ${\displaystyle \Gamma }$ and type ${\displaystyle \tau }$.

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

${\displaystyle {\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 ${\displaystyle id}$, with type ${\displaystyle \tau '}$, is added to ${\displaystyle \Gamma }$:

${\displaystyle {\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.

## Further reading

• Luca Cardelli, "Type Systems", ACM Computing Surveys