Tipos W vs tipos inductivos

La teoría de tipos de Martin-Löf usa tipos W para definir estructuras inductivas como enteros, listas, etc. Sin embargo, el cálculo de construcciones inductivas no las usa de la misma manera, los tipos inductivos parecen ser más como esquemas de axiomas.

¿Son equivalentes estos dos enfoques (parecen ser)? ¿Hay alguna razón filosófica por la cual uno es mejor que el otro (para mí, los tipos W se sienten más intuitivos, porque son solo árboles de estructura especial)? Lo cual es más fácil desde el punto de vista de la implementación (los tipos inductivos parecen ser mejores para mí, ya que para que los tipos W sean útiles, necesitamos al menos tipos y productos finitos disponibles en el núcleo de un sistema)

(Supongo que por 'esquemas de axioma', tienes en mente el trabajo de Giménez )

Extensionalmente, los tipos W y los esquemas de axioma de Giménez son equivalentes.

Sin embargo, en una configuración intensiva, no llegarás lejos con los tipos W: son demasiado extensionales (por la definición misma de la codificación) para ser aptos para la programación. Esto ha sido discutido por varios autores, especialmente:

• Conor McBride: http://mazzo.li/epilogue/index.html%3Fp=324.html
• Peter Dybjer, "Representando conjuntos definidos inductivamente por ordenamientos bien en la teoría de tipos de Martin-Löf"
• Guogen & Luo, "Tipos de datos inductivos: tipos de ordenamiento bien revisados"