Function

Definition

A function type is a binary type constructor whose elements are functions from one type to another. The function type from type $A$ to type $B$ is denoted $A\to B$.

An element $f:A\to B$ is a function that maps each element of type $A$ to an element of type $B$.

Type-Theoretic Rules

Function types have the following introduction and elimination rules:

• Introduction (lambda abstraction): Given an expression $e:B$ with free variable $x:A$, we can form $\lambda x.e:A\to B$
• Elimination (application): Given $f:A\to B$ and $a:A$, we can form $f(a):B$

The key property is the $\beta$-reduction rule: $(\lambda x.e)(a)\equiv e[a/x]$ where $e[a/x]$ denotes substituting $a$ for $x$ in $e$.

Properties

• Syntactically, function types associate right: $A\to B\to C$ means $A\to (B\to C)$
• Function types form an exponential object in category theory: $B^A$ denotes the type of functions from $A$ to $B$

Relationship to Product Types

Function types and product types are dual in a precise sense:

• Product introduction requires providing both components; elimination extracts one
• Function introduction abstracts over an input; elimination requires providing an input

This duality is formalized in the adjunction $(-)\times A⊣(-{)}^A$ in category theory.

Related Concepts

• Product Type: The dual construction to function types
• Product Type: A generalization where the output type may depend on the input value
• Lambda Calculus: The foundational system for function types
• Currying: The correspondence between $A\times B\to C$ and $A\to B\to C$