W-типы против индуктивных типов

Теория типов Мартина-Лёфа использует W-типы для определения индуктивных структур, таких как целые числа, списки и т. Д. Однако, исчисление индуктивных конструкций не использует их одинаково, индуктивные типы там больше похожи на схемы аксиом.

Являются ли эти два подхода эквивалентными (они кажутся)? Есть ли философские причины, по которым одно лучше другого (для меня W-типы кажутся более интуитивными, потому что это просто деревья особой структуры)? Что проще с точки зрения реализации (мне кажется, что для меня лучше использовать индуктивные типы, так как для того, чтобы W-типы были полезны, нам нужны по крайней мере конечные типы и продукты, доступные в ядре системы)

(Я предполагаю, что под «схемами аксиомы» вы имеете в виду работу Гименеса )

В расширенном плане схемы W-типов и аксиом Гименеса эквивалентны.

Тем не менее, в интенсиональных настройках вы не будете далеко ходить с W-типами: они слишком экстенсиональны (по определению кодировки), чтобы быть пригодными для программирования. Это обсуждалось несколькими авторами, особенно:

• Конор МакБрайд: http://mazzo.li/epilogue/index.html%3Fp=324.html
• Питер Дибьер, «Представление индуктивно определенных множеств с помощью упорядочений в теории типов Мартина-Лёфа»
• Guogen & Luo, "Индуктивные типы данных: снова упорядоченные типы"