タイピング環境

型理論では、型付け環境（または型付けコンテキスト）は、変数名とデータ型の関連を表します。

より正式には、環境はペアの集合または順序付けられたリストであり、通常は と記述されます。ここで、は変数とその型です。 ${\displaystyle \ガンマ}$${\displaystyle \langle x,\tau \rangle }$${\displaystyle x:\tau}$${\displaystyle x}$${\displaystyle \tau}$

判決​

${\displaystyle \Gamma \vdash e:\tau }$

は「文脈内に型がある」と読みます。^[1]${\displaystyle e}$${\displaystyle \tau}$${\displaystyle \ガンマ}$

各関数本体の型チェック:

${\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 {\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}}}$$

静的に型付けされた プログラミング言語では、これらの環境は、特定のプログラムまたは式 の型チェックを行うための型付け規則によって使用され、維持されます。

• 型システム