Циклопедия скорбит по жертвам террористического акта в Крокус-Сити (Красногорск, МО)

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

Материал из Циклопедии
Перейти к навигации Перейти к поиску

Зависимый тип (в информатике) — вид типа, зависящего от значения.

Примеры[править]

Тип списков длиной в N чисел — зависимый, так как зависит от параметра N.

Значение[править]

Изоморфизм Карри-Говарда сопоставляет:

  • зависимым Π-типам — квантор всеобщности ∀
  • зависимым Σ-типам — квантор существования ∃

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

Реализация[править]

Практическую проблему представляет вычисление равенства двух типов.

Зависимые типы реализованы в языках:

Таксономия[править]

В лямбда-кубе Барендрегта зависимые типы — одна из осей куба. Наиболее выразительной системой куба является исчисление конструкций, сочетающее зависимые типы, полиморфизм и операторы над типами.