Тип конструктора
В области математической логики и информатики , известной как теория типов , конструктор типов — это функция типизированного формального языка , которая создает новые типы из старых. Считается, что базовые типы создаются с использованием конструкторов нулевых типов. Некоторые конструкторы типов принимают в качестве аргумента другой тип, например, конструкторы для типов продуктов , типов функций , мощных типов и типов списков . Новые типы могут быть определены путем рекурсивного составления конструкторов типов.
Например, просто типизированное лямбда-исчисление можно рассматривать как язык с единственным конструктором небазового типа — конструктором функционального типа. Типы продуктов обычно можно считать «встроенными» в типизированных лямбда-исчислениях посредством каррирования .
Говоря абстрактно, конструктор типа — это n -арный оператор типа, принимающий в качестве аргумента ноль или более типов и возвращающий другой тип. Используя каррирование, операторы n -арного типа могут быть (пере)писаны как последовательность применений операторов унарного типа. Следовательно, мы можем рассматривать операторы типа как просто типизированное лямбда-исчисление, имеющее только один базовый тип, обычно обозначаемый и произносится как «тип», который является типом всех типов в базовом языке, которые теперь называются собственными типами , чтобы отличать их от типов операторов типов в их собственном исчислении, которые называются видами .
Операторы типа могут связывать переменные типа. Например, для задания структуры просто типизированного λ-исчисления на уровне типа требуются операторы связывания или операторы типов более высокого порядка. Эти операторы типа привязки соответствуют 2-й оси λ-куба и теориям типов, таким как просто типизированное λ-исчисление с операторами типа λ ω . Объединение операторов типа с полиморфным λ-исчислением ( Система F ) дает Систему F ω .
Некоторые языки функционального программирования явно используют конструкторы типов. Ярким примером является Haskell , в котором все data Считается, что объявления типов объявляют конструкторы типов, а базовые типы (или конструкторы нулевых типов) называются константами типов. [1] [2] Конструкторы типов также можно рассматривать как параметрические полиморфные типы данных .
См. также [ править ]
Ссылки [ править ]
- ^ Марлоу, Саймон (апрель 2010 г.), «4.1.2 Синтаксис типов» , Отчет о языке Haskell 2010 , получено 15 августа 2023 г.
- ^ «Конструктор» . ХаскеллВики . Проверено 15 августа 2023 г.
- Пирс, Бенджамин (2002). Типы и языки программирования . МТИ Пресс. ISBN 0-262-16209-1 . , глава 29, «Операторы типов и сортировка»
- П.Т. Джонстон , «Зарисовки слона» , с. 940