Tipos W versus tipos indutivos

A teoria dos tipos de Martin-Löf usa os tipos W para definir estruturas indutivas, como números inteiros, listas, etc. No entanto, o cálculo de construções indutivas não as utiliza da mesma maneira; tipos indutivos parecem mais com esquemas de axiomas.

Essas duas abordagens são equivalentes (elas parecem ser)? Existem razões filosóficas pelas quais uma é melhor que a outra (para mim, os tipos W parecem mais intuitivos, porque são apenas árvores de estrutura especial)? O que é mais fácil do ponto de vista da implementação (os tipos indutivos parecem melhores para mim, pois para os tipos W serem úteis, precisamos que pelo menos tipos e produtos finitos estejam disponíveis no núcleo do sistema)

(Estou assumindo que, por 'esquemas de axioma', você tenha em mente o trabalho de Gimenez )

Extensionalmente, os tipos W e os esquemas axiais de Gimenez são equivalentes.

No entanto, em um cenário intensional, você não irá muito longe com os tipos W: eles são muito extensivos (pela própria definição da codificação) para serem adequados à programação. Isso foi discutido por vários autores, especialmente:

• Conor McBride: http://mazzo.li/epilogue/index.html%3Fp=324.html
• Peter Dybjer, "Representando conjuntos definidos indutivamente por pedidos de poços na teoria de tipos de Martin-Löf"
• Guogen & Luo, "Tipos de dados indutivos: tipos bem ordenados revisitados"