<p>The question you are asking is interesting and known. You are using the so-called impredicative encoding of the natural numbers. Let me explain a bit of the background.</p>
<p>Given a type constructor <span class="math-container">$T : \mathsf{Type} \to \mathsf{Type}$</span>, we might be interested in the &quot;minimal&quot; type <span class="math-container">$A$</span> satisfying <span class="math-container">$A \cong T(A)$</span>. In terms of category theory <span class="math-container">$T$</span> is a functor and <span class="math-container">$A$</span> is the initial <span class="math-container">$T$</span>-algebra. For example, if <span class="math-container">$T(X) = 1 + X$</span> then <span class="math-container">$A$</span> corresponds to the natural numbers. If <span class="math-container">$T(X) = 1 + X \times X$</span> then <span class="math-container">$A$</span> is the type of finite binary trees.</p>
<p>An idea with long history is that the initial <span class="math-container">$T$</span>-algebra is the type
<span class="math-container">$$A \mathrel{{:}{=}} \prod_{X : \mathsf{Type}} (T(X) \to X) \to X.$$</span>
(You are using Agda notation for dependent products, but I am using a more traditional mathematical notation.) Why should this be? Well, <span class="math-container">$A$</span> essentially encodes the recursion principle for the initial <span class="math-container">$T$</span>-algebra: given any <span class="math-container">$T$</span>-algebra <span class="math-container">$Y$</span> with a structure morphism <span class="math-container">$f : T(Y) \to Y$</span>, we get an algebra homomorphism <span class="math-container">$\phi : A \to Y$</span> by
<span class="math-container">$$\phi(a) = a \, Y \, f.$$</span>
So we see that <span class="math-container">$A$</span> is <em>weakly</em> initial for sure. For it to be initial we would have to know that <span class="math-container">$\phi$</span> is unique as well. This is not true without further assumptions, but the details are technical and nasty and require reading some background material. For instance, if we can show a satisfactory <a href="http://en.wikipedia.org/wiki/Parametricity" rel="nofollow noreferrer"><em>parametricty</em> theorem</a> then we win, but there are also other methods (such as massaging the definition of <span class="math-container">$A$</span> and assuming the <span class="math-container">$K$</span>-axiom and function extensionality).</p>
<p>Let us apply the above to <span class="math-container">$T(X) = 1 + X$</span>:
<span class="math-container">$$\mathsf{Nat} =
  \prod_{X : \mathsf{Type}} ((1 + X) \to X) \to X =
  \prod_{X : \mathsf{Type}} (X \times (X \to X)) \to X = \\
  \prod_{X : \mathsf{Type}} X \to (X \to X) \to X.
$$</span>
We got Church numerals! And we also understand now that we will get a recursion principle for free, because the Church numerals <em>are</em> the recursion principle for numbers, but we will not get induction without parametricity or a similar device.</p>
<p>The tehcnical answer to your question is this: there exist models of type theory in which the type <code>SimpleNat</code> contains <em>exotic</em> elements that do not correspond to numerals, and moreover, these elements break the induction principle. The type <code>SimpleNat</code> in these models is too big and is only a <em>weak</em> initial algebra.</p>

