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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск
Типизация данных

Типобезопасность
Вывод типов
Статическая типизация
Динамическая типизация
Сильная и слабая типизация
Зависимые типы
Утиная типизация

Зависимый тип в информатике и логике — тип, который зависит от некоторого значения. Зависимые типы играют ключевую роль в интуиционистской теории типов[en] и построении функциональных языков программирования таких как ATS, Agda и Epigram.

К примеру, тип, описывающий nкортежи действительных чисел будет является зависимым, так как он «зависит» от величины n.

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

Изоморфизм Карри — Ховарда позволяет строить типы для выражения сколь угодно сложных математических свойств. Если предоставлено конструктивное доказательство того, что тип «заселён» (то есть, существует хотя бы одно значение этого типа), компилятор сможет проверить это доказательство и превратить его в исполняемый код, вычисляющий значение. Наличие проверки доказательств делает зависимо-типизированные языки схожими с программным обеспечением автоматизации доказательств (например, интерактивный доказатель теорем Coq).

Системы лямбда-куба[править | править исходный текст]

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