Конструктор типов: различия между версиями

По сути, конструктор типов представляет собой [[арность|''<code>n</code>''-арный]] '''ти́повый оператор''' ({{lang-en|type operator}}, оператор над типами), принимающий на входе ноль или более типов, и возвращающий другой тип. При использовании [[каррирование|каррирования]] ''<code>n</code>''-арный ти́повый оператор может быть представлен последовательным применением унарных ти́повых операторов. Следовательно, ти́повые операторы можно рассматривать как [[просто типизированное лямбда-исчисление]], имеющее единственный тип, обычно обозначаемый «<code>*</code>» (читается «''тип''»), являющийся типом всех типов в нижележащем языке, которые в этом случае можно называть ''характерными типами'', чтобы отличать их от типов ти́повых операторов в их собственном исчислении — {{iw|[[Род (теория типов)|'''родов типов'''|en|Kind (type theory)}}]].

Однако, использование ти́повых операторов в качестве обоснования просто типизированного лямбда-исчисления — это больше, чем просто формализация — это делает возможными ти́повые операторы высших порядков (см. {{iw|[[Род (теория типов)#Примеры|примеры родов типов'''|en|Kind (type theory)#Examples}}]]). Ти́повые операторы соотносятся со второй осью в [[Лямбда-куб|лямбда-кубе]], приводя к просто типизированному лямбда-исчислению с ти́повыми операторами — λ_ω. Комбинация ти́повых операторов с полиморфным лябда-исчислением ({{nowrap|[[Система F|системой F]]}}) порождает {{iw|Система F-омега|{{nowrap|систему Fω}}|en|System F-omega}}.

* {{iw|[[Род (теория типов)||en|Kind (type theory)}}]]