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 recursive types within the theory.

I know you can use impredicative universes as in System F to encode recursive 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.

There's not really any standard terminology here but maybe types you can perform induction on should be called inductive types and types you only have recursion on should be called "recursive types." Anyhow "recursive types" are very weird regardless. Still an interesting construction though

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.

Answer 3

I think my question has been very ambiguous. I wanted to post a sort of template of the "boring answers."

Given a "schema" in the form of a polynomial endofunctor an inductive type can be constructed using the builtin support for inductive types, explicitly postulated as an axiom, or defined impredicatively along with some form of axiomised parametricity.

Require Import Coq.Unicode.Utf8.

Module Type Schema.
  Axiom tag: Set.
  Axiom field: tag → Set.
End Schema.

Module Type W (Import S: Schema).
  (* permits a universe bump, hack around a lack of impredicative set *)
  Axiom t: Type.

  Axiom sup: ∀ s: tag, (field s → t) → t.

  Axiom t_ind: ∀ (P: t → Prop), (∀ s p, (∀ f: field s, P (p f)) → P (sup s p)) → ∀ x, P x.
  Axiom t_rec: ∀ (P: t → Set), (∀ s p, (∀ f: field s, P (p f)) → P (sup s p)) → ∀ x, P x.
  Axiom t_rect: ∀ (P: t → Type), (∀ s p, (∀ f: field s, P (p f)) → P (sup s p)) → ∀ x, P x.
End W.

Module BuiltIn (S: Schema): W S.
  Inductive w := w_intro s (p: S.field s → w).

  Definition t := w.
  Definition sup := w_intro.

  Definition t_ind := w_ind.
  Definition t_rec := w_rec.
  Definition t_rect := w_rect.
End BuiltIn.

Module Postulate (Import S: Schema): W S.
  Axiom t: Set.

  Axiom sup: ∀ s: tag, (field s → t) → t.

  Axiom t_ind: ∀ (P: t → Prop), (∀ s p, (∀ f: field s, P (p f)) → P (sup s p)) → ∀ x, P x.
  Axiom t_rec: ∀ (P: t → Set), (∀ s p, (∀ f: field s, P (p f)) → P (sup s p)) → ∀ x, P x.
  Axiom t_rect: ∀ (P: t → Type), (∀ s p, (∀ f: field s, P (p f)) → P (sup s p)) → ∀ x, P x.
End Postulate.

Module ImpredicativeParametric (Import S: Schema): W S.
  Definition t := ∀ A, (∀ s, (field s → A) → A) → A.

  Definition sup s (p: field s → t): t.
  Proof.
    intros ? k.
    apply (k s).
    intro x.
    apply (p x).
    apply k.
  Defined.

  (* Some form of parametricity must be axiomized *)
  Axiom t_ind: ∀ (P: t → Prop), (∀ s p, (∀ f: field s, P (p f)) → P (sup s p)) → ∀ x, P x.
  Axiom t_rec: ∀ (P: t → Set), (∀ s p, (∀ f: field s, P (p f)) → P (sup s p)) → ∀ x, P x.
  Axiom t_rect: ∀ (P: t → Type), (∀ s p, (∀ f: field s, P (p f)) → P (sup s p)) → ∀ x, P x.
End ImpredicativeParametric.