(Redirected from Typing context )
In type theory , a typing environment (or typing context ) represents the association between variable names and data types .
More formally, an environment
Γ
{\displaystyle \Gamma }
is a set or ordered list of pairs
⟨
x
,
τ
⟩
{\displaystyle \langle x,\tau \rangle }
, usually written as
x
:
τ
{\displaystyle x:\tau }
, where
x
{\displaystyle x}
is a variable and
τ
{\displaystyle \tau }
its type.
The judgement
Γ
⊢
e
:
τ
{\displaystyle \Gamma \vdash e:\tau }
is read as "
e
{\displaystyle e}
has type
τ
{\displaystyle \tau }
in context
Γ
{\displaystyle \Gamma }
".
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\}}
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}}}
In statically typed programming languages , these environments are used and maintained by typing rules to type check a given program or expression.
See also
References
"Simply Typed λ-calculus" (PDF).
Categories :
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
**DISCLAIMER** We are not affiliated with Wikipedia, and Cloudflare.
The information presented on this site is for general informational purposes only and does not constitute medical advice.
You should always have a personal consultation with a healthcare professional before making changes to your diet, medication, or exercise routine.
AI helps with the correspondence in our chat.
We participate in an affiliate program. If you buy something through a link, we may earn a commission 💕
↑