Types W vs types inductifs

La théorie des types de Martin-Löf utilise des types W pour définir des structures inductives comme des nombres entiers, des listes, etc.

Ces deux approches sont-elles équivalentes (elles semblent l'être)? Y a-t-il des raisons philosophiques pour lesquelles l'une est meilleure que l'autre (pour moi, les types W semblent plus intuitifs, car ce ne sont que des arbres de structure spéciale)? Ce qui est plus facile du point de vue de la mise en œuvre (les types inductifs semblent être meilleurs pour moi, car pour que les types W soient utiles, nous avons besoin d'au moins des types et des produits finis disponibles dans le cœur d'un système)

(Je suppose que par «schémas axiomes», vous avez à l'esprit le travail de Gimenez )

Extensionnellement, les schémas de type W et d'axiome de Gimenez sont équivalents.

Cependant, dans un cadre intensionnel, vous n'irez pas loin avec les types W: ils sont trop extensionnels (par la définition même de l'encodage) pour être adaptés à la programmation. Cela a été discuté par plusieurs auteurs, en particulier:

• Conor McBride: http://mazzo.li/epilogue/index.html%3Fp=324.html
• Peter Dybjer, "Représenter des ensembles définis par induction par des ordres de puits dans la théorie des types de Martin-Löf"
• Guogen & Luo, "Types de données inductifs: les types bien ordonnés revisités"