1.4 Dependent function types

In type theory we often use a more general version of functiontypes, called a $\mathrm{\Pi }$-type or dependent function type. The elements ofa $\mathrm{\Pi }$-type are functionswhose codomain type can vary depending on theelement 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 cartesianproduct over a given type.

Given a type $A:𝒰$ and a family $B:A\to 𝒰$, we may constructthe type of dependent functions ${\prod }_{(x:A)}B(x):𝒰$.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: todefine $f:{\prod }_{(x:A)}B(x)$, where $f$ is the name of a dependent function to bedefined, we need an expression $\mathrm{\Phi }:B(x)$ possibly involving the variable $x:A$,and we write

$$f(x)Ü\mathrm{ƒ}\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 rulegiven $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 alloccurrences 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{𝖥𝗂𝗇}:\mathbb{N}\to 𝒰$ whose values are the standard finite sets, with elements $0_n,1_n,\mathrm{\dots },{(n-1)}_n:\mathrm{𝖥𝗂𝗇}(n)$.There is then a dependent function $\mathrm{𝖿𝗆𝖺𝗑}:{\prod }_{(n:\mathbb{N})}\mathrm{𝖥𝗂𝗇}(n+1)$which returns the “largest” element of each nonempty finite type, $\mathrm{𝖿𝗆𝖺𝗑}(n)Ü\mathrm{ƒ}\equiv n_{n+1}$.As was the case for $\mathrm{𝖥𝗂𝗇}$ itself, we cannot define $\mathrm{𝖿𝗆𝖺𝗑}$ 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 polymorphicover 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{𝗂𝖽}:{\prod }_{(A:𝒰)}A\to A$, which we define by $\mathrm{𝗂𝖽}Ü\mathrm{ƒ}\equiv \lambda (A:𝒰).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{𝗂𝖽}}_A(x)Ü\mathrm{ƒ}\equiv x$.Moreover, if an argument can be inferred from context, we may omit it altogether.For instance, if $a:A$, then writing $\mathrm{𝗂𝖽}(a)$ is unambiguous, since $\mathrm{𝗂𝖽}$ must mean ${\mathrm{𝗂𝖽}}_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{𝗌𝗐𝖺𝗉}:{\prod }_{(A:𝒰)}B:𝒰C:𝒰(A\to B\to C)\to (B\to A\to C)$$

We can define this by

$$\mathrm{𝗌𝗐𝖺𝗉}(A,B,C,g)Ü\mathrm{ƒ}\equiv \lambda b.ag(a)(b).$$

We might also equivalently write the type arguments as subscripts:

$${\mathrm{𝗌𝗐𝖺𝗉}}_{A,B,C}(g)(b,a)Ü\mathrm{ƒ}\equiv g(a,b).$$

Note that as we did for ordinary functions, we use currying to define dependent functions withseveral arguments (such as $\mathrm{𝗌𝗐𝖺𝗉}$). However, in the dependent case the second domain maydepend on the first one, and the codomain may depend on both. That is,given $A:𝒰$ and type families $B:A\to 𝒰$ and $C:{\prod }_{(x:A)}B(x)\to 𝒰$, we may constructthe type ${\prod }_{(x:A)}y:B(x)C(x,y)$ of functions with twoarguments.(Like $\lambda$-abstractions, $\mathrm{\Pi }$s automatically scope over the rest of the expression unless delimited; thus $C:{\prod }_{(x:A)}B(x)\to 𝒰$ means $C:{\prod }_{(x:A)}(B(x)\to 𝒰)$.)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{𝗌𝗐𝖺𝗉}$ could also be written as

$$\mathrm{𝗌𝗐𝖺𝗉}:{\prod }_{(A,B,C:𝒰)}(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)$.