Agda (язык программирования)

• Обзор Agda

  • Agda — функциональный язык программирования с зависимой типизацией, разработанный Ульфом Нореллом. 
  • Система Agda была разработана Катариной Коканд в 1999 году и является полностью переработанной версией. 
  • Agda является помощником по доказательству и использует парадигму propositions-as-types. 

• Особенности Agda

  • Индуктивные типы являются основным способом определения типов данных, аналогично алгебраическим типам в языках с независимой типизацией. 
  • Зависимое типизированное сопоставление с образцом используется для доказательства теорем вместо принципов индукции и рекурсии. 
  • Метапеременные играют ключевую роль в программировании на Agda, позволяя уточнять типы и создавать поэтапные программы. 
  • Автоматизация проверки типов включает в себя написание тактик и использование рефлексии для упрощения сложных доказательств. 
  • Проверка завершения работы программы является важной особенностью Agda, гарантирующей последовательность логики языка. 

• Стандартная библиотека и поддержка Юникода

  • Agda имеет обширную стандартную библиотеку, которая активно развивается. 
  • Язык сильно зависит от Unicode в исходном коде, что отражается в использовании сочетаний клавиш в редакторе. 

• Компиляторы и серверные части

  • Существуют два бэкэнда компилятора: MAlonzo для Haskell и один для JavaScript. 

• Дополнительные ресурсы

  • Ссылки на плейлисты, учебные пособия и популярные летние школы по теории гомотопических типов.