Правило типа

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

Выражение типа записывается как. Среда ввода записывается как. Обозначение для вывода является обычным для секвенций и правил вывода и имеет следующий общий вид ${\ 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 \ тау _ {я}}$ ${\ displaystyle \ Gamma _ {i}}$${\ displaystyle i = 1..n}$${\ displaystyle e}$${\ displaystyle \ Gamma}$${\ Displaystyle \ тау}$.

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

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