<p>Let <span class="math-container">$F : \mathsf{Type} \to \mathsf{Type}$</span> be a type constructor and let <span class="math-container">$W_F$</span> be the inductive type defined by <span class="math-container">$W_F = F W_F$</span>. Not every <span class="math-container">$F$</span> has such an inductive types, but this is not important for this discussion.</p>

<p>The starting point of Church's encodings is the observation that <span class="math-container">$W_F$</span> ought to be
<span class="math-container">$$\forall T : \mathsf{Type} \,.\, (F T \to T) \to T.$$</span>
Thus, to get an induction principle out of a Church encoding, we take the following steps:</p>

<ol>
<li>Rewrite the Church encoding in the form <span class="math-container">$\forall T : \mathsf{Type} \,.\, (F T \to T) \to T$</span> for a suitable <span class="math-container">$F$</span>.</li>
<li>Derive an induction principle for <span class="math-container">$F$</span>, as in <a href="https://cstheory.stackexchange.com/a/46270/7050">your own answer to your own question</a>.</li>
</ol>

<p>Let us try a couple of examples.</p>

<h3>Unit type</h3>

<p><span class="math-container">\begin{align*}
\mathsf{unit} &amp;= \forall T . T \to T \\
&amp;= \forall T . (1 \to T) \to T \\
&amp;= \forall T . (F T \to T) \to T
\end{align*}</span>
where <span class="math-container">$F X = 1$</span>.</p>

<h3>Empty type</h3>

<p><span class="math-container">\begin{align*}
\mathsf{unit} &amp;= \forall T . T \\
&amp;= \forall T . 1 \to T \\
&amp;= \forall T . (0 \to T) \to T \\
&amp;= \forall T . (F T \to T) \to T
\end{align*}</span>
where <span class="math-container">$F X = 0$</span>.</p>

<h3>Natural numbers</h3>

<p><span class="math-container">\begin{align*}
\mathsf{nat} &amp;= \forall T . (T \to T) \to (T \to T) \\
&amp;= \forall T . (T \to T) \times T \to T \\
&amp;= \forall T . T \times (T \to T) \to T \\
&amp;= \forall T . ((1 + T) \to T) \to T \\
&amp;= \forall T . (F T \to T) \to T
\end{align*}</span>
where <span class="math-container">$F X = 1 + X$</span>.</p>

<h3>Binary trees</h3>

<p>We can also go backwards. The binary trees are the inductive type for <span class="math-container">$F X = 1 + X \times X$</span>, thus their Church encoding is</p>

