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

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

Два распространенных примера зависимых типов — зависимые функции и зависимые пары . Тип возвращаемого значения зависимой функции может зависеть от значения ( а не только типа) одного из ее аргументов. Например, функция, которая принимает положительное целое число , может возвращать массив длины , где длина массива является частью типа массива. (Обратите внимание, что это отличается от полиморфизма и обобщенного программирования , оба из которых включают тип в качестве аргумента.) Зависимая пара может иметь второе значение, тип которого зависит от первого значения. Придерживаясь примера с массивом, зависимая пара может использоваться для сопряжения массива с его длиной безопасным для типов способом.${\displaystyle n}$${\displaystyle n}$

Зависимые типы добавляют сложности к системе типов. Решение о равенстве зависимых типов в программе может потребовать вычислений. Если в зависимых типах допускаются произвольные значения, то решение о равенстве типов может включать решение о том, производят ли две произвольные программы одинаковый результат; следовательно, разрешимость проверки типов может зависеть от семантики равенства данной теории типов, то есть от того, является ли теория типов интенсиональной или экстенсиональной . ^[1]

В 1934 году Хаскелл Карри заметил, что типы, используемые в типизированном лямбда-исчислении и в его комбинаторном логическом аналоге, следовали той же схеме, что и аксиомы в пропозициональной логике . Идя дальше, для каждого доказательства в логике существовала соответствующая функция (терм) в языке программирования. Одним из примеров Карри было соответствие между просто типизированным лямбда-исчислением и интуиционистской логикой . ^[2]

Логика предикатов является расширением пропозициональной логики, добавляя квантификаторы. Говард и де Брейн расширили лямбда-исчисление, чтобы соответствовать этой более мощной логике, создав типы для зависимых функций, которые соответствуют «для всех», и зависимые пары, которые соответствуют «существует». ^[3]

Благодаря этой и другим работам Говарда, предложения как типы известны как соответствие Карри–Говарда .

Грубо говоря, зависимые типы похожи на тип индексированного семейства множеств . Более формально, если задан тип в универсуме типов , можно иметь семейство типов , которое назначает каждому термину тип . Мы говорим, что тип изменяется в зависимости от .${\displaystyle A:{\mathcal {U}}}$${\displaystyle {\mathcal {U}}}$ ${\displaystyle B:A\to {\mathcal {U}}}$${\displaystyle а:А}$${\displaystyle B(a):{\mathcal {U}}}$${\displaystyle B(a)}$${\displaystyle а}$

Функция, тип возвращаемого значения которой меняется в зависимости от ее аргумента (т.е. не существует фиксированной области значений ), является зависимой функцией , а тип этой функции называется типом зависимого произведения , пи-типом ( типом Π ) или типом зависимой функции . ^[4] Из семейства типов мы можем построить тип зависимых функций , члены которого являются функциями, которые принимают член и возвращают член в . Для этого примера тип зависимой функции обычно записывается как или .${\displaystyle B:A\to {\mathcal {U}}}$${\textstyle \prod _{x:A}B(x)}$${\displaystyle а:А}$${\displaystyle B(a)}$${\textstyle \prod _{x:A}B(x)}$${\textstyle \prod {(x:A)}B(x)}$

Если — постоянная функция, то соответствующий зависимый тип произведения эквивалентен обычному типу функции . То есть, оценочно равен , когда не зависит от .${\displaystyle B:A\to {\mathcal {U}}}$${\textstyle \prod _{x:A}B}$${\displaystyle A\to B}$${\displaystyle Б}$${\displaystyle x}$

Название «Π-тип» происходит от идеи, что их можно рассматривать как декартово произведение типов. Π-типы также можно понимать как модели кванторов всеобщности .

