Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Coq vs. Agda

Я нежно люблю Агдочку за превосходный синтаксис, шикарные имплисит-параметры, идеальный паттерн-матчинг и всякие экспериментальные фичи (особенно, конечно, индуктивно-рекурсивные типы и индексированные коиндуктивные типы), но вынужден признать, что за пределами этого сахарка у Агды не осталось никаких преимуществ перед Coq'ом — только недостатки.

Новый Coq 8.7 умеет и эта-конверсии для функций и рекордов, и прекрасно сделанный полиморфизм по вселенным, более того там (в отличие от Агды) вселенные ещё и куммулятивны, более того, куммулятивность распространяется и на все индуктивные типы (зависимые от вселенных). И к этому всему добавляется (недоступный в Агде) импредикативный Prop (классификатор подобъектов в категорной семантике), чувствительно облегчающий жизнь. И за ним, в отличие от Агды стоит полноценно описанная и проверенная в реферируемой публикации теория: pCuIC(+UP) — Predicative Calculus of Cumulative Inductive Constructions with Universe Polymorphism (https://arxiv.org/abs/1710.03912 + https://www.irif.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf)

Им бы ещё только Polynomial Inductive-Recursive Definitions добавить, и на этом вопрос золотого стандарта интуиционистских теорий типов догомотопической эры был бы закрыт.
Subscribe

Recent Posts from This Journal

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

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

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 1 comment