Залежний тип

Зале́жний тип (англ. dependent type) в інформатиці та логіці — тип, який залежить від деякого значення. Залежні типи відіграють ключову роль в інтуїціоністській теорії типів і побудові функційних мов програмування таких як , Agda, ^[en] та .

Наприклад, тип, що описує n-кортежі дійсних чисел, є залежним, оскільки він «залежить» від величини n.

Рішення про рівність залежних типів у програмі може вимагати обчислень. Якщо в залежних типах допущено використання довільних значень, то рішення про рівність типів може включати перевірку рівності результату роботи двох довільних програм. Таким чином, перевірка типу стає нерозв'язною задачею.

Ізоморфізм Каррі — Говарда дозволяє будувати типи для вираження як завгодно складних математичних властивостей. Якщо надано конструктивне доведення того, що тип «заселений» (тобто, існує хоча б одне значення цього типу), компілятор зможе перевірити це доведення і перетворити його на виконуваний код, що обчислює значення. Наявність перевірки доведень робить залежно-типізовані мови схожими з програмним забезпеченням автоматизації доведень (наприклад, інтерактивне доведення теорем Coq).

Системи лямбда-куба

Генк Барендрегт розробив лямбда-куб як засіб класифікації систем типів за трьома осями. Кожен із восьми кутів кубічної діаграми відповідає системі типів. У найбіднішій вершині куба міститься , а в найбагатшій — числення конструкцій. Трьом осям куба відповідають три різні доповнення до просто типізованого лямбда-числення: доповнення залежних типів, доповнення поліморфізму і доповнення конструкторів типів вищого порядку.

Формальне визначення

Дуже спрощено залежний тип можна подати як тип індексованого сімейства множин. Формальніше, для типу ${\displaystyle A:{\mathcal {U}}}$ (де ${\displaystyle {\mathcal {U}}}$ — всесвіт типів), можна визначити сімейство типів ${\displaystyle B}$, що зіставляє кожному терму ${\displaystyle a:A}$ тип ${\displaystyle B(a):{\mathcal {U}}}$, що записується як ${\displaystyle B:A\to {\mathcal {U}}}$. Функцію, чия область значень варіюється залежно від її аргументу, називають залежною функцією. Тип цієї функції називають залежним добутком типів, пі-типом або просто залежним типом. Залежний тип записують для цього випадку як

${\displaystyle \Pi _{(x:A)}B(x)}$

або

${\displaystyle \Pi (x:A),B(x)}$.

Якщо ${\displaystyle B}$ є константою, то залежний тип спрощується до звичайної функції ${\displaystyle A\to B}$. Інакше кажучи, ${\displaystyle \Pi _{(x:A)}B}$ рівнозначний функційному типу ${\displaystyle A\to B}$. Назва «пі-тип» наголошує, що такий тип є декартовим добутком типів. Пі-типи також можна подати як моделі кванторів загальності.

Наприклад, якщо ${\displaystyle {\mbox{Vec}}({\mathbb {R} },n)}$ — кортеж з ${\displaystyle n}$ дійсних чисел, то ${\displaystyle \Pi _{(n:{\mathbb {N} })}{\mbox{Vec}}({\mathbb {R} },n)}$ — тип функцій, які для будь-якого натурального ${\displaystyle n}$ повертають кортеж дійсних чисел розміру ${\displaystyle n}$ . Звичайний функційний простір є тим окремим випадком, коли область значень не залежить від вхідного параметра: наприклад, ${\displaystyle \Pi _{(n:{\mathbb {N} })}\;{\mathbb {R} }}$ — тип функцій з натуральних у дійсні, що позначаються ${\displaystyle {\mathbb {N} }\to {\mathbb {R} }}$ у .

є важливим прикладом залежних функцій, тобто функції, що мають залежний тип. Для певного заданого типу такі функції обробляють значення цього типу, чи значення типу, побудованого з урахуванням цього типу. Поліморфна функція, що повертає значення типу ${\displaystyle C}$, матиме поліморфний тип, що записується як

${\displaystyle \Pi _{(A:{\mathcal {U}})}A\to C}$

Література

• Chlipala, A. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. — MIT Press, 2013. — 440 p. — . (текст із сайту автора(англ.))
• Jeremy Paul Condit. Dependent Types for Safe Systems Software. — PhD dissertation. — University of California at Berkeley, 2007.