1.4 Dependent function types

In type theory we often use a more general version of function types, called a $\Pi$ -type or dependent function type. The elements of a $\Pi$ -type are functions whose codomain type can vary depending on the element of the domain to which the function is applied, called dependent functions. The name “ $\Pi$ -type” is used because this type can also be regarded as the cartesian product over a given type.

Given a type $A:\mathcal{U}$ and a family $B:A\to\mathcal{U}$ , we may construct the type of dependent functions $\textstyle\prod_{(x:A)}B(x):\mathcal{U}$ . There are many alternative notations for this type, such as

\textstyle\prod_{(x:A)}B(x)\qquad\prod_{(x:A)}\,B(x)\qquad\prod({\textstyle x:% A}),\ B(x).

If $B$ is a constant family, then the dependent product type is the ordinary function type:

\textstyle\prod_{(x:A)}B\equiv(A\to B).

Indeed, all the constructions of $\Pi$ -types are generalizations of the corresponding constructions on ordinary function types.

We can introduce dependent functions by explicit definitions: to define $f:\textstyle\prod_{(x:A)}B(x)$ , where $f$ is the name of a dependent function to be defined, we need an expression $\Phi:B(x)$ possibly involving the variable $x : A$ , and we write

f(x)܃\!\!\equiv\Phi\qquad\mbox{for $x:A$}.

Alternatively, we can use $\lambda$ -abstraction

{\lambda}x:A:{.\,}\Phi\ :\ \textstyle\prod_{(x:A)}B(x).

(1.4.1)

As with non-dependent functions, we can apply a dependent function $f:\textstyle\prod_{(x:A)}B(x)$ to an argument $a : A$ to obtain an element $f(a):B(a)$ . The equalities are the same as for the ordinary function type, i.e. we have the computation rule given $a : A$ we have $f(a)\equiv\Phi^{\prime}$ and $({\lambda}x:A:{.\,}\Phi)(a)\equiv\Phi^{\prime}$ , where $\Phi^{\prime}$ is obtained by replacing all occurrences of $x$ in $\Phi$ by $a$ (avoiding variable capture, as always). Similarly, we have the uniqueness principle $f\equiv({\lambda}x{.\,}f(x))$ for any $f:\textstyle\prod_{(x:A)}B(x)$ .

As an example, recall from §1.3 (http://planetmath.org/13universesandfamilies) that there is a type family $\mathsf{Fin}:\mathbb{N}\to\mathcal{U}$ whose values are the standard finite sets, with elements $0_{n},1_{n},\dots,(n-1)_{n}:\mathsf{Fin}(n)$ . There is then a dependent function $\mathsf{fmax}:\textstyle\prod_{(n:\mathbb{N})}\mathsf{Fin}(n+1)$ which returns the “largest” element of each nonempty finite type, $\mathsf{fmax}(n)܃\!\!\equiv n_{n+1}$ . As was the case for $\mathsf{Fin}$ itself, we cannot define $\mathsf{fmax}$ yet, but we will be able to soon; see http://planetmath.org/node/87562Exercise 1.9.

Another important class of dependent function types, which we can define now, are functions which are polymorphic over a given universe. A polymorphic function is one which takes a type as one of its arguments, and then acts on elements of that type (or other types constructed from it). An example is the polymorphic identity function $\mathsf{id}:\textstyle\prod_{(A:\mathcal{U})}A\to A$ , which we define by $\mathsf{id}{}܃\!\!\equiv{\lambda}(A\,{:}\,\mathcal{U}){.\,}{x:A}x$ .

We sometimes write some arguments of a dependent function as subscripts. For instance, we might equivalently define the polymorphic identity function by $\mathsf{id}_{A}(x)܃\!\!\equiv x$ . Moreover, if an argument can be inferred from context, we may omit it altogether. For instance, if $a : A$ , then writing $\mathsf{id}(a)$ is unambiguous, since $\mathsf{id}$ must mean $\mathsf{id}_{A}$ in order for it to be applicable to $a$ .

Another, less trivial, example of a polymorphic function is the “swap” operation that switches the order of the arguments of a (curried) two-argument function:

\mathsf{swap}:\textstyle\prod_{(A:\mathcal{U})}{B:\mathcal{U}}{C:\mathcal{U}}(% A\to B\to C)\to(B\to A\to C)

We can define this by

\mathsf{swap}(A,B,C,g)܃\!\!\equiv{\lambda}b{.\,}{a}g(a)(b).

We might also equivalently write the type arguments as subscripts:

\mathsf{swap}_{A,B,C}(g)(b,a)܃\!\!\equiv g(a,b).

Note that as we did for ordinary functions, we use currying to define dependent functions with several arguments (such as $\mathsf{swap}$ ). However, in the dependent case the second domain may depend on the first one, and the codomain may depend on both. That is, given $A:\mathcal{U}$ and type families $B:A\to\mathcal{U}$ and $C:\textstyle\prod_{(x:A)}B(x)\to\mathcal{U}$ , we may construct the type $\textstyle\prod_{(x:A)}{y:B(x)}C(x,y)$ of functions with two arguments. (Like $\lambda$ -abstractions, $\Pi$ s automatically scope over the rest of the expression unless delimited; thus $C:\textstyle\prod_{(x:A)}B(x)\to\mathcal{U}$ means $C:\textstyle\prod_{(x:A)}(B(x)\to\mathcal{U})$ .) In the case when $B$ is constant and equal to $A$ , we may condense the notation and write $\textstyle\prod_{(x,y:A)}$ ; for instance, the type of $\mathsf{swap}$ could also be written as

\mathsf{swap}:\textstyle\prod_{(A,B,C:\mathcal{U})}(A\to B\to C)\to(B\to A\to C).

Finally, given $f:\textstyle\prod_{(x:A)}{y:B(x)}C(x,y)$ and arguments $a : A$ and $b:B(a)$ , we have $f(a)(b):C(a,b)$ , which, as before, we write as $f(a,b):C(a,b)$ .

Title	1.4 Dependent function types
Canonical name	14DependentFunctionTypes
Date of creation	2013-11-07 20:32:18
Last modified on	2013-11-07 20:32:18
Owner	PMBookProject (1000683)
Last modified by	rspuzio (6075)
Numerical id	23
Author	PMBookProject (6075)
Entry type	Feature
Classification	msc 03B15