1.2 Function types
Given types and , we can construct the type of functions with domain and codomain . 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 and an element of the domain , we can apply the function to obtain an element of the codomain , denoted and called the value of at . It is common in type theory to omit the parentheses and denote simply by , and we will sometimes do this as well.
But how can we construct elements of ? There are two equivalent 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, — and saying we define by giving an equation
where is a variable and is an expression which may use . In order for this to be valid, we have to check that assuming .
Now we can compute by replacing the variable in with . As an example, consider the function which is defined by . (We will define and in §1.9 (http://planetmath.org/19thenaturalnumbers).) Then is judgmentally equal to .
If we don’t want to introduce a name for the function, we can use -abstraction. Given an expression of type which may use , as above, we write to indicate the same function defined by (1.2.1). Thus, we have
For the example in the previous paragraph, we have the typing judgment
We generally omit the type of the variable in a -abstraction and write , since the typing is inferable from the judgment that the function has type . By convention, the “scope” of the variable binding “” is the entire rest of the expression, unless delimited with parentheses. Thus, for instance, should be parsed as , not as (which would, in this case, be ill-typed anyway).
Another equivalent notation is
We may also sometimes use a blank “” in the expression in place of a variable, to denote an implicit -abstraction. For instance, is another way to write .
Now a -abstraction is a function, so we can apply it to an argument . We then have the following computation rule11Use of this equality is often referred to as -conversion or -reduction., which is a definitional equality:
where is the expression in which all occurrences of have been replaced by . Continuing the above example, we have
Note that from any function , we can construct a lambda abstraction function . Since this is by definition “the function that applies to its argument” we consider it to be definitionally equal to :22Use of this equality is often referred to as -conversion or -expansion.
This equality is the uniqueness principle for function types, because it shows that is uniquely determined by its values.
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 , 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 defined as
Now if we have assumed somewhere that , then what is ? It would be wrong to just naively replace by everywhere in the expression “” defining , obtaining , because this means that gets captured. Previously, the substituted was referring to our assumption, 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 in this example? Note that bound (or “dummy”) variables such as in the expression have only a local meaning, and can be consistently replaced by any other variable, preserving the binding structure. Indeed, is declared to be judgmentally equal33Use of this equality is often referred to as -conversion. \indexfootalpha-conversion@-conversion to . It follows that is judgmentally equal to , and that answers our question. (Instead of , any variable distinct from 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 , then is not but rather . 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 and and results in would be given the type . 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 and as a function which takes one input and returns another function, which then takes a second input and returns the result. That is, we consider two-variable functions to belong to an iterated function type, . We may also write this without the parentheses, as , with associativity to the right as the default convention. Then given and , we can apply to and then apply the result to , obtaining . To avoid the proliferation of parentheses, we allow ourselves to write as even though there are no products involved. When omitting parentheses around function arguments entirely, we write for , with the default associativity now being to the left so that 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 by giving an equation
where assuming and . Using -abstraction this corresponds to
which may also be written as
We can also implicitly abstract over multiple variables by writing multiple blanks, e.g. means . Currying a function of three or more arguments is a straightforward extension of what we have just described.
|Title||1.2 Function types|
|Date of creation||2013-11-07 19:39:53|
|Last modified on||2013-11-07 19:39:53|
|Last modified by||rspuzio (6075)|