<p>(I'm assuming that by 'axiom schemas', you have in mind the work of <a href="http://link.springer.com/chapter/10.1007/3-540-60579-7_3">Gimenez</a>)</p>

<p>Extensionally, W-types and Gimenez' axiom schemas are equivalent. </p>

<p>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 :</p>

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

CC BY-SA 3.0
2014-05-05T16:33:46.723Z
You can also add Programming in Martin-Lof type theory by Nordstrom et all.
Konstantin Solomatov
CC BY-SA 4.0
2024-09-30T00:16:49.563Z
In the presence of `Id` types (equality types) and eta for pair types there is an alternative encoding that has the expected computational behavior. [Why not W? (own work)]<https://doi.org/10.4230/LIPIcs.TYPES.2020.8> demonstrates this.
Jasper Hugunin
CC BY-SA 3.0
2014-05-05T12:06:26.057Z
2014-05-05T12:06:26.057Z
pedagand
<p>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. </p>

<p>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)</p>

<lo.logic><type-theory>
W-types vs Inductive types
Konstantin Solomatov
# W-types vs Inductive types

(Asked by: username_0 on 2014-04-17)

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)

**Tags:** lo.logic, type-theory

---

## 1 answers

### Answer by username_1 on 2014-05-05. Score: 10 | Accepted answer

(I'm assuming that by 'axiom schemas', you have in mind the work of [Gimenez](http://link.springer.com/chapter/10.1007/3-540-60579-7_3))

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 & Luo, "Inductive data types: well-ordering types revisited"

> **Comments:**
> **username_0**: You can also add Programming in Martin-Lof type theory by Nordstrom et all.  
> **username_2**: In the presence of `Id` types (equality types) and eta for pair types there is an alternative encoding that has the expected computational behavior. [Why not W? (own work)]<https://doi.org/10.4230/LIPIcs.TYPES.2020.8> demonstrates this.  

---

