Тип добуток також Π тип добуток типів англ product type конструкція у мовах програмування й інтуїціоністській теорії тип

Тип-добуток (також $Π$ -тип, добуток типів; англ. product type) — конструкція у мовах програмування й інтуїціоністській теорії типів, тип даних, побудований як декартів добуток початкових типів; іншими словами — кортеж типів, чи «кортеж як тип»^[⇨]. Використані типи і порядок їх слідування визначають сигнатуру типу-добутку; порядок проходження об'єктів у створюваному кортежі зберігається протягом його часу життя відповідно до заданої сигнатури.

Наприклад, якщо типи A і B є множинами значень a і b відповідно, то складений з них декартів добуток записується як A×B, і отриманий тип-добуток являє собою множину можливих пар (a,b).

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

У мовах, що використовують виклик за значенням, тип-добуток може інтерпретуватися як добуток у категорії типів. У відповідності Каррі-Говарда типи-добутки відповідають кон'юнкції в логіці (операції AND).

Частковий випадок добутку двох типів часто називають «парою» або точніше «впорядкованою парою». Добуток довільної скінченної кількості типів називається «n-арним типом-добутком» або «кортежем з n типів». В українськомовній літературі також є варіант найменування «упорядкована n-ка» (узагальнення від «двійка», «трійка» і т. д.), лінгвістично побудований за аналогією з англійським терміном «tuple» (див. кортеж).

Вироджена форма типу-добутку — добуток нуля типів — являє собою ^[en] (англ. unit type, «тип юніт»), тобто тип, представлений єдиним значенням. Системи типів деяких мов (наприклад, Python) можуть передбачати один або кілька унікальних одиничних типів, не сумісних з типом кортежу з нуля елементів.

Типи-добутки вбудовано в більшість функційних мов програмування. Наприклад, добуток type₁× … × type_n записується як type₁ * … * type_n в ML або як (type₁,…,type_n) у Haskell. В обох мовах кортежі записуються як (v₁,…,v_n) і їх компоненти добуваються шляхом зіставлення зі зразком. На додачу до цього більшість функційних мов надає алгебричні типи даних, що розширюють поняття як типу-добутку, так і . Алгебричні типи, задані єдиним , ізоморфні типам-добуткам.

Кортеж типів як чисте втілення типу-добутку служить формальним обґрунтуванням для частіше вживаного у мовах складеного типу «запис»^[⇨], хоча в деяких мовах реалізовано обидва контейнери. Різниця зазвичай полягає в тому, що кортежі задають і зберігають порядок проходження своїх компонентів у пам'яті ЕОМ (це важливо при зверненні до їх компонентів за допомогою адресної арифметики), але не надають можливості доступу до них за допомогою кваліфікованих ідентифікаторів, а записи, навпаки, визначають ідентифікатори, але не визначають порядок. Проте, є винятки:

у мові 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.

[1] М.О.Денисьєвський та інші (2005). (PDF) (укр.) . Київ: Видавничо-поліграфічний центр "Київський університет". с. 9. Архів оригіналу (PDF) за 15 лютого 2020. Процитовано 17 листопада 2020. {{}}: Вказано більш, ніж один |pages= та |page= ()