Представление индуктивных типов

Question

Я реализовал лямбда-исчисление с зависимой типизацией в духе этой статьи: http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf Исчисление, работает, и я экспериментировал с ним и расширил несколько вещей: много вселенных, жестко закодированная индукция аксиомы. Тем не менее, я хочу добавить индуктивные типы, чтобы делать более сложные вещи.

Я думаю о двух способах сделать это

• Представьте Fin-N, Product и W-типы и представьте им индуктивные типы.
• Генерация аксиом индукции и рекурсии.

Мне не нравится ни один из способов. Первый - слишком низкий уровень и требует значительных усилий для перехода с языка высокого уровня на основной язык. Второй способ довольно трудоемкий и подвержен ошибкам, поскольку генерация принципов рекурсии сложных индуктивных типов имеет много угловых случаев, то есть положительных / отрицательных случаев.

Как это можно сделать? Как типы реализованы в существующих системах, таких как Coq, Agda и Idris?

Answer 1

Извините, но я не знаю об Идрисе.

Для Агды я рекомендую кандидатскую диссертацию Ульфа Норелла в качестве отправной точки, но с тех пор система развивалась.

Coq вводит третий пункт в вашем списке: автоматически сгенерированные предикаты. Каждый индуктивный тип поставляется с 3 (1 в некоторых особых случаях) индукционными схемами, которые автоматически определяются для пользователя и называются your_type_rect, your_type_rec а также your_type_ind (только последний в особых случаях). Это фактические термины языков, автоматически генерируемые для пользователя и используемые induction тактика (я не уверен на 100% в этом последнем), а не аксиомы.

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

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

Бест В.