Function type
Encyclopedia
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.
function:
When looking at the example type signature of for example C#, one should note that the type of the function
s as the domain and the boolean
s 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 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 set-theoretic 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 function
s is not sufficient either if the programming language allows us to write non-terminating computations (which is the case if the programming language is Turing complete). We need to restrict ourselves 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.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, a function type (also arrow type or exponential) is the type of a variable or parameter
Parameter (computer science)
In computer programming, a parameter is a special kind of variable, used in a subroutine to refer to one of the pieces of data provided as input to the subroutine. These pieces of data are called arguments...
to which a function has or can be assigned or the result type of a higher-order function
Higher-order function
In mathematics and computer science, higher-order functions, functional forms, or functionals are functions which do at least one of the following:*take one or more functions as an input*output a 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
Type constructor
In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old. Typical type constructors encountered are product types, function types, power types and list types. Basic types are considered...
· → ·, is a higher-kinded type). In theoretical settings and languages where functions are defined in curried form, such as the simply typed lambda calculus
Simply typed lambda calculus
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a 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.
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 compositionFunction composition (computer science)
In computer science, function composition is an act or mechanism to combine simple functions to build more complicated ones...
function:
| Language | Notation | Example type signature Type signature In computer science, a type signature or type annotation defines the inputs and outputs for a function, subroutine or method. A type signature includes at least the function name and the number of its arguments... |
|
|---|---|---|---|
| With first-class function First-class function In computer science, a programming language is said to have first-class functions if it treats functions as first-class objects. Specifically, this means that the language supports passing functions as arguments to other functions, returning them as the values from other functions, and assigning... s, parametric polymorphism Parametric polymorphism In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without... |
C# | Func<α1,α2,...,αn,ρ> |
Func |
| Haskell Haskell (programming language) Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the... |
α -> ρ |
compose :: (a -> b) -> (b -> c) -> a -> c |
|
| Scala | (α1,α2,...,αn) => ρ |
def compose[A, B, C](f: B => C, g: A => B): A => C |
|
| Without first-class function First-class function In computer science, a programming language is said to have first-class functions if it treats functions as first-class objects. Specifically, this means that the language supports passing functions as arguments to other functions, returning them as the values from other functions, and assigning... s, parametric polymorphism Parametric polymorphism In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without... |
C C (programming language) C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system.... |
ρ (*)(α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<B,C>,Func> .Denotational semantics
The function type in programming languages does not correspond to the space of all set-theoretic functions. If we take the countably infinite type of natural numberNatural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s as the domain and the boolean
Boolean
Boolean may refer to:* Boolean algebra, a logical calculus of truth values or set membership* Boolean algebra , a set with operations resembling logical ones* Boolean data type, a certain datatype in computer science...
s as range, then there are an uncountably infinite number (2ℵ0 = c
Cardinality of the continuum
In set theory, the cardinality of the continuum is the cardinality or “size” of the set of real numbers \mathbb R, sometimes called the continuum. It is an infinite cardinal number and is denoted by |\mathbb R| or \mathfrak c ....
) of set-theoretic 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 set-theoretic functions effectively solves the halting problem
Halting problem
In computability theory, the halting problem can be stated as follows: Given a description of a computer program, decide whether the program finishes running or continues to run forever...
.
Denotational semantics
Denotational semantics
In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
concerns itself with finding more appropriate models (called domains
Domain theory
Domain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer science, where it is used to specify denotational...
) to model programming language concepts such as function types. It turns out that restricting ourselves to the set of computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
s is not sufficient either if the programming language allows us to write non-terminating computations (which is the case if the programming language is Turing complete). We need to restrict ourselves 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 categoryCartesian closed categoryIn category theory, a category is cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in...
- CurryingCurryingIn mathematics and computer science, currying is the technique of transforming a function that takes multiple arguments in such a way that it can be called as a chain of functions each with a single argument...
- Exponential objectExponential objectIn mathematics, specifically in category theory, an exponential object is the categorical equivalent of a function space in set theory. Categories with all finite products and exponential objects are called cartesian closed categories...
, category-theoretic equivalent - First-class functionFirst-class functionIn computer science, a programming language is said to have first-class functions if it treats functions as first-class objects. Specifically, this means that the language supports passing functions as arguments to other functions, returning them as the values from other functions, and assigning...
- Function spaceFunction spaceIn mathematics, a function space is a set of functions of a given kind from a set X to a set Y. It is called a space because in many applications it is a topological space, a vector space, or both.-Examples:...
, set-theoretic equivalent