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 :

| cite | improve this answer | |
  • 1
    $\begingroup$ You can also add Programming in Martin-Lof type theory by Nordstrom et all. $\endgroup$ – Konstantin Solomatov May 5 '14 at 16:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.