Тип-добуток
Тип-добуток (також Π-тип, добуток типів; англ. product type) — конструкція у мовах програмування й інтуїціоністській теорії типів, тип даних, побудований як декартів добуток початкових типів; іншими словами — кортеж типів, чи «кортеж як тип»[⇨]. Використані типи і порядок їх слідування визначають сигнатуру типу-добутку; порядок проходження об'єктів у створюваному кортежі зберігається протягом його часу життя відповідно до заданої сигнатури.
Наприклад, якщо типи A і B є множинами значень a і b відповідно, то складений з них декартів добуток записується як A×B, і отриманий тип-добуток являє собою множину можливих пар (a,b).
Теоретичне і прикладне значення[ред. | ред. код]
У мовах, що використовують виклик за значенням, тип-добуток може інтерпретуватися як добуток у категорії типів. У відповідності Каррі-Говарда типи-добутки відповідають кон'юнкції в логіці (операції AND).
Частковий випадок добутку двох типів часто називають «парою» або точніше «впорядкованою парою». Добуток довільної скінченної кількості типів називається «n-арним типом-добутком» або «кортежем з n типів». В українськомовній літературі також є варіант найменування «упорядкована n-ка»[1] (узагальнення від «двійка», «трійка» і т. д.), лінгвістично побудований за аналогією з англійським терміном «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.
{{cite book}}: Вказано більш, ніж один|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.
| |||||||||||||||||||||||