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

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

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

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

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

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

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

В языках программирования[править | править вики-текст]

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

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

Standard ML[править | править вики-текст]

В современных реализациях Standard ML примитивные типы, такие как char, int, word, real, определены в модулях стандартной библиотеки («Basis») как нуль-арные конструкторы типов и экспортированы в общую область видимости, т.е. на верхний уровень (англ. top-level) доступа компилятора. Такие классические агрегатные типы как массивы и списки реализованы аналогично, в виде унарных конструкторов типов 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.

Haskell[править | править вики-текст]

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

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