1.2 Function types


Given types A and B, we can construct the type AB of functions with domain A and codomain B. We also sometimes refer to functions as maps. Unlike in set theoryMathworldPlanetmath, functions are not defined as functional relations; rather they are a primitive conceptMathworldPlanetmath in type theoryPlanetmathPlanetmath. 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:AB 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 fa, and we will sometimes do this as well.

But how can we construct elements of AB? There are two equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath ways: either by direct definition or by using λ-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:AB by giving an equation

f(x)ÜƒΦ (1.2.1)

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

Now we can compute f(a) by replacing the variable x in Φ with a. As an example, consider the function f: which is defined by f(x)܃x+x. (We will define 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 λ-abstraction. Given an expression Φ of type B which may use x:A, as above, we write λ(x:A).Φ to indicate the same function defined by (1.2.1). Thus, we have

(λ(x:A).Φ):AB.

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

(λ(x:).x+x):.

As another example, for any types A and B and any element y:B, we have a constant function (λ(x:A).y):AB.

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

Another equivalent notation is

(xΦ):AB.

We may also sometimes use a blank “” in the expression Φ in place of a variable, to denote an implicit λ-abstraction. For instance, g(x,) is another way to write λy.g(x,y).

Now a λ-abstraction is a function, so we can apply it to an argument a:A. We then have the following computation rule11Use of this equality is often referred to as β-conversion or β-reductionPlanetmathPlanetmath., which is a definitional equality:

(λx.Φ)(a)Φ

where Φ is the expression Φ in which all occurrences of x have been replaced by a. Continuing the above example, we have

(λx.x+x)(2)2+2.

Note that from any function f:AB, we can construct a lambda abstraction function λ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:22Use of this equality is often referred to as η-conversion or η-expansion.

f(λ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 λ-abstraction: i.e., we can read a definition of f:AB by

f(x)܃Φ

as

f܃λx.Φ.

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 structureMathworldPlanetmath of expressions. By the binding structure we mean the invisible link generated by binders such as λ, Π and Σ (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:() defined as

f(x)܃λy.x+y.

Now if we have assumed somewhere that y:, then what is f(y)? It would be wrong to just naively replace x by y everywhere in the expression “λy.x+y” defining f(x), obtaining λy.y+y, because this means that y gets captured. Previously, the substituted y was referring to our assumptionPlanetmathPlanetmath, but now it is referring to the argument of the λ-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 λy.x+y have only a local meaning, and can be consistently replaced by any other variable, preserving the binding structure. Indeed, λy.x+y is declared to be judgmentally equal33Use of this equality is often referred to as α-conversion. \indexfootalpha-conversion@α-conversion to λz.x+z. It follows that f(y) is judgmentally equal to λ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)܃12dtx-t, then f(t) is not 12dtt-t but rather 12dst-s. A λ-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×BC. 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(BC). We may also write this without the parentheses, as f:ABC, 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 productsPlanetmathPlanetmathPlanetmath involved. 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 to this situation: we can define a named function f:ABC by giving an equation

f(x,y)܃Φ

where Φ:C assuming x:A and y:B. Using λ-abstraction this corresponds to

f܃λx.λy.Φ,

which may also be written as

f܃xyΦ.

We can also implicitly abstract over multiple variables by writing multiple blanks, e.g. g(,) means λx.λy.g(x,y). Currying a function of three or more arguments is a straightforward extensionPlanetmathPlanetmathPlanetmath 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