В компьютерной науке и логике , зависимый тип является типом , определение которого зависит от значения. Это перекрывающаяся особенность теории типа и системы типа . В интуиционистской теории типов зависимые типы используются для кодирования таких логических кванторов, как «для всех» и «существует». В языках функционального программирования, таких как Agda , ATS , Coq , F * , Epigram и Idris., зависимые типы могут помочь уменьшить количество ошибок, позволяя программисту назначать типы, которые дополнительно ограничивают набор возможных реализаций.
Двумя распространенными примерами зависимых типов являются зависимые функции и зависимые пары. Тип возвращаемого значения зависимой функции может зависеть от значения (а не только типа) одного из ее аргументов. Например, функция, которая принимает положительное целое число может возвращать массив длины , где длина массива является частью типа массива. (Обратите внимание, что это отличается от полиморфизма и универсального программирования , оба из которых включают тип в качестве аргумента.) Зависимая пара может иметь второе значение, тип которого зависит от первого значения. Придерживаясь примера с массивом, зависимая пара может использоваться для связывания массива с его длиной безопасным для типов способом.
Зависимые типы усложняют систему типов. Определение равенства зависимых типов в программе может потребовать вычислений. Если в зависимых типах разрешены произвольные значения, тогда определение равенства типов может включать определение того, дают ли две произвольные программы одинаковый результат; следовательно, проверка типов может стать неразрешимой .
История
В 1934 году Хаскелл Карри заметил, что типы, используемые в типизированном лямбда-исчислении и в его аналоге комбинаторной логики , следуют той же схеме, что и аксиомы в логике высказываний . Далее, для каждого доказательства в логике существовала функция (термин) сопоставления на языке программирования. Одним из примеров Карри было соответствие между просто типизированным лямбда-исчислением и интуиционистской логикой . [1]
Логика предикатов - это расширение логики высказываний, добавляющее кванторы. Говард и де Брейн расширили лямбда-исчисление, чтобы соответствовать этой более мощной логике, создав типы для зависимых функций, которые соответствуют «для всех», и зависимых пар, которые соответствуют «существует». [2]
(Из-за этой и других работ Говарда пропозиции как типы известны как соответствие Карри – Ховарда .)
Формальное определение
Π тип
Грубо говоря, зависимые типы похожи на тип индексированного семейства множеств. Более формально, учитывая тип во вселенной типов , может быть семейство типов , который присваивает каждому термину тип . Мы говорим, что тип B (a) меняется с a .
Функция, тип возвращаемого значения которой зависит от ее аргумента (т.е. нет фиксированного кодомена ), является зависимой функцией, и тип этой функции называется зависимым типом продукта , пи-типом или зависимым типом функции . [3] Из семейства типов мы можем построить тип зависимых функций , чьи члены являются функциями, которые принимают член и вернуть срок в . В этом примере тип зависимой функции обычно записывается как или же
Если является постоянной функцией, соответствующий зависимый тип продукта эквивалентен обычному типу функции . Это, суждено равно когда B не зависит от x .
Название «пи-тип» происходит от идеи, что их можно рассматривать как декартово произведение типов. Pi-типа также можно понимать как модели из кванторов .
Например, если мы напишем для n наборов действительных чисел , тобудет типом функции, которая, учитывая натуральное число n , возвращает кортеж действительных чисел размера n . Обычное функциональное пространство возникает как частный случай, когда тип диапазона фактически не зависит от ввода. Например это тип функций от натуральных чисел до действительных чисел, который записывается как в типизированном лямбда-исчислении.
Для более конкретного примера, принимая равным семейству целых чисел без знака от 0 до 255, (те , которые вы может поместиться в 8 бит или 1 байт) и В (а) = Х для 256 произвольного Х «ы , тогдапревращается в произведение X 0 × X 1 × X 2 × ... × X 253 × X 254 × X 255 именно потому, что конечный набор целых чисел от 0 до 255 в конечном итоге остановится на только что упомянутых границах, что приведет к конечному codomain зависимой функции.
Σ тип
Двойное зависимого типа продукта является зависимым типом пары , зависит от типа суммы , сигма-тип , или (смешения) зависит от типа продукта . [3] Сигма-типы также можно понимать как кванторы существования . Продолжая приведенный выше пример, если во вселенной типов, есть тип и семейство типов , то существует зависимый тип пары . (Альтернативные обозначения аналогичны обозначениям типов Π.)
Тип зависимой пары отражает идею упорядоченной пары, в которой тип второго члена зависит от значения первого. Если тогда а также . Если B - постоянная функция, то тип зависимой пары становится (оценочно равен) типом продукта , то есть обычным декартовым произведением.
В качестве более конкретного примера возьмем A снова равным семейству беззнаковых целых чисел от 0 до 255, а B (a) снова равным X a для еще 256 произвольных X a , тогдапревращается в сумму X 0 + X 1 + X 2 + ... + X 253 + X 254 + X 255 по тем же причинам, что и то, что произошло с кодоменом зависимой функции.
Пример как экзистенциальная количественная оценка
Позволять быть каким-то типом, и пусть . По переписке Карри-Говарда , Б можно интерпретировать как логический предикат на условиях А . Для данного, является ли тип B (a) обитаемым, указывает, удовлетворяет ли a этому предикату. Соответствие может быть расширено до экзистенциальной квантификации и зависимых пар: утверждениеистинно тогда и только тогда, когда тип заселен.
Например, меньше или равно тогда и только тогда, когда существует другое натуральное число такое, что m + k = n . В логике это утверждение кодифицируется экзистенциальной количественной оценкой:
Системы лямбда-куба
Хенк Барендрегт разработал лямбда-куб как средство классификации систем типов по трем осям. Каждый из восьми углов полученной кубической диаграммы соответствует системе типов с простым типизированным лямбда-исчислением в наименее выразительном углу и исчислением конструкций в наиболее выразительном. Три оси куба соответствуют трем различным дополнениям простого типизированного лямбда-исчисления: добавлению зависимых типов, добавлению полиморфизма и добавлению конструкторов типов с более высоким родом (например, функций от типов к типам). Лямбда-куб далее обобщается системами чистых типов .
Теория зависимых типов первого порядка
Система чистых зависимых типов первого порядка, соответствующих логической структуре LF , получается путем обобщения типа функционального пространства просто типизированного лямбда-исчисления на зависимый тип продукта.
Теория зависимых типов второго порядка
Система зависимых типов второго порядка получается из позволяя количественную оценку конструкторов типов. В этой теории оператор зависимого произведения включает в себя как оператор просто типизированного лямбда-исчисления и Связующая System F .
Полиморфное лямбда-исчисление высшего порядка с зависимым типом
Система высшего порядка расширяет ко всем четырем формам абстракции от лямбда-куба : функции от терминов к терминам, типы к типам, термины к типам и типы к терминам. Система соответствует исчислению конструкций , производная которых, исчисление индуктивных построений, является базовой системой помощника доказательства Coq .
Синхронный язык программирования и логика
Соответствие Карри – Ховарда подразумевает, что можно сконструировать типы, которые выражают произвольно сложные математические свойства. Если пользователь может предоставить конструктивное доказательство того, что тип является обитаемым (то есть, что значение этого типа существует), то компилятор может проверить доказательство и преобразовать его в исполняемый компьютерный код, который вычисляет значение, выполняя построение. Функция проверки проверки делает языки с зависимой типизацией тесно связанными с помощниками проверки . Аспект генерации кода обеспечивает мощный подход к формальной проверке программ и коду , несущему доказательство , поскольку код является производным непосредственно из механически проверенного математического доказательства.
Сравнение языков с зависимыми типами
Язык | Активно развивается | Парадигма [fn 1] | Тактика | Условия доказательства | Проверка прекращения | Типы могут зависеть от [fn 2] | Вселенные | Доказательство несоответствия | Извлечение программы | При извлечении удаляются нерелевантные термины |
---|---|---|---|---|---|---|---|---|---|---|
Ада 2012 | Да [4] | Императив | Да [5] | Да (необязательно) [6] | ? | Любой термин [fn 3] | ? | ? | Ада | ? |
Агда | Да [7] | Чисто функциональный | Мало / ограничено [fn 4] | да | Да (необязательно) | Любой срок | Да (необязательно) [fn 5] | Аргументы, не относящиеся к доказательству [9] Утверждения, не относящиеся к доказательству [10] | Haskell , JavaScript | Да [9] |
АТС | Да [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 . Цитировать журнал требует
|journal=
( помощь ) - ^ Бове, Ана; Питер Дибьер (2008). «Зависимые типы в действии» (PDF) . Цитировать журнал требует
|journal=
( помощь ) - ^ а б «ΠΣ: зависимые типы без сахара» (PDF) .
- ^ "Страница загрузки сообщества GNAT" .
- ^ «Предикаты подтипа RM3.2.4» .
- ^ SPARK - доказуемое подмножество Ada
- ^ "Страница загрузки Агды" .
- ^ "Agda Ring Solver" .
- ^ а б «Анонс: 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» .
- ^ «Гуру СВН» .
- ^ а б Аарон Стамп (6 апреля 2009 г.). «Проверенное программирование в гуру» (PDF) . Архивировано из оригинального (PDF) 29 декабря 2009 года . Проверено 28 сентября 2010 года .
- ^ Адам Петчер (1 апреля 2008 г.). «Решение объединяемости по модулю основных уравнений в теории операционных типов» (PDF) . Проверено 14 октября 2010 года .
- ^ "Репозиторий Idris git" .
- ^ «Идрис, язык с зависимыми типами - расширенная аннотация» (PDF) . Архивировано из оригинального (PDF) 16 июля 2011 года.
- ^ а б Эдвин Брэди. «Чем отличается Идрис от других языков программирования с зависимой типизацией?» .
- ^ «Матита СВН» . Архивировано из оригинала на 2006-05-08 . Проверено 29 сентября 2010 .
- ^ "Домашняя страница Занаду" .
дальнейшее чтение
- Мартин-Лёф, Пер (1984). Интуиционистская теория типов (PDF) . Bibliopolis.
- Нордстрём, Бенгт ; Петерссон, Кент; Смит, Ян М. (1990). Программирование в теории типов Мартина-Лёфа: введение . Издательство Оксфордского университета. ISBN 9780198538141.
- Барендрегт, Х. (1992). «Лямбда-исчисления с типами» . По Абрамскому, С .; Gabbay, D .; Майбаум, Т. (ред.). Справочник по логике в компьютерных науках . Оксфордские научные публикации .
- Макбрайд, Конор ; МакКинна, Джеймс (январь 2004 г.). «Вид слева» . Журнал функционального программирования . 14 (1): 69–111. DOI : 10.1017 / s0956796803004829 .
- Альтенкирх, Торстен ; Макбрайд, Конор ; МакКинна, Джеймс (апрель 2005 г.). «Почему важны зависимые типы» (PDF) . Цитировать журнал требует
|journal=
( помощь ) - Норелл, Ульф (сентябрь 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