Зависимые типы
Зависимый тип (в информатике) — вид типа, зависящего от значения.
Примеры[править]
Тип списков длиной в N чисел — зависимый, так как зависит от параметра N.
Значение[править]
Изоморфизм Карри-Говарда сопоставляет:
- зависимым Π-типам — квантор всеобщности ∀
- зависимым Σ-типам — квантор существования ∃
Таким образом, достаточно богатые типы могут использоваться для выражения математических свойств, описываемых логикой первого порядка. Конструктивное доказательство существования значений у такого типа будет в подобном языке программным текстом, компилируемым в исполняемый код. Это дает возможность писать программы, корректные «по построению».
Реализация[править]
Практическую проблему представляет вычисление равенства двух типов.
Зависимые типы реализованы в языках:
Таксономия[править]
В лямбда-кубе Барендрегта зависимые типы — одна из осей куба. Наиболее выразительной системой куба является исчисление конструкций, сочетающее зависимые типы, полиморфизм и операторы над типами.