Environment (type theory)

☆ Save On Wikipedia ↗

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

More formally, an environment Γ {\displaystyle \Gamma } {\displaystyle \Gamma } is a set or ordered list of pairs ⟨ x , τ ⟩ {\displaystyle \langle x,\tau \rangle } {\displaystyle \langle x,\tau \rangle }, usually written as x : τ {\displaystyle x:\tau } {\displaystyle x:\tau }, where x {\displaystyle x} {\displaystyle x} is a variable and τ {\displaystyle \tau } {\displaystyle \tau } its type.

The judgement

Γ ⊢ e : τ {\displaystyle \Gamma \vdash e:\tau } {\displaystyle \Gamma \vdash e:\tau }

is read as " e {\displaystyle e} {\displaystyle e} has type τ {\displaystyle \tau } {\displaystyle \tau } in context Γ {\displaystyle \Gamma } {\displaystyle \Gamma } ".[1]

For each function body type checks:

Γ = { ( f , τ 1 × . . . × τ n → τ 0 ) | ( f , x s , ( τ 1 , . . . , τ n ) , t f , τ 0 ) ∈ e } {\displaystyle \Gamma =\{(f,\tau _{1}\times ...\times \tau _{n}\to \tau _{0})|(f,xs,(\tau _{1},...,\tau _{n}),t_{f},\tau _{0})\in e\}} {\displaystyle \Gamma =\{(f,\tau _{1}\times ...\times \tau _{n}\to \tau _{0})|(f,xs,(\tau _{1},...,\tau _{n}),t_{f},\tau _{0})\in e\}}

Typing Rules Example: Γ ⊢ b : B o o l , Γ ⊢ t 1 : τ , Γ ⊢ t 2 : τ Γ ⊢ ( if ( b ) t 1 else t 2 ) : τ {\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}}} {\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}}}

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

References