|
|
| (не показана 1 промежуточная версия этого же участника) |
| Строка 1: |
Строка 1: |
| '''Тип-произведение''' (также {{math|Π}}''-тип'', ''произведение типов''; {{lang-en|product type}}) — конструкция в [[язык программирования|языках программирования]] и [[Интуиционистская теория типов|интуиционистской теории типов]], [[тип данных]], построенный как [[декартово произведение]] исходных типов; другими словами — [[Кортеж (информатика)|кортеж]] типов, или «''кортеж как тип''»{{переход|#Кортеж}}. Использованные типы и порядок их следования определяют {{iw|Сигнатура типа|сигнатуру|en|Type signature}} типа-произведения; порядок следования объектов в создаваемом кортеже сохраняется на протяжении его времени жизни согласно заданной сигнатуре. | | '''Тип-произведение''' — конструкция в [[язык программирования|языках программирования]] и [[Интуиционистская теория типов|интуиционистской теории типов]], [[тип данных]], построенный как [[декартово произведение]] исходных типов; другими словами — [[Кортеж (информатика)|кортеж]] типов. Использованные типы и порядок их следования определяют типа-произведения; порядок следования объектов в создаваемом кортеже сохраняется на протяжении его времени жизни согласно заданной сигнатуре. |
| | |
| Например, если типы <code>''A''</code> и <code>''B''</code> представляют собой множества значений <code>''a''</code> и <code>''b''</code> соответственно, то составленное из них декартово произведение записывается как <code>''A''</code>×<code>''B''</code>, и полученный тип-произведение представляет собой всё множество возможных пар <code>(''a'',''b'')</code>.
| |
|
| |
|
| == Теоретическое и прикладное значение == | | == Теоретическое и прикладное значение == |
| В языках, использующих [[вызов по значению]], тип-произведение может интерпретироваться как [[Произведение (теория категорий)|произведение в категории типов]]. В [[Соответствие Карри — Ховарда|соответствии Карри-Ховарда]] типы-произведения соответствуют [[конъюнкция|конъюнкции]] в логике (операции <code>AND</code>). | | В языках, использующих [[вызов по значению]], тип-произведение может интерпретироваться как [[Произведение (теория категорий)|произведение в категории типов]]. |
| | |
| Частный случай произведения двух типов часто называют «''парой''» или более точно «''упорядоченной парой''». Произведение произвольного конечного количества типов называется «''[[арность|n-арным]] типом-произведением''» или «''кортежем из n типов''». В русскоязычной литературе также присутствует вариант наименования «''упорядоченная энка''» (обобщение от «''двойка''», «''тройка''» и т. д.), лингвистически построенный по аналогии с английским термином «''tuple''» (см. [[:en:Tuple (computer science)|кортеж {{ref-en}}]]).
| |
| | |
| Вырожденная форма типа-произведения — произведение нуля типов — представляет собой {{iw|единичный тип||en|unit type}} ({{lang-en|unit type}}, «''тип юнит''»), то есть тип, представленный единственным значением. [[Система типов|Системы типов]] некоторых языков (например, [[Python]]) могут предусматривать один или несколько уникальных единичных типов, не совместимых с ''типом кортежа из нуля элементов''.
| |
| | |
| Типы-произведения встроены в большинство [[функциональное программирование|функциональных]] языков программирования. Например, произведение ''type<sub>1</sub>''× … × ''type<sub>n</sub>'' записывается как ''type<sub>1</sub>''<code> * </code>…<code> * </code>''type<sub>n</sub>'' в [[ML]] или как <code>(</code>''type<sub>1</sub>''<code>,</code>…<code>,</code>''type<sub>n</sub>''<code>)</code> в [[Haskell]]. В обоих языках [[Кортеж (информатика)|кортежи]] записываются как <code>(</code>''v<sub>1</sub>''<code>,</code>…<code>,</code>''v<sub>n</sub>''<code>)</code> и их компоненты извлекаются посредством [[сопоставление с образцом|сопоставления с образцом]]. В дополнение к этому большинство функциональных языков предоставляет [[Алгебраический тип данных|алгебраические типы данных]], расширяющие понятия как типа-произведения, так и [[тип-сумма|типа-суммы]]. Алгебраические типы, заданные единственным [[Конструктор (функциональное программирование)|конструктором]], [[изоморфизм|изоморфны]] типам-произведениям.
| |
| | |
| Кортеж типов как чистое воплощение типа-произведения служит формальным обоснованием для более часто встречающегося в языках составного типа «[[Запись (тип данных)|запись]]»{{переход|#Запись}}, хотя в некоторых языках реализованы оба контейнера. Разница обычно заключается в том, что кортежи задают и сохраняют порядок следования своих компонентов в памяти ЭВМ (это важно при обращении к их компонентам посредством [[Указатель (тип данных)#адресная арифметика|адресной арифметики]]), но не предоставляют возможности доступа к ним посредством квалифицированных идентификаторов, а записи, наоборот, определяют идентификаторы, но не определяют порядок следования. Однако, есть исключения:
| |
| * в языке [[Standard ML]] кортежи значений с целью оптимизации размещения в памяти реализуются посредством записей, у которых в качестве идентификаторов компонентов используются их порядковые номера в кортеже; адресная арифметика недоступна; типы перестают существовать после компиляции; и требуемый порядок следования принуждается только при {{iw|Внешнеязыковой интерфейс|межъязыковом взаимодействии|en|Foreign Function Interface}}.
| |
| * в языке [[Си (язык программирования)|Си]] тип данных «''[[Структура (программирование)|структура]]''» (<code>struct</code>){{переход|#Структура (Си)}} соединяет в себе свойства записей и кортежей, то есть позволяет назначать компонентам идентификаторы и одновременно гарантирует сохранение порядка их следования. Кроме того, в отличие от записей и кортежей, структуры в Си могут содержать [[Указатель (программирование)|указатели]] на собственные объекты, что позволяет непосредственно строить {{iw|рекурсивный тип данных|рекурсивные типы данных|en|Recursive data type}}.
| |
| | |
| == Реализация в языках программирования ==
| |
|
| |
|
| === {{якорь|tuple type|Кортеж}} Кортежи ===
| | Кортеж типов как чистое воплощение типа-произведения служит формальным обоснованием для более часто встречающегося в языках составного типа, хотя в некоторых языках реализованы оба контейнера. Разница обычно заключается в том, что кортежи задают и сохраняют порядок следования своих компонентов в памяти ЭВМ (это важно при обращении к их компонентам посредством адресной арифметики), но не предоставляют возможности доступа к ним посредством квалифицированных идентификаторов, а записи, наоборот, определяют идентификаторы, но не определяют порядок следования. |
| {{main|Кортеж (информатика)}}
| |
|
| |
|
| === {{якорь|record type|Запись}} Записи ===
| |
| {{main|Запись (тип данных)}}
| |
| Во многих языках запись представляет собой [[агрегирование (программирование)|агрегатный тип данных]], [[инкапсуляция (программирование)|инкапсулирующий]] без [[Сокрытие (программирование)|сокрытия]] набор [[Значение_(информатика)|значений]] различных типов.
| |
|
| |
|
| В одних языках (например, в [[Си (язык программирования)|Си]] или [[Паскаль (язык программирования)|Паскале]]) порядок размещения значений в памяти задаётся при определении типа и сохраняется на протяжении времени жизни объектов, что даёт возможность косвенного доступа (например, через [[Указатель (тип данных)|указатели]]); в других языках (например, в [[ML]]) порядок размещения не определён, так что доступ к значениям возможен только по квалифицированному идентификатору. В некоторых языках, хотя порядок следования и сохраняется, но [[Выравнивание данных|выравнивание]] контролируется компилятором, так что использование адресной арифметики может оказаться платформенно-зависимым. Некоторые языки позволяют присваивание между экземплярами разных записей, игнорируя различия в идентификаторах компонентов записей, и основываясь только на порядке следования. Другие языки, напротив, учитывают только совпадение имён, разрешая различия в порядке их определения. | | В одних языках (например, в [[Си]] или [[Pascal|Паскале]]) порядок размещения значений в памяти задаётся при определении типа и сохраняется на протяжении времени жизни объектов, что даёт возможность косвенного доступа (например, через [[Указатель (тип данных)|указатели]]); в других языках (например, в [[ML]]) порядок размещения не определён, так что доступ к значениям возможен только по квалифицированному идентификатору. В некоторых языках, хотя порядок следования и сохраняется, но [[Выравнивание данных|выравнивание]] контролируется компилятором, так что использование адресной арифметики может оказаться платформенно-зависимым. Некоторые языки позволяют присваивание между экземплярами разных записей, игнорируя различия в идентификаторах компонентов записей, и основываясь только на порядке следования. Другие языки, напротив, учитывают только совпадение имён, разрешая различия в порядке их определения. |
|
| |
|
| Впервые записи были представлены в языке [[Кобол]], где они имели довольно сложную нотацию. При проверке согласования типов, Кобол учитывает только совпадение имён полей записей и не учитывает совпадение порядка их следования. | | Впервые записи были представлены в языке [[Кобол]], где они имели довольно сложную нотацию. При проверке согласования типов, Кобол учитывает только совпадение имён полей записей и не учитывает совпадение порядка их следования. |
| Строка 31: |
Строка 13: |
| [[Кортеж (информатика)|Кортежи]] служат формальным обоснованием записей в [[теория типов|теории типов]]. В то же время, в языках кортежи временами могут реализовываться посредством записей, использующих в качестве идентификаторов индексные номера полей в получаемом кортеже. | | [[Кортеж (информатика)|Кортежи]] служат формальным обоснованием записей в [[теория типов|теории типов]]. В то же время, в языках кортежи временами могут реализовываться посредством записей, использующих в качестве идентификаторов индексные номера полей в получаемом кортеже. |
|
| |
|
| === {{якорь|struct type|Структура|Структура (Си)}} Структуры в Си ===
| |
| {{main|Структура (язык Си)}}
| |
| В языке [[Си (язык программирования)|Си]], '''структура''' (<code>struct</code>) — [[агрегирование (программирование)|композитный тип данных]], [[инкапсуляция (программирование)|инкапсулирующий]] без [[Сокрытие (программирование)|сокрытия]] набор [[Значение_(информатика)|значений]] различных типов. Порядок размещения значений в памяти задаётся при определении типа и сохраняется на протяжении времени жизни объектов, что даёт возможность косвенного доступа (например, через [[Указатель (тип данных)|указатели]]).
| |
|
| |
| == Примечания ==
| |
| {{примечания}}
| |
|
| |
| == Ссылки ==
| |
| * {{статья
| |
| | автор =
| |
| | заглавие = Homotopy Type Theory: Univalent Foundations of Mathematics, section 1.5
| |
| | язык = en
| |
| | издательство = The Univalent Foundations Program, Institute for Advanced Study
| |
| | ссылка = http://homotopytypetheory.org/2013/06/20/the-hott-book/
| |
| | ref =
| |
| }}
| |
| * {{книга
| |
| | автор = [[Харпер, Роберт|Роберт Харпер]]
| |
| | заглавие = Введение в Стандартный ML
| |
| | издательство = Carnegie Mellon University
| |
| | год = 1986
| |
| | страниц = 97
| |
| | isbn = PA 15213-3891
| |
| | ссылка =
| |
| | ref = Harper
| |
| }}
| |
| * {{книга
| |
| | автор = Эммануэль Шалуа, Паскаль Манури, Бруно Пагано
| |
| | заглавие = Разработка программ с помощью Objective Caml
| |
| | издательство =
| |
| | год = 2007
| |
| | страниц =
| |
| | isbn =
| |
| | ссылка =
| |
| | ref = Шалуа-Манури-Пагано
| |
| }}
| |
|
| |
| {{типы данных}}
| |
|
| |
| [[Категория:Типы данных]]
| |
| [[Категория:Теория типов]]
| |
| [[Категория:Структуры данных]] | | [[Категория:Структуры данных]] |
| [[Категория:Инкапсуляция (программирование)]]
| |
| [[Категория:Типы данных СУБД]]
| |
| [[Категория:Составные типы данных]]
| |
Тип-произведение — конструкция в языках программирования и интуиционистской теории типов, тип данных, построенный как декартово произведение исходных типов; другими словами — кортеж типов. Использованные типы и порядок их следования определяют типа-произведения; порядок следования объектов в создаваемом кортеже сохраняется на протяжении его времени жизни согласно заданной сигнатуре.
Теоретическое и прикладное значение
В языках, использующих вызов по значению, тип-произведение может интерпретироваться как произведение в категории типов.
Кортеж типов как чистое воплощение типа-произведения служит формальным обоснованием для более часто встречающегося в языках составного типа, хотя в некоторых языках реализованы оба контейнера. Разница обычно заключается в том, что кортежи задают и сохраняют порядок следования своих компонентов в памяти ЭВМ (это важно при обращении к их компонентам посредством адресной арифметики), но не предоставляют возможности доступа к ним посредством квалифицированных идентификаторов, а записи, наоборот, определяют идентификаторы, но не определяют порядок следования.
В одних языках (например, в Си или Паскале) порядок размещения значений в памяти задаётся при определении типа и сохраняется на протяжении времени жизни объектов, что даёт возможность косвенного доступа (например, через указатели); в других языках (например, в ML) порядок размещения не определён, так что доступ к значениям возможен только по квалифицированному идентификатору. В некоторых языках, хотя порядок следования и сохраняется, но выравнивание контролируется компилятором, так что использование адресной арифметики может оказаться платформенно-зависимым. Некоторые языки позволяют присваивание между экземплярами разных записей, игнорируя различия в идентификаторах компонентов записей, и основываясь только на порядке следования. Другие языки, напротив, учитывают только совпадение имён, разрешая различия в порядке их определения.
Впервые записи были представлены в языке Кобол, где они имели довольно сложную нотацию. При проверке согласования типов, Кобол учитывает только совпадение имён полей записей и не учитывает совпадение порядка их следования.
Кортежи служат формальным обоснованием записей в теории типов. В то же время, в языках кортежи временами могут реализовываться посредством записей, использующих в качестве идентификаторов индексные номера полей в получаемом кортеже.
