Comments 22
inProp просто говорит, что любые два элемента утверждения (то есть типа, лежащего в \Prop) равны. Аксиома K эквивалентна UIP, которая говорит, что любые два элемента типа равенства равны. Другими словами, что тип равенства является утверждением.
Кстати, пока готовилась эта статья, вышла версия языка 1.1, в которой inProp больше нет, так как теперь любые два элемента утверждения вычислительно равны (а не только пропозиционально).
Да, мне только потом пришло в голову, что inProp универсальнее. Будет ли корректной ментальной моделью сказать, что inProp эквивалентна семейству K-подобных аксиом для каждого возможного предиката?
Я бы не сказал, что он универсальнее. Тут просто причина в том, что в Arend есть специальная вселенная утверждений. Разумеется, должен быть способ доказать, что она эквивалентна обычной вселенной типов, являющихся утверждениями. Для этого есть несколько механизмов. Один из них — это inProp, который в точности говорит, что все типы в \Prop являются утверждениями.
Лично для меня профит от Prop/Agda-style irrelevance/Idris-style erasure в том, что, ну, доказательства стираются и не утекают в рантайм, и вы их случайно в рантайме не начнёте вычислять (что может быть медленно).
Я бы сказал, что в Arend нет понятия рантайма. Если говорить более формально, то в нем есть выражения, которые вообще не вычисляются. Элиминация из \Prop в не \Prop — это действительно проблема, но если запретить таким функциям вычисляться, то всё будет хорошо. Именно таким образом эта проблема решается в Arend.
То есть, для примера доказательств сортированности списка из статьи, метатеория языка гарантирует, что есть последовательность некоторых редукций (каких?), которая приводит термы друг в друга?
Я не совсем понял о каких термах идет речь. В общем, эквивалентность не обязательно должна работать через редукции. Например, эта-эквивалентность часто без редукций проверяется. Аналогично, чтобы проверить эквивалентность термов, имеющих тип в \Prop, достаточно проверить в какой вселенной лежит их тип.
Ну вот вы написали, скажем, функцию сортировки и что-то про неё доказали. А что вы дальше с этой функцией делаете?
На этом всё. Так как язык ориентирован именно на доказательство теорем, то большой необходимости запускать функции нет. Это может быть полезно и в математике, но не в первую очередь.
Мой поинт в том, что бывают случаи, когда вычисляться таки надо.
Мне кажется, что есть какое-то недопонимание. Если все функции не будут вычисляться, то проблемы с termination вообще не будет. В Arend 1.1 появилось новое ключевое слово \sfunc для определения функций, которые вычисляться не будут. Любая функция, которая элиминирует из \Prop в не \Prop, обязана быть \sfunc. С termination checker'ом это никак не связано, так как просто проблемные функции не вычисляются.
Если я правильно понимаю, что такое computational equality, то этого недостаточно, и нужно предъявить цепочку преобразований. Скорее всего, у нас просто небольшое расхождение в терминологии.
На самом деле большой разницы нет между тем, чтобы проверять произвольное отношение эквивалентности или отношение, которое задается через редукцию. Второе является частным случаем первого, а первое сводится ко второму. Для этого просто достаточно добавить фиктивный терм и сказать, что все эквивалентные термы редуцируются к нему.
Статья на хабре: новый язык программирования, jetbrains, inteliJ, обычное хипстерство, вдруг, HoTT, взрыв мозга, читать пословно.
Спасибо за описание.
Вопрос. Написано:
Сумма типов A + B. В Haskell этот тип называется Either A B. Так как этот тип населен тогда и только тогда, когда один из типов A или B населен, то эта конструкция соответствует логическому «или».
А если A и B населены, то A+B населено или нет?
Ох, что вы творите…
Правильно ведь понимаю, что язык назван в честь Гейтинга? Добавьте в статью!
Наивная попытка сказать, что типом вселенной \Type, по определению, является сама \Type приводит к парадоксу Жирара
Я не очень понял суть этого парадокса, но если он эквивалентен парадоксу Рассела, то причина его не в том, что теория противоречива, а в том, что бинарная логика принципиально не полна, ибо не позволяет оперировать произвольными выражениями. В частности, она не позволяет отличать "ненаселённый тип" от "противоречивого типа", для которого понятие "населённости" вообще не применимо. Отсюда и возникает парадокс, ведь "тип всех ненаселённых типов" — это как раз "противоречивый тип", а не "ненаселённый".
Подробнее я рассказывал об этом тут: https://habr.com/ru/post/522578/
Не сказал бы, что существенно сложней. Он вытекает из понятия актуальной бесконечности, которое противоречиво само по себе, отсюда и множество парадоксов. Все они имеют похожую фабулу:
- Актуализируем бесконечность — это позволяет работать с ней, как с конечным объектом.
- Для любого конечного объекта можно построить строго больший объект не равный данному.
- Формулируем исходный объект из (1) так, чтобы он заведомо включал и любые производные от него типа (2).
- Получаем противоречие.
Самая простая формулировка, без запутывающей мишуры в виде множеств, типов, отображений и тд, выглядит так:
- Берём самое большое натуральное число и обозначим его как ∞ (актуализация бесконечности).
- Прибавляем единичку — получаем ещё более большое число.
- Но увеличение натурального числа на 1 даёт натуральное число.
- Следовательно наше новое более большое число должно быть меньше либо равно самого большого натурального числа из (1).
С натуральными числами все более-менее договорились, что так делать нельзя. Но со множествами так и продолжают ходить по тем же граблям.
И проблема тут не в формулировке бесконечной сущности (самое больше число, множество всех множеств и тп), а в том, что операция (2), которая применима лишь к конечным сущностям, применяется вдруг к бесконечным (актуализация бесконечности).
Arend – язык с зависимыми типами, основанный на HoTT (часть 1)