Skip to main content
Share Your Experience: Take the 2024 Developer Survey
9 votes

Example of a term in system F which is not typable in the simply typed lambda calculus

Reacting to the previous answers, I think this is the simplest self-application which only contains types which have closed inhabitants. $$\lambda\,(f\,:\,\forall\,\alpha.\,\alpha\to\alpha).\,f\,(\...
András Kovács's user avatar
7 votes

Example of a term in system F which is not typable in the simply typed lambda calculus

Damiano Mazza's example uses an uninhabited type, $∀ X ⋅ X$. It is correct, but raises the obvious question whether one can do without. Here is an example that I find quite natural: $$Λ \ A B ⋅ λ \ (p ...
Jean Abou Samra's user avatar
7 votes
Accepted

Example of a term in system F which is not typable in the simply typed lambda calculus

Every normal term may be typed in system F (I can't seem to find a reference now, I'll come back with one when I have some more time). So, for example, letting $A:=\forall X.X$, then $$x^A(A\to\alpha)...
Damiano Mazza's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible