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?


1 Answer 1


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 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.

  • 10
    $\begingroup$ I agree that the answer is great, but a few references might be useful here: Geuvers' paper on non-derivability of induction and Neel K's and Derek Dreyer's paper on getting (some) induction from parametricity. I'm not aware of a paper that fully explores the relationship though. $\endgroup$
    – cody
    Commented Mar 27, 2015 at 16:40
  • 1
    $\begingroup$ I am not too strong on references in this area, thanks @cody! $\endgroup$ Commented Mar 27, 2015 at 18:05
  • $\begingroup$ @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? $\endgroup$
    – winitzki
    Commented Nov 1, 2020 at 22:30
  • $\begingroup$ 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. $\endgroup$
    – winitzki
    Commented Jan 16, 2023 at 10:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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