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 the result type of a higher-order function 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 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 BA, based on the fact that there exist exactly BA (exponentially many) set-theoretic 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 higher-order function composition function:
| Language | Notation | Example type signature | |
|---|---|---|---|
| With first-class functions, parametric polymorphism |
C++11 | std::function<ρ (α1,α2,...,αn)>
|
function<function<int(int)>(function<int(int)>, function<int(int)>)> compose;
|
| C# | Func<α1,α2,...,αn,ρ>
|
Func<A,C> compose(Func<A,B> f, Func<B,C> g);
| |
| Go | func(α1,α2,...,αn) ρ
|
var compose func(func(int)int, func(int)int) func(int)int
| |
| Haskell | α -> ρ
|
compose :: (a -> b) -> (b -> c) -> a -> c
| |
| Objective-C/C/C++ with Blocks | ρ (^)(α1,α2,...,αn)
|
int (^compose(int (^f)(int), int (^g)(int)))(int);
| |
| OCaml | α -> ρ
|
compose : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
| |
| Scala | (α1,α2,...,αn) => ρ
|
def compose[A, B, C](f: B => C, g: A => B): A => C
| |
| Standard ML | α -> ρ
|
compose : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
| |
| Without first-class functions, parametric polymorphism |
C | ρ (*)(α1,α2,...,αn)
|
int (*compose(int (*f)(int), int (*g)(int)))(int);
|
When looking at the example type signature of for example C#, one should note that the type of the function compose is actually Func<Func<A,B>,Func<B,C>,Func<A,C>>.
Von Manalac </3
See also
- Cartesian closed category
- Currying
- Exponential object, category-theoretic equivalent
- First-class function
- Function space, set-theoretic equivalent
References
- Pierce, Benjamin C. Types and Programming Languages. The MIT Press. pp. 99–100.
- Mitchell, John C. Foundations for Programming Languages. The MIT Press.
- function type at the nLab
- Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study. See section 1.2.