Индукция-рекурсия

• Основы индукционно-рекурсивной теории типов

  • Индукционно-рекурсия позволяет одновременно объявлять тип и функцию для этого типа. 
  • Созданные типы остаются предикативными, но позволяют создавать более крупные типы, включая вселенные. 
  • Правила для генерации элементов типа могут использоваться для определения функций. 

• Исторический контекст

  • Индукционно-рекурсивная теория возникла из исследований Мартина-Лефа в интуиционистской теории типов. 
  • Мартин-Леф намекнул на существование паттерна для правил формирования типов, который сохраняет свойства теории типов. 
  • Дайбьер и Сетцер разработали новый формирователь типов, который позволил создавать новые индукционно-рекурсивные определения. 

• Примеры и использование

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

• Рекомендации и дополнительные ресурсы

  • Ссылки на внешние ресурсы, включая публикации Питера Дайбьера и слайды, посвященные индукции-рекурсии.