<p>Source 1 does not say anything about deriving the induction principle for inductive types, it's only about non-dependent recursion. Source 2 says that deriving the induction principle is not possible. So there's no conflict between the the two.</p>
<p>Note though that even the recursion principle that's derivable in source 2, is weaker than the recursion principle that would be definable in a type theory with a universe hierarchy of more than one universe. That's because the encoding only allows computing elements of small types by recursion. For instance, the lambda-encoding does not allow a recursively defined <code>Bool -&gt; Set</code> function, where <code>Bool : Set</code> and <code>Set</code> itself is in some larger universe.</p>
<p><a href="https://dl.acm.org/doi/10.1145/3209108.3209130" rel="nofollow noreferrer">This source</a> derives induction for lambda-encoded data, using some additional assumptions (function extensionality, impredicative identity type). But even here the small-elimination restriction that I mentioned is still present, which limits the usability quite a bit.</p>

CC BY-SA 4.0
2024-02-04T15:25:16.477Z
Indeed, they do not contradict. But I just thought that they both related to my question because dependent inductive types seem to be somewhere "in-between" the two.
Thank you for the link!
Andrew
CC BY-SA 4.0
2024-02-04T14:49:30.300Z
2024-02-04T14:49:30.300Z
András Kovács
<p>I am learning pure type systems to better understand functional (and general) programming.</p>
<p>My question arises mainly from the two facts:</p>
<ol>
<li><p>It is known that we <strong>can</strong> define (co)inductive types in pure System-Fw (see <a href="https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt" rel="nofollow noreferrer">Recursive types for free</a>).</p>
</li>
<li><p>At the same time, it is known that we <strong>cannot</strong> come up with an inductive encoding that would allow us to derive the induction principle in <span class="math-container">$\lambda P2$</span> (see <a href="https://link.springer.com/chapter/10.1007/3-540-45413-6_16" rel="nofollow noreferrer">Induction Is Not Derivable in Second Order Dependent Type Theory</a>).</p>
</li>
</ol>
<p>My question is: is it true that we cannot define an (inhabited) dependent inductive type (e.g <code>Vector</code> from Idris)</p>
<pre><code>data Vect : Nat -&gt; Type -&gt; Type where
   Nil  : Vect Z a
   Cons : a -&gt; Vect k a -&gt; Vect (S k) a
</code></pre>
<p>and pattern match on it similarly to pattern matching on <code>Sum</code> types in (1) in a pure type system such as Calculus of Constructions?</p>

<type-theory><dependent-type><type-systems>
Derivability of `Vector` in pure calculus of constructions
Andrew
# Derivability of `Vector` in pure calculus of constructions

(Asked by: username_0 on 2024-02-04)

I am learning pure type systems to better understand functional (and general) programming.
My question arises mainly from the two facts:

It is known that we can define (co)inductive types in pure System-Fw (see Recursive types for free).

At the same time, it is known that we cannot come up with an inductive encoding that would allow us to derive the induction principle in $\lambda P2$ (see Induction Is Not Derivable in Second Order Dependent Type Theory).


My question is: is it true that we cannot define an (inhabited) dependent inductive type (e.g Vector from Idris)
data Vect : Nat -> Type -> Type where
   Nil  : Vect Z a
   Cons : a -> Vect k a -> Vect (S k) a

and pattern match on it similarly to pattern matching on Sum types in (1) in a pure type system such as Calculus of Constructions?

**Tags:** type-theory, dependent-type, type-systems

---

## 1 answers

### Answer by username_1 on 2024-02-04. Score: 2

Source 1 does not say anything about deriving the induction principle for inductive types, it's only about non-dependent recursion. Source 2 says that deriving the induction principle is not possible. So there's no conflict between the the two.

Note though that even the recursion principle that's derivable in source 2, is weaker than the recursion principle that would be definable in a type theory with a universe hierarchy of more than one universe. That's because the encoding only allows computing elements of small types by recursion. For instance, the lambda-encoding does not allow a recursively defined `Bool -> Set` function, where `Bool : Set` and `Set` itself is in some larger universe.

[This source](https://dl.acm.org/doi/10.1145/3209108.3209130) derives induction for lambda-encoded data, using some additional assumptions (function extensionality, impredicative identity type). But even here the small-elimination restriction that I mentioned is still present, which limits the usability quite a bit.

> **Comments:**
> **username_0**: Indeed, they do not contradict. But I just thought that they both related to my question because dependent inductive types seem to be somewhere "in-between" the two. Thank you for the link!  

---

