Typing environment

In type theory a typing environment (or typing context) represents the association between variable names and data types. More formally an environment [math]\displaystyle{ \Gamma }[/math] is a set or ordered list of pairs [math]\displaystyle{ \langle x,\tau \rangle }[/math], usually written as [math]\displaystyle{ x:\tau }[/math], where [math]\displaystyle{ x }[/math] is a variable and [math]\displaystyle{ \tau }[/math] its type.

The judgement

[math]\displaystyle{ \Gamma \vdash e:\tau }[/math]

is read as "[math]\displaystyle{ e }[/math] has type [math]\displaystyle{ \tau }[/math] in context [math]\displaystyle{ \Gamma }[/math] ".

For each function body type checks:

[math]\displaystyle{ \Gamma = \{(f,\tau_1\times...\times\tau_n \to \tau_0)|(f,xs,(\tau_1,...,\tau_n),t_f,\tau_0)\in e\} }[/math]

Typing Rules Example: [math]\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} }[/math]

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