Typing environment

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

More formally an environment ${\displaystyle \Gamma }$ is a set or ordered list of pairs ${\displaystyle \langle x,\tau \rangle }$, usually written as ${\displaystyle x:\tau }$, where ${\displaystyle x}$ is a variable and ${\displaystyle \tau }$ its type.

The judgement

${\displaystyle \Gamma \vdash e:\tau }$

is read as "${\displaystyle e}$ has type ${\displaystyle \tau }$ in context ${\displaystyle \Gamma }$ ".^[1]

For each function body type checks:

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

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

References

1. "Simply Typed λ-calculus" (PDF).