Конструктор типов

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

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

Просто типизированное лямбда-исчисление можно рассматривать как язык с единственным конструктором типов — конструктором функционального типа. Каррирование позволяет рассматривать типы-произведения в типизированном лямбда-исчислении как встроенные.

По сути, конструктор типов представляет собой n-арный ти́повый оператор (англ. type operator, оператор над типами), принимающий на входе ноль или более типов, и возвращающий другой тип. При использовании каррирования n-арный ти́повый оператор может быть представлен последовательным применением унарных ти́повых операторов. Следовательно, ти́повые операторы можно рассматривать как просто типизированное лямбда-исчисление, имеющее единственный тип, обычно обозначаемый «*» (читается «тип»), являющийся типом всех типов в нижележащем языке, которые в этом случае можно называть характерными типами, чтобы отличать их от типов ти́повых операторов в их собственном исчислении — родо́в типов.

Однако, использование ти́повых операторов в качестве обоснования просто типизированного лямбда-исчисления — это больше, чем просто формализация — это делает возможными ти́повые операторы высших порядков (см. Род (теория типов)#Примеры, полиморфизм в высших родах). Ти́повые операторы соотносятся со второй осью в лямбда-кубе, приводя к просто типизированному лямбда-исчислению с ти́повыми операторами — λω. Комбинация ти́повых операторов с полиморфным лямбда-исчислением (системой F) порождает систему Fω.

Конструкторы типов интенсивно используются в полнотиповом программировании.

Источник: Википедия