Ванин, Сергей Сергеевич (конструктор)
- 1 year ago
- 0
- 0
В теории типов , конструктор типов представляет собой конструкцию полиморфно типизируемого формального языка , которая строит новые типы из старых.
Примерами типичных конструкторов типов служат типы-произведения , функциональные типы и списки . Примитивные типы представляются конструкторами типов нулевой арности . Новые типы могут строиться посредством рекурсивной композиции конструкторов типов.
Просто типизированное лямбда-исчисление можно рассматривать как язык с единственным конструктором типов — конструктором функционального типа. Каррирование позволяет рассматривать типы-произведения в типизированном лямбда-исчислении как встроенные.
По сути, конструктор типов представляет собой
n
-арный
ти́повый оператор
(
англ.
type operator
, оператор над типами), принимающий на входе ноль или более типов, и возвращающий другой тип. При использовании
каррирования
n
-арный ти́повый оператор может быть представлен последовательным применением унарных ти́повых операторов. Следовательно, ти́повые операторы можно рассматривать как
просто типизированное лямбда-исчисление
, имеющее единственный тип, обычно обозначаемый «
*
» (читается «
тип
»), являющийся типом всех типов в нижележащем языке, которые в этом случае можно называть
характерными типами
, чтобы отличать их от типов ти́повых операторов в их собственном исчислении —
родо́в типов
.
Однако, использование ти́повых операторов в качестве обоснования просто типизированного лямбда-исчисления — это больше, чем просто формализация — это делает возможными ти́повые операторы высших порядков (см. Род (теория типов)#Примеры , полиморфизм в высших родах ). Ти́повые операторы соотносятся со второй осью в лямбда-кубе , приводя к просто типизированному лямбда-исчислению с ти́повыми операторами — λ ω . Комбинация ти́повых операторов с полиморфным лямбда-исчислением ( системой F ) порождает .
Конструкторы типов интенсивно используются в полнотиповом программировании .
В языках программирования семейства ML конструктор типов представляется функцией над типами — т.е. функцией, которая получает на входе одни типы и возвращает другие типы. Оптимизирующие компиляторы исполняют эти функции статически, т.е. (см., например, MLton ).
В классических диалектах
ML
(
Standard ML
,
OCaml
) для
n
-арных конструкторов типов используется нотация
кортежей
. В
Haskell
возможны
каррированные
конструкторы типов. Классические диалекты
ML
при конструировании новых типов используют постфиксный синтаксис (например, «
int list
»), а
Haskell
— префиксный («
List Int
»).
В современных реализациях
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
для определения конструкторов типов есть уже три конструкции —
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)
.