Function type


In computer science, a function type is the type of a variable or parameter to which a function has or can be assigned, or an argument or result type of a higher-order function taking or returning a function.
A function type depends on the type of the parameters and the result type of the function. In theoretical settings and programming languages where functions are defined in curried form, such as the simply typed lambda calculus, a function type depends on exactly two types, the domain A and the range B. Here a function type is often denoted, following mathematical convention, or, based on there existing exactly set-theoretic functions mappings A to B in the category of sets. The class of such maps or functions is called the exponential object. The act of currying makes the function type adjoint to the product type; this is explored in detail in the article on currying.
The function type can be considered to be a special case of the dependent product type, which among other properties, encompasses the idea of a polymorphic function.

Programming languages

The syntax used for function types in several programming languages can be summarized, including an example type signature for the higher-order function composition function:
When looking at the example type signature of, for example C#, the type of the function is actually Func,Func<B,C>,Func>.
Due to type erasure in C++11's std::function, it is more common to use templates for higher order function parameters and type inference for closures.

Denotational semantics

The function type in programming languages does not correspond to the space of all set-theoretic functions. Given the countably infinite type of natural numbers as the domain and the booleans as range, then there are an uncountably infinite number of set-theoretic functions between them. Clearly this space of functions is larger than the number of functions that can be defined in any programming language, as there exist only countably many programs and one of the set-theoretic functions effectively solves the halting problem.
Denotational semantics concerns itself with finding more appropriate models to model programming language concepts such as function types. It turns out that restricting expression to the set of computable functions is not sufficient either if the programming language allows writing non-terminating computations. Expression must be restricted to the so-called continuous functions. Even then, the set of continuous function contains the parallel-or function, which cannot be correctly defined in all programming languages.