Incomputer science andmathematical logic, afunction type (orarrow type orexponential) is the type of avariable orparameter to which afunction has or can be assigned, or an argument or result type of ahigher-order 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 unappliedtype constructor· → ·, is ahigher-kinded type). In theoretical settings andprogramming languages where functions are defined incurried form, such as thesimply typed lambda calculus, a function type depends on exactly two types, thedomainA and therangeB. Here a function type is often denotedA →B, following mathematical convention, orBA, based on there existing exactlyBA (exponentially many)set-theoretic functions mappingsA toB in thecategory of sets. The class of such maps or functions is called theexponential object. The act ofcurrying makes the function typeadjoint to theproduct type; this is explored in detail in the article on currying.
The function type can be considered to be a special case of thedependent product type, which among other properties, encompasses the idea of apolymorphic function.
The syntax used for function types in several programming languages can be summarized, including an example type signature for the higher-orderfunction composition function:
| Language | Notation | Exampletype signature | |
|---|---|---|---|
| Withfirst-class functions, parametric polymorphism | C# | Func<α1,α2,...,αn,ρ> | Func<A,C>compose(Func<B,C>f,Func<A,B>g); |
| Haskell | α ->ρ | compose::(b->c)->(a->b)->a->c | |
| OCaml | α ->ρ | compose:('b->'c)->('a->'b)->'a->'c | |
| Scala | (α1,α2,...,αn) =>ρ | defcompose[A,B,C](f:B=>C,g:A=>B):A=>C | |
| Standard ML | α ->ρ | compose:('b->'c)->('a->'b)->'a->'c | |
| Swift | α ->ρ | funccompose<A,B,C>(f:(B)->C,g:(A)->B)->(A)->C | |
| Rust | fn(α1,α2,...,αn) ->ρ | fncompose<A,B,C>(f:fn(A)->B,g:fn(B)->C)->fn(A)->C | |
| Withfirst-class functions, withoutparametric polymorphism | Go | func(α1,α2,...,αn)ρ | varcomposefunc(func(int)int,func(int)int)func(int)int |
| C++,Objective-C, withblocks | ρ (^)(α1,α2,...,αn) | int(^compose(int(^f)(int),int(^g)(int)))(int); | |
| Withoutfirst-class functions, parametric polymorphism | C | ρ (*)(α1,α2,...,αn) | int(*compose(int(*f)(int),int(*g)(int)))(int); |
| C++11 | Not unique.
| function<function<int(int)>(function<int(int)>,function<int(int)>)>compose; | |
When looking at the example type signature of, for example C#, the type of the functioncompose is actuallyFunc<Func<A,B>,Func<B,C>,Func<A,C>>.
Due totype erasure in C++11'sstd::function, it is more common to usetemplates forhigher order function parameters andtype inference (auto) forclosures.
The function type in programming languages does not correspond to the space of all set-theoretic functions. Given thecountably infinite type ofnatural numbers as the domain and the Booleans as range, then there are anuncountably 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 thehalting problem.
Denotational semantics concerns itself with finding more appropriate models (calleddomains) to model programming language concepts such as function types. It turns out that restricting expression to the set ofcomputable functions is not sufficient either if the programming language allows writingnon-terminating computations (which is the case if the programming language isTuring complete). Expression must be restricted to the so-calledcontinuous functions (corresponding to continuity in theScott topology, not continuity in the real analytical sense). Even then, the set of continuous function contains theparallel-or function, which cannot be correctly defined in all programming languages.[clarification needed]