The meaning and relevance of the locution ''no terminating implementation'' in type theory
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 &quot;implementation&quot; 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 &quot;terminating&quot; 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).