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

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.

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