В области математической логики и информатика , известной как теория типа , конструктор типа является характерной чертой типизированного формального языка , который строит новые типы из старых. Считается, что базовые типы построены с использованием конструкторов нулевого типа. Некоторые конструкторы типа принимают другой тип в качестве аргумента, например, конструкторов для типов продукции , типов функций , типов питания и типов списков . Новые типы могут быть определены путем рекурсивного составления конструкторов типов.
Например, просто типизированное лямбда-исчисление можно рассматривать как язык с одним конструктором типа - конструктором типа функции. Типы продуктов обычно можно считать "встроенными" в типизированных лямбда-исчислениях посредством каррирования .
Абстрактно конструктор типа - это оператор n -арного типа, принимающий в качестве аргумента ноль или более типов и возвращающий другой тип. Используя каррирование, операторы n -арного типа могут быть (пере) записаны как последовательность приложений операторов унарного типа. Следовательно, мы можем рассматривать операторы типов как просто типизированное лямбда-исчисление, которое имеет только один базовый тип, обычно обозначаемый и произносимый как «тип», который является типом всех типов в базовом языке, которые теперь называются собственными типами в чтобы отличить их от типов операторов типов в их собственном исчислении, которые называются видами .
Операторы типа могут связывать переменные типа. Например, для задания структуры λ-исчисления с простой типизацией на уровне типа требуются операторы связывания или операторы типа более высокого порядка. Эти операторы типа связывания соответствуют 2- й оси λ-куба и теории типов, такие как λ-исчисление простого типа с операторами типов, λ ω . Комбинируя операторы типа с полиморфным λ-исчислением ( Система F ), получаем Систему F ω .
См. Также [ править ]
Ссылки [ править ]
- Пирс, Бенджамин (2002). Типы и языки программирования . MIT Press. ISBN 0-262-16209-1., глава 29, «Типовые операторы и Kinding»
- П. Т. Джонстон , Эскизы слона , с. 940
