Зависимый тип

Зависимый тип (англ. 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.