From Wikipedia, the free encyclopedia
In type theory a typing environment (or typing context) represents the association between variable names and data types.
More formally an environment
is a set or ordered list of pairs
, usually written as
, where
is a variable and
its type.
The judgement
![{\displaystyle \Gamma \vdash e:\tau }](https://wikimedia.org/api/rest_v1/media/math/render/svg/5d81021541d21575e83379f1892249a966de5d89)
is read as "
has type
in context
".[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\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/037ab06f22af5a6fa11913f4aeeac3c4e47c4b93)
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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f73d297082b6507ab7c65a4530f1e4ea8f36fc72)
In statically typed programming languages these environments are used and maintained by typing rules to type check a given program or expression.
See also[edit]
References[edit]