Отношения между контрактами и зависимой типизацией

31

Я читал несколько статей о зависимых типах и контрактах программирования. Из большей части того, что я прочитал, кажется, что контракты - это динамически проверяемые ограничения, а зависимые типы проверяются статически.

Были некоторые бумаги, которые заставили меня думать, что возможно иметь контракты, которые частично проверяются статически:

При этом, похоже, происходит значительное совпадение, и моя категоризация контрактов и зависимых типов начинает исчезать.

Есть ли что-то более глубокое в этих концепциях, которые я пропускаю? Или это действительно просто нечеткие категории, представляющие одну и ту же концепцию?

Брайан МакКенна
источник

Ответы:

26

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

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

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

Эти два взгляда не совпадают, но они связаны между собой. По сути, дело в том, что с контрактами мы начинаем с универсальной области ценностей и используем контракты, чтобы сократить расходы. Но когда мы используем типы, мы стараемся указывать меньшие домены значений (с желаемым свойством) заранее. Таким образом, мы можем связать их с помощью типо-ориентированных семейств отношений (т. Е. Логических отношений). Например, см. Недавнюю «Вину за все» Ахмеда, Финдлера, Зика и Вадлера или «Значение типов Рейнольдсом : от внутренней до внешней семантики» .

Нил Кришнасвами
источник
Почему вы говорите, что контракты не содержат квантификаторов?
Раду GRIGore
3
Потому что вы обычно не можете использовать тесты для определения универсально количественных свойств функций, вот и все.
Нил Кришнасвами
3
Если квантификаторы не распространяются на конечные области, в этом случае их можно рассматривать как большие союзы и дизъюнкции. Или, если вы хотите получить фантазию, вы можете проверить определенные виды количественных выражений, при условии, что квантиры располагаются по доступным для поиска типам Мартина Эскардо (которые могут быть бесконечными).
Андрей Бауэр
2
@Radu: Я называю такие вещи, как JML & co "программной логикой". Языки утверждений программной логики не ограничиваются тем, чтобы быть терминами из языка программ. Это позволяет вам исключить такие вещи, как недопустимые или побочные утверждения, которые не имеют хорошей логической интерпретации. (Тем не менее, такие вещи имеют значение для проверки контракта - см. Недавнюю работу Пучеллы и Туве в ESOP по использованию императивных контрактов с отслеживанием состояния для отслеживания свойств линейности.)
Нил Кришнасвами
2
Это потому, что я неправильно ввел фамилию Тов. См. «Контракты с контролем
Нил Кришнасвами,
13

(Довольно абстрактная) проблема, с которой сталкиваются как типы, так и контракты: «Как обеспечить, чтобы программы имели определенные свойства?». Здесь существует внутреннее противоречие между способностью выражать более широкий класс свойств и способностью проверять, есть ли у программы свойство или нет. Системы типов обычно обеспечивают очень специфическое свойство (программа никогда не дает сбой определенным образом) и имеют алгоритм проверки типов. С другой стороны, контракты позволяют вам указывать очень широкий диапазон свойств (скажем, вывод этой программы - простое число), но не поставляются с алгоритмом проверки.

Тем не менее, тот факт, что нет алгоритма проверки контракта (который всегда работает), не означает, что почти нет алгоритмов проверки контракта (которые имеют тенденцию работать на практике). Я бы порекомендовал вам взглянуть на Spec # и плагин Jessie Frama-C . Они оба работают, выражая «эта программа подчиняется этому контракту» как оператор в логике первого порядка посредством генерации условия проверки , а затем запрашивая SMTРешатель, чтобы пойти попытаться найти доказательство. Если решающему не удается найти доказательство, то либо программа неверна, либо, ну, решатель не смог найти существующее доказательство. (Вот почему это «почти» алгоритм проверки контракта.) Существуют также инструменты, основанные на символическом выполнении, что примерно означает, что «эта программа подчиняется этому контракту» выражается в виде набора предложений (в некоторой логике). Смотрите, например, jStar .

Работа Фланагана пытается извлечь лучшее из обоих миров таким образом, чтобы вы могли быстро проверить типичные свойства и затем потрудиться на отдых. Я не очень знаком с гибридными типами, но я помню, как автор говорил, что его мотивом было придумать решение, которое требует меньше аннотаций (чем его предыдущая работа над ESC / Java). В некотором смысле, однако, существует некоторая слабая интеграция между типами и контрактами и в ESC / Java (и в Spec #): при проверке контрактов решателю сообщается, что проверка типов прошла успешно, поэтому он может получить эту информацию.

Раду ГРИГОРЕ
источник
7

Контракты могут быть проверены статически. Если вы посмотрите на старую работу Даны Сюй по ESC / Haskell , она смогла осуществить полную проверку контракта во время компиляции, полагаясь только на доказательство теорем для арифметики. Прекращение решается простым пределом глубины, если я правильно помню:

Лиам О'Коннор
источник
6

И контракты, и типы позволяют вам представлять спецификации Hoare-стиля (до / после условия) для функций. Оба могут быть проверены статически во время компиляции или динамически во время выполнения.

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

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

Джейсон Райх
источник
Немного обманчиво говорить, что аннотации в стиле Хоара можно проверять статически. Если логика FO, как обычно, то проблема, безусловно, неразрешима. Но да, я знаю, что вы имели в виду, что можно попытаться и даже преуспеть во многих ситуациях.
Раду GRIGore
1
У меня сложилось впечатление, что создание доказательства может быть неразрешимым, но проверка доказательства должна быть. Многие языки с зависимой типизацией полагаются на то, что пользователь предоставит доказательство ценности типа теоремы.
Джейсон Райх
Вы правы. Но я живу в автоматизированном мире, где пользователя обычно не просят предоставить доказательство.
Раду GRIGore