<p><span class="math-container">\begin{align*}
\mathsf{tree} &amp;= \forall T . (F T \to T) \to T \\
&amp;= \forall T . ((1 + T \times T) \to T) \to T \\
&amp;= \forall T . (T \times (T \times T \to T) \to T \\
&amp;= \forall T . T \to (T \to T \to T) \to T
\end{align*}</span></p>

<p>It all works beautifully.</p>

CC BY-SA 4.0
2020-02-20T11:29:29.793Z
I wonder, the definition of Unit above relies already on `1` and so you already need induction on unit (and sums and products) to use this method.
Labbekak
CC BY-SA 4.0
2020-02-20T19:08:49.743Z
Correct. There might be a way to improve, I think. The Church encoding already *is* the non-dependent elimination principle, so we just have to figure out how to throw in dependencies.
Andrej Bauer
CC BY-SA 4.0
2020-02-21T08:22:45.737Z
I think that's what Self types and the Cedille language can do, but it's kind of tricky and only seems to work for a Curry-style system.
Labbekak
CC BY-SA 4.0
2020-02-15T21:03:25.400Z
2020-02-15T21:03:25.400Z
Andrej Bauer
<p>I am looking for an algorithm to go from a Church-encoded datatype to their induction principle in the Calculus of Constructions. For example:</p>

<pre><code>Unit = {t : *} -&gt; t -&gt; t
~&gt;
(x : Unit) -&gt; {P : Unit -&gt; *} -&gt; P (\{t} x. x) -&gt; P x
</code></pre>

<pre><code>Nat = {t : *} -&gt; t -&gt; (t -&gt; t) -&gt; t
~&gt;
(x : Nat) -&gt; {P : Nat -&gt; *} -&gt; P (\{t} z s. z) -&gt; ({m : Nat} -&gt; P m -&gt; P (\{t} z s. s (m {t} z s))) -&gt; P x
</code></pre>

<p>It seems like this should be possible for any Church-encoded datatype. Does anybody know such an algorithm/translation or resources on it?</p>

<type-theory><calculus-of-constructions><inductive-type>
From Church-encoding to induction principle
Labbekak
# From Church-encoding to induction principle

(Asked by: username_0 on 2020-02-15)

I am looking for an algorithm to go from a Church-encoded datatype to their induction principle in the Calculus of Constructions. For example:
Unit = {t : *} -> t -> t
~>
(x : Unit) -> {P : Unit -> *} -> P (\{t} x. x) -> P x

Nat = {t : *} -> t -> (t -> t) -> t
~>
(x : Nat) -> {P : Nat -> *} -> P (\{t} z s. z) -> ({m : Nat} -> P m -> P (\{t} z s. s (m {t} z s))) -> P x

It seems like this should be possible for any Church-encoded datatype. Does anybody know such an algorithm/translation or resources on it?

**Tags:** type-theory, calculus-of-constructions, inductive-type


---

## 1 answers

### Answer by username_1 on 2020-02-15. Score: 6 | Accepted answer

Let $F : \mathsf{Type} \to \mathsf{Type}$ be a type constructor and let $W\_F$ be the inductive type defined by $W\_F = F W\_F$. Not every $F$ has such an inductive types, but this is not important for this discussion.

The starting point of Church's encodings is the observation that $W\_F$ ought to be
$$\forall T : \mathsf{Type} \,.\, (F T \to T) \to T.$$
Thus, to get an induction principle out of a Church encoding, we take the following steps:

1. Rewrite the Church encoding in the form $\forall T : \mathsf{Type} \,.\, (F T \to T) \to T$ for a suitable $F$.
2. Derive an induction principle for $F$, as in [your own answer to your own question](https://cstheory.stackexchange.com/a/46270/7050).

Let us try a couple of examples.

### Unit type

\begin{align\*}
\mathsf{unit} &= \forall T . T \to T \\
&= \forall T . (1 \to T) \to T \\
&= \forall T . (F T \to T) \to T
\end{align\*}
where $F X = 1$.

### Empty type

\begin{align\*}
\mathsf{unit} &= \forall T . T \\
&= \forall T . 1 \to T \\
&= \forall T . (0 \to T) \to T \\
&= \forall T . (F T \to T) \to T
\end{align\*}
where $F X = 0$.

### Natural numbers

\begin{align\*}
\mathsf{nat} &= \forall T . (T \to T) \to (T \to T) \\
&= \forall T . (T \to T) \times T \to T \\
&= \forall T . T \times (T \to T) \to T \\
&= \forall T . ((1 + T) \to T) \to T \\
&= \forall T . (F T \to T) \to T
\end{align\*}
where $F X = 1 + X$.

### Binary trees

We can also go backwards. The binary trees are the inductive type for $F X = 1 + X \times X$, thus their Church encoding is

\begin{align\*}
\mathsf{tree} &= \forall T . (F T \to T) \to T \\
&= \forall T . ((1 + T \times T) \to T) \to T \\
&= \forall T . (T \times (T \times T \to T) \to T \\
&= \forall T . T \to (T \to T \to T) \to T
\end{align\*}

It all works beautifully.

> **Comments:**
> **username_0**: I wonder, the definition of Unit above relies already on `1` and so you already need induction on unit (and sums and products) to use this method.  
> **username_1**: Correct. There might be a way to improve, I think. The Church encoding already *is* the non-dependent elimination principle, so we just have to figure out how to throw in dependencies.  
> **username_0**: I think that's what Self types and the Cedille language can do, but it's kind of tricky and only seems to work for a Curry-style system.  

---

