Зависимые типы против типов уточнения

Может ли кто-нибудь объяснить разницу между зависимыми типами и типами уточнения? Насколько я понимаю, тип уточнения содержит все значения типа, выполняющего предикат. Есть ли особенность зависимых типов, которая их отличает?

Если это поможет, я натолкнулся на уточненные типы через проект Liquid Haskell и зависимые типы через Coq и Agda. Тем не менее, я ищу объяснение того, как теории отличаются.

terminology programming-languages type-theory functional-programming dependent-types jmite
источник

Ответы:

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

Как пользователь, «логика» спецификаций в системах LiquidHaskell и типах уточнения в целом ограничена разрешимыми фрагментами, так что проверка (и вывод) полностью автоматическая, то есть не требуется «проверочных терминов» того типа, который необходим в полном объеме. зависимая настройка. Это приводит к значительной автоматизации. Например, сравните сортировку вставки в LH:

http://ucsd-progsys.github.io/lh-workshop/04-case-study-insertsort.html#/ordered-lists

против в Идрисе

https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr

Однако автоматизация имеет свою цену. Нельзя использовать произвольные функции в качестве спецификаций, как можно в полностью зависимом мире, что ограничивает класс свойств, которые можно написать.

Таким образом, одна цель систем уточнения состоит в том, чтобы расширить класс того, что может быть указано, а класс полностью зависимых систем - автоматизировать то, что может быть доказано. Возможно, есть счастливое место встречи, где мы можем получить лучшее из обоих миров!

Ранджит Джхала
источник

Есть ли способ каким-то образом механически отобразить спецификацию на основе уточняющего типа в спецификацию на основе зависимого типа? Или такой «изоморфизм» еще недостаточно изучен?

Эрик Аллик

AFAIK такой «изоморфизм» мало изучен. Хотя есть некоторые недавние работы, см .: «Формализация простых типов уточнения в Coq» Лемана и Тантера (которые скоро появятся ... вот

репозиторий

Как насчет зависимых от пути типов в Scala?

Ян Бо

@RanjitJhala Я думаю, вы случайно ошиблись в последнем параграфе своих целей?

Нолдорин

@ Noldorin Я бы сказал, что Ранджит правильно понял свой последний абзац. "тип уточнения ... ограничен разрешаемыми фрагментами, так что проверка (и вывод) полностью автоматическая" против "проверочных терминов ... необходимых в ... зависимых [типах]". Таким образом, люди, работающие с уточняющими типами, пытаются расширить, сколько можно указать в уточняющем типе, и в то же время автоматически распознавать / проверять, в то время как те, кто работает с зависимыми типами, пытаются автоматизировать создание проверочных терминов.

Райф

$T$ $P$ $T$

{v : T ∣ P (v)}

$\{v:T \mid P(v)\}$

T

$T$

$\{x:T_1 \to T_2 \mid P\}$

Система Liquid Type, описанная в [1], действительно разрешима, и Liquid Haskell действительно использует решатели SMT. Однако для Liquid Haskell также требуются проверочные термины (или значения, так как они вызываются на языке с независимой типизацией): если вы садитесь за написание программы на Liquid Haskell, вы пишете свои собственные функции, а не только типы.

[1] http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf

Daniil
источник

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

fread2281

Зависимые типы - это типы, которые в любом случае зависят от значений. Классическим примером является «тип векторов длины n», где nэто значение. Типы уточнения, как вы говорите в вопросе, состоят из всех значений данного типа, которые удовлетворяют данному предикату. Например, тип положительных чисел. Эти понятия не особенно связаны (что я знаю). Конечно, вы также можете разумно иметь зависимые типы уточнения, такие как «тип всех чисел больше чем n».

Алексей романов
источник

Является ли одно подмножеством другого? Типы уточнения кажутся решаемыми с помощью SMT, но зависимые типы требуют ваших собственных

проверочных

"Является ли одно подмножеством другого?" Нет. Вот почему я привел примеры уточняющего типа, который не является зависимым, и зависимого типа, который не является уточнением.

Алексей Романов

типы уточнения не могут быть закодированы с сигмой?

fread2281

Ваш пример, кажется, не демонстрирует вашу точку зрения. Положительные числа определяются как числа, превышающие 0. Не означает ли это, что «тип положительных чисел» в точности является «типом всех чисел, превышающих 0»?

akdom

Разве не возможно, чтобы существовал уточняющий предикат, который также обеспечивает длину вектора?

CMCDragonkai