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

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

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

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

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

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

В языках программирования

В языках программирования семейства ML конструктор типов представляется функцией над типами — т.е. функцией, которая получает на входе одни типы и возвращает другие типы. Оптимизирующие компиляторы исполняют эти функции статически, т.е. (см., например, MLton ).

В классических диалектах ML ( Standard ML , OCaml ) для n -арных конструкторов типов используется нотация кортежей . В Haskell возможны каррированные конструкторы типов. Классические диалекты ML при конструировании новых типов используют постфиксный синтаксис (например, « int list »), а Haskell — префиксный (« List Int »).

Standard ML

В современных реализациях Standard ML примитивные типы, такие как char , int , word , real , определены в модулях стандартной библиотеки ( SML Basis ) как нуль-арные конструкторы типов (подробнее см. управление разрядностью чисел в ML ). Такие классические агрегатные типы как массивы и списки реализованы аналогично, но уже представляют собой унарные конструкторы типов vector (массивы неизменяемых элементов), array (массивы изменяемых элементов) и list .

В Standard ML для определения конструкторов типов есть две разные конструкции — type и datatype . Первая определяет псевдоним имеющегося конструктора типов или их композиции, вторая вводит новый алгебраический тип данных со своими конструкторами . Вновь определяемые конструкторы типов могут принимать любое количество аргументов. В качестве аргумента конструктора типов используется переменная типа . Типы, параметризованные одним и более аргументами, называются полиморфными ; типы без аргументов — мономорфными.

datatype t0 = T of int * real             (* 0 аргументов *)
type 'a t1 = 'a * int                     (* 1 аргумент   *)
datatype ('a, 'b) t2 = A | B of 'a * 'b   (* 2 аргумента  *)
type ('a, 'b, 'c) t3 = 'a * ('b -> 'c)    (* 3 аргумента  *)

Здесь определено четыре конструктора типов: t0 , t1 , t2 и t3 . Для создания объектов типов 'a t1 и 'a t2 необходимо вызывать их конструкторы T , A и B .

Пример композиции конструкторов типов, показывающий построение новых типов:

type t4 = t0 t1

Здесь в качестве фактического значения ти́повой переменной 'a конструктора типов t1 используется тип t0 . Полученный тип представляет собой кортеж из двух элементов, из которых второй является целым числом, а первый был построен применением конструктора T к кортежу из целого и вещественного.

Более сложный пример:

type 'a t5 = ('a, 'a, 'a) t3 t1

Объектами типа t5 будут кортежи из двух элементов, первый из которых является частным случаем типа t3 , у которого все три аргумента должны быть идентичными, а второй — целым числом.

Haskell

В Haskell для определения конструкторов типов есть уже три конструкции — type , data и newtype .

Конструкции type и data используются аналогично type и datatype в Standard ML , однако, имеются следующие отличия:

• синтаксис префиксный (параметр указывается после конструктора);
• синтаксис требует (а не рекомендует, как в большинстве языков) различать регистр в идентификаторах: компоненты слоя типов в языке (конструкторы типов, конструкторы значений , классы типов ) должны начинаться только с заглавной буквы, а компоненты слоя значений — только со строчных;
• переменные типа не должны отмечаться апострофами, но записываются также строчными буквами;
• и конструкторы типов, и конструкторы значений могут быть каррированными .

Пример:

data Point a = Pt a a

На самом деле, во всех языках семейства ML конструкторы типов и конструкторы значений находятся в разных пространствах имён, поэтому в подобных случаях можно использовать один и тот же идентификатор:

data Point a = Point a a

Использование алгебраического типа приводит к некоторым потерям производительности, так как конструктор значений применяется динамически. Замена его на псевдоним типа (определяемый через type ) повышает эффективность, но снижает типобезопасность (так как становится невозможно контролировать уникальные свойства надстроенного типа, сужающие его применение относительно лежащего в его основе). Для решения этой дилеммы в Haskell была добавлена конструкция newtype :

newtype Point a = Point (a, a)

Определённый таким образом тип может иметь один и только один конструктор его значений , причём ровно с одним параметром. В исходном коде такие типы используются идентично тем, что были определены через data , что даёт типобезопасность. Однако в исполняемом коде newtype не существует как отдельные сущность, вместо него используется тип параметра его конструктора. В данном случае исполняемый код для операций с Point a будет так же эффективен, как и код для операций с кортежами (a, a) .

См.также

• Переменная типа
• Алгебраический тип данных и его конструктор
• Тип данных
• Система F для лямбда-исчисления с параметрическим полиморфизмом
• Класс типов
• Род (теория типов)

Ссылки

• Pierce, Benjamin C. . — MIT Press , 2002. — ISBN 0-262-16209-1 .
  • Перевод на русский язык: Пирс Б. Типы в языках программирования. — , 2012. — 680 с. — ISBN 978-5-7913-0082-9 .
• , Peter Wegner. // . — New York, NY, USA: ACM , 1985. — Т. 17 , вып. 4 . — С. 471–523 . — ISSN . — doi : .
• . ( (англ.) ) // IFIP State-of-the-Art Reports. — New York: Springer-Verlag, 1991. — Вып. Formal Description of Programming Concepts . — С. 431–507 .
• . Sketches of an Elephant. — С. 940 .