1.2 Function types

Given types $A$ and $B$, we can construct the type $A\to B$ of functionswith domain $A$ and codomain $B$.We also sometimes refer to functions as maps.Unlike in set theory, functions are not defined asfunctional 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$, wecan applythe 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 $fa$, 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 definitionmeans thatwe introduce a function by giving it a name — let’s say, $f$ — and sayingwe define $f:A\to B$ by giving an equation

$$f(x)Ü\mathrm{ƒ}\equiv \mathrm{\Phi }$$(1.2.1)

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

Now we can compute $f(a)$ by replacing the variable $x$ in $\mathrm{\Phi }$ with$a$. As an example, consider the function $f:\mathbb{N}\to \mathbb{N}$ which isdefined by $f(x)Ü\mathrm{ƒ}\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 $\mathrm{\Phi }$ of type $B$ which may use $x:A$, as above, we write $\lambda (x:A).\mathrm{\Phi }$ to indicate the same function defined by (1.2.1).Thus, we have

$$(\lambda (x:A).\mathrm{\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.\mathrm{\Phi }$, since the typing $x:A$ is inferable from the judgment that the function $\lambda x.\mathrm{\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 \mathrm{\Phi }):A\to B.$$

We may also sometimes use a blank “$\text{–}$” in the expression $\mathrm{\Phi }$ in place of a variable, to denote an implicit $\lambda$-abstraction.For instance, $g(x,\text{–})$ 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, which is a definitional equality:

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

where ${\mathrm{\Phi }}^{\prime }$ is theexpression $\mathrm{\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$:

$$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 reducedto simple definitions by using $\lambda$-abstraction: i.e., we can reada definition of $f:A\to B$ by

$$f(x)Ü\mathrm{ƒ}\equiv \mathrm{\Phi }$$

as

$$fÜ\mathrm{ƒ}\equiv \lambda x.\mathrm{\Phi }.$$

When doing calculations involving variables, we have to becareful when replacing a variable with an expression that also involvesvariables, because we want to preserve the binding structure ofexpressions. By the binding structure we mean theinvisible link generated by binders such as $\lambda$, $\mathrm{\Pi }$ and$\mathrm{\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)Ü\mathrm{ƒ}\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”)variablessuch as $y$ in the expression $\lambda y.x+y$have only a local meaning, and can be consistently replaced by anyother variable, preserving the binding structure. Indeed, $\lambda y.x+y$ is declared to be judgmentally equal 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)Ü\mathrm{ƒ}\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. Oneway to define functions in several variables would be to use thecartesian product, which will be introduced later; a function withparameters $A$ and $B$ and results in $C$ would be given the type$f:A\times B\to C$. However, there is another choice that avoidsusing 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$, withassociativity 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 towrite $f(a)(b)$ as $f(a,b)$ even though there are no productsinvolved.When omitting parentheses around function arguments entirely, we write $fab$ for $(fa)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 tothis situation: we can define a named function $f:A\to B\to C$ bygiving an equation

$$f(x,y)Ü\mathrm{ƒ}\equiv \mathrm{\Phi }$$

where $\mathrm{\Phi }:C$ assuming $x:A$ and $y:B$. Using $\lambda$-abstraction thiscorresponds to

$$fÜ\mathrm{ƒ}\equiv \lambda x.\lambda y.\mathrm{\Phi },$$

which may also be written as

$$fÜ\mathrm{ƒ}\equiv x\mapsto y\mapsto \mathrm{\Phi }.$$

We can also implicitly abstract over multiple variables by writing multiple blanks, e.g. $g(\text{–},\text{–})$ 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.