Тип-произведение: различия между версиями

Материал из Поле цифровой дидактики
← Предыдущая правкаСледующая правка →
м 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]]) порядок размещения не определён, так что доступ к значениям возможен только по квалифицированному идентификатору. В некоторых языках, хотя порядок следования и сохраняется, но [[Выравнивание данных|выравнивание]] контролируется компилятором, так что использование адресной арифметики может оказаться платформенно-зависимым. Некоторые языки позволяют присваивание между экземплярами разных записей, игнорируя различия в идентификаторах компонентов записей, и основываясь только на порядке следования. Другие языки, напротив, учитывают только совпадение имён, разрешая различия в порядке их определения.
В одних языках (например, в [[Си (язык программирования)|Си]] или [[Паскаль (язык программирования)|Паскале]]) порядок размещения значений в памяти задаётся при определении типа и сохраняется на протяжении времени жизни объектов, что даёт возможность косвенного доступа (например, через [[Указатель (тип данных)|указатели]]); в других языках (например, в [[ML]]) порядок размещения не определён, так что доступ к значениям возможен только по квалифицированному идентификатору. В некоторых языках, хотя порядок следования и сохраняется, но [[Выравнивание данных|выравнивание]] контролируется компилятором, так что использование адресной арифметики может оказаться платформенно-зависимым. Некоторые языки позволяют присваивание между экземплярами разных записей, игнорируя различия в идентификаторах компонентов записей, и основываясь только на порядке следования. Другие языки, напротив, учитывают только совпадение имён, разрешая различия в порядке их определения.
Строка 31: Строка 12:
[[Кортеж (информатика)|Кортежи]] служат формальным обоснованием записей в [[теория типов|теории типов]]. В то же время, в языках кортежи временами могут реализовываться посредством записей, использующих в качестве идентификаторов индексные номера полей в получаемом кортеже.
[[Кортеж (информатика)|Кортежи]] служат формальным обоснованием записей в [[теория типов|теории типов]]. В то же время, в языках кортежи временами могут реализовываться посредством записей, использующих в качестве идентификаторов индексные номера полей в получаемом кортеже.


=== {{якорь|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 = Шалуа-Манури-Пагано
}}
{{типы данных}}
[[Категория:Типы данных]]
[[Категория:Теория типов]]
[[Категория:Структуры данных]]
[[Категория:Структуры данных]]
[[Категория:Инкапсуляция (программирование)]]
[[Категория:Типы данных СУБД]]
[[Категория:Составные типы данных]]

Версия от 12:21, 19 октября 2022

Тип-произведение — конструкция в языках программирования и интуиционистской теории типов, тип данных, построенный как декартово произведение исходных типов; другими словами — кортеж типов. Использованные типы и порядок их следования определяют типа-произведения; порядок следования объектов в создаваемом кортеже сохраняется на протяжении его времени жизни согласно заданной сигнатуре.

Теоретическое и прикладное значение

В языках, использующих вызов по значению, тип-произведение может интерпретироваться как произведение в категории типов. В\ Кортеж типов как чистое воплощение типа-произведения служит формальным обоснованием для более часто встречающегося в языках составного типа «запись»Шаблон:Переход, хотя в некоторых языках реализованы оба контейнера. Разница обычно заключается в том, что кортежи задают и сохраняют порядок следования своих компонентов в памяти ЭВМ (это важно при обращении к их компонентам посредством адресной арифметики), но не предоставляют возможности доступа к ним посредством квалифицированных идентификаторов, а записи, наоборот, определяют идентификаторы, но не определяют порядок следования.


В одних языках (например, в Си или Паскале) порядок размещения значений в памяти задаётся при определении типа и сохраняется на протяжении времени жизни объектов, что даёт возможность косвенного доступа (например, через указатели); в других языках (например, в ML) порядок размещения не определён, так что доступ к значениям возможен только по квалифицированному идентификатору. В некоторых языках, хотя порядок следования и сохраняется, но выравнивание контролируется компилятором, так что использование адресной арифметики может оказаться платформенно-зависимым. Некоторые языки позволяют присваивание между экземплярами разных записей, игнорируя различия в идентификаторах компонентов записей, и основываясь только на порядке следования. Другие языки, напротив, учитывают только совпадение имён, разрешая различия в порядке их определения.

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

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

Источник — http://digida.mgpu.ru/index.php?title=Тип-произведение&oldid=4606