# Why are recursive types needed as primitives for proofs in dependent type systems?

I'm relatively new to type theory and dependent programming. I've been studying the calculus of constructions (CoC) and other pure type systems. I'm particularly interested in using it as a proof-preserving intermediate representation for a compiler system.

I understand that (co-)recursive types are representable, computationally, using $\Pi$ as the only type constructor. I've read, though, that they cannot be used to build proofs by induction (forgive me, I can't find where now!), e.g., that I couldn't prove that $0\neq 1$ in plain CoC (even though $\texttt{Nat}$ is typeable as $\Pi(\mathbb{N}:*).\Pi(S:\mathbb{N}\rightarrow\mathbb{N}).\Pi(Z:\mathbb{N}).\mathbb{N}$).

I assume this is why they built the calculus of inductive constructions (CIC). Is this correct? But why? I couldn't find any material explaining why such proofs cannot be represented without using (co-)inductive types as primitives. If this is not true, then why add them as primitives in CIC?

I'm not an expert, but I'll share what I understood so far with an example.

Let's consider the boolean type in CoC, using its standard encoding: $$\begin{array}{l} \mathbb{B} = \Pi_{\tau:*} \tau \to \tau \to \tau \\ \mathsf{tt} = \lambda \tau:*,x:\tau,y:\tau.\ x \\ \mathsf{ff} = \lambda \tau:*,x:\tau,y:\tau.\ y \end{array}$$ We might expect to be able to prove $$\Pi_{b : \mathbb{B}} b={\sf tt} \lor b = {\sf ff} \qquad(*)$$ Indeed, this quickly follows from the dependent elimination/induction principle we have e.g. in CiC $$\mathbb{B}_{ind} : \Pi_{P:\mathbb{B}\to*} P({\sf tt}) \rightarrow P({\sf ff}) \rightarrow \Pi_{b:\mathbb{B}} P(b)$$

However, we can not really expect (*) to hold in all models of CoC! Intuitively, a value in $\mathbb{B}$ should roughly be a family of functions $\{f_\tau\}_{\tau}$ assigning to each type $\tau$ a value in the interpretation of $\tau\to\tau\to\tau$. But this does not force $f_\tau$ to be one between the values of $\sf tt,ff$. We could have e.g. (informally) $$f_{\mathbb{N}}(n)(m) = n+m$$

To be sure that the values of $\sf tt,ff$ are the only possible values, we need to restrict ourselves to parametric models. Indeed (I think) the property $(*)$ can be proven from the free theorem associated to the polytype $\mathbb{B}$.

However, as far as I understand, CoC does not rule out ad-hoc models, where parametricity does not hold. In some of those, $(*)$ is simply false. By soundness, in the presence of a countermodel, we conclude that $(*)$ is not inhabited in CoC. Consequently, there's no $\mathbb{B}_{ind}$ term in CoC, either.

• I'm not sure I follow. For example, given an expression as $(\lambda(Nat:*).(...)) (\Pi(\mathbb{N}:*).\Pi(S:\mathbb{N}\rightarrow\mathbb{N}).\Pi(Z:\mathbb{N}).\mathbb{N})$, there are many ways that I could make constructors for Nat, but, ultimately, wouldn't them all be built up from either $S$ or $Z$? – paulotorrens Jan 6 '17 at 18:01
• @paulotorrens Inside the logic, yes, I believe that these are the only options. But in a model of CoC (an ad-hoc model), there might be values of $Nat$ which can not be defined through $S,Z$. Think of a natural value $n$ such that $n(T)(S_T)(Z_T) = Z_T$ for all types $T$ except for $T=\mathbb{B}$ where instead $n(\mathbb{B})(S)(Z) = S(Z)$. The value $n$ behaves as "zero" on most types, and as "one" for booleans. We can't write $\lambda T:*. {\sf if}\ T=\mathbb{B}\ {\sf then}\ \ldots$ in CoC to define that value $n$, but in an ad-hoc model that value might be present nevertheless. – chi Jan 6 '17 at 22:04
• @paulotorrens Maybe you can understand the issue more easily if you think about $\Pi_{T:*} T\to T$. This type is only inhabited by (polymorphic) identity, and in parametric models that's indeed the only possible value for terms of that type. But, in an ad-hoc model, we might define a value $v(T)(x) = x$ for all types $T$ but for $T=\mathbb{N}$ where $v(\mathbb{N})(x) = x+1$. – chi Jan 6 '17 at 22:08