# 1.4 Dependent function types

In type theory^{} we often use a more general version of function
types, called a $\mathrm{\Pi}$-type or dependent function type. The elements of
a $\mathrm{\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 “$\mathrm{\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 ${\prod}_{(x:A)}B(x):\mathcal{U}$.
There are many alternative notations^{} for this type, such as

$${\prod}_{(x:A)}B(x)\mathit{\hspace{1em}\hspace{1em}}{\prod}_{(x:A)}B(x)\mathit{\hspace{1em}\hspace{1em}}\prod (x:A),B(x).$$ |

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

$${\prod}_{(x:A)}B\equiv (A\to B).$$ |

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

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

$$f(x)\xdc\mathrm{\x83}\equiv \mathrm{\Phi}\mathit{\hspace{1em}\hspace{1em}}\text{for}x:A.$$ |

Alternatively, we can use $\lambda $-abstraction

$$\lambda x:A:.\mathrm{\Phi}:{\prod}_{(x:A)}B(x).$$ | (1.4.1) |

As with non-dependent functions, we can apply a dependent function $f:{\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 {\mathrm{\Phi}}^{\prime}$ and $(\lambda x:A:.\mathrm{\Phi})(a)\equiv {\mathrm{\Phi}}^{\prime}$, where ${\mathrm{\Phi}}^{\prime}$ is obtained by replacing all occurrences of $x$ in $\mathrm{\Phi}$ by $a$ (avoiding variable capture, as always). Similarly, we have the uniqueness principle $f\equiv (\lambda x.f(x))$ for any $f:{\prod}_{(x:A)}B(x)$.

As an example, recall from §1.3 (http://planetmath.org/13universesandfamilies) that there is a type family $\mathrm{\U0001d5a5\U0001d5c2\U0001d5c7}:\mathbb{N}\to \mathcal{U}$ whose values are the standard finite sets^{}, with elements ${0}_{n},{1}_{n},\mathrm{\dots},{(n-1)}_{n}:\mathrm{\U0001d5a5\U0001d5c2\U0001d5c7}(n)$.
There is then a dependent function $\mathrm{\U0001d5bf\U0001d5c6\U0001d5ba\U0001d5d1}:{\prod}_{(n:\mathbb{N})}\mathrm{\U0001d5a5\U0001d5c2\U0001d5c7}(n+1)$
which returns the “largest” element of each nonempty finite type, $\mathrm{\U0001d5bf\U0001d5c6\U0001d5ba\U0001d5d1}(n)\xdc\mathrm{\x83}\equiv {n}_{n+1}$.
As was the case for $\mathrm{\U0001d5a5\U0001d5c2\U0001d5c7}$ itself, we cannot define $\mathrm{\U0001d5bf\U0001d5c6\U0001d5ba\U0001d5d1}$ 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^{} $\mathrm{\U0001d5c2\U0001d5bd}:{\prod}_{(A:\mathcal{U})}A\to A$, which we define by $\mathrm{\U0001d5c2\U0001d5bd}\xdc\mathrm{\x83}\equiv \lambda (A:\mathcal{U}).x:Ax$.

We sometimes write some arguments of a dependent function as subscripts. For instance, we might equivalently define the polymorphic identity function by ${\mathrm{\U0001d5c2\U0001d5bd}}_{A}(x)\xdc\mathrm{\x83}\equiv x$. Moreover, if an argument can be inferred from context, we may omit it altogether. For instance, if $a:A$, then writing $\mathrm{\U0001d5c2\U0001d5bd}(a)$ is unambiguous, since $\mathrm{\U0001d5c2\U0001d5bd}$ must mean ${\mathrm{\U0001d5c2\U0001d5bd}}_{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:

$$\mathrm{\U0001d5cc\U0001d5d0\U0001d5ba\U0001d5c9}:{\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

$$\mathrm{\U0001d5cc\U0001d5d0\U0001d5ba\U0001d5c9}(A,B,C,g)\xdc\mathrm{\x83}\equiv \lambda b.ag(a)(b).$$ |

We might also equivalently write the type arguments as subscripts:

$${\mathrm{\U0001d5cc\U0001d5d0\U0001d5ba\U0001d5c9}}_{A,B,C}(g)(b,a)\xdc\mathrm{\x83}\equiv g(a,b).$$ |

Note that as we did for ordinary functions, we use currying to define dependent functions with several arguments (such as $\mathrm{\U0001d5cc\U0001d5d0\U0001d5ba\U0001d5c9}$). 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:{\prod}_{(x:A)}B(x)\to \mathcal{U}$, we may construct the type ${\prod}_{(x:A)}y:B(x)C(x,y)$ of functions with two arguments. (Like $\lambda $-abstractions, $\mathrm{\Pi}$s automatically scope over the rest of the expression unless delimited; thus $C:{\prod}_{(x:A)}B(x)\to \mathcal{U}$ means $C:{\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 ${\prod}_{(x,y:A)}$; for instance, the type of $\mathrm{\U0001d5cc\U0001d5d0\U0001d5ba\U0001d5c9}$ could also be written as

$$\mathrm{\U0001d5cc\U0001d5d0\U0001d5ba\U0001d5c9}:{\prod}_{(A,B,C:\mathcal{U})}(A\to B\to C)\to (B\to A\to C).$$ |

Finally, given $f:{\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 |