Среда ввода

В теории типов среда типизации (или контекст типизации ) представляет собой связь между именами переменных и типами данных .

Более формально среда $\Gamma$ представляет собой набор или упорядоченный список пар $\langle x,\tau \rangle$, обычно записываемый как $x:\tau$, где $x$ является переменной и $\tau$ его тип.

Решение ​

$\Gamma \vdash e:\tau$

читается как " $e$ имеет тип $\tau$ в контексте $\Gamma$ ".

Для каждого типа тела функции проверяется:

$\Gamma =\{(f,\tau _{1}\times ...\times \tau _{n}\to \tau _{0})|(f,xs,(\tau _{1},...,\tau _{n}),t_{f},\tau _{0})\in e\}$

Пример правил ввода: $${\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}}$$

В статически типизированных языках программирования эти среды используются и поддерживаются путем ввода правил для проверки типа данной программы или выражения.

См. также

• Типовая система