In computer science, 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 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 A and the range B. Here a function type is often denoted A → B, following mathematical convention, or BA, based on there existing exactly BA (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 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. Contents 1 Programming languages 2 Denotational semantics 3 See also 4 References Programming languages[edit] 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: Language Notation Example type signature With first-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) => ρ def compose[A, B, C](f: B => C, g: A => B): A => C Standard ML α -> ρ compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c Swift α -> ρ func compose<A,B,C>(f: B -> C, g: A -> B) -> A -> C With first-class functions, without parametric polymorphism Go func(α1,α2,...,αn) ρ var compose func(func(int)int, func(int)int) func(int)int C, C++, Objective-C, with blocks ρ (^)(α1,α2,...,αn) int (^compose(int (^f)(int), int (^g)(int)))(int); Without first-class functions, parametric polymorphism C ρ (*)(α1,α2,...,αn) int (*compose(int (*f)(int), int (*g)(int)))(int); C++11 Not unique. std::function<ρ (α1,α2,...,αn)> is the more general type (see below). 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 function compose is actually
Func<Func<A,B>,Func<B,C>,Func<A,C>>.
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
(auto) for closures.
Denotational semantics[edit]
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 (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.
Cartesian closed category Currying Exponential object, category-theoretic equivalent First-class function Function space, set-theoretic equivalent References[edit] 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 in nLab Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study. See section 1.2. v t e Data types Uninterpreted Bit
Byte
Trit
Tryte
Word
Numeric Arbitrary-precision or bignum Complex Decimal Fixed point Floating point Double precision Extended precision Half precision Long double Minifloat Octuple precision Quadruple precision Single precision Integer signedness Interval Rational Pointer Address physical virtual Reference Text Character String null-terminated Composite Algebraic data type generalized Array Associative array Class Dependent Equality Inductive List Object metaobject Option type Product Record Set Union tagged Other Boolean Bottom type Collection Enumerated type Exception Function type Opaque data type Recursive data type Semaphore Stream Top type Type class Unit type Void Related topics Abstract data type Data structure Generic Kind metaclass Parametric polymorphism Primitive data type Protocol interface Subtyping Type constructor Type conversion Type system Type theory See also platform-dependent and independent un |