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

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

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

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

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

Формальне визначення
Дуже спрощено залежний тип можна подати як тип індексованого сімейства множин. Формальніше, для типу  (де  — всесвіт типів), можна визначити сімейство типів , що зіставляє кожному терму  тип , що записується як . Функцію, чия область значень варіюється залежно від її аргументу, називають залежною функцією. Тип цієї функції називають залежним добутком типів, пі-типом або просто залежним типом. Залежний тип записують для цього випадку як

: 

або

: .

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

Наприклад, якщо  — кортеж з  дійсних чисел, то  — тип функцій, які для будь-якого натурального  повертають кортеж дійсних чисел розміру  . Звичайний  є тим окремим випадком, коли область значень не залежить від вхідного параметра: наприклад,  — тип функцій з натуральних у дійсні, що позначаються  у просто типізованому лямбда-обчисленні.


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

: 

Література
*  ( текст із сайту автора)
* 






