1.4 Dependent function types

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

Given a type A:𝒰 and a family B:A𝒰, we may construct the type of dependent functions (x:A)B(x):𝒰. There are many alternative notationsDlmfDlmfDlmfDlmfDlmf for this type, such as

(x:A)B(x)  (x:A)B(x)  (x:A),B(x).

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


Indeed, all the constructions of Π-types are generalizationsPlanetmathPlanetmath of the corresponding constructions on ordinary function types.

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

f(x)܃Φ  for x:A.

Alternatively, we can use λ-abstraction

λx:A:.Φ:(x:A)B(x). (1.4.1)

As with non-dependent functions, we can apply a dependent function f:(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)Φ and (λx:A:.Φ)(a)Φ, where Φ is obtained by replacing all occurrences of x in Φ by a (avoiding variable capture, as always). Similarly, we have the uniqueness principle f(λx.f(x)) for any f:(x:A)B(x).

As an example, recall from §1.3 (http://planetmath.org/13universesandfamilies) that there is a type family 𝖥𝗂𝗇:𝒰 whose values are the standard finite setsMathworldPlanetmath, with elements 0n,1n,,(n-1)n:𝖥𝗂𝗇(n). There is then a dependent function 𝖿𝗆𝖺𝗑:(n:)𝖥𝗂𝗇(n+1) which returns the “largest” element of each nonempty finite type, 𝖿𝗆𝖺𝗑(n)܃nn+1. As was the case for 𝖥𝗂𝗇 itself, we cannot define 𝖿𝗆𝖺𝗑 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 universePlanetmathPlanetmath. 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 functionMathworldPlanetmath 𝗂𝖽:(A:𝒰)AA, which we define by 𝗂𝖽܃λ(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 𝗂𝖽A(x)܃x. Moreover, if an argument can be inferred from context, we may omit it altogether. For instance, if a:A, then writing 𝗂𝖽(a) is unambiguous, since 𝗂𝖽 must mean 𝗂𝖽A in order for it to be applicable to a.

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


We can define this by


We might also equivalently write the type arguments as subscripts:


Note that as we did for ordinary functions, we use currying to define dependent functions with several arguments (such as 𝗌𝗐𝖺𝗉). 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:𝒰 and type families B:A𝒰 and C:(x:A)B(x)𝒰, we may construct the type (x:A)y:B(x)C(x,y) of functions with two arguments. (Like λ-abstractions, Πs automatically scope over the rest of the expression unless delimited; thus C:(x:A)B(x)𝒰 means C:(x:A)(B(x)𝒰).) In the case when B is constant and equal to A, we may condense the notation and write (x,y:A); for instance, the type of 𝗌𝗐𝖺𝗉 could also be written as


Finally, given f:(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