"Recursive types for free!" -- But doesn't this contradict the fact that $\mathbb{N} \notin \mathbf{FinSet}$?

Question

From what I understand based on Philip Wadler's comment, polymorphic lambda calculus has least fixed points for all its covariant endofunctors. Here's a quote:

Thus, it is safe to extend the polymorphic lambda calculus by adding least fixpoint types with type variables in positive position. Indeed, no extension is required: such types already exist in the language! If $F X$ represents a type containing $X$ in positive position only, then least fixpoints may be defined in terms of universal quantification:

$$\mathrm{Lfix}_X F X = \forall X[(F X \rightarrow X) \rightarrow X]$$

On so many levels, I don't get this, but to keep this question brief I'll just emphasize one thing that's bugging me about it. A special case of Philip Wadler's comment is that $$\mathbb{N} \cong \forall X[(1+X \rightarrow X) \rightarrow X].$$ But if this is true, then it means that $\mathbf{FinSet}$ can't interpret the polymorphic lambda calculus with sum types. But surely it can, because polymorphic lambda calculus is just like the simply typed calculus, but with type variables and a mechanism for doing generics? What am I missing here?

Answer 1

I am not sure what is the source of confusion here exactly, so let me note some things:

First, the following two statements are not contradictory

1. A type theory has an infinite type, i.e. a type with infinite number of judgementally distinct closed terms.
2. A type theory has a model where closed types are finite sets.

Example: simply typed lambda calculus with an empty base type ι. It has the type (ι → ι) → (ι → ι) with countably infinite closed terms, and also a model where ι is the empty set, hence all types are finite sets.

In the other direction, we can also interpret ι as the set of natural numbers. So, having finite set models doesn't say much about finiteness of syntactic types.

Also, note that the relation between polymorphic LC (or: System F) and simply typed LC is rather tenuous. The former is not merely the latter with some features thrown in. The expressive power of System F is vastly beyond STLC. The proof-theoretic strength of System F is the same as that of second-order arithmetic, with no known combinatorial description.