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.

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 *B*^{A}, based on there existing exactly *B*^{A} (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.

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<` | `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 | `(` | `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(` | `fncompose<A,B,C>(f: fn(A)-> B,g: fn(B)-> C)-> fn(A)-> C` | |

With first-class functions, without parametric polymorphism | Go | `func(` | `varcomposefunc(func(int)int,func(int)int)func(int)int` |

C++, Objective-C, with blocks |
| `int(^compose(int(^f)(int),int(^g)(int)))(int);` | |

Without first-class functions, parametric polymorphism | C |
| `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 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.

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.

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.

- Cartesian closed category
- Currying
- Exponential object, category-theoretic equivalent
- First-class function
- Function space, set-theoretic equivalent

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 model***M* 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).
*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*.

This page is based on this Wikipedia article

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.