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

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

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

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

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

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

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

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

Для улучшения этой статьи желательно?: Найти и оформить в виде сносок ссылки на авторитетные источники, подтверждающие написанное.