Function type (${\tau }_1\to {\tau }_2$)

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.

The two central typing judgment rules areThe 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. ^[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

A data type describing a callable procedure's parameter types and any return type. A traversal callback taking an integer and producing no data result can be passed using an Oberon declaration such as Visit = PROCEDURE(x: INTEGER).

A procedure passed as an argument to another procedure. For a nested procedure under lexical scope, the argument must preserve both its code and its defining environment, for example as a programming closure.

If $A^{\prime }<:A$ and $B<:B^{\prime }$, a function of type $A\to B$ safely supplies a contract of type $A^{\prime }\to B^{\prime }$. Every input permitted by the new contract is already accepted, and every possible returned value meets the weakened result promise. This proves contravariance of inputs and covariance of outputs. Reversing either direction can respectively supply an unsupported input or promise a result more specific than the implementation returns. A language's generic type object constructor may nevertheless be invariant unless its declaration exposes the appropriate variance.