Construction of inductive types "the hard way"

Question

Most theorem provers simply axiomize inductive types (or equivalently W types) in the abstract which is fine.

But I'm curious about explicit constructions of inductive types within the theory.

I suppose I'm interested in both inductive types and "weak inductive types" (weak initial algebras) such as impredicative encodings. I think the term I've most found in my searches has been "weak natural numbers object." Inductive types can be better but weak inductive types are cool too.

I know you can use impredicative universes as in System F to encode inductive types. Or you can just accept a universe bump. And apparently if you internalize a small amount of parametricity you can construct appropriate induction principles.

But I'm pretty sure I've heard you can construct inductive types other ways. I think maybe you need to assume some classical principles? I've read some stuff on transfinite induction I still don't really get. I think once you have a base inductive type of ordinals you can construct other inductive types in those terms?

I have a hunch you can abuse impredicative proof irrelevant propositions and natural numbers to construct inductive types but I don't really have anything solid here.

Also for some reason I think it's easier to construct free monads the hard way instead of inductive types? I'm not sure this is an important issue.

I don't think W types and polynomial endofunctors directly solve the problem. They provide some clarifying language for how to talk about inductive types but they're not quite an explicit construction.

There's a paper "Induction Is Not Derivable in Second Order Dependent Type Theory" I don't understand yet but I think all this means is you need to assume more axioms than second order dependent type theory?

Answer 1

In the HOLish settings, these types (starting with the natural numbers) are indeed constructed from first principles; they're certainly not axiomatised. Harrison had an early (1995) paper on how to do this, and the technology has developed from there.

Harrison's construction doesn't use ordinals, but encodes its types as trees underneath and then uses an inductive relation and the HOL type definition principle to prune away values that are not desired.

The more capable and more recent technology in Isabelle/HOL (“bounded natural functors”) does have some fancy cardinality reasoning behind it. There's a nice 2012 LICS paper on this tech by Traytel et al.

Answer 2

There are a lot of questions in your question, so I don’t think it’s easy to answer all of them at once, but let me still try and give a picture in the dependently typed setting.

First you cannot get "real" inductive types using only (impredicative) encoding, because you lack the ability to prove an induction principle – you can only define a recursor. This is the essence of Geuvers' Induction Is Not Derivable in Second Order Dependent Type Theory.

Another possibility is thus to encode all inductive types using only a number of basic ones, with usually W-types as the main ingredient. If you only care about the content up to propositional equality Inductive Types in Homotopy Type Theory shows that this is doable in HoTT, eg. you can construct a lot of types that are propositionally initial if you assume only a few base types (including W types). However, if you care about computational content, i.e. you want to have conversion rules and not you equalities, this get a bit trickier. Here the best reference I know is Why not W?, which covers quite some distance in that direction.

Finally, another direction of research in trying to decompose inductive types in "simple" descriptions is that on containers (see for instance Indexed Containers). I’m less familiar with that line of thought, but from what I gathered the idea here is to give a notion of "description" of an inductive type (or something closely related), that can be used to generate the usual data (type, constructors, recursor…), but also can be used to do meta-programming.