Jones N.D.Partial evaluation and automatic program generation.1999

24 Functions, Types, and Expressions

1. 8a 2 A 8b; b0 2 B : (a; b) 2 f and (a; b0) 2 f implies b = b0. 2. 8a 2 A 9b 2 B such that (a; b) 2 f.

Property 1 says f is single-valued, meaning that each a in A is mapped to at most one b in B. This b is usually written f(a) or just fa. Property 2 says f is total, meaning that each a in A is mapped to at least one b in B. In other words, f(a) is de ned for every a in A.

In computer science we often meet functions which are unde ned for some arguments. A partial function f from A to B (written f : A!B) is a subset f of A B that satis es 1, but not necessarily 2. A natural example is the function that maps a program's input to the corresponding output. This function is unde ned for any input that causes the program to go into an in nite loop. We shall use the notation

f(a) = ?

(where ? is called bottom) to indicate that f(a) is unde ned, i.e. that f contains no pair of form (a; b). Sometimes ? will be treated as if it were a special value. Thus it is possible to consider a partial function f : A!B as a total function which

t

may yield the unde ned value ?, that is, f : A!(B + f?g).

Note that every total function is also a partial function, whereas the converse is not true.

Examples

Suppose sets X and Y have x and y elements, respectively. It is easy to see that there are in all yx di erent total functions from X to Y . Further, there must be (y + 1)x di erent partial functions from X to Y (to see this, think of `unde ned' as the special value ?). If, for example, X = fred; greeng and Y = fred; blueg then

the set of total functions from X to Y is: ff1; f2; f3; f4g;

the set of partial functions from X to Y is: ff1; f2; f3; f4; f5; f6; f7; f8; f9g;

where the functions f1; . . . ; f9 are de ned as follows:

Functions 25

Equality of functions

Two functions f; g : A!B are equal, written f = g, if

8a 2 A: f(a) = g(a)

Note that for partial functions f and g, and a 2 A, this means that either both f(a) and g(a) are unde ned (?), or both are de ned and equal.

Composition of functions

The composition of two functions f : A!B and g : B!C is the function g f : A!C such that (g f)(a) = g(f(a)) for any a 2 A.

Finite functions and updating

When a1; . . . ; an 2 A and b1; . . . ; bn 2 B, the notation [a1 7!b1; . . . ; an 7!bn] denotes the partial function g : A!B such that

g(x) = ( bi if x = ai for some i ? if x =6 ai for all i

When f : A!B is a partial function, the notation f[a1 7!b1; . . . ; an 7!bn] denotes the partial function g : A!B such that

g(x) = ( bi if x = ai for some i f (x) if x 6= ai for all i

and is called the result of updating f by [ai 7!bi] (also called overriding).

Functions and algorithms

The term `function' as used in programming languages like Pascal, Lisp, Scheme, or ML, is not the same as the mathematical concept. The rst reason is that a Pascal `function declaration' speci es an algorithm, i.e. a recipe for computing the declared function. An example algorithm to compute the factorial n! of n, programmed in Pascal:

function fac(n:integer):integer; begin

if n = 0 then fac := 1 else fac := n * fac(n - 1)

end

On the other hand, a mathematical function f is just a set of ordered pairs. For instance,

f(n) = the nth digit of 's decimal expansion

speci es a well-de ned function on the natural numbers even though it does not say how to compute f (n) for a given natural number n.

A second di erence is that a Pascal-de ned `function' need not even be singlevalued. For example, consider the following function declaration:

26 Functions, Types, and Expressions

var global:integer;

function f(a:integer):integer; begin

global := global + 1; f := a + global

end

Repeated execution of the call f(1) may return di erent values every time, since every call changes the value of the variable global.

2.2Types in programming languages

For the purpose of this book, a type can be considered a set of values. The concept is non-trivial due to the many ways that new values can be built up from old, and the next few sections will discuss several of them. A more sophisticated treatment of types involves partial orders and domain theory as in denotational semantics; but the view of types as sets of values will be su cient for the greater part of this book, except brie y in some of the last chapters.

2.2.1Product and function types

If f is a partial function from A to B we write f : A!B, and say f has type A!B. For example, f(n) = n! has type N !N where N = f0; 1; 2; . . .g is the set of natural numbers. More generally we can form some simple type expressions. Each of these denotes a set of values, obtained by the following rules:

1.The names of various standard sets are type expressions, including

N = f0; 1; 2; . . .g, the set of natural numbers;

Z = f. . . ; ,2; ,1; 0; 1; 2; . . .g, the set of integers;

B = ftrue; falseg, the set of booleans, also called truth values;

ID, the set of all identi ers ( nite strings of letters or digits that begin with a letter).

2.If A1; . . . ; An are types (sets), then A1 An is the Cartesian product of A1, A2, . . . , and An.

3.If A and B are types (sets), then

A!B is the set of partial functions from A to B;

t

A!B is the set of total functions from A to B.

A function f : A!B is higher-order if either A or B is a function type. If neither A nor B is a function type, then f is rst-order.

Types in programming languages 27

Some examples of function de nitions and their types

Following are several examples of function de nitions with appropriate types. Note that the same de nition may be compatible with several types, for example square

The list above contains:

1.a recursively de ned function g (note that g(n) is n factorial);

2.functions h; k with structured data as arguments and results;

3.a function sum, which takes a function as an argument.

The function arrow associates to the right, so A!(B!C) can be abbreviated A!B!C. If f : A!B!C then f(a) : B!C for any a 2 A, so f is a functionproducing function. Function application associates to the left, so f a b means (f(a))(b), assuming f : A!B!C, and a 2 A, b 2 B.

Higher-order functions

A higher-order function is a function which takes a function as argument or returns a function as its result (when applied). The functions sum, add, power, and twice de ned above are higher-order. For instance, add(1) is the function which, given any argument x, returns x + 1; and power(2) is the `squaring function', so

add(1)(7) = 8 and power(2)(7) = 49

The higher-order function twice takes a function as its rst argument and yields a function as its result. For example, twice(square) is the function j which raises its argument to the fourth power:

twice(square) = j; where j(x) = (x2)2 = x4

28 Functions, Types, and Expressions

Curried functions

Compare the function add above with the familiar addition function plus(x; y) = x + y. They are related as follows:

The di erence is that plus takes both its arguments at the same time, whereas add can be applied to a single argument and so is a function-producing function. We say that add is a curried version of plus. The term `curry' stems from the name of H.B. Curry, a mathematical logician. The idea is attributed also to M. Sch•on nkel (1924).

Programming notations for product and function types

We have discussed functions as mathematical objects, and the type notation used to describe them. We now see how they are realized in two programming languages.

Pascal

Pascal is a statically typed imperative programming language [127], and has builtin product types. The declaration

var T: record

a:A; b:B

end

declares variable T to be a pair of a and b; its type is the Cartesian product of types A and B. The components of T are referred to in Pascal by selectors as T.a and T.b.

Pascal also has built-in function types and function calls. The declaration

function f(a1:A1, a2:A2,..., an:An) : B;

de nes a function f : A1 An ! B. The arguments a1,. . . , an may be of any de nable type, including functions, so sum as seen above may be programmed directly in Pascal. However, the result type B is severely restricted by Pascal (to pointer or scalar types). Consequently, function k (whose result is a pair), and the functions add and power (whose results are functions) cannot be directly expressed in Pascal, but sum and twice can.

ML

Standard ML is a statically typed functional programming language [185]. ML makes much use of pattern matching for manipulating structured values such as

Types in programming languages 29

pairs or lists. The declaration

fun f (x: int, y: int) = abs(x - y) < 2

declares a function f whose (single) argument is a pair of integers and whose result is a boolean. Function f's argument has product type int * int, corresponding to Z Z above. Function f's result type is bool, corresponding to B above. This result type is not given explicitly in the program but can be inferred automatically.

ML allows expressions that evaluate to a pair, which cannot be done in Pascal. An example expression is: (x-1,x+1).

ML treats functions as any other kind of values, and there are no restrictions on the argument and result types of a function. Thus all the example functions above can be directly de ned in ML. The function-producing function add is de ned in ML by

fun add (x: int) (y: int) = x + y

and then add(1) denotes the `add one' function.

Scheme

Scheme is a functional language [49], related to Lisp, and is dynamically typed. Thus in general the type of an expression cannot be determined until run time. The atomic values in Scheme are numbers 4.5 and atoms 'foo. So-called S-expressions are used to build composite data structures. A pair (a; b) can be represented as the S-expression '(a . b), or alternatively as '(a b).

Scheme has function de nitions, but no pattern matching. Application of a function (or operator) f to an argument a is written pre x as (f a). Thus function f shown above is de ned in Scheme by:

(define (f x y) (< (abs (- x y)) 2))

2.2.2Type inference

When x is a variable and t a type, we write x : t to indicate that the value of x belongs to type t.

We say that an expression is well-typed if all operators and functions in the expression are applied to arguments of a suitable type. When e is an expression, we write e : t to indicate that e is well-typed and that the value of e has type t. For instance, 3 + 5 : N .

Now suppose e is an expression, such as x + x, which contains occurrences of the variable x. Then the type e can be determined only under some assumptions about the type of x. Such assumptions are represented by a type environment= [x 7!t; . . .], which maps x to its type, so x = t.

The assertion that `whenever x : N, then x + x : N' is written as follows:

30Functions, Types, and Expressions

[x 7! N] ` x + x : N

More generally, the notation ` e : t is called a judgement and means that `in type environment , expression e is well-typed and has type t'.

Type inference is often based on a set of type inference rules, one for each form of expression in the language. For an expression which is a variable occurrence, we have the assertion:

[x 7!t] ` x : t

since the type of a variable occurrence is determined by the type environment. (Recall that [x 7!t] is the same function as , except that it maps x to t.)

Now consider an expression not e whose value is the negation of the value of its subexpression e. If subexpression e is well-typed and has type B, then the entire expression is well-typed and has type B. This is expressed by the inference rule, where the part above the line is called the premise:

` e : B

` not e : B

Now consider an expression e1 + e2, which is the sum of two subexpressions e1 and e2. If each subexpression is well-typed and has type Z, then the entire expression is well-typed and has type Z. This is expressed by a two-premise inference rule:

` e1 : Z ` e2 : Z` e1 + e2 : Z

Now consider an expression (e1; e2) which builds a pair. If e1 has type t1 and e2 has type t2, and both are well-typed, then the pair (e1; e2) is well-typed and has type t1 t2:

` e1 : t1 ` e2 : t2` (e1; e2) : t1 t2

When f is a function of type t!t0, and e is an (argument) expression of type t, and both are well-typed, then the application f(e) is well-typed and has type t0:

` f : t!t0 ` e : t

` f(e) : t0

Using type inference rules, the type of a complex expression can be inferred from the assumptions (about the types of variables) held in the type environment .

For instance, when = [m 7! Z; n 7! Z], then the inference

` m : Z ` n : Z ` m : Z ` n : Z

` m + n : Z ` m , n : Z

` (m + n; m , n) : Z Z