Typing environment explained

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 x ... x \tau} _{n} \to \tau _{0)|(f,xs,(\tau} _{1,...,\tau} _{n),t} _{f,\tau} _{0)\in} e\}

Typing Rules Example:$$\backslash begin\backslash Gamma\backslash vdash\; b:Bool,\; \backslash Gamma\backslash vdash\; t\_1:\backslash tau,\; \backslash Gamma\backslash vdash\; t\_2:\backslash tau\backslash \backslash \backslash hline\backslash Gamma\; \backslash vdash\; (\backslash text(b)\; t\_1\; \backslash text\; t\_2):\; \backslash tau\; \backslash \backslash \backslash end$$

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

See also

• Type system

Notes and References

1. Web site: Simply Typed λ-calculus.