Typing environment

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

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

The judgement

: $\backslash Gamma\; \backslash vdash\; e:\backslash tau$

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

For each function body type checks:

:$\backslash Gamma\; =\; \backslash \{(f,\backslash tau\_1\backslash times...\backslash times\backslash tau\_n\; \backslash to\; \backslash tau\_0)|(f,xs,(\backslash tau\_1,...,\backslash tau\_n),t\_f,\backslash tau\_0)\backslash in\; e\backslash \}$

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.{{Cite web| title=Simply Typed λ-calculus|url=https://www.cs.cornell.edu/courses/cs4110/2012fa/lectures/lecture19.pdf}}