In
computer science and
mathematical logic, a function type (or arrow type or exponential) 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
In mathematics and computer science, a higher-order function (HOF) is a function that does at least one of the following:
* takes one or more functions as arguments (i.e. a procedural parameter, which is a parameter of a procedure that is itself ...
taking or returning a function.
A function type depends on the type of the parameters and the result type of the function (it, or more accurately the unapplied
type constructor , is a
higher-kinded type). 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
Domain may refer to:
Mathematics
*Domain of a function, the set of input values for which the (total) function is defined
**Domain of definition of a partial function
**Natural domain of a partial function
**Domain of holomorphy of a function
* Do ...
''A'' and the
range ''B''. Here a function type is often denoted , following mathematical convention, or , based on there existing exactly (exponentially many)
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
In mathematics and computer science, currying is the technique of translating the evaluation of a function that takes multiple arguments into evaluating a sequence of functions, each with a single argument. For example, currying a function f that ...
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
In programming language theory and type theory, polymorphism is the provision of a single interface (computing), interface to entities of different Data type, types or the use of a single symbol to represent multiple different types.: "Polymorph ...
.
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
In mathematics, function composition is an operation that takes two functions and , and produces a function such that . In this operation, the function is applied to the result of applying the function to . That is, the functions and ...
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
In mathematics and computer science, a higher-order function (HOF) is a function that does at least one of the following:
* takes one or more functions as arguments (i.e. a procedural parameter, which is a parameter of a procedure that is itsel ...
parameters and
type inference (
auto) 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
In mathematics, a set is countable if either it is finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function from it into the natural numbers; ...
type of
natural numbers as the domain and the booleans as range, then there are an
uncountably infinite number (2
ℵ0 =
c) 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 (a program being a finite sequence of a finite number of symbols) and one of the set-theoretic functions effectively solves the
halting problem.
Denotational semantics
In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called ''denotations'' ...
concerns itself with finding more appropriate models (called
domains) 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 (which is the case if the programming language is
Turing complete). Expression must be restricted to the so-called ''
continuous functions'' (corresponding to continuity in the
Scott topology, not continuity in the real analytical sense). Even then, the set of continuous function contains the ''parallel-or'' function, which cannot be correctly defined in all programming languages.
See also
*
Cartesian closed category
*
Currying
In mathematics and computer science, currying is the technique of translating the evaluation of a function that takes multiple arguments into evaluating a sequence of functions, each with a single argument. For example, currying a function f that ...
*
Exponential object, category-theoretic equivalent
*
First-class function
*
Function space
In mathematics, a function space is a set of functions between two fixed sets. Often, the domain and/or codomain will have additional structure which is inherited by the function space. For example, the set of functions from any set into a vect ...
, set-theoretic equivalent
References
*
*
*
''Homotopy Type Theory: Univalent Foundations of Mathematics'', The Univalent Foundations Program, Institute for Advanced Study ''See section 1.2''.
{{Data types
Data types
Subroutines
Type theory