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

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

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

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

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

Однако, использование ти́повых операторов в качестве обоснования просто типизированного лямбда-исчисления — это больше, чем просто формализация — это делает возможными ти́повые операторы высших порядков (см. Род (теория типов)#Примеры, полиморфизм в высших родах). Ти́повые операторы соотносятся со второй осью в лямбда-кубе, приводя к просто типизированному лямбда-исчислению с ти́повыми операторами — λ_ω. Комбинация ти́повых операторов с полиморфным лямбда-исчислением (системой F) порождает <span class="nowrap">систему Fω</span>^[en].

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

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

В языках программирования семейства ML конструктор типов представляется функцией над типами — т.е. функцией, которая получает на входе одни типы и возвращает другие типы. Оптимизирующие компиляторы исполняют эти функции статически, т.е. на этапе компиляции^[en] (см., например, 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 для лямбда-исчисления с параметрическим полиморфизмом
• Класс типов
• Род (теория типов)
• Рекурсивный тип данных^[en]

Ссылки

• Pierce, Benjamin C. Types and Programming Languages. — MIT Press, 2002. — ISBN 0-262-16209-1.
  • Перевод на русский язык: Пирс Б. Типы в языках программирования. — Добросвет, 2012. — 680 с. — ISBN 978-5-7913-0082-9.
• Лука Карделли^[en], Peter Wegner. On Understanding Types, Data Abstraction, and Polymorphism // ACM Computing Surveys. — New York, NY, USA: ACM, 1985. — Т. 17, вып. 4. — С. 471–523. — ISSN 0360-0300. — doi:10.1145/6041.6042.
• Лука Карделли^[en]. Typeful programming ( (англ.)) // IFIP State-of-the-Art Reports. — New York: Springer-Verlag, 1991. — Вып. Formal Description of Programming Concepts. — С. 431–507.
• P.T. Johnstone^[en]. Sketches of an Elephant. — С. 940.

Эта страница в последний раз была отредактирована 8 октября 2017 в 08:40.