Конструктор типов
В области математической логики и информатики , известной как теория типов , конструктор типов — это функция типизированного формального языка , которая создает новые типы из старых. Считается, что базовые типы создаются с использованием конструкторов пустых типов. Некоторые конструкторы типов принимают другой тип в качестве аргумента, например, конструкторы типов продуктов , типов функций , типов мощности и типов списков . Новые типы могут быть определены рекурсивно составленными конструкторами типов.
Например, просто типизированное лямбда-исчисление можно рассматривать как язык с одним конструктором типа — конструктором функционального типа. Типы продуктов обычно можно считать «встроенными» в типизированные лямбда-исчисления посредством каррирования .
Абстрактно, конструктор типа — это оператор n - арного типа, принимающий в качестве аргумента ноль или более типов и возвращающий другой тип. Используя каррирование, операторы n - арного типа могут быть (пере)писаны как последовательность приложений операторов унарного типа. Следовательно, мы можем рассматривать операторы типа как просто типизированное лямбда-исчисление, которое имеет только один базовый тип, обычно обозначаемый , и произносится как «тип», который является типом всех типов в базовом языке, которые теперь называются правильными типами в для того, чтобы отличить их от типов операторов типа в их собственном исчислении, которые называются видами .
Операторы типа могут связывать переменные типа. Например, для задания структуры просто типизированного λ-исчисления на уровне типов требуются связывающие операторы типов или операторы типов более высокого порядка. Эти операторы типа привязки соответствуют 2-й оси λ-куба и теориям типов, таким как простое λ-исчисление с операторами типа λ ω . Объединение операторов типов с полиморфным λ-исчислением ( System F ) дает System F ω .