Typing environment

In type theory a typing environment (or typing context) represents the association between variable names and data types. More formally an environment $\mathrm{\Gamma }$ is a set or ordered list of pairs $⟨x,\tau ⟩$, usually written as $x:\tau$, where $x$ is a variable and $\tau$ its type.

The judgement

$\mathrm{\Gamma }⊢e:\tau$

is read as "$e$ has type $\tau$ in context $\mathrm{\Gamma }$ ".

For each function body type checks:

$\mathrm{\Gamma }=\{(f,{\tau }_1\times ...\times {\tau }_n\to {\tau }_0)|(f,xs,({\tau }_1,...,{\tau }_n),t_f,{\tau }_0)\in e\}$

Typing Rules Example: $$\begin{array}{c}\mathrm{\Gamma }⊢b:Bool,\mathrm{\Gamma }⊢t_1:\tau ,\mathrm{\Gamma }⊢t_2:\tau \\ \mathrm{\Gamma }⊢(\text{if}(b)t_1\text{else}{t}_2):\tau \\ \end{array}$$

In statically typed programming languages these environments are used and maintained by typing rules to type check a given program or expression.

See also

• Type system