<p>I am not 100% sure this is what you want, but assuming you are looking for a  type theory with a closed set of type constructors, which can model inductive families, then what you want are <em>indexed containers</em> or <em>dependent polynomial functors</em>. What you should look at first is:</p>

<ol>
<li><p>Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride and Peter Morris's 2014 draft <a href="https://www.cs.nott.ac.uk/~psztxa/publ/ICont.pdf" rel="noreferrer"><em>Indexed Containers</em></a>. </p>

<p>This paper is an expanded version of Altenkirch and Morris's 2009 LICS paper. It is all formalized in Agda, and gives a set of codes for defining all the strictly positive families. If you need it, it also gives an interpretation of them into W-types (and M-types for coinductive families). This is probably what you want to look at first. </p>

<p>It may also be worth looking at <a href="https://core.ac.uk/download/pdf/82087952.pdf" rel="noreferrer"><em>Containers: Constructing Strictly Positive Types</em></a> by Michael Abbott, Thorsten Altenkirch and Neil Ghani for the non-dependent case.</p></li>
</ol>

<p>Category theorists also invented this concept, which they dubbed <em>dependent polynomial functors</em>. The original paper, and some I found helpful for reading it are:</p>

<ol start="2">
<li><p><a href="http://www1.maths.leeds.ac.uk/%7Epmtng/Publications/gambino-hyland.pdf" rel="noreferrer"><em>Wellfounded trees and dependent polynomial functors</em></a> by Nicola Gambino and Martin Hyland. TYPES 2003.</p></li>
<li><p><a href="https://www.cl.cam.ac.uk/~mpf23/papers/Algebra/gpf.pdf" rel="noreferrer"><em>Generalized Polynomial Functors</em></a> Marcelo Fiore, ICALP 2012. There is a bit more logical intuition in this paper. </p></li>
<li><p><a href="https://dl.acm.org/citation.cfm?id=2036927" rel="noreferrer"><em>A foundation for GADTs and inductive families: dependent polynomial functor approach</em></a>. Makoto Hamana and Marcelo Fiore, WGP 2011. This paper shows how to interpret indexed families as polynomial functors. </p></li>
</ol>

<p>Now, you might also ask whether or not inductive families are "the morally correct" syntax for indexed containers. The answer is: probably not, but this is because containers/polynomials are too rich to have an obvious syntax.</p>

<ul>
<li><p>Tamara von Glehn's PhD thesis, <a href="https://core.ac.uk/download/pdf/35280857.pdf" rel="noreferrer"><em>Polynomials and Models of Dependent Type Theory</em></a>, builds models of dependent type theory out of polynomial functors. This implies that the correct syntax for datatypes in type theory is type theory itself, and I just don't know how to connect that to language design. Someone should give it a try, though!</p></li>
<li><p>Pierre Hyvernat has an LMCS 2014 paper, <a href="https://arxiv.org/pdf/1403.0833.pdf" rel="noreferrer"><em>A Linear Category of Polynomial Functors</em></a>, which uses a different notion of morphism to give polynomials a monoidal closed structure. So perhaps datatype declarations should be written in a linear type theory? </p></li>
</ul>

