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]

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

See also

• Type system
• Type rule
• Type theory

References

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