Тип правила

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

Обозначение [ править ]

Выражение типа записывается как . Среда ввода записывается как . Обозначение для вывода является обычным для секвенций и правил вывода и имеет следующий общий вид${\ displaystyle e}$${\ Displaystyle \ тау}$${\ Displaystyle е \!: \! \ тау}$${\displaystyle \Gamma }$

${\displaystyle {\frac {\Gamma _{1}\vdash e_{1}\!:\!\tau _{1}\quad \cdots \quad \Gamma _{n}\vdash e_{n}\!:\!\tau _{n}}{\Gamma \vdash e\!:\!\tau }}}$

Секвенции над линией - это посылки, которые должны быть выполнены для применения правила, дающего вывод: секвенции под линией. Это можно прочитать так: если выражение имеет тип в среде для всех , тогда выражение будет иметь среду и тип${\displaystyle e_{i}}$${\displaystyle \tau _{i}}$ ${\displaystyle \Gamma _{i}}$${\displaystyle i=1..n}$${\displaystyle e}$${\displaystyle \Gamma }$${\displaystyle \tau }$ .

Например, простой язык для выполнения арифметических вычислений действительных чисел может иметь следующие правила:

${\displaystyle {\frac {\Gamma \vdash e_{1}\!:\!real\quad \Gamma \vdash e_{2}\!:\!real}{\Gamma \vdash e_{1}+e_{2}\!:\!real}}\qquad {\frac {\Gamma \vdash e_{1}\!:\!integer\quad \Gamma \vdash e_{2}:integer}{\Gamma \vdash e_{1}+e_{2}\!:\!integer}}\qquad \cdots }$

Правило типа может не иметь предпосылок, и обычно в этих случаях строка опускается. Правило типа также может изменять среду, добавляя новые переменные в предыдущую среду; например, объявление может иметь следующее правило типа , в которое добавляется новая переменная с типом :${\displaystyle id}$${\displaystyle \tau '}$${\displaystyle \Gamma }$

${\displaystyle {\frac {\Gamma \vdash e'\!:\!\tau '\quad \Gamma ,id\!:\!\tau '\vdash e\!:\!\tau }{\Gamma \vdash {\text{let id = }}e'{\text{ in }}e{\text{ end}}:\!\tau }}}$

Здесь синтаксис выражения let соответствует синтаксису Standard ML . Таким образом, правила типов можно использовать для получения типов составных выражений, как при естественном выводе .

См. Также [ править ]

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

Дальнейшее чтение [ править ]

• Карделли, Лука (март 1996). «Типовые системы» (PDF) . ACM Computing Surveys . 28 (1): 263–264. DOI : 10.1145 / 234313.234418 .

${\displaystyle \Gamma \vdash x:{\text{Int}}}$

Эта статья по теории языков программирования или теории типов незавершена . Вы можете помочь Википедии, расширив ее .

• v
• t
• e