Typing environment

In type theory, a typing environment (or typing context) represents the association between variable names and data types.

More formally, an environment $\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

$\Gamma ⊢e:\tau$

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

For each function body type checks:

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

Typing Rules Example: $$\begin{array}{c}\Gamma ⊢b:Bool,\Gamma ⊢t_1:\tau ,\Gamma ⊢t_2:\tau \\ \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