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 $\langle x,\tau \rangle$, usually written as $x:\tau$, where $x$ is a variable and $\tau$ its type.

The judgement

$\Gamma \vdash e:\tau$

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

For each function body type checks:

$\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}\Gamma \vdash b:Bool,\Gamma \vdash t_{1}:\tau ,\Gamma \vdash t_{2}:\tau \\\hline \Gamma \vdash ({\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