CC BY-SA 4.0
2019-10-07T23:57:20.483Z
I haven't gone through them exhaustively, but I think the problem with all these citations is that they are basically W-types. For instance, containers are a way of packaging/manipulating the parameters of a W-type. Those let you represent 'the right' trees, but they don't generally let you derive the induction principle for the inductive family you're representing without function extensionality, because 'first order' stuff from the family is represented as higher-order stuff in the (indexed) W-type.
Dan Doel
CC BY-SA 4.0
2019-10-07T23:58:43.030Z
So, one solution that I've seen (related to OTT work, I think) is to have a more complicated language that retains the first-orderness of the right pieces of an inductive family definition. But I think that's what's being rejected as "levitation/datatype-generic-programming," so I don't know what else to suggest. :)
Dan Doel
CC BY-SA 4.0
2019-10-08T00:07:13.473Z
I suppose the obvious other suggestion is to realize that the lack of function extensionality in intensional type theory is a defect that we know how to overcome without losing its nice properties, not a moral principle to hold to.
Dan Doel
CC BY-SA 4.0
2019-10-02T17:07:35.483Z
2019-10-02T17:07:35.483Z
Neel Krishnaswami
<p>I published a paper in Types 2020 <a href="https://doi.org/10.4230/LIPIcs.TYPES.2020.8" rel="nofollow noreferrer">Why not W?</a> which shows that W types (plus  propositional equality with J that computes and sigma types with eta) are sufficient to construct all the intensional inductive families you want. So you can do your metatheory just assuming W types (you probably don't want Fix) and all the results apply immediately to the whole menagerie of inductive families.</p>
<p>The trick in that paper is as follows. Everyone knows that defining <span class="math-container">$N = W_{x:\{\hat{S},\hat{O}\}}(1 \text{ if } x = \hat{S} \text{ else } 0)%$</span> is no good, because you have as many representations of 0 as you do functions <span class="math-container">$0 \to N$</span>, which intensionally is a lot. You can't prove the induction principle without function extensionality to say <span class="math-container">$(0 \to N) \cong 1$</span>, and even then you don't get good computation rules. But nobody ever said that was the only way to define <span class="math-container">$N$</span> in terms of <span class="math-container">$W$</span>. Starting from this definition of <span class="math-container">$N$</span>, you can inductively define a predicate that, in the <span class="math-container">$\sup(\hat{O}, f)$</span> case, consists of a witness of proposional equality <span class="math-container">$Id(!_N, f)$</span> (where <span class="math-container">$!_N : 0 \to N$</span> is the <em>cannonical</em> function from 0). This allows defining the induction principle, it computes, you get canonicity as long as reflexivity is the only closed proof of equality (so broken in homotopy type theory), and it generalizes to all the inductive families you want.</p>

CC BY-SA 4.0
2024-10-06T00:31:27.230Z
2024-10-06T00:31:27.230Z
Jasper Hugunin
<p>I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction principles).</p>

<p>For example, I'm thinking:</p>

<ul>
<li>You can use propositional equality to turn an inductive family into an inductive type with equality constraints on the indices</li>
<li>You can use Sigma types to encode sums-of-products</li>
<li><p>You can get inductive types with a fixed-point type:</p>

<p><code>data Fix : (Type -&gt; Type) -&gt; Type where</code>
  <code>Fold : (f : Type -&gt; Type) -&gt; f (Fix f) -&gt; Fix f</code></p>

<p>which is fine as long as <code>f</code> is strictly positive. </p></li>
</ul>

<p>But I'm not certain that these give you the full power of inductive families, particularly whether <code>Fix</code> gives you the full power of eliminators/structural recursion for inductive families.</p>

<p><strong>Are there any references on what is sufficient to model inductive families?</strong></p>

<p>I'm aware of:</p>

<ul>
<li>W-types, which don't work well in an intensional setting.</li>
<li>Church-encodings, which aren't powerful enough to prove that (0 != 1), and also don't work well in a predicative setting</li>
<li>Levitation/datatype-generic-programming, which seems to give you all of inductive families, but at the expense of having to keep a runtime representation of every type, with a lot of complexity related to this representation. This seems like a chainsaw where I need a knife.</li>
</ul>

