Правило ввода

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

Обозначения

Правила типизации определяют структуру типизации отношения , которое связывает синтаксические термины с их типами. Синтаксически отношение типизации обычно обозначается двоеточием, например $e:\tau$ означает, что выражение $e$ имеет тип $\tau$. Сами правила обычно задаются с использованием обозначения естественного вывода . Например, следующие правила типизации определяют отношение типизации для простого языка логических значений :

${\frac {}{{\mathsf {true}}:{\mathsf {Bool}}}}\qquad {\frac {}{{\mathsf {false}}:{\mathsf {Bool}}}}\qquad {\frac {e_{1}:{\mathsf {Bool}}\quad \;e_{2}:\tau \quad \;e_{3}:\tau }{\mathbf {if} \ e_{1}\ \mathbf {then} \ e_{2}\ \mathbf {else} \ e_{3}:\tau }}$

Каждое правило гласит, что вывод под чертой может быть выведен из посылок над чертой. Первые два правила не имеют посылок над чертой, поэтому являются аксиомами . Третье правило имеет помещения над линией (точнее, три посылки), поэтому это правило вывода .

В языках программирования тип переменной зависит от того, где она привязана , что требует применения контекстно-зависимых правил типизации. Эти правила определяются типичным решением , обычно записываемым $\Gamma \vdash e:\tau$, который утверждает, что выражение $e$ имеет тип $\tau$ в контексте набора текста $\Gamma$ который связывает переменные с их типами. Контексты ввода иногда дополняются типами отдельных переменных; например, $\Gamma ,x{:}\tau _{1}\vdash e:\tau _{2}$ можно прочитать как «контекст $\Gamma$ дополнено информацией о том, что выражение $x$ имеет тип $\tau _{1}$ приводит к выводу, что выражение $e$ имеет тип $\tau _{2}$". Эту запись можно использовать для указания правил типизации для ссылок на переменные и лямбда-абстракции в просто типизированном лямбда-исчислении :

${\frac {x{:}\tau \in \Gamma }{\Gamma \vdash x:\tau }}\qquad {\frac {\Gamma ,x{:}\tau _{1}\vdash e:\tau _{2}}{\Gamma \vdash (\lambda x{:}\tau _{1}.\,e):\tau _{1}\rightarrow \tau _{2}}}$

Аналогично, следующее правило типизации описывает $\mathbf {let}$ конструкция стандартного ML :

${\frac {\Gamma \vdash e_{1}:\tau _{1}\qquad \Gamma ,x{:}\tau _{1}\vdash e_{2}:\tau _{2}}{\Gamma \vdash \mathbf {let} \ x=e_{1}\ \mathbf {in} \ e_{2}\ \mathbf {end} :\tau _{2}}}$

Не все системы правил типизации напрямую определяют алгоритм проверки типов . Например, правило типизации для применения параметрически полиморфной функции в системе типов Хиндли-Милнера требует «угадывания» соответствующего типа, для которого должна быть создана функция. Адаптация декларативной системы правил к разрешимому алгоритму требует создания отдельной алгоритмической системы, которая, как можно доказать, определяет то же самое отношение типизации.

См. также

• Суждение (математическая логика)
• Типовая система
• Теория типов
• Переписка Карри-Ховарда
• Секвенционное исчисление

Дальнейшее чтение

• Карделли, Лука (март 1996 г.). «Типовые системы» (PDF) . Обзоры вычислительной техники ACM . 28 (1): 263–264. дои : 10.1145/234313.234418 . S2CID   227408784 .