# Tag Info

14

$\mathsf{id}$ and $\mathsf{const}$ are not variables of the calculus, but syntactic sugar for $\lambda x \rightarrow x$ and $\lambda x \rightarrow \lambda y \rightarrow x$ respectively. This is stated at the end of §2.2 and subtly conveyed by the use of a sans-serif font rather than italics (this is a typographic convention of this particular document, not a ...

7

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

7


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