= Function type
{title2=$\tau_1\to\tau_2$}
{wiki}
A <function type> $\tau_1\to\tau_2$ classifies functions that accept arguments of type $\tau_1$ and produce results of type $\tau_2$ if they return. For example, $\lambda x.x+1$ has <function type> $\mathrm{int}\to\mathrm{int}$ in our teaching <programming language>, while $\lambda b.\mathrm{if}\ b\ \mathrm{then}\ 1\ \mathrm{else}\ 2$ has <function type> $\mathrm{bool}\to\mathrm{int}$. A <function type> specifies how a function may be used; it does not guarantee that a call returns.
\Image[/function-typechecking-tree.png]
{title=Checking an integer function call from its parts}
{description=An addition rule checks the body of a <lambda abstraction>, the abstraction rule gives its <function type>, and <lambda application> checks the argument and obtains the result type. Arrows run from prerequisite <typing judgments> to their conclusions.}
The two central <typing judgment> rules are
$$
\frac{\Gamma,x:\tau_1\vdash e:\tau_2}{\Gamma\vdash\lambda x.e:\tau_1\to\tau_2},\qquad
\frac{\Gamma\vdash f:\tau_1\to\tau_2\qquad\Gamma\vdash a:\tau_1}{\Gamma\vdash f\,a:\tau_2}.
$$
The <lambda abstraction> rule checks the body under an extended <typing context>; the <lambda application> rule checks that the argument has exactly the required type. These rules describe our <simple type> examples. https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html[Software Foundations, Programming Language Foundations, The Simply Typed Lambda-Calculus: typing rules]{ref}
For $(\lambda x.x+1)\,3$, assume $x:\mathrm{int}$; both $x$ and $1$ have type `int`, so $x+1$ has type `int`. The abstraction therefore has <function type> $\mathrm{int}\to\mathrm{int}$. Since $3$ has type `int`, the call has type `int` and evaluates to $4$. Replacing $3$ by `true` fails the argument requirement. This local derivation explains each step without running the program.
Arrows associate to the right: $\tau_1\to\tau_2\to\tau_3$ means $\tau_1\to(\tau_2\to\tau_3)$, a function returning another function. For instance, $\lambda x.\lambda y.x+y$ has <function type> $\mathrm{int}\to(\mathrm{int}\to\mathrm{int})$. Supplying one <integer> yields a function awaiting the second. Functions can also be arguments: $(\mathrm{int}\to\mathrm{int})\to\mathrm{int}$ accepts an <integer>-to-<integer> function and has an <integer> result type.
// Target: computer-science.bigb
Back to article page