CC BY-SA 4.0
2019-09-30T19:47:56.917Z
Not sure what are your constraints (e.g. what you'd consider as minimal, and also your `Fix` breaks consistency), but my [calculus of united constructions](https://dl.acm.org/citation.cfm?doid=3331554.3342607) might give you some ideas (it's likely not "minimal" in your sense).
Stefan
CC BY-SA 4.0
2019-10-01T07:08:24.623Z
Unless you make your requirement for a "minimal" type system more precise, the answer is "the minimal necessary type theory to model inductive families is type theory with inductive families".
Andrej Bauer
CC BY-SA 4.0
2019-10-01T16:48:35.947Z
@AndrejBauer I guess what I really mean is "finite" or "fixed" i.e. is there a fixed set of type constructors I can have in my theory that will give me a language equivalent to one where I can define my own inductive families. Minimal really is just "smaller is better" i.e. levitation seems to fit what I'm doing, but it's rather large and complex, and I'm wondering if it can be done smaller.
Joey Eremondi
CC BY-SA 4.0
2019-10-01T20:54:05.253Z
And I suppose you do not consider a formalization which allows the user to specify new inductive families to be a "fixed set of type constructors"?
Andrej Bauer
CC BY-SA 4.0
2019-10-01T22:05:25.193Z
@AndrejBauer exactly. Basically, I'm looking to have a closed theory I can reason about on paper, and then say "and this is equivalent to a theory in which users can define their own families"
Joey Eremondi
<type-theory><functional-programming><dependent-type><typed-lambda-calculus><proof-assistants>
Fixed set of type constructors to simulate all intensional inductive families?
Joey Eremondi
# Fixed set of type constructors to simulate all intensional inductive families?

(Asked by: username_0 on 2019-09-30)

I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction principles).

For example, I'm thinking:

* You can use propositional equality to turn an inductive family into an inductive type with equality constraints on the indices
* You can use Sigma types to encode sums-of-products
* You can get inductive types with a fixed-point type:

  `data Fix : (Type -> Type) -> Type where`
  `Fold : (f : Type -> Type) -> f (Fix f) -> Fix f`

  which is fine as long as `f` is strictly positive.

But I'm not certain that these give you the full power of inductive families, particularly whether `Fix` gives you the full power of eliminators/structural recursion for inductive families.

**Are there any references on what is sufficient to model inductive families?**

I'm aware of:

* W-types, which don't work well in an intensional setting.
* Church-encodings, which aren't powerful enough to prove that (0 != 1), and also don't work well in a predicative setting
* Levitation/datatype-generic-programming, which seems to give you all of inductive families, but at the expense of having to keep a runtime representation of every type, with a lot of complexity related to this representation. This seems like a chainsaw where I need a knife.

**Tags:** type-theory, functional-programming, dependent-type, typed-lambda-calculus, proof-assistants

> **Comments:**
> **username_1**: Not sure what are your constraints (e.g. what you'd consider as minimal, and also your `Fix` breaks consistency), but my [calculus of united constructions](https://dl.acm.org/citation.cfm?doid=3331554.3342607) might give you some ideas (it's likely not "minimal" in your sense).  
> **username_2**: Unless you make your requirement for a "minimal" type system more precise, the answer is "the minimal necessary type theory to model inductive families is type theory with inductive families".  
> **username_0**: @AndrejBauer I guess what I really mean is "finite" or "fixed" i.e. is there a fixed set of type constructors I can have in my theory that will give me a language equivalent to one where I can define my own inductive families. Minimal really is just "smaller is better" i.e. levitation seems to fit what I'm doing, but it's rather large and complex, and I'm wondering if it can be done smaller.  
> **username_2**: And I suppose you do not consider a formalization which allows the user to specify new inductive families to be a "fixed set of type constructors"?  
> **username_0**: @AndrejBauer exactly. Basically, I'm looking to have a closed theory I can reason about on paper, and then say "and this is equivalent to a theory in which users can define their own families"  

---

## 2 answers

### Answer by username_3 on 2019-10-02. Score: 5

I am not 100% sure this is what you want, but assuming you are looking for a type theory with a closed set of type constructors, which can model inductive families, then what you want are *indexed containers* or *dependent polynomial functors*. What you should look at first is:

1. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride and Peter Morris's 2014 draft [*Indexed Containers*](https://www.cs.nott.ac.uk/~psztxa/publ/ICont.pdf).

   This paper is an expanded version of Altenkirch and Morris's 2009 LICS paper. It is all formalized in Agda, and gives a set of codes for defining all the strictly positive families. If you need it, it also gives an interpretation of them into W-types (and M-types for coinductive families). This is probably what you want to look at first.

   It may also be worth looking at [*Containers: Constructing Strictly Positive Types*](https://core.ac.uk/download/pdf/82087952.pdf) by Michael Abbott, Thorsten Altenkirch and Neil Ghani for the non-dependent case.

Category theorists also invented this concept, which they dubbed *dependent polynomial functors*. The original paper, and some I found helpful for reading it are:

2. [*Wellfounded trees and dependent polynomial functors*](http://www1.maths.leeds.ac.uk/%7Epmtng/Publications/gambino-hyland.pdf) by Nicola Gambino and Martin Hyland. TYPES 2003.
3. [*Generalized Polynomial Functors*](https://www.cl.cam.ac.uk/~mpf23/papers/Algebra/gpf.pdf) Marcelo Fiore, ICALP 2012. There is a bit more logical intuition in this paper.
4. [*A foundation for GADTs and inductive families: dependent polynomial functor approach*](https://dl.acm.org/citation.cfm?id=2036927). Makoto Hamana and Marcelo Fiore, WGP 2011. This paper shows how to interpret indexed families as polynomial functors.

Now, you might also ask whether or not inductive families are "the morally correct" syntax for indexed containers. The answer is: probably not, but this is because containers/polynomials are too rich to have an obvious syntax.

* Tamara von Glehn's PhD thesis, [*Polynomials and Models of Dependent Type Theory*](https://core.ac.uk/download/pdf/35280857.pdf), builds models of dependent type theory out of polynomial functors. This implies that the correct syntax for datatypes in type theory is type theory itself, and I just don't know how to connect that to language design. Someone should give it a try, though!
* Pierre Hyvernat has an LMCS 2014 paper, [*A Linear Category of Polynomial Functors*](https://arxiv.org/pdf/1403.0833.pdf), which uses a different notion of morphism to give polynomials a monoidal closed structure. So perhaps datatype declarations should be written in a linear type theory?

> **Comments:**
> **username_4**: I haven't gone through them exhaustively, but I think the problem with all these citations is that they are basically W-types. For instance, containers are a way of packaging/manipulating the parameters of a W-type. Those let you represent 'the right' trees, but they don't generally let you derive the induction principle for the inductive family you're representing without function extensionality, because 'first order' stuff from the family is represented as higher-order stuff in the (indexed) W-type.  
> **username_4**: So, one solution that I've seen (related to OTT work, I think) is to have a more complicated language that retains the first-orderness of the right pieces of an inductive family definition. But I think that's what's being rejected as "levitation/datatype-generic-programming," so I don't know what else to suggest. :)  
> **username_4**: I suppose the obvious other suggestion is to realize that the lack of function extensionality in intensional type theory is a defect that we know how to overcome without losing its nice properties, not a moral principle to hold to.  

---

### Answer by username_5 on 2024-10-06. Score: 3

I published a paper in Types 2020 [Why not W?](https://doi.org/10.4230/LIPIcs.TYPES.2020.8) which shows that W types (plus propositional equality with J that computes and sigma types with eta) are sufficient to construct all the intensional inductive families you want. So you can do your metatheory just assuming W types (you probably don't want Fix) and all the results apply immediately to the whole menagerie of inductive families.

The trick in that paper is as follows. Everyone knows that defining $N = W\_{x:\{\hat{S},\hat{O}\}}(1 \text{ if } x = \hat{S} \text{ else } 0)%$ is no good, because you have as many representations of 0 as you do functions $0 \to N$, which intensionally is a lot. You can't prove the induction principle without function extensionality to say $(0 \to N) \cong 1$, and even then you don't get good computation rules. But nobody ever said that was the only way to define $N$ in terms of $W$. Starting from this definition of $N$, you can inductively define a predicate that, in the $\sup(\hat{O}, f)$ case, consists of a witness of proposional equality $Id(!\_N, f)$ (where $!\_N : 0 \to N$ is the *cannonical* function from 0). This allows defining the induction principle, it computes, you get canonicity as long as reflexivity is the only closed proof of equality (so broken in homotopy type theory), and it generalizes to all the inductive families you want.


---

