Тип-добуток (також Π-тип, добуток типів; англ. product type) — конструкція у мовах програмування й інтуїціоністській теорії типів, тип даних, побудований як декартів добуток початкових типів; іншими словами — кортеж типів, чи «кортеж як тип»[⇨]. Використані типи і порядок їх слідування визначають сигнатуру типу-добутку; порядок проходження об'єктів у створюваному кортежі зберігається протягом його часу життя відповідно до заданої сигнатури.
Наприклад, якщо типи A
і B
є множинами значень a
і b
відповідно, то складений з них декартів добуток записується як A
×B
, і отриманий тип-добуток являє собою множину можливих пар (a,b)
.
Теоретичне і прикладне значення
У мовах, що використовують виклик за значенням, тип-добуток може інтерпретуватися як добуток у категорії типів. У відповідності Каррі-Говарда типи-добутки відповідають кон'юнкції в логіці (операції AND
).
Частковий випадок добутку двох типів часто називають «парою» або точніше «впорядкованою парою». Добуток довільної скінченної кількості типів називається «n-арним типом-добутком» або «кортежем з n типів». В українськомовній літературі також є варіант найменування «упорядкована n-ка» (узагальнення від «двійка», «трійка» і т. д.), лінгвістично побудований за аналогією з англійським терміном «tuple» (див. кортеж).
Вироджена форма типу-добутку — добуток нуля типів — являє собою [en] (англ. unit type, «тип юніт»), тобто тип, представлений єдиним значенням. Системи типів деяких мов (наприклад, Python) можуть передбачати один або кілька унікальних одиничних типів, не сумісних з типом кортежу з нуля елементів.
Типи-добутки вбудовано в більшість функційних мов програмування. Наприклад, добуток type1× … × typen записується як type1 *
… *
typen в ML або як (
type1,
…,
typen)
у Haskell. В обох мовах кортежі записуються як (
v1,
…,
vn)
і їх компоненти добуваються шляхом зіставлення зі зразком. На додачу до цього більшість функційних мов надає (алгебричні типи даних), що розширюють поняття як типу-добутку, так і . Алгебричні типи, задані єдиним , ізоморфні типам-добуткам.
Кортеж типів як чисте втілення типу-добутку служить формальним обґрунтуванням для частіше вживаного у мовах складеного типу «запис»[⇨], хоча в деяких мовах реалізовано обидва контейнери. Різниця зазвичай полягає в тому, що кортежі задають і зберігають порядок проходження своїх компонентів у пам'яті ЕОМ (це важливо при зверненні до їх компонентів за допомогою адресної арифметики), але не надають можливості доступу до них за допомогою кваліфікованих ідентифікаторів, а записи, навпаки, визначають ідентифікатори, але не визначають порядок. Проте, є винятки:
- у мові Standard ML кортежі значень з метою оптимізації розміщення в пам'яті реалізуються за допомогою записів, у яких як ідентифікатори компонентів використовуються їхні порядкові номери в кортежі; адресна арифметика недоступна; типи перестають існувати після компіляції; і необхідний порядок слідування є примусовим тільки за [en].
- у мові C тип даних «структура» (
struct
)[⇨] поєднує властивості записів і кортежів, тобто дозволяє призначати компонентам ідентифікатори і одночасно гарантує збереження порядку їх слідування. Крім того, на відміну від записів і кортежів, структури Сі можуть містити вказівники на власні об'єкти, що дозволяє безпосередньо будувати (рекурсивні типи даних).
Реалізація в мовах програмування
Кортежі
Записи
В багатьох мовах запис являє собою , який інкапсулює без набір значень різних типів.
В одних мовах (наприклад, в Сі або Паскалі) порядок розміщення значень у пам'яті задається під час визначення типу і зберігається протягом часу життя об'єктів, що дає можливість непрямого доступу (наприклад, через вказівники); в інших мовах (наприклад, в ML) порядок розміщення не визначений, так що доступ до даних можливий тільки за кваліфікованим ідентифікатором. У деяких мовах, хоча порядок проходження і зберігається, але (вирівнювання) контролює компілятор, так що використання адресної арифметики може виявитися платформно-залежним. Деякі мови дозволяють присвоювання між екземплярами різних записів, нехтуючи відмінності в ідентифікаторах компонентів записів, і ґрунтуючись тільки на порядку слідування. Інші мови, навпаки, враховують тільки збіг назв, дозволяючи відмінності в порядку їх визначення.
Вперше записи представлено в мові Кобол, де вони мали досить складну нотацію. Під час перевірки узгодження типів, Кобол враховує тільки збіг назв полів записів і не враховує порядку їх слідування.
Кортежі служать формальним обґрунтуванням записів у теорії типів. Разом з тим, у мовах кортежі часом можуть реалізовуватися за допомогою записів, що використовують як ідентифікатори індексні номери полів в одержуваному кортежі.
Структури в Сі
В мові Сі, структура (struct
) — , який інкапсулює без набір значень різних типів. Порядок розміщення значень у пам'яті задається під час визначення типу і зберігається протягом часу життя об'єктів, що дає можливість непрямого доступу (наприклад, через вказівники).
Примітки
- М.О.Денисьєвський та інші (2005). (PDF) (укр.) . Київ: Видавничо-поліграфічний центр "Київський університет". с. 9. Архів оригіналу (PDF) за 15 лютого 2020. Процитовано 17 листопада 2020.
{{}}
: Вказано більш, ніж один|pages=
та|page=
()
Посилання
- Homotopy Type Theory: Univalent Foundations of Mathematics, section 1.5. — The Univalent Foundations Program, Institute for Advanced Study. з джерела 30 жовтня 2020. Процитовано 17 листопада 2020.
- [en]. Введение в Стандартный ML. — Carnegie Mellon University, 1986. — 97 с. — ISBN PA 15213-3891.
- Эммануэль Шалуа, Паскаль Манури, Бруно Пагано. Разработка программ с помощью Objective Caml. — 2007.
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет