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

Системы типов
Общие понятия
Безопасность типов
Основные категории
Статический против динамического Манифест против предполагаемого Номинальные и структурные Утка печатает
Второстепенные категории
Зависимый Чувствительный к потоку Постепенный Пересечение Скрытый Уточнение Субструктурный Уникальный Абстрактный
Смотрите также
Сильный и слабый набор текста

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

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

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

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

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

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

(Из-за этой и других работ Говарда пропозиции как типы известны как соответствие Карри – Ховарда .)

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

${\ displaystyle \ Pi}$ тип [ редактировать ]

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

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

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

Например, если мы напишем для 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}$

$\Sigma$ тип [ редактировать ]

Двойное зависимого типа продукта является зависимым типом пары , зависит от типа суммы , сигма-тип , или (смешения) зависит от типа продукта . ^[3] Сигма-типы также можно понимать как кванторы существования . Продолжая приведенный выше пример, если во вселенной типов есть тип и семейство типов , то существует зависимый тип пары. ${\mathcal {U}}$ $A:{\mathcal {U}}$ $B:A\to {\mathcal {U}}$

\sum _{x:A}B(x).

Тип зависимой пары отражает идею упорядоченной пары, в которой тип второго члена зависит от значения первого. Если

(a,b):\sum _{x:A}B(x),

потом и . Если B - постоянная функция, то тип зависимой пары становится (по оценкам равен) типом продукта , то есть обычным декартовым произведением .

a:A

b:B(a)

A\times B

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

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

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

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

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

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

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

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

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

Полиморфное лямбда-исчисление с зависимым типом более высокого порядка [ править ]

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

Синхронный язык программирования и логика [ править ]

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

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

Язык	Активно развивается	Парадигма ^{[fn 1]}	Тактика	Условия доказательства	Проверка прекращения	Типы могут зависеть от ^{[fn 2]}	Вселенные	Доказательство несоответствия	Извлечение программы	Извлечение удаляет нерелевантные термины
Ада 2012	Да ^[4]	Императив	Да ^[5]	Да (необязательно) ^[6]	?	Любой термин ^{[fn 3]}	?	?	Ада	?
Агда	Да ^[7]	Чисто функциональный	Мало / ограничено ^{[fn 4]}	да	Да (необязательно)	Любой срок	Да (необязательно) ^{[fn 5]}	Аргументы, не относящиеся к доказательству ^[9] Утверждения, не относящиеся к доказательству ^[10]	Haskell , JavaScript	Да ^[9]
ATS	Да ^[11]	Функциональный / императивный	Нет ^[12]	да	да	Статические термины ^[13]	?	да	да	да
Cayenne	Нет	Чисто функциональный	Нет	да	Нет	Любой срок	Нет	Нет	?	?
Галлина ( Coq )	Да ^[14]	Чисто функциональный	да	да	да	Любой срок	Да ^{[fn 6]}	Нет	Haskell , Scheme и OCaml	да
Зависимый ML	Нет ^{[fn 7]}	?	?	да	?	Натуральные числа	?	?	?	?
F *	Да ^[15]	Функциональный и императивный	Да ^[16]	да	Да (необязательно)	Любой чистый термин	да	да	OCaml , F # и C	да
Гуру	Нет ^[17]	Чисто функциональный ^[18]	hypjoin ^[19]	Да ^[18]	да	Любой срок	Нет	да	Carraway	да
Идрис	Да ^[20]	Чисто функциональный ^[21]	Да ^[22]	да	Да (необязательно)	Любой срок	да	Нет	да	Да, агрессивно ^[22]
Худой	да	Чисто функциональный	да	да	да	Любой срок	да	да	да	да
Матита	Да ^[23]	Чисто функциональный	да	да	да	Любой срок	да	да	OCaml	да
NuPRL	да	Чисто функциональный	да	да	да	Любой срок	да	?	да	?
ПВС	да	?	да	?	?	?	?	?	?	?
мудрец	Нет ^{[fn 8]}	Чисто функциональный	Нет	Нет	Нет	?	Нет	?	?	?
Двенадцать	да	Логическое программирование	?	да	Да (необязательно)	Любой (LF) термин	Нет	Нет	?	?
Занаду	Нет ^[24]	Императив	?	?	?	?	?	?	?	?

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

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

Сноски [ править ]

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

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

