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

Особенность типизированного формального языка, которая строит новые типы из старых

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

Например, просто типизированное лямбда-исчисление можно рассматривать как язык с единственным небазовым конструктором типа — конструктором типа функции. Типы продуктов обычно можно считать «встроенными» в типизированных лямбда-исчислениях посредством каррирования .

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

Операторы типа могут связывать переменные типа. Например, задание структуры просто типизированного λ-исчисления на уровне типа требует связывания или операторов типа более высокого порядка. Эти связывающие операторы типа соответствуют 2-й оси λ -куба и теориям типов, таким как просто типизированное λ-исчисление с операторами типа, λ _ω . Объединение операторов типа с полиморфным λ-исчислением ( System F ) дает System F _ω .

Некоторые функциональные языки программирования явно используют конструкторы типов. Ярким примером является Haskell , в котором все dataобъявления типов считаются объявлениями конструкторов типов, а базовые типы (или конструкторы типов nullary) называются константами типов. ^[1]^[2] Конструкторы типов также можно рассматривать как параметрические полиморфные типы данных .

Смотрите также

Ссылки

↑ Марлоу, Саймон (апрель 2010 г.), «4.1.2 Синтаксис типов», Haskell 2010 Language Report , получено 15 августа 2023 г.
^ "Конструктор". HaskellWiki . Получено 15 августа 2023 г. .

Пирс, Бенджамин (2002). Типы и языки программирования . MIT Press. ISBN 0-262-16209-1., глава 29, «Операторы типов и типы»
ПТ Джонстон , Зарисовки слона , стр. 940

[1] Марлоу, Саймон (апрель 2010 г.), «4.1.2 Синтаксис типов», Haskell 2010 Language Report , получено 15 августа 2023 г.

[2] "Конструктор". HaskellWiki . Получено 15 августа 2023 г. .