Тип-произведение
Тип-произведение (также Π-тип, произведение типов; англ. product type) — конструкция в языках программирования и интуиционистской теории типов, тип данных, построенный как декартово произведение исходных типов; другими словами — кортеж типов, или «кортеж как тип». Использованные типы и порядок их следования определяют сигнатуру типа-произведения; порядок следования объектов в создаваемом кортеже сохраняется на протяжении его времени жизни согласно заданной сигнатуре.
Например, если типы A и B представляют собой множества значений a и b соответственно, то составленное из них декартово произведение записывается как A×B, и полученный тип-произведение представляет собой всё множество возможных пар (a,b).
Теоретическое и прикладное значение
В языках, использующих вызов по значению, тип-произведение может интерпретироваться как произведение в категории типов. В соответствии Карри-Ховарда типы-произведения соответствуют конъюнкции в логике (операции AND).
Частный случай произведения двух типов часто называют «парой» или более точно «упорядоченной парой». Произведение произвольного конечного количества типов называется «n-арным типом-произведением» или «кортежем из n типов». В русскоязычной литературе также присутствует вариант наименования «упорядоченная энка» (обобщение от «двойка», «тройка» и т. д.), лингвистически построенный по аналогии с английским термином «tuple» (см. кортеж (англ.)).
Вырожденная форма типа-произведения — произведение нуля типов — представляет собой единичный тип (англ. unit type, «тип юнит»), то есть тип, представленный единственным значением. Системы типов некоторых языков (например, Python) могут предусматривать один или несколько уникальных единичных типов, не совместимых с типом кортежа из нуля элементов.
Типы-произведения встроены в большинство функциональных языков программирования. Например, произведение type1× … × typen записывается как type1 * … * typen в ML или как (type1,…,typen) в Haskell. В обоих языках кортежи записываются как (v1,…,vn) и их компоненты извлекаются посредством сопоставления с образцом. В дополнение к этому большинство функциональных языков предоставляет алгебраические типы данных, расширяющие понятия как типа-произведения, так и типа-суммы. Алгебраические типы, заданные единственным конструктором, изоморфны типам-произведениям.
Кортеж типов как чистое воплощение типа-произведения служит формальным обоснованием для более часто встречающегося в языках составного типа «запись», хотя в некоторых языках реализованы оба контейнера. Разница обычно заключается в том, что кортежи задают и сохраняют порядок следования своих компонентов в памяти ЭВМ (это важно при обращении к их компонентам посредством адресной арифметики), но не предоставляют возможности доступа к ним посредством квалифицированных идентификаторов, а записи, наоборот, определяют идентификаторы, но не определяют порядок следования. Однако, есть исключения:
- в языке Standard ML кортежи значений с целью оптимизации размещения в памяти реализуются посредством записей, у которых в качестве идентификаторов компонентов используются их порядковые номера в кортеже; адресная арифметика недоступна; типы перестают существовать после компиляции; и требуемый порядок следования принуждается только при межъязыковом взаимодействии.
- в языке Си тип данных «структура» (
struct) соединяет в себе свойства записей и кортежей, то есть позволяет назначать компонентам идентификаторы и одновременно гарантирует сохранение порядка их следования. Кроме того, в отличие от записей и кортежей, структуры в Си могут содержать указатели на собственные объекты, что позволяет непосредственно строить рекурсивные типы данных.
Реализация в языках программирования
Кортежи
Записи
Во многих языках запись представляет собой агрегатный тип данных, инкапсулирующий без сокрытия набор значений различных типов.
В одних языках (например, в Си или Паскале) порядок размещения значений в памяти задаётся при определении типа и сохраняется на протяжении времени жизни объектов, что даёт возможность косвенного доступа (например, через указатели); в других языках (например, в ML) порядок размещения не определён, так что доступ к значениям возможен только по квалифицированному идентификатору. В некоторых языках, хотя порядок следования и сохраняется, но выравнивание контролируется компилятором, так что использование адресной арифметики может оказаться платформенно-зависимым. Некоторые языки позволяют присваивание между экземплярами разных записей, игнорируя различия в идентификаторах компонентов записей, и основываясь только на порядке следования. Другие языки, напротив, учитывают только совпадение имён, разрешая различия в порядке их определения.
Впервые записи были представлены в языке Кобол, где они имели довольно сложную нотацию. При проверке согласования типов, Кобол учитывает только совпадение имён полей записей и не учитывает совпадение порядка их следования.
Кортежи служат формальным обоснованием записей в теории типов. В то же время, в языках кортежи временами могут реализовываться посредством записей, использующих в качестве идентификаторов индексные номера полей в получаемом кортеже.
Структуры в Си
В языке Си, структура (struct) — композитный тип данных, инкапсулирующий без сокрытия набор значений различных типов. Порядок размещения значений в памяти задаётся при определении типа и сохраняется на протяжении времени жизни объектов, что даёт возможность косвенного доступа (например, через указатели).
Примечания
Ссылки
- Homotopy Type Theory: Univalent Foundations of Mathematics, section 1.5 (англ.). — The Univalent Foundations Program, Institute for Advanced Study.
- Роберт Харпер. Введение в Стандартный ML. — Carnegie Mellon University, 1986. — 97 с. — ISBN PA 15213-3891.
- Эммануэль Шалуа, Паскаль Манури, Бруно Пагано. Разработка программ с помощью Objective Caml. — 2007.