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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

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

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

Однако, использование ти́повых операторов в качестве обоснования просто типизированного лямбда-исчисления — это больше, чем просто формализация — это делает возможными ти́повые операторы высших порядков (см. примеры родов типов). Ти́повые операторы соотносятся со второй осью в лямбда-кубе, приводя к просто типизированному лямбда-исчислению с ти́повыми операторами — λω. Комбинация ти́повых операторов с полиморфным лябда-исчислением (системой F) порождает систему Fω[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, однако, имеются следующие отличия:

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

Пример:

data Point a = Pt a a

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

data Point a = Point a a

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

newtype Point a = Point a a

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


См.также[править | править вики-текст]

Ссылки[править | править вики-текст]