1.2 Function types

Given types $A$ and $B$ , we can construct the type $A\to B$ of functions with domain $A$ and codomain $B$ . We also sometimes refer to functions as maps. Unlike in set theory, functions are not defined as functional relations; rather they are a primitive concept in type theory. We explain the function type by prescribing what we can do with functions, how to construct them and what equalities they induce.

Given a function $f:A\to B$ and an element of the domain $a : A$ , we can apply the function to obtain an element of the codomain $B$ , denoted $f(a)$ and called the value of $f$ at $a$ . It is common in type theory to omit the parentheses and denote $f(a)$ simply by $f\,a$ , and we will sometimes do this as well.

But how can we construct elements of $A\to B$ ? There are two equivalent ways: either by direct definition or by using $\lambda$ -abstraction. Introducing a function by definition means that we introduce a function by giving it a name — let’s say, $f$ — and saying we define $f:A\to B$ by giving an equation

f(x)܃\!\!\equiv\Phi

(1.2.1)

where $x$ is a variable and $\Phi$ is an expression which may use $x$ . In order for this to be valid, we have to check that $\Phi:B$ assuming $x : A$ .

Now we can compute $f(a)$ by replacing the variable $x$ in $\Phi$ with $a$ . As an example, consider the function $f:\mathbb{N}\to\mathbb{N}$ which is defined by $f(x)܃\!\!\equiv x+x$ . (We will define $\mathbb{N}$ and $+$ in §1.9 (http://planetmath.org/19thenaturalnumbers).) Then $f(2)$ is judgmentally equal to $2+2$ .

If we don’t want to introduce a name for the function, we can use $\lambda$ -abstraction. Given an expression $\Phi$ of type $B$ which may use $x : A$ , as above, we write ${\lambda}(x\,{:}\,A).\,\Phi$ to indicate the same function defined by (1.2.1). Thus, we have

({\lambda}(x\,{:}\,A).\,\Phi):A\to B.

For the example in the previous paragraph, we have the typing judgment

({\lambda}(x\,{:}\,\mathbb{N}).\,x+x):\mathbb{N}\to\mathbb{N}.

As another example, for any types $A$ and $B$ and any element $y : B$ , we have a constant function $({\lambda}(x\,{:}\,A).\,y):A\to B$ .

We generally omit the type of the variable $x$ in a $\lambda$ -abstraction and write ${\lambda}x.\,\Phi$ , since the typing $x : A$ is inferable from the judgment that the function ${\lambda}x.\,\Phi$ has type $A\to B$ . By convention, the “scope” of the variable binding “ ${\lambda}x.\,$ ” is the entire rest of the expression, unless delimited with parentheses. Thus, for instance, ${\lambda}x.\,x+x$ should be parsed as ${\lambda}x.\,(x+x)$ , not as $({\lambda}x.\,x)+x$ (which would, in this case, be ill-typed anyway).

Another equivalent notation is

(x\mapsto\Phi):A\to B.

We may also sometimes use a blank “ $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ ” in the expression $\Phi$ in place of a variable, to denote an implicit $\lambda$ -abstraction. For instance, $g(x,\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ is another way to write ${\lambda}y.\,g(x,y)$ .

Now a $\lambda$ -abstraction is a function, so we can apply it to an argument $a : A$ . We then have the following computation rule¹¹Use of this equality is often referred to as $\beta$ -conversion or $\beta$ -reduction., which is a definitional equality:

({\lambda}x.\,\Phi)(a)\equiv\Phi^{\prime}

where $\Phi^{\prime}$ is the expression $\Phi$ in which all occurrences of $x$ have been replaced by $a$ . Continuing the above example, we have

({\lambda}x.\,x+x)(2)\equiv 2+2.

Note that from any function $f:A\to B$ , we can construct a lambda abstraction function ${\lambda}x.\,f(x)$ . Since this is by definition “the function that applies $f$ to its argument” we consider it to be definitionally equal to $f$ :²²Use of this equality is often referred to as $\eta$ -conversion or $\eta$ -expansion.

f\equiv({\lambda}x.\,f(x)).

This equality is the uniqueness principle for function types, because it shows that $f$ is uniquely determined by its values.

The introduction of functions by definitions with explicit parameters can be reduced to simple definitions by using $\lambda$ -abstraction: i.e., we can read a definition of $f:A\to B$ by

f(x)܃\!\!\equiv\Phi

f܃\!\!\equiv{\lambda}x.\,\Phi.

When doing calculations involving variables, we have to be careful when replacing a variable with an expression that also involves variables, because we want to preserve the binding structure of expressions. By the binding structure we mean the invisible link generated by binders such as $\lambda$ , $\Pi$ and $\Sigma$ (the latter we are going to meet soon) between the place where the variable is introduced and where it is used. As an example, consider $f:\mathbb{N}\to(\mathbb{N}\to\mathbb{N})$ defined as

f(x)܃\!\!\equiv{\lambda}y.\,x+y.

Now if we have assumed somewhere that $y:\mathbb{N}$ , then what is $f(y)$ ? It would be wrong to just naively replace $x$ by $y$ everywhere in the expression “ ${\lambda}y.\,x+y$ ” defining $f(x)$ , obtaining ${\lambda}y.\,y+y$ , because this means that $y$ gets captured. Previously, the substituted $y$ was referring to our assumption, but now it is referring to the argument of the $\lambda$ -abstraction. Hence, this naive substitution would destroy the binding structure, allowing us to perform calculations which are semantically unsound.

But what is $f(y)$ in this example? Note that bound (or “dummy”) variables such as $y$ in the expression ${\lambda}y.\,x+y$ have only a local meaning, and can be consistently replaced by any other variable, preserving the binding structure. Indeed, ${\lambda}y.\,x+y$ is declared to be judgmentally equal³³Use of this equality is often referred to as $\alpha$ -conversion. \indexfootalpha-conversion@ $\alpha$ -conversion to ${\lambda}z.\,x+z$ . It follows that $f(y)$ is judgmentally equal to ${\lambda}z.\,y+z$ , and that answers our question. (Instead of $z$ , any variable distinct from $y$ could have been used, yielding an equal result.)

Of course, this should all be familiar to any mathematician: it is the same phenomenon as the fact that if $f(x)܃\!\!\equiv\int_{1}^{2}\frac{dt}{x-t}$ , then $f(t)$ is not $\int_{1}^{2}\frac{dt}{t-t}$ but rather $\int_{1}^{2}\frac{ds}{t-s}$ . A $\lambda$ -abstraction binds a dummy variable in exactly the same way that an integral does.

We have seen how to define functions in one variable. One way to define functions in several variables would be to use the cartesian product, which will be introduced later; a function with parameters $A$ and $B$ and results in $C$ would be given the type $f:A\times B\to C$ . However, there is another choice that avoids using product types, which is called currying (after the mathematician Haskell Curry).

The idea of currying is to represent a function of two inputs $a : A$ and $b : B$ as a function which takes one input $a : A$ and returns another function, which then takes a second input $b : B$ and returns the result. That is, we consider two-variable functions to belong to an iterated function type, $f:A\to(B\to C)$ . We may also write this without the parentheses, as $f:A\to B\to C$ , with associativity to the right as the default convention. Then given $a : A$ and $b : B$ , we can apply $f$ to $a$ and then apply the result to $b$ , obtaining $f(a)(b):C$ . To avoid the proliferation of parentheses, we allow ourselves to write $f(a)(b)$ as $f(a,b)$ even though there are no products involved. When omitting parentheses around function arguments entirely, we write $f\,a\,b$ for $(f\,a)\,b$ , with the default associativity now being to the left so that $f$ is applied to its arguments in the correct order.

Our notation for definitions with explicit parameters extends to this situation: we can define a named function $f:A\to B\to C$ by giving an equation

f(x,y)܃\!\!\equiv\Phi

where $\Phi:C$ assuming $x : A$ and $y : B$ . Using $\lambda$ -abstraction this corresponds to

f܃\!\!\equiv{\lambda}x.\,{\lambda}y.\,\Phi,

which may also be written as

f܃\!\!\equiv x\mapsto y\mapsto\Phi.

We can also implicitly abstract over multiple variables by writing multiple blanks, e.g. $g(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt},\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt})$ means ${\lambda}x.\,{\lambda}y.\,g(x,y)$ . Currying a function of three or more arguments is a straightforward extension of what we have just described.

Title	1.2 Function types
Canonical name	12FunctionTypes
Date of creation	2013-11-07 19:39:53
Last modified on	2013-11-07 19:39:53
Owner	PMBookProject (1000683)
Last modified by	rspuzio (6075)
Numerical id	14
Author	PMBookProject (6075)
Entry type	Feature
Classification	msc 03B15