# Function type

Last updated

In computer science and mathematical logic, 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.

## Contents

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 AB, 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.

## Programming languages

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:

LanguageNotationExample 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) => ρ``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`
With first-class functions,
without parametric polymorphism
Go `func(α1,α2,...,αn) ρ``varcomposefunc(func(int)int,func(int)int)func(int)int`
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

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 (20 = 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.

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 expression to the set of computable functions is not sufficient either if the programming language allows writing non-terminating computations (which is the case if the programming language is Turing complete). Expression must be restricted 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.

## Related Research Articles In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that a Cartesian product of a collection of non-empty sets is non-empty. Informally put, the axiom of choice says that given any collection of bins, each containing at least one object, it is possible to make a selection of exactly one object from each bin, even if the collection is infinite. Formally, it states that for every indexed family of nonempty sets there exists an indexed family of elements such that for every . The axiom of choice was formulated in 1904 by Ernst Zermelo in order to formalize his proof of the well-ordering theorem.

In mathematics, a countable set is a set with the same cardinality as some subset of the set of natural numbers. A countable set is either a finite set or a countably infinite set. Whether finite or infinite, the elements of a countable set can always be counted one at a time and—although the counting may never finish—every element of the set is associated with a unique natural number.

In mathematics and computer science, currying is the technique of converting a function that takes multiple arguments into a sequence of functions that each take a single argument. For example, currying a function that takes three arguments creates three functions: Discrete mathematics is the study of mathematical structures that are fundamentally discrete rather than continuous. In contrast to real numbers that have the property of varying "smoothly", the objects studied in discrete mathematics – such as integers, graphs, and statements in logic – do not vary smoothly in this way, but have distinct, separated values. Discrete mathematics therefore excludes topics in "continuous mathematics" such as calculus or Euclidean geometry. Discrete objects can often be enumerated by integers. More formally, discrete mathematics has been characterized as the branch of mathematics dealing with countable sets. However, there is no exact definition of the term "discrete mathematics." Indeed, discrete mathematics is described less by what is included than by what is excluded: continuously varying quantities and related notions.

Mathematical logic is a subfield of mathematics exploring the applications of formal logic to mathematics. It bears close connections to metamathematics, the foundations of mathematics, and theoretical computer science. The unifying themes in mathematical logic include the study of the expressive power of formal systems and the deductive power of formal proof systems.

Model theory is the branch of mathematical logic that deals with the relation between a formal theory and its interpretations, called models. A theory consists of a set of sentences in a formal language, which consists generally of the axioms of the theory, and all theorems that can be deduced from them. A model is a realization of the theory inside another theory.

In mathematics, logic, and computer science, a type system is a formal system in which every term has a "type" which defines its meaning and the operations that may be performed on it. Type theory is the academic study of type systems. Automata theory is the study of abstract machines and automata, as well as the computational problems that can be solved using them. It is a theory in theoretical computer science. The word automata comes from the Greek word αὐτόματα, which means "self-making". In mathematics, general topology is the branch of topology that deals with the basic set-theoretic definitions and constructions used in topology. It is the foundation of most other branches of topology, including differential topology, geometric topology, and algebraic topology. Another name for general topology is point-set topology.

Domain theory is a branch of mathematics that studies special kinds of partially ordered sets (posets) 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 semantics, especially for functional programming languages. Domain theory formalizes the intuitive ideas of approximation and convergence in a very general way and is closely related to topology.

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of deriving theorems from axioms. It can be conceptualized as sculpting out necessary conditions from sufficient ones.

In mathematics, a function space is a set of functions between two fixed sets. Often, the domain and/or codomain will have additional structure which is inherited by the function space. For example, the set of functions from any set X into a vector space has a natural vector space structure given by pointwise addition and scalar multiplication. In other scenarios, the function space might inherit a topological or metric structure, hence the name function space.

In mathematical logic, and particularly in its subfield model theory, a saturated modelM is one that realizes as many complete types as may be "reasonably expected" given its size. For example, an ultrapower model of the hyperreals is -saturated, meaning that every descending nested sequence of internal sets has a nonempty intersection, see Goldblatt (1998).

In mathematical logic, a theory is categorical if it has exactly one model. Such a theory can be viewed as defining its model, uniquely characterizing its structure.

In mathematics and computer science, apply is a function that applies a function to arguments. It is central to programming languages derived from lambda calculus, such as LISP and Scheme, and also in functional languages. It has a role in the study of the denotational semantics of computer programs, because it is a continuous function on complete partial orders. Apply is also a continuous function in homotopy theory, and, indeed underpins the entire theory: it allows a homotopy deformation to be viewed as a continuous path in the space of functions. Likewise, valid mutations (refactorings) of computer programs can be seen as those that are "continuous" in the Scott topology.

In programming languages and type theory, a product of types is another, compounded, type in a structure. The "operands" of the product are types, and the structure of a product type is determined by the fixed order of the operands in the product. An instance of a product type retains the fixed order, but otherwise may contain all possible instances of its primitive data types. The expression of an instance of a product type will be a tuple, and is called a "tuple type" of expression. A product of types is a direct product of two or more types.

In type theory, a system has inductive types if it has facilities for creating a new type along with constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion. In mathematical logic and computer science, homotopy type theory refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies.

In mathematics, equivalent definitions are used in two somewhat different ways. First, within a particular mathematical theory, a notion may have more than one definition. These definitions are equivalent in the context of a given mathematical structure. Second, a mathematical structure may have more than one definition.

• Pierce, Benjamin C. (2002). . 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.