Правило набора текста
Как система типов назначает тип синтаксической конструкции

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

Обозначение

Правила типизации определяют структуру типизированного отношения , которое связывает синтаксические термины с их типами. [1] : 92  Синтаксически типизированное отношение обычно обозначается двоеточием, например обозначает, что выражение имеет тип . Сами правила обычно указываются с использованием нотации естественного вывода . [1] : 26  Например, следующие правила типизации определяют типизированное отношение для простого языка булевых значений : [1] : 93  е : τ {\displaystyle е:\тау } е {\displaystyle е} τ {\displaystyle \тау}

т г ты е : Б о о л ф а л с е : Б о о л е 1 : Б о о л е 2 : τ е 3 : τ я ф   е 1   т час е н   е 2   е л с е   е 3 : τ {\displaystyle {\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 }}}

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

В языках программирования тип переменной зависит от того, где она связана , что требует контекстно-зависимых правил типизации. Эти правила задаются суждением о типизации , обычно записанным , которое гласит, что выражение имеет тип в контексте типизации , который связывает переменные с их типами. Контексты типизации иногда дополняются типами отдельных переменных; например, можно прочитать как «контекст, дополненный информацией о том, что выражение имеет тип, дает суждение о том, что выражение имеет тип ». Эта нотация может использоваться для задания правил типизации для ссылок на переменные и лямбда-абстракции в простом типизированном лямбда-исчислении : [1] : 101–102  Г ⊢ е : τ {\displaystyle \Gamma \vdash e:\tau } е {\displaystyle е} τ {\displaystyle \тау} Г {\displaystyle \Гамма} Г , х : τ 1 ⊢ е : τ 2 {\displaystyle \Gamma,x{:}\tau _{1}\vdash e:\tau _{2}} Г {\displaystyle \Гамма} х {\displaystyle x} τ 1 {\displaystyle \тау _{1}} е {\displaystyle е} τ 2 {\displaystyle \тау _{2}}

х : τ ∈ Г Г ⊢ х : τ Г , х : τ 1 ⊢ е : τ 2 Г ⊢ ( λ х : τ 1 . е ) : τ 1 → τ 2 {\displaystyle {\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}}}}

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

Г ⊢ е 1 : τ 1 Г , х : τ 1 ⊢ е 2 : τ 2 Г ⊢ л е т   х = е 1   я н   е 2   е н г : τ 2 {\displaystyle {\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 {конец} :\тау _{2}}}}

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

Смотрите также

Ссылки

  1. ^ abcde Пирс, Бенджамин С. (2002). Типы и языки программирования (1-е изд.). Кембридж, Массачусетс: MIT Press. ISBN 0262162091.
  2. ^ Баез, Джон. "The n-Category Café". golem.ph.utexas.edu . Получено 30 сентября 2022 г. .
  3. ^ Клеман, Доминик; Деспейру, Тьерри; Кан, Жиль; Деспейру, Жоэль (8 августа 1986 г.). "Простой аппликативный язык: Mini-ML". Труды конференции ACM 1986 г. по LISP и функциональному программированию - LFP '86 (PDF) . Ассоциация вычислительной техники. стр.  13–27 . doi :10.1145/319838.319847. ISBN 0897912004. S2CID  5126579.
  4. ^ Данфилд, Яна; Кришнасвами, Нил (23 мая 2021 г.). «Двунаправленная печать». ACM Computing Surveys . 54 (5): 98:19. arXiv : 1908.05839 . doi : 10.1145/3450952 . ISSN  0360-0300. S2CID  201058734.

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

  • Карделли, Лука (март 1996 г.). «Системы типов». ACM Computing Surveys . 28 (1): 263– 264. doi : 10.1145/234313.234418 . S2CID  227408784.
  • Cardelli, Luca (июнь 2004 г.). Type Systems, 41 страница. Computer Science Handbook, 2nd Edition, Ch. 97. Под редакцией Allen B. Tucker. ISBN 9780429209390. Получено 5 января 2025 г.
Г ⊢ {\displaystyle \Гамма \!\vdash}

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

Взято с "https://en.wikipedia.org/w/index.php?title=Typing_rule&oldid=1267595777"