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

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

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

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

История [ править ]

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

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

(Благодаря этой и другим работам Ховарда предложения как типы известны как соответствие Карри-Ховарда .)

Формальное определение [ править ]

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

Тип P [ править ]

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

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

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

В качестве более конкретного примера возьмем $A$ как тип целых чисел без знака от 0 до 255 (те, которые умещаются в 8 бит или 1 байт) и $B (a) = X a$ для $a : A$ , тогда ${\textstyle \prod _{x:A}B(x)}$ превращается в произведение $X 0 \times X 1 \times X 2 \times ... \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)}$ . (Альтернативные обозначения аналогичны обозначениям $типов Π$ .)

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

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

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

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

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

m\leq n\iff \exists {k}{\in }\mathbb {N} \,m+k=n.

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

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

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

Системы лямбда-куба [ править ]

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

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

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

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

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

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

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

Язык одновременного программирования и логика [ править ]

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

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

Язык	Активно развивается	Парадигма ^[а]	Тактика	Условия доказательства	Проверка завершения	Типы могут зависеть от ^[б]	Вселенные	Доказательство неуместно	Извлечение программы	Извлечение стирает ненужные термины
Был 2012 год	Да ^[5]	Императив	Да ^[6]	Нет	?	Любой срок ^[с]	?	?	Есть	?
приглашенный	Да ^[7]	Чисто функциональный	Мало/ограничено ^[д]	Да	Да (необязательно)	Любой срок	Да (необязательно) ^[Это]	Аргументы, не имеющие значения для доказательства ^[9] Предложения, не имеющие отношения к доказательству ^[10]	Хаскелл , JavaScript	Да ^[9]
АТС	Да ^[11]	Функциональный/императивный	Нет ^[12]	Да	Да	Статические условия ^[13]	?	Да	Да	Да
Кайенна	Нет	Чисто функциональный	Нет	Да	Нет	Любой срок	Нет	Нет	?	?
Курица ( Кок )	Да ^[14]	Чисто функциональный	Да	Да	Да	Любой срок	Да ^[ф]	Да ^[15]	Haskell , Scheme и OCaml	Да
Зависимый ОД	Нет ^[г]	?	?	Да	?	Натуральные числа	?	?	?	?
Ф*	Да ^[16]	Функциональный и императивный	Да ^[17]	Да	Да (необязательно)	Любой чистый термин	Да	Да	OCaml , F# и C	Да
Учитель	Нет ^[18]	Чисто функциональный ^[19]	Гип-соединение ^[20]	Да ^[19]	Да	Любой срок	Нет	Да	Каррауэй	Да
Идрис	Да ^[21]	Чисто функциональный ^[22]	Да ^[23]	Да	Да (необязательно)	Любой срок	Да	Нет	Да	Да ^[23]
Наклонять	Да	Чисто функциональный	Да	Да	Да	Любой срок	Да	Да	Да	Да
Карандаш	Да ^[24]	Чисто функциональный	Да	Да	Да	Любой срок	Да	Да	OCaml	Да
НуПРЛ	Да	Чисто функциональный	Да	Да	Да	Любой срок	Да	?	Да	?
ПВС	Да	?	Да	?	?	?	?	?	?	?
Sage. Архивировано 9 ноября 2020 г. в Wayback Machine.	Нет ^[час]	Чисто функциональный	Нет	Нет	Нет	?	Нет	?	?	?
Двенадцать	Да	Логическое программирование	?	Да	Да (необязательно)	Любой (LF) термин	Нет	Нет	?	?

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

См. также [ править ]

Ссылки [ править ]