^ Соренсен, Мортен Хайне Б .; Павел Уржичин (1998). "Лекции об изоморфизме Карри-Ховарда". CiteSeerX 10.1.1.17.7385 . Cite journal requires |journal= (help)
^ Бове, Ана; Питер Дибьер (2008). «Зависимые типы в действии» (PDF) . Cite journal requires |journal= (help)
^ a b «ΠΣ: зависимые типы без сахара» (PDF) .
^ "Страница загрузки сообщества GNAT" .
^ «Предикаты подтипа RM3.2.4» .
^ SPARK - это доказуемое подмножество Ada
^ "Страница загрузки Агды" .
^ "Agda Ring Solver" .
^ a b "Объявление: Agda 2.2.8" . Архивировано из оригинала на 2011-07-18 . Проверено 28 сентября 2010 .
^ "Список изменений Agda 2.6.0" .
^ "Загрузки ATS2" .
^ "электронное письмо от изобретателя ATS Хунвэй Си" .
^ "Прикладная система типов: подход к практическому программированию с доказательством теорем" (PDF) .
^ "Coq ИЗМЕНЕНИЯ в репозитории Subversion" .
^ "F * изменения на GitHub" .
^ "Примечания к выпуску F * v0.9.5.0 на GitHub" .
^ "Гуру СВН" .
^ a b Аарон Стамп (6 апреля 2009 г.). «Проверенное программирование в гуру» (PDF) . Архивировано из оригинального (PDF) 29 декабря 2009 года . Проверено 28 сентября 2010 года .
^ Адам Petcher (1 апреля 2008). "Решение объединяемости по модулю основных уравнений в теории операционных типов" (PDF) . Проверено 14 октября 2010 года .
^ "Репозиторий Idris git" .
^ «Идрис, язык с зависимыми типами - расширенная аннотация» (PDF) . Архивировано из оригинального (PDF) 16 июля 2011 года.
^ а б Эдвин Брэди. «Чем отличается Идрис от других языков программирования с зависимой типизацией?» .
^ "Матита СВН" . Архивировано из оригинала на 2006-05-08 . Проверено 29 сентября 2010 .
^ "Домашняя страница Xanadu" .

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

Мартин-Лёф, Пер (1984). Интуиционистская теория типов (PDF) . Bibliopolis.
Нордстрём, Бенгт ; Петерссон, Кент; Смит, Ян М. (1990). Программирование в теории типов Мартина-Лёфа: введение . Издательство Оксфордского университета. ISBN 9780198538141.
Барендрегт, Х. (1992). «Лямбда-исчисления с типами» . По Абрамскому, С .; Gabbay, D .; Майбаум, Т. (ред.). Справочник по логике в компьютерных науках . Оксфордские научные публикации .
Макбрайд, Конор ; МакКинна, Джеймс (январь 2004 г.). «Вид слева» . Журнал функционального программирования . 14 (1): 69–111. DOI : 10.1017 / s0956796803004829 .
Альтенкирх, Торстен ; Макбрайд, Конор ; МакКинна, Джеймс (апрель 2005 г.). «Почему важны зависимые типы» (PDF) . Cite journal requires |journal= (help)
Норелл, Ульф (сентябрь 2007 г.). На пути к практическому языку программирования, основанному на теории зависимых типов (PDF) (PhD). Гётеборг, Швеция: Департамент компьютерных наук и инженерии, Технологический университет Чалмерса. ISBN 978-91-7291-996-9.
Ури, Николас; Свиерстра, Воутер (2008). «Сила Пи» (PDF) . ICFP '08: Материалы 13-й международной конференции ACM SIGPLAN по функциональному программированию . С. 39–50. DOI : 10.1145 / 1411204.1411213 . ISBN 9781595939197.
Норелл, Ульф (2009). «Зависимо типизированное программирование в Agda» (PDF) . В Koopman, P .; Plasmeijer, R .; Свиерстра, Д. (ред.). Расширенное функциональное программирование. AFP 2008 . Конспект лекций по информатике. 5832 . Springer. С. 230–266. DOI : 10.1007 / 978-3-642-04652-0_5 . ISBN 978-3-642-04651-3.
Ситниковский, Боро (2018). Нежное введение в зависимые типы с помощью Idris . Бережливое издательство. ISBN 978-1723139413.

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

Зависимо типизированное программирование 2008
Зависимо типизированное программирование 2010
Зависимо типизированное программирование 2011
"Зависимый тип" в Haskell Wiki
теория зависимых типов в nLab
зависимый тип в nLab
зависимый тип продукта в nLab
тип зависимой суммы в nLab
зависимый продукт в nLab
зависимая сумма в nLab

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

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

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

[12] Программа расчета колец^[8]

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

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

[21] Заменено ATS

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

[curry_howard-1] Соренсен, Мортен Хайне Б .; Павел Уржичин (1998). "Лекции об изоморфизме Карри-Ховарда". CiteSeerX 10.1.1.17.7385 . Cite journal requires |journal= (help)

[dep_types_at_work-2] Бове, Ана; Питер Дибьер (2008). «Зависимые типы в действии» (PDF) . Cite journal requires |journal= (help)

[without-sugar-3] «ΠΣ: зависимые типы без сахара» (PDF) .

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

[7] «Предикаты подтипа RM3.2.4» .

[8] SPARK - это доказуемое подмножество Ada

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

[11] "Agda Ring Solver" .

[agda-2.2.8-14] "Объявление: Agda 2.2.8" . Архивировано из оригинала на 2011-07-18 . Проверено 28 сентября 2010 .

[15] "Список изменений Agda 2.6.0" .

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

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

[18] "Прикладная система типов: подход к практическому программированию с доказательством теорем" (PDF) .

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

[22] "F * изменения на GitHub" .

[23] "Примечания к выпуску F * v0.9.5.0 на GitHub" .

[24] "Гуру СВН" .

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

[hypjoin-paper-26] Адам Petcher (1 апреля 2008). "Решение объединяемости по модулю основных уравнений в теории операционных типов" (PDF) . Проверено 14 октября 2010 года .

[27] "Репозиторий Idris git" .

[28] «Идрис, язык с зависимыми типами - расширенная аннотация» (PDF) . Архивировано из оригинального (PDF) 16 июля 2011 года.

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

[30] "Матита СВН" . Архивировано из оригинала на 2006-05-08 . Проверено 29 сентября 2010 .

[32] "Домашняя страница Xanadu" .

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