Введение

Тип, определение которого зависит от значения

В информатике и логике зависимый тип — это тип, определение которого зависит от значения. Это пересекающаяся область теории типов и систем типов. В интуиционистской теории типов зависимые типы используются для кодирования кванторов логики, таких как «для всех» и «существует». В функциональных языках программирования, таких как Agda, ATS, Coq, F*, Epigram, Idris и Lean, зависимые типы помогают снизить количество ошибок, позволяя программисту назначать типы, которые ещё больше ограничивают набор возможных реализаций. Два распространённых примера зависимых типов — зависимые функции и зависимые пары. Тип возвращаемого значения зависимой функции может зависеть от значения (а не только типа) одного из её аргументов. Например, функция, принимающая положительное целое число, может возвращать массив длиной *n*, где длина массива является частью типа массива. (Обратите внимание, что это отличается от полиморфизма и обобщённого программирования, оба из которых используют тип в качестве аргумента.) Зависимая пара может иметь второе значение, тип которого зависит от первого значения. Если вернуться к примеру массива, зависимая пара может быть использована для безопасного связывания массива с его длиной. Зависимые типы добавляют сложности в систему типов. Определение равенства зависимых типов в программе может потребовать вычислений. Если в зависимых типах допускаются произвольные значения, то определение равенства типов может включать в себя определение того, выдают ли две произвольные программы один и тот же результат; следовательно, разрешимость проверки типов может зависеть от семантики равенства в данной теории типов, то есть от того, является ли теория типов интенсиональной или экстенсиональной.

История

В 1934 году Хаскелл Карри заметил, что типы, используемые в типизированном лямбда-исчислении, и в его комбинаторной логике, следовали той же закономерности, что и аксиомы в пропозициональной логике. Более того, для каждого доказательства в логике существовала соответствующая функция (терм) в языке программирования. Одним из примеров Карри было соответствие между просто типизированным лямбда-исчислением и интуиционистской логикой. Логика предикатов является расширением пропозициональной логики, добавляющим кванторы. Говард и де Брюйн расширили лямбда-исчисление, чтобы оно соответствовало этой более мощной логике, создав типы для зависимых функций, соответствующие "для всех", и зависимых пар, соответствующие "существует". (Благодаря этому и другим работам Говарда, концепция "предложения как типы" известна как соответствие Карри — Говарда.)

Формальное определение

В широком смысле, зависимые типы аналогичны типу индексированного семейства множеств. Более формально, для данного типа в вселенной типов можно определить семейство типов, которое сопоставляет каждому терму тип. Мы говорим, что тип зависит от a.

Тип

Функция, тип возвращаемого значения которой зависит от её аргумента (то есть не имеет фиксированного кодомена), является зависимой функцией, а тип этой функции называется зависимым типом произведения, пи-типом (тип Π) или зависимым типом функции. Для более конкретного примера, пусть A снова будет типом беззнаковых целых чисел от 0 до 255, и пусть снова будет равно для 256 более произвольных , тогда переходит в сумму .

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

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

Теория зависимых типов первого порядка

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

Теория зависимых типов второго порядка

Система зависимых типов второго порядка получается из, позволяя квантификацию над конструкторами типов. В этой теории зависимый оператор произведения включает в себя как оператор применения в просто типизированном лямбда-исчислении, так и связывание в системе F.

Высший порядок зависимо типизированного полиморфного лямбда-расчета

Система высшего порядка охватывает все четыре формы абстракции из лямбда-куба: функции от термов к термам, типы к типам, термы к типам и типы к термам. Эта система соответствует исчислению конструкций, производным от которого является исчисление индуктивных конструкций – базовая система ассистента Coq.

Одновременный язык программирования и логика

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