The meaning and relevance of the locution ''no terminating implementation'' in type theory

Question

In the context of a discussion of Haskell https://stackoverflow.com/questions/62509788/the-intuition-behind-the-definition-of-the-co-reader-monad, I was told that

There is no terminating implementation for the polymorphic type $(e \to a) \to a$

and that we couldn't have a function of type $((e \to a) \to a) \to e$ or a function of type $(r \to x) \to x$, for these would not be ''implementable''.

These types are well formed in the STLC, in the sense that we can construct them using the rules of type-formation. And I don't see why we can't form lambda terms of this shape, such as $\lambda c_{((a \to t) \to t)}. \, b_a$, or $\lambda p_{e \to a}.\,b_a$.

What is therefore the problem? Specifically, what is a ''terminating implementation'' in the context of the STLC? I believe this relates to the fact that $(e \to \bot) \to \bot$ is not constructively equivalent to $e$, but I would appreciate if someone could spell this out for me.

Answer 1

You can always inhabit a type by a free variable: the type $\tau$ is inhabited by the free variable $x_\tau$. When people speak about "implementation" of a type they mean a closed term, i.e., one without free variables. The examples you gave contain free variables, namely $b_a$.

In pure simply-typed $\lambda$-calculus all terms are "terminating" in the sense that the calculus is strongly normalizing, so whatever reductions you take they will always lead to the (unique) normal form.

In $\lambda$-calculus extended with recursive definitions (such as Haskell) we can inhabit every type $\tau$ with a closed term, for instance in Haskell the type t is inhabited by a defined as

a :: t
a = a

Once we have recursive definitions, it is easy to write closed terms that do not terminate (or do not have a normal form).