W-types vs Inductive types Martin-Löf type theory uses W-types to define inductive structures like integers, lists, etc. However, calculus of inductive constructions doesn't use them in the same way, inductive types there seems to be more like axiom schemas. 

Are these two approaches equivalent (they seem to be)? Are there any philosophical reasons why one is better than the other (for me, W-types feel like more intuitive, because the are just trees of special structure)? Which is easier from implementation point of view (inductive types seems to be better for me, since for W-types to be useful we need at least finite types and products to be available in a system's core)
(I'm assuming that by 'axiom schemas', you have in mind the work of Gimenez)

Extensionally, W-types and Gimenez' axiom schemas are equivalent. 

However, in an intensional setting, you won't go far with W-types: they are too extensional (by the very definition of the encoding) to be fit for programming. This has been discussed by several authors, especially :


Conor McBride: http://mazzo.li/epilogue/index.html%3Fp=324.html
Peter Dybjer, "Representing inductively defined sets by wellorderings in Martin-Löf's type theory"
Guogen &amp; Luo, "Inductive data types: well-ordering types revisited"