6
$\begingroup$

To define a (non-indexed) W-type all we need is a type $A:U$ and a function $B:A\to U$ and we get a type $W_{a:A}B(a)$. To check that this definition is valid we only need to check that the definitions of $A$ and $B$ are valid.

Now general inductive types seem like very scary beasts and I still don't entirely understand what a proof checker kernel (e.g. in Coq) is doing to make sure the definition is valid.

In intensional type theory there is apparently a big gap between W-types and general inductive types. For example the generic W-type recursion applied to the W-type encoding of unary natural numbers is not as strong as standard recursion for natural numbers.

So the question is: is there a way to set up inductive types so that to check the validity of a definition you only need to check the validity of finitely many non-inductive typing judgements?

A strongly normalizing type theory can't fully interpret itself but I guess we could have a partially defined quote unquote specifically for the bits of data necessary to define inductive types. Can you suggest any references?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
14
$\begingroup$

It turns out that $W$ types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types you want, with the expected computation rules, and even canonicity. This is a very recent result of mine, you can read a preprint at Why not W?, which has been accepted for publication in the TYPES 2020 post-proceedings.

The idea is that even though the standard construction of say the natural numbers from W types does not work, as is well known, a refined, slightly more complicated construction can be made to work. The way my refinement works is to use identity types to pick out the elements of the standard construction which are in canonical form.

This puts general inductive types on an internal, finitary footing, which is a large simplification of the theory. However, there remain some practical problems to be looked at around efficiency and usability.

Other, prior work on simplifying the theory of inductive types includes The Gentle Art of Levitation, by James Chapman, Pierre-Evariste Dagand, Conor McBride, and Peter Morris.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ Are you aware of Carneiro's github.com/digama0/lean-type-theory (specifically Section 5)? $\endgroup$
    – user61651
    Mar 17, 2021 at 9:42
  • 1
    $\begingroup$ This is a remarkably cute construction— thanks for posting it (and inventing it, too). $\endgroup$
    – Neel Krishnaswami
    Mar 17, 2021 at 9:55
  • $\begingroup$ @einzwein Carneiro's master's thesis claims (in Section 5.4), but does not prove, that the iota rule (computation for inductives) holds definitionally. Frankly, I believe that this claim is wrong for the construction as written in his Section 5, unless we move to extensional type theory. He reproduces a folkloric reduction of indexed inductive types to non-indexed inductive types + eq, but no more. My paper shows how to modify his construction and rescue his claimed results. $\endgroup$
    – Jasper Hugunin
    Mar 18, 2021 at 6:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.