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 14DependentFunctionTypes 2013-11-07 20:32:18 2013-11-07 20:32:18 PMBookProject (1000683) rspuzio (6075) 23 PMBookProject (6075) Feature msc 03B15