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.

  • 1
    $\begingroup$ 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. $\endgroup$ – Labbekak Feb 20 '20 at 11:29
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Feb 20 '20 at 19:08
  • 1
    $\begingroup$ 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. $\endgroup$ – Labbekak Feb 21 '20 at 8:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.