Например, если мы напишем для n -кортежей действительных чисел , то будет типом функции, которая, учитывая натуральное число n , возвращает кортеж действительных чисел размера n . Обычное пространство функций возникает как особый случай, когда тип диапазона фактически не зависит от входных данных. Например, это тип функций от натуральных чисел до действительных чисел, который записывается как в типизированном лямбда-исчислении.${\displaystyle \operatorname {Vec} (\mathbb {R} ,n)}$${\textstyle \prod _{n:\mathbb {N}}\operatorname {Vec} (\mathbb {R},n)}$ ${\textstyle \prod _{n:\mathbb {N} {\mathbb {R} }}$${\displaystyle \mathbb {N} \to \mathbb {R} }$

Для более конкретного примера, принимая в качестве типа беззнаковых целых чисел от 0 до 255 (тех, которые помещаются в 8 бит или 1 байт) и для , то преобразуется в произведение . ${\displaystyle А}$${\displaystyle B(a)=X_{a}}$${\displaystyle а:А}$${\textstyle \prod _{x:A}B(x)}$${\displaystyle X_{0}\times X_{1}\times X_{2}\times \ldots \times X_{253}\times X_{254}\times X_{255}}$

Двойственный зависимому типу продукта — зависимый тип пары , зависимый тип суммы , сигма-тип или (что сбивает с толку) зависимый тип продукта . ^[4] Сигма-типы также можно понимать как экзистенциальные квантификаторы . Продолжая приведенный выше пример, если во вселенной типов есть тип и семейство типов , то есть зависимый тип пары . (Альтернативные обозначения аналогичны обозначениям Π -типов.)${\displaystyle {\mathcal {U}}}$${\displaystyle A:{\mathcal {U}}}$${\displaystyle B:A\to {\mathcal {U}}}$${\textstyle \sum _{x:A}B(x)}$

Тип зависимой пары отражает идею упорядоченной пары, где тип второго члена зависит от значения первого. Если то и . Если — постоянная функция, то тип зависимой пары становится (оценочно равен) типу продукта , то есть обычному декартову произведению . ^[4]${\textstyle (a,b):\sum _{x:A}B(x),}$${\displaystyle а:А}$${\displaystyle b:B(a)}$${\displaystyle Б}$${\displaystyle A\times B}$

Для более конкретного примера, снова принимая тип беззнаковых целых чисел от 0 до 255, и снова принимая значение для более произвольного 256 , затем сводится к сумме .${\displaystyle А}$${\displaystyle B(a)}$${\displaystyle X_{a}}$${\displaystyle X_{a}}$${\textstyle \sum _{x:A}B(x)}$${\displaystyle X_{0}+X_{1}+X_{2}+\ldots +X_{253}+X_{254}+X_{255}}$

Пусть будет некоторым типом, и пусть . По соответствию Карри–Ховарда, может быть интерпретировано как логический предикат на терминах . Для заданного , является ли тип обитаемым, указывает на то, удовлетворяет ли этому предикату. Соответствие может быть распространено на экзистенциальную квантификацию и зависимые пары: предложение истинно тогда и только тогда, когда тип обитаем.${\displaystyle A:{\mathcal {U}}}$${\displaystyle B:A\to {\mathcal {U}}}$${\displaystyle Б}$${\displaystyle А}$${\displaystyle а:А}$${\displaystyle B(a)}$${\displaystyle а}$${\displaystyle \exists {a}{\in }A\,B(a)}$${\textstyle \sum _{a:A}B(a)}$

Например, меньше или равно тогда и только тогда, когда существует другое натуральное число, такое что . В логике это утверждение кодифицируется экзистенциальной квантификацией:${\displaystyle m:\mathbb {N} }$${\displaystyle n:\mathbb {N}}$${\displaystyle k:\mathbb {N} }$${\displaystyle м+к=н}$

$${\displaystyle m\leq n\если \существует {k}{\in }\mathbb {N} \,m+k=n.}$$

Это предложение соответствует типу зависимой пары:

$${\displaystyle \sum _{k:\mathbb {N} }m+k=n.}$$

То есть доказательством утверждения, что число меньше или равно, является пара, содержащая как неотрицательное число , представляющее собой разность между и , так и доказательство равенства .${\displaystyle м}$${\displaystyle n}$${\displaystyle к}$${\displaystyle м}$${\displaystyle n}$${\displaystyle м+к=н}$

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

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

Система зависимых типов второго порядка получается из разрешения квантификации по конструкторам типов. В этой теории оператор зависимого произведения включает в себя как оператор простого типизированного лямбда-исчисления, так и связующее устройство Системы F.${\displaystyle \лямбда \Пи 2}$${\displaystyle \лямбда \Пи}$${\displaystyle \to}$${\displaystyle \forall}$

Система более высокого порядка распространяется на все четыре формы абстракции от лямбда-куба : функции от термов к термовам, типы к типам, термов к типам и типы к термовам. Система соответствует исчислению конструкций , производная которой, исчисление индуктивных конструкций , является базовой системой помощника доказательства Coq .${\displaystyle \лямбда \Пи \омега}$${\displaystyle \лямбда \Пи 2}$

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

• Типизированное лямбда-исчисление
• Интуиционистская теория типов

• Зависимо типизированное программирование 2008
• Зависимо типизированное программирование 2010
• Зависимо типизированное программирование 2011
• «Зависимый тип» на Haskell Wiki
• Теория зависимых типов в n Lab
• зависимый тип в n Lab
• зависимый тип продукта в n Lab
• зависимый тип суммы в n Lab
• зависимый продукт в n Lab
• зависимая сумма в n Lab