Function type
In computer science, a function type (also 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 higherorder function 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 higherkinded type). In theoretical settings and 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 A → B, following mathematical convention, or B^{A}, based on the fact that there exist exactly B^{A} (exponentially many) settheoretic functions mapping A to B.
The function type can be considered to be a special case of the dependent product type. Among other properties, the dependent product type encompasses the idea of a polymorphic function.
Programming languages
The following table summarized the syntax used for function types in several programming languages, including an example type signature for the higherorder function composition function:
Language  Notation  Example type signature  

With firstclass functions, parametric polymorphism 
C#  Func<α_{1},α_{2},...,α_{n},ρ> 

Haskell  α > ρ 


OCaml  α > ρ 


Scala  (α_{1},α_{2},...,α_{n}) => ρ 


Standard ML  α > ρ 


Swift  α > ρ 


With firstclass functions, without parametric polymorphism 
Go  func(α_{1},α_{2},...,α_{n}) ρ 

ObjectiveC/C/C++ with Blocks  ρ (^)(α_{1},α_{2},...,α_{n}) 


Without firstclass functions, parametric polymorphism 
C  ρ (*)(α_{1},α_{2},...,α_{n}) 

C++11  Not unique.


When looking at the example type signature of for example C#, one should note that the type of the function
is actually compose
Func<Func<A,B>,Func<B,C>,Func<A,C>>
.
Note that because of type erased nature of C++11's std::function
, it is more common to use templates for higher order function parameters and type inference (auto
) for closures.
Denotational semantics
The function type in programming languages does not correspond to the space of all settheoretic functions. If we take the countably infinite type of natural numbers as the domain and the booleans as range, then there are an uncountably infinite number (2^{ℵ0} = c) of settheoretic functions between them. Clearly this space of functions is larger than the number of functions we can define 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 settheoretic functions effectively solves the halting problem.
Denotational semantics concerns itself with finding more appropriate models (called domains) to model programming language concepts such as function types. It turns out that restricting ourselves to the set of computable functions is not sufficient either if the programming language allows us to write nonterminating computations (which is the case if the programming language is Turing complete). We need to restrict ourselves to the socalled 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 parallelor function, which cannot be correctly defined in all programming languages.
See also
 Cartesian closed category
 Currying
 Exponential object, categorytheoretic equivalent
 Firstclass function
 Function space, settheoretic equivalent
References
 Pierce, Benjamin C. Types and Programming Languages. The MIT Press. pp. 99–100.<templatestyles src="Module:Citation/CS1/styles.css"></templatestyles>
 Mitchell, John C. Foundations for Programming Languages. The MIT Press.<templatestyles src="Module:Citation/CS1/styles.css"></templatestyles>
 function type in nLab
 Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study. See section 1.2.