Конструктор типов: различия между версиями
| [отпатрулированная версия] | [отпатрулированная версия] |
Содержимое удалено Содержимое добавлено
м →Преамбула: промахнулся |
Исправил опечатку в слове "лямбда". |
||
Строка 8:
По сути, конструктор типов представляет собой [[арность|''<code>n</code>''-арный]] '''ти́повый оператор''' ({{lang-en|type operator}}, оператор над типами), принимающий на входе ноль или более типов, и возвращающий другой тип. При использовании [[каррирование|каррирования]] ''<code>n</code>''-арный ти́повый оператор может быть представлен последовательным применением унарных ти́повых операторов. Следовательно, ти́повые операторы можно рассматривать как [[просто типизированное лямбда-исчисление]], имеющее единственный тип, обычно обозначаемый «<code>*</code>» (читается «''тип''»), являющийся типом всех типов в нижележащем языке, которые в этом случае можно называть ''характерными типами'', чтобы отличать их от типов ти́повых операторов в их собственном исчислении — [[Род (теория типов)|родо́в типов]].
Однако, использование ти́повых операторов в качестве обоснования просто типизированного лямбда-исчисления — это больше, чем просто формализация — это делает возможными ти́повые операторы высших порядков (см. [[Род (теория типов)#Примеры]], [[полиморфизм в высших родах]]). Ти́повые операторы соотносятся со второй осью в [[лямбда-куб]]е, приводя к просто типизированному лямбда-исчислению с ти́повыми операторами — λ<sub>ω</sub>. Комбинация ти́повых операторов с полиморфным
Конструкторы типов интенсивно используются в [[полнотиповое программирование|полнотиповом программировании]].
| |||