1.4 Dependent function types
In type theory we often use a more general version of function types, called a -type or dependent function type. The elements of a -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 “-type” is used because this type can also be regarded as the cartesian product over a given type.
Given a type and a family , we may construct the type of dependent functions . There are many alternative notations for this type, such as
If is a constant family, then the dependent product type is the ordinary function type:
Indeed, all the constructions of -types are generalizations of the corresponding constructions on ordinary function types.
We can introduce dependent functions by explicit definitions: to define , where is the name of a dependent function to be defined, we need an expression possibly involving the variable , and we write
Alternatively, we can use -abstraction
As with non-dependent functions, we can apply a dependent function to an argument to obtain an element . The equalities are the same as for the ordinary function type, i.e. we have the computation rule given we have and , where is obtained by replacing all occurrences of in by (avoiding variable capture, as always). Similarly, we have the uniqueness principle for any .
As an example, recall from §1.3 (http://planetmath.org/13universesandfamilies) that there is a type family whose values are the standard finite sets, with elements . There is then a dependent function which returns the “largest” element of each nonempty finite type, . 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 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 , which we define by .
We sometimes write some arguments of a dependent function as subscripts. For instance, we might equivalently define the polymorphic identity function by . Moreover, if an argument can be inferred from context, we may omit it altogether. For instance, if , then writing is unambiguous, since must mean in order for it to be applicable to .
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 and type families and , we may construct the type of functions with two arguments. (Like -abstractions, s automatically scope over the rest of the expression unless delimited; thus means .) In the case when is constant and equal to , we may condense the notation and write ; for instance, the type of could also be written as
Finally, given and arguments and , we have , which, as before, we write as .
|Title||1.4 Dependent function types|
|Date of creation||2013-11-07 20:32:18|
|Last modified on||2013-11-07 20:32:18|
|Last modified by||rspuzio (6075)|