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

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

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

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

История

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

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

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

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

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

Тип П

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

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

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

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

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

Тип Σ

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

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

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

Пример как экзистенциальная квантификация

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Сравнение языков с зависимыми типами

^ Это относится к основному языку, а не к какой-либо тактике ( процедуре доказательства теорем ) или подъязыку генерации кода.
^ С учетом семантических ограничений, таких как ограничения вселенной.
^ Static_Predicate для ограниченных терминов, Dynamic_Predicate для проверки любого термина в приведении типа по типу Assert
^ Решатель колец ^[8]
^ Необязательные вселенные, необязательный полиморфизм юниверсов и необязательные явно указанные вселенные
^ Вселенные, автоматически выведенные ограничения вселенной (не то же самое, что полиморфизм вселенной Agda) и необязательная явная печать ограничений вселенной
^ Был заменен на ATS
^ Последняя статья Sage и последний снимок кода датированы 2006 годом.
^ Static_Predicate для ограниченных терминов, Dynamic_Predicate для проверки любого термина в приведении типа по типу Assert

Смотрите также

Ссылки

^ Хофманн, Мартин (1995), Экстенсиональные концепции в теории интенсиональных типов (PDF)
^ Сёренсен, Мортен Хайне Б.; Ужичин, Павел (1998), Лекции об изоморфизме Карри-Ховарда , CiteSeerX 10.1.1.17.7385
^ Бове, Ана; Дибьер, Питер (2008). Зависимые типы на работе (PDF) (Отчет). Технологический университет Чалмерса.
^ abc Altenkirch, Thorsten; Danielsson, Nils Anders; Löh, Andres; Oury, Nicolas (2010). "ΠΣ: Зависимые типы без сахара" (PDF) . В Blume, Matthias; Kobayashi, Naoki; Vidal, German (ред.). Функциональное и логическое программирование, 10-й международный симпозиум, FLOPS 2010, Сендай, Япония, 19–21 апреля 2010 г. Труды . Конспект лекций по информатике. Том 6009. Springer. стр. 40–55. doi :10.1007/978-3-642-12251-4_5.
^ «Установка GNAT Ada с использованием ALIRE» .
^ "§3.2.4 Предикаты подтипов". Справочное руководство по языку программирования Ada (редакция 2012 г.).
^ "Страница загрузки Agda".
^ "Agda Ring Solver".
^ ab "Объявление: Agda 2.2.8". Архивировано из оригинала 2011-07-18 . Получено 2010-09-28 .
^ "Журнал изменений Agda 2.6.0".
^ "ATS2 загрузки".
^ "электронное письмо от изобретателя ATS Хунвэя Си".
^ Си, Хунвэй (март 2017 г.). «Прикладная система типов: подход к практическому программированию с доказательством теорем» (PDF) . arXiv : 1703.08683 .
^ «Изменения Coq в репозитории Subversion».
^ «Введение SProp в Coq 8.10».
^ "F* изменения на GitHub". GitHub .
^ "Заметки о выпуске F* v0.9.5.0 на GitHub". GitHub .
^ «Гуру SVN».
^ ab Aaron Stump (6 апреля 2009 г.). "Verified Programming in Guru" (PDF) . Архивировано из оригинала (PDF) 29 декабря 2009 г. . Получено 28 сентября 2010 г. .
^ Petcher, Adam (май 2008). Решение стыкуемости по модулю основных уравнений в теории операциональных типов (PDF) (магистр наук). Вашингтонский университет . Получено 14 октября 2010 г.
^ "Idris git repository". GitHub . 17 мая 2022 г.
^ Брэди, Эдвин. «Идрис, язык с зависимыми типами — расширенная абстракция» (PDF) . CiteSeerX 10.1.1.150.9442 .
^ ab Брэди, Эдвин. «Как Idris соотносится с другими языками программирования с зависимой типизацией?».
^ "Matita SVN". Архивировано из оригинала 2006-05-08 . Получено 2010-09-29 .
^ "Установка SPARK с использованием ALIRE".
^ "§3.2.4 Предикаты подтипов". Справочное руководство по языку программирования Ada (редакция 2012 г.).
^ "5.11.6. Библиотека лемм SPARK". Руководство пользователя SPARK (25.0 ред.).
^ "5.2.8. Договоры о расторжении". Руководство пользователя SPARK (25.0 ред.).
^ "1.2. Вызов и использование CCG". Дополнение к руководству пользователя генератора общего кода GNAT Pro (ред. 25.0).
^ «Компиляция с помощью компилятора, не поддерживающего SPARK». Руководство пользователя SPARK (ред. 25.0).

Дальнейшее чтение

Мартин-Лёф, Пер (1984). Интуиционистская теория типов (PDF) . Библиополис.
Нордстрем, Бенгт; Петерссон, Кент; Смит, Ян М. (1990). Программирование в теории типов Мартина-Лёфа: введение. Издательство Оксфордского университета. ISBN 9780198538141.
Barendregt, H. (1992). "Лямбда-исчисления с типами". В Abramsky, S.; Gabbay, D.; Maibaum, T. (ред.). Справочник по логике в компьютерных науках . Oxford Science Publications . doi :10.1017/CBO9781139032636. hdl : 2066/17231 .
Брандл, Хельмут (2022). Исчисление конструкций
МакБрайд, Конор ; МакКинна, Джеймс (январь 2004 г.). «Взгляд слева». Журнал функционального программирования . 14 (1): 69–111. doi : 10.1017/s0956796803004829 . S2CID 6232997.
Альтенкирх, Торстен ; Макбрайд, Конор ; Маккинна, Джеймс (2006). "Почему зависимые типы имеют значение" (PDF) . Труды 33-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования, POPL 2006, Чарльстон, Южная Каролина, США, 11-13 января . ISBN 1-59593-027-2.
Норелл, Ульф (сентябрь 2007 г.). На пути к практическому языку программирования на основе теории зависимых типов (PDF) (PhD). Гетеборг, Швеция: Кафедра компьютерных наук и инжиниринга, Технологический университет Чалмерса. ISBN 978-91-7291-996-9.
Oury, Nicolas; Swierstra, Wouter (2008). "The Power of Pi" (PDF) . ICFP '08: Труды 13-й международной конференции ACM SIGPLAN по функциональному программированию . стр. 39–50. doi :10.1145/1411204.1411213. ISBN 9781595939197. S2CID 16176901.
Норелл, Ульф (2009). «Зависимо типизированное программирование в Agda» (PDF) . В Купмане, П.; Пласмейер, Р.; Свирстра, Д. (ред.). Продвинутое функциональное программирование. АФП 2008 . Конспекты лекций по информатике. Том. 5832. Спрингер. стр. 230–266. дои : 10.1007/978-3-642-04652-0_5. ISBN 978-3-642-04651-3.
Ситниковски, Боро (2018). Мягкое введение в зависимые типы с Идрисом . Бережливое издательское дело. ISBN 978-1723139413.
Макбрайд, Конор ; Нордвалл-Форсберг, Фредрик (2022). «Системы типов для программ, учитывающих измерения» (PDF) . Передовые математические и вычислительные инструменты в метрологии и испытаниях XII . Достижения в области математики для прикладных наук. World Scientific. стр. 331–345. doi :10.1142/9789811242380_0020. ISBN 9789811242380. S2CID 243831207.

Внешние ссылки

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