^ Хофманн, Мартин (1995), Экстенсиональные концепции в теории интенсиональных типов (PDF)
^ Соренсен, Мортен Хейне Б.; Уржичин, Павел (1998), Лекции по изоморфизму Карри-Ховарда , CiteSeerX 10.1.1.17.7385
^ Бове, Ана; Дибьер, Питер (2008), Зависимые типы на работе (PDF) , Технологический университет Чалмерса
^ Перейти обратно: ^а ^б ^с Альтенкирх, Торстен; Даниэльссон, Нильс Андерс; Лё, Андрес; Ури, Николя (2010). «ΠΣ: Зависимые типы без сахара» (PDF) . В Блюме, Матиас; Кобаяши, Наоки; Видаль, Герман (ред.). Функциональное и логическое программирование, 10-й Международный симпозиум, FLOPS 2010, Сендай, Япония, 19-21 апреля 2010 г. Труды . Конспекты лекций по информатике. Том. 6009. Спрингер. стр. 40–55. дои : 10.1007/978-3-642-12251-4_5 .
^ «Страница загрузки сообщества GNAT» .
^ «§3.2.4 Предикаты подтипа» . Справочное руководство по Ada (изд. 2012 г.).
^ «Страница загрузки Агда» .
^ «Решатель колец Агда» .
^ Перейти обратно: ^а ^б «Анонс: Агда 2.2.8» . Архивировано из оригинала 18 июля 2011 г. Проверено 28 сентября 2010 г.
^ «Журнал изменений Agda 2.6.0» .
^ «Загрузки ATS2» .
^ «электронное письмо от изобретателя ATS Хунвэя Си» .
^ Си Цзиньпин, Хунвэй (март 2017 г.). «Система прикладных типов: подход к практическому программированию с доказательством теорем» (PDF) . arXiv : 1703.08683 .
^ «ИЗМЕНЕНИЯ Coq в репозитории Subversion» .
^ «Внедрение SProp в Coq 8.10» .
^ «F* изменения на GitHub» . Гитхаб .
^ «Примечания к выпуску F* v0.9.5.0 на GitHub» . Гитхаб .
^ «Гуру СВН» .
^ Перейти обратно: ^а ^б Аарон Стамп (6 апреля 2009 г.). «Проверенное программирование в Guru» (PDF) . Архивировано из оригинала (PDF) 29 декабря 2009 года . Проверено 28 сентября 2010 г.
^ Петчер, Адам (май 2008 г.). Решение основных уравнений соединяемости по модулю в теории операционных типов (PDF) (MSc). Вашингтонский университет . Проверено 14 октября 2010 г.
^ «Гит-репозиторий Идриса» . Гитхаб . 17 мая 2022 г.
^ Брэди, Эдвин. «Идрис, язык с зависимыми типами — расширенная аннотация» (PDF) . CiteSeerX 10.1.1.150.9442 .
^ Перейти обратно: ^а ^б Брэди, Эдвин. «Чем Idris отличается от других языков программирования с зависимой типизацией?» .
^ «Матита СВН» . Архивировано из оригинала 8 мая 2006 г. Проверено 29 сентября 2010 г.

Дальнейшее чтение [ править ]

Мартин-Лёф, Пер (1984). Интуиционистская теория типов (PDF) . Библиополис.
Нордстрем, Бенгт ; Петерссон, Кент; Смит, Ян М. (1990). Программирование в теории типов Мартина-Лёфа: введение . Издательство Оксфордского университета. ISBN 9780198538141 .
Барендрегт, Х. (1992). «Лямбда-исчисления с типами» . В Абрамский С.; Габбай, Д.; Майбаум, Т. (ред.). Справочник по логике в информатике . Оксфордские научные публикации . дои : 10.1017/CBO9781139032636 . hdl : 2066/17231 .
Брандл, Хельмут (2022). Расчет конструкций
Макбрайд, Конор ; Маккинна, Джеймс (январь 2004 г.). «Взгляд слева» . Журнал функционального программирования . 14 (1): 69–111. дои : 10.1017/s0956796803004829 . S2CID 6232997 .
Альтенкирх, Торстен ; Макбрайд, Конор ; Маккинна, Джеймс (2006). «Почему зависимые типы имеют значение» (PDF) . Материалы 33-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования, POPL 2006, Чарльстон, Южная Каролина, США, 11-13 января . ISBN 1-59593-027-2 .
Норелл, Ульф (сентябрь 2007 г.). На пути к практическому языку программирования, основанному на теории зависимых типов (PDF) (доктор философии). Гетеборг, Швеция: Факультет компьютерных наук и инженерии Технологического университета Чалмерса. ISBN 978-91-7291-996-9 .
Ури, Николя; Свирстра, Воутер (2008). «Сила Пи» (PDF) . ICFP '08: Материалы 13-й международной конференции ACM SIGPLAN по функциональному программированию . стр. 39–50. дои : 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 . Достижения математики для прикладных наук. Всемирная научная. стр. 331–345. дои : 10.1142/9789811242380_0020 . ISBN 9789811242380 . S2CID 243831207 .

Внешние ссылки [ править ]

[5] Это относится к основному доказательства теорем языку, а не к какой-либо тактике ( процедуре ) или подъязыку генерации кода.

[6] С учетом семантических ограничений, таких как ограничения юниверса.

[9] Static_Predicate для ограниченных терминов, Dynamic_Predicate для проверки любого термина при приведении типа в стиле Assert.

[12] Решатель колец ^[8]

[13] Необязательные юниверсы, необязательный полиморфизм юниверсов и необязательные явно указанные юниверсы.

[20] Вселенные, автоматически выведенные ограничения юниверсов (не то же самое, что полиморфизм юниверсов Agda) и необязательная явная печать ограничений юниверсов.

