# From Church-encoding to induction principle

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?

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.

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.

• 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 Feb 20 '20 at 11:29
• 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 Feb 20 '20 at 19:08
• 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 Feb 21 '20 at 8:22