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.


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).

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.