CC BY-SA 3.0
2015-03-27T16:40:31.730Z
I agree that the answer is great, but a few references might be useful here: [Geuvers' paper on non-derivability of induction](http://www.cs.ru.nl/~herman/PUBS/IndNonder.ps.gz) and [Neel K's and Derek Dreyer's paper on getting (some) induction from parametricity](https://www.mpi-sws.org/~neelk/final-csl-internalizing-parametricity.pdf). I'm not aware of a paper that fully explores the relationship though.
cody
CC BY-SA 3.0
2015-03-27T18:05:44.790Z
I am not too strong on references in this area, thanks @cody!
Andrej Bauer
CC BY-SA 4.0
2020-11-01T22:30:16.020Z
@AndrejBauer I have tried to derive that `A = forall X. (F X -> X) -> X` is the initial F-algebra by using parametricity but I don't seem to get quite the right result. There are easily written implementations of functions `fix: F A -> A` and `unfix: A -> F A`. I am using the parametricity theorem for the type signature `forall X. (F X -> X) -> X` and I am trying to show that `unfix . fix = id`.  But it only follows that `unfix . fix` equals a certain function of type `A -> A`, namely, `\a -> a(fix)`,  that is not obviously equal to identity. What am I missing?
winitzki
CC BY-SA 4.0
2023-01-16T10:49:34.600Z
I was using dinaturality and I was missing the fact that the parametricity theorem is stronger than naturality or dinaturality. It is possible to use "strong dinaturality" to prove that `unfix . fix = id`. For that, one needs to show that "strong dinaturality" holds for type signatures `forall X. (F X -> X) -> X`. This gives a shortcut for the proof, without having to resort to fully general relational parametricity.
winitzki
CC BY-SA 4.0
2015-03-25T22:19:37.940Z
2023-01-16T13:04:35.600Z
2023-01-16T13:04:35.600Z
Andrej Bauer
<p>Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way:</p>

<pre><code>SimpleNat = (R : Set) → R → (R → R) → R

zero : SimpleNat
zero = λ R z _ → z

suc : SimpleNat → SimpleNat
suc sn = λ R z s → s (sn R z s)

SimpleNatRec : (R : Set) → R → (R → R) → SimpleNat → R
SimpleNatRec R z s sn = sn R z s
</code></pre>

<p>However, it seems that we can't define Church numerals with the following type of Induction principle:</p>

<pre><code>NatInd : (C : Nat -&gt; Set) -&gt; (C zero) -&gt; ((n : Nat) -&gt; C n -&gt; C (suc n)) -&gt; (n : Nat) -&gt; (C n)
</code></pre>

<p>Why is it so? How can I prove this? It seems that the problem is with defining a type for Nat which becomes recursive. Is it possible to amend lambda calculus to allow this?</p>

<type-theory><lambda-calculus><dependent-type>
Why it's impossible to declare an induction principle for Church numerals
Konstantin Solomatov
# Why it's impossible to declare an induction principle for Church numerals

(Asked by: username_0 on 2015-03-25)

Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way:
SimpleNat = (R : Set) → R → (R → R) → R

zero : SimpleNat
zero = λ R z _ → z

suc : SimpleNat → SimpleNat
suc sn = λ R z s → s (sn R z s)

SimpleNatRec : (R : Set) → R → (R → R) → SimpleNat → R
SimpleNatRec R z s sn = sn R z s

However, it seems that we can't define Church numerals with the following type of Induction principle:
NatInd : (C : Nat -> Set) -> (C zero) -> ((n : Nat) -> C n -> C (suc n)) -> (n : Nat) -> (C n)

Why is it so? How can I prove this? It seems that the problem is with defining a type for Nat which becomes recursive. Is it possible to amend lambda calculus to allow this?

**Tags:** type-theory, lambda-calculus, dependent-type


---

## 1 answers

### Answer by username_1 on 2015-03-25. Score: 24 | Accepted answer

The question you are asking is interesting and known. You are using the so-called impredicative encoding of the natural numbers. Let me explain a bit of the background.

Given a type constructor $T : \mathsf{Type} \to \mathsf{Type}$, we might be interested in the "minimal" type $A$ satisfying $A \cong T(A)$. In terms of category theory $T$ is a functor and $A$ is the initial $T$-algebra. For example, if $T(X) = 1 + X$ then $A$ corresponds to the natural numbers. If $T(X) = 1 + X \times X$ then $A$ is the type of finite binary trees.

An idea with long history is that the initial $T$-algebra is the type
$$A \mathrel{{:}{=}} \prod\_{X : \mathsf{Type}} (T(X) \to X) \to X.$$
(You are using Agda notation for dependent products, but I am using a more traditional mathematical notation.) Why should this be? Well, $A$ essentially encodes the recursion principle for the initial $T$-algebra: given any $T$-algebra $Y$ with a structure morphism $f : T(Y) \to Y$, we get an algebra homomorphism $\phi : A \to Y$ by
$$\phi(a) = a \, Y \, f.$$
So we see that $A$ is *weakly* initial for sure. For it to be initial we would have to know that $\phi$ is unique as well. This is not true without further assumptions, but the details are technical and nasty and require reading some background material. For instance, if we can show a satisfactory [*parametricty* theorem](http://en.wikipedia.org/wiki/Parametricity) then we win, but there are also other methods (such as massaging the definition of $A$ and assuming the $K$-axiom and function extensionality).

Let us apply the above to $T(X) = 1 + X$:
$$\mathsf{Nat} =
\prod\_{X : \mathsf{Type}} ((1 + X) \to X) \to X =
\prod\_{X : \mathsf{Type}} (X \times (X \to X)) \to X = \\
\prod\_{X : \mathsf{Type}} X \to (X \to X) \to X.
$$
We got Church numerals! And we also understand now that we will get a recursion principle for free, because the Church numerals *are* the recursion principle for numbers, but we will not get induction without parametricity or a similar device.

The tehcnical answer to your question is this: there exist models of type theory in which the type `SimpleNat` contains *exotic* elements that do not correspond to numerals, and moreover, these elements break the induction principle. The type `SimpleNat` in these models is too big and is only a *weak* initial algebra.

> **Comments:**
> **username_2**: I agree that the answer is great, but a few references might be useful here: [Geuvers' paper on non-derivability of induction](http://www.cs.ru.nl/~herman/PUBS/IndNonder.ps.gz) and [Neel K's and Derek Dreyer's paper on getting (some) induction from parametricity](https://www.mpi-sws.org/~neelk/final-csl-internalizing-parametricity.pdf). I'm not aware of a paper that fully explores the relationship though.  
> **username_1**: I am not too strong on references in this area, thanks @username_2!  
> **username_3**: @AndrejBauer I have tried to derive that `A = forall X. (F X -> X) -> X` is the initial F-algebra by using parametricity but I don't seem to get quite the right result. There are easily written implementations of functions `fix: F A -> A` and `unfix: A -> F A`. I am using the parametricity theorem for the type signature `forall X. (F X -> X) -> X` and I am trying to show that `unfix . fix = id`.  But it only follows that `unfix . fix` equals a certain function of type `A -> A`, namely, `\a -> a(fix)`,  that is not obviously equal to identity. What am I missing?  
> **username_3**: I was using dinaturality and I was missing the fact that the parametricity theorem is stronger than naturality or dinaturality. It is possible to use "strong dinaturality" to prove that `unfix . fix = id`. For that, one needs to show that "strong dinaturality" holds for type signatures `forall X. (F X -> X) -> X`. This gives a shortcut for the proof, without having to resort to fully general relational parametricity.  

---

