Залежний тип

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

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

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

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

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

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

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

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

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

або

$\Pi (x:A),B(x)$.

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

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

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

$\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. — ISBN 9780262026659. (текст із сайту автора(англ.))
• Jeremy Paul Condit. Dependent Types for Safe Systems Software. — PhD dissertation. — University of California at Berkeley, 2007.