[22] Был заменен ATS.

[32] Последняя статья Sage и последний снимок кода датированы 2006 годом.

[extensional-1] Хофманн, Мартин (1995), Экстенсиональные концепции в теории интенсиональных типов (PDF)

[curry_howard-2] Соренсен, Мортен Хейне Б.; Уржичин, Павел (1998), Лекции по изоморфизму Карри-Ховарда , CiteSeerX 10.1.1.17.7385

[dep_types_at_work-3] Бове, Ана; Дибьер, Питер (2008), Зависимые типы на работе (PDF) , Технологический университет Чалмерса

[without-sugar-4] Перейти обратно: ^а ^б ^с Альтенкирх, Торстен; Даниэльссон, Нильс Андерс; Лё, Андрес; Ури, Николя (2010). «ΠΣ: Зависимые типы без сахара» (PDF) . В Блюме, Матиас; Кобаяши, Наоки; Видаль, Герман (ред.). Функциональное и логическое программирование, 10-й Международный симпозиум, FLOPS 2010, Сендай, Япония, 19-21 апреля 2010 г. Труды . Конспекты лекций по информатике. Том. 6009. Спрингер. стр. 40–55. дои : 10.1007/978-3-642-12251-4_5 .

[7] «Страница загрузки сообщества GNAT» .

[8] «§3.2.4 Предикаты подтипа» . Справочное руководство по Ada (изд. 2012 г.).

[10] «Страница загрузки Агда» .

[11] «Решатель колец Агда» .

[agda-2.2.8-14] Перейти обратно: ^а ^б «Анонс: Агда 2.2.8» . Архивировано из оригинала 18 июля 2011 г. Проверено 28 сентября 2010 г.

[15] «Журнал изменений Agda 2.6.0» .

[16] «Загрузки ATS2» .

[17] «электронное письмо от изобретателя ATS Хунвэя Си» .

[18] Си Цзиньпин, Хунвэй (март 2017 г.). «Система прикладных типов: подход к практическому программированию с доказательством теорем» (PDF) . arXiv : 1703.08683 .

[19] «ИЗМЕНЕНИЯ Coq в репозитории Subversion» .

[21] «Внедрение SProp в Coq 8.10» .

[23] «F* изменения на GitHub» . Гитхаб .

[24] «Примечания к выпуску F* v0.9.5.0 на GitHub» . Гитхаб .

[25] «Гуру СВН» .

[guru-book-26] Перейти обратно: ^а ^б Аарон Стамп (6 апреля 2009 г.). «Проверенное программирование в Guru» (PDF) . Архивировано из оригинала (PDF) 29 декабря 2009 года . Проверено 28 сентября 2010 г.

[hypjoin-paper-27] Петчер, Адам (май 2008 г.). Решение основных уравнений соединяемости по модулю в теории операционных типов (PDF) (MSc). Вашингтонский университет . Проверено 14 октября 2010 г.

[28] «Гит-репозиторий Идриса» . Гитхаб . 17 мая 2022 г.

[29] Брэди, Эдвин. «Идрис, язык с зависимыми типами — расширенная аннотация» (PDF) . CiteSeerX 10.1.1.150.9442 .

[idris-compare-30] Перейти обратно: ^а ^б Брэди, Эдвин. «Чем Idris отличается от других языков программирования с зависимой типизацией?» .

[31] «Матита СВН» . Архивировано из оригинала 8 мая 2006 г. Проверено 29 сентября 2010 г.

[1]

[2]

[3]

[4]

[а]

[б]

[5]

[6]

[с]

[7]

[д]

[Это]

[9]

[10]

[11]

[12]

[13]

[14]

[ф]

[15]

[г]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[час]

[8]

v т Это Основные темы Основ математики
Математическая логика	Аксиомы Пеано Математическая индукция Формальная система Аксиоматическая система система Гильберта Естественный вычет Математическое доказательство Теория моделей Математический конструктивизм Модальная логика Список тем математической логики
Теория множеств	Набор Наивная теория множеств Аксиоматическая теория множеств Теория множеств Цермело Теория множеств Цермело – Френкеля Конструктивная теория множеств Описательная теория множеств Определенность Парадокс Рассела Список тем теории множеств
Теория типов	Аксиома сводимости Простая теория типов Теория зависимых типов Интуиционистская теория типов Теория гомотопических типов Одновалентные фундаменты Парадокс Жирара
Теория категорий	Категория Теория топоса Категория наборов Теория высших категорий ∞-группоид теория ∞-топоса Математический структурализм Глоссарий теории категорий Список тем теории категорий