Haskell is a functional programming language: that means that the main way in which we compute things is by defining functions which describe how to transform the inputs into the required output. Haskell has a collection of built-in data types which we can use to model the data in the problem domain, including numbers, booleans, lists, tuples and data types.
Haskell is also functional in a more distinctive way: functions are data in Haskell, and can be treated just like data of any other type.
Functions can be combined using operators, just like the numbers can be combined using the arithmetical operators.
Haskell provides lambda abstractions, which allow us to describe functions directly by expressions, rather than having to define and name a function in order to use it.
Functions can be the inputs and outputs of other functions in exactly the same way as any other type. Functions which have other functions as arguments or results are called higher-order functions.
In particular, the syntax of Haskell makes it particularly easy to partially apply functions and operators, so that functions are returned as the results of applying functions.
This chapter covers these topics, setting the scene for Developing higher-order programs where will put these ideas into practice.
Finally, we’ll also see that we can start to write function-level definitions – sometimes called ‘point-free’ definitions – which can be more concise, more readable and more suitable for program verification and transformation. Indeed, the chapter concludes with some examples of program verification involving higher-order polymorphic functions, and we see there that the theorems proved about them are reusable in exactly the same way that the functions themselves are reusable.
This section describes the built-in operators for function composition and application, as well as defining a new operator, forward composition, which composes functions in the ‘natural’ order.
Function composition is one of the simplest ways of structuring a program: do a number of things one after the other: each part can be designed and implemented separately.
Haskell has the function composition operator over functions built in. The operator, which is denoted by the ‘.’ between the two functions, has the effect of ‘wiring together’ two functions: passing the output of one to the input of another, and it is . This is pictured in Function composition, where the annotations of the arrows in the diagram indicate the types of elements involved.
For any functions f and g, the effect of f.g is given by the definition
(f.g) x = f (g x) -- (comp.1)
Not all pairs of functions can be composed. The output of g, g x, becomes the input of f, so that the output type of g must equal the input type of f.
Recalling the Picture example, we have already seen a definition of rotate:
Using the composition operator we can say directly that rotate is the composition of flipH with flipV: like
rotate = flipV . flipH -- (rotate.2)
Notice that we explained the definition (rotate.2) as the ‘composition of flipH with flipV’: why that way round? We do this because flipH is the function that is applied first, with flipV being applied to the result of the first application. We are able to compose flipH with flipV because the output of flipH and the input of flipV are both of Picture type.
In general, the constraint on which functions can be composed is expressed by giving ‘.’ the type
which shows that, if we call the first input f and the second g,
The input of f and the output of g are of the same type: b.
The result f.g has the same input type, a, as g and the same output type, c, as f.
Composition is associative, that is f.(g.h) is equal to (f.g).h for all f, g and h. We can therefore write f.g.h unambiguously to mean ‘do h, then g, then f’.1
The ‘binding power’ of composition
There is a common error caused by the binding powers of function application and function composition.
It is an error to write f.g x thinking it means (f.g) applied to x. Because function application binds more tightly than anything else, it is interpreted by the system as f.(g x), which will often lead to a type error. For example, evaluating
not.not True
gives the type error message
Couldn't match expected type `a -> Bool'
against inferred type `Bool'
In the second argument of `(.)', namely `not True'
In the expression: not . not True
In the definition of `it': it = not . not True
since there is an attempt to treat not True as a function to be composed with not. Such a function needs to have type a -> Bool, whereas it actually has type Bool.
In applying a composition we therefore need to be sure that it is parenthesized like this:
The order in f.g is significant, and can be confusing; (f.g) means ‘first apply g and then apply f to the result’, so the function that is applied first comes second in the composition.
It is simple in Haskell to define an operator for composition which takes its arguments in the opposite order to ‘.’, like this:
infixl 9 >.>
(>.>) :: (a -> b) -> (b -> c) -> (a -> c)
g >.> f = f . g -- (fcomp.1)
This definition has the effect that
(g >.> f) x = (f.g) x = f (g x) -- (fcomp.2)
showing that, as it were, the order of the f and g is swapped before the functions are applied. The rotate example can then be written
rotate = flipH >.> flipV
which we can read as flipHthenflipV, with the functions being applied from left to right.
The notation ‘>.>’ contains a ‘.’ to show that it is a form of composition, with the arrows showing the direction in which information is flowing. We will tend to use ‘>.>’ in situations where a number of functions are composed, and it is therefore tiresome to read some lines down the page in order to work out the effect of a function definition.
We’re familiar in Haskell with how to write the application of a function f to an argument e: we just write f next to e, like this: f e. In other words, we juxtapose the function and its argument.
We can also explicitly write down an application using the application operator, ‘$’, like this: f $ e. Why on earth would we want to do this, when we can write it without the ‘$’? There are two reasons that an explicit application gets used:
Many Haskell programmers use ‘$’ as an alternative to parentheses, so you may well see this in libraries that people have written. Instead of writing something like
flipV (flipH (rotate horse))
it is possible to write:
flipV flipH rotate horse
with the same meaning. Arguably this is a little clearer, and it is shorter! Incidentally you can see from this example that ‘$’ is right associative.
We need to use the application operator as a function, as in the example
zipWith ($) [sum,product] [[1,2],[3,4]]
where the application operator is applied to corresponding elements of the two lists.
Application and composition
Application and composition can get confused. Function composition combines two functions, while application combines a function and an argument (which can be a function, of course). If, for example, f has type Integer -> Bool, then
f.x means f composed with the functionx; x therefore needs to be of type s -> Integer for some type s.
f x means f applied to the object x, so x must therefore be an integer.
f $ x also means f applied to the object x, and so x must again be an integer.
Exercises
11.1 Redefine the function printBill from the supermarket billing exercise in Extended exercise: supermarket billing so that composition is used. Repeat the exercise using forward composition, >.>.
11.2 If id is the polymorphic identity function, defined by id x = x, explain the behaviour of the expressions
(id.f) (f.id) id f
If f is of type Int -> Bool, at what instance of its most general type a -> a is id used in each case? What type does f have if f id is properly typed?
11.3 Define a function composeList which composes a list of functions into a single function. You should give the type of composeList, and explain why the function has this type. What is the effect of your function on an empty list of functions?
11.4 What is the type of the application operator, $?
11.5 What is the result of the expression given above:
zipWith ($) [sum,product] [[1,2],[3,4]]
11.6 If id is the polymorphic identity function, defined by id x = x, explain the behaviour of the expressions
(id $ f) (f $ id) id ($)
If f is of type Int -> Bool, at what instance of its most general type a -> a is id used in each case? What type does f have if f $ id is properly typed?
Haskell definitions give us a way of defining functions, and once we have defined a function we can use its name to refer to it, as in the application
map addOne [2,3,4]
assuming that we’ve already defined
addOne x = x+1
Haskell gives us a way of writing down an expression that means ‘the function that adds one to a number’ directly, without having to give it a name. We write
\x -> x+1
which we can read as saying ‘the function that takes x to x+1’, the initial ‘\’ signalling that it’s a function. So, we can add one to all the numbers in the list [2,3,4] by writing the expression
map (\x -> x+1) [2,3,4]
An expression like (\x -> x+1) is called a lambda abstraction.
Why is a called a ‘lambda abstraction’?
The ‘lambda’ comes from the lambda calculus, a mathematical theory of functions. The symbol ‘\’ is the closest ASCII character to the Greek character lambda, λ, used in the λ-calculus. One of the inventors of the λ-calculus was Haskell B. Curry, after whom Haskell is named.
The ‘abstraction’ comes from the fact that the expression (\x -> e) is a function, which ‘abstracts away’ from the particular expression e.
Let’s take a look at some other uses of this notation now. Suppose that we want to take a list of functions and apply them all to a particular argument,
mapFuns :: [a->b] -> a -> [b]
giving a list of results. We might do this in playing a game of Rock - Paper - Scissors where we apply a number of different strategies to the current game position, and then compare the different results; we’ll come back to this scenario later in the chapter.
We could define the function by recursion, like this:
mapFuns [] x = []
mapFuns (f:fs) x = f x : mapFuns fs x
but in fact we can use map in making the definition: what we have to do at each element of the list (remember, each element is a function) is to apply it to x, so
mapFuns fs x = map (\f -> f x) fs
What’s important to see here is that the function (\f -> f x) depends on the value of x, and so we cannot define it as a top level function. We could, alternatively, define it in a where clause,
mapFuns fs x = map applyToX fs
where
applyToX f = f x
The first definition is clearer, and defines the operative function directly, rather than having to name and define it in a where clause, separately from where it is used; of course, either is OK, and it’s a matter of taste which you might use.
One of the main uses of lambda abstractions is to define functions which are the results of functions. Let’s look at the example of the function
addNum :: Integer -> (Integer -> Integer)
The function takes an integer, 17 say, and returns a function: in this case the function that adds 17 to its argument. The definition says this directly:
Another example which uses a lambda abstraction is given by the ‘plumbing’ illustrated in Plumbing f and g together..
Plumbing f and g together.
The object shown is a function, whose arguments are x and y. The result of the function is
g (f x) (f y)
so the overall effect is to give a function which applies f to each of its (two) arguments before applying g to the results. Again, the definition states this directly:
comp2 :: (a -> b) -> (b -> b -> c) -> (a -> a -> c)
comp2 f g = (\x y -> g (f x) (f y))
To add together the squares of 3 and 4 we can write
comp2 sq add 3 4
where add and sq have the obvious definitions.
In general, a lambda abstraction is an anonymous version of the sort of function we have defined earlier. In other words, the function f defined by
f x y z = result
and the function
\x y z -> result
have exactly the same effect.
We shall see in the next section that partial application will make many definitions – including some of the functions here – more straightforward. On the other hand the lambda abstraction is more general, and thus can be used in situations when a partial application could not.
Exercises
11.7 Using a lambda abstraction, the Boolean function not and the built-in function elem describe a function of type
Char -> Bool
which is True only on non-whitespace characters, that is those which are not elements of the list " \t\n".
11.8 Define a function total
total :: (Integer -> Integer) -> (Integer -> Integer)
so that total f is the function which at value n gives the total
f 0 + f 1 + ... + f n
You should be able to do this using built-in functions, rather than using recursion.
11.9 Given a function f of type a -> b -> c, write down a lambda abstraction that describes the function of type b -> a -> c which behaves like f but which takes its arguments in the other order. Pictorially,
11.10 Using the last exercise, or otherwise, give a definition of the function
flip :: (a -> b -> c) -> (b -> a -> c)
which reverses the order in which its function argument takes its arguments.
In this section we’ll discover how it is possible to partially apply functions in Haskell, and what the effect of this is. Underlying the Haskell approach to functions is what is called the curried representation of functions, in honour of Haskell Curry; this is introduced in the section after this.
The function multiply multiplies together two arguments,
multiply :: Int -> Int -> Int
multiply x y = x*y
We can view the function as a box, with two input arrows and an output arrow.
If we apply the function to two arguments, the result is a number; so that, for instance, multiply 2 3 equals 6.
What happens if multiply is applied to one argument 2? Pictorially, we have
From the picture we can see that this represents a function, as there is still one input arrow to the function awaiting a value. This function will, when given the awaited argument y, return double its value, namely 2*y.
This is an example of a general phenomenon: any function taking two or more arguments can be partially applied to one or more arguments. This gives a powerful way of forming functions as results.
In this definition there are two partial applications:
multiply 2 is a function from integers to integers, given by applying multiply to one rather than two arguments;
map (multiply 2) is a function from [Int] to [Int], given by partially applying map.
Partial application is being put to two different uses here.
In the first case – multiply 2 – the partial application is used to form the function which multiplies by two, and which is passed to map to form the doubleAll function.
the second partial application – of map to multiply 2 – could be avoided by writing the argument to doubleAll
doubleAll xs = map (multiply 2) xs
but it is quite possible to write a function level definition like this, and it is shorter and clearer than the definition with the arguments supplied.
which when applied to an integer n was intended to return the function which adds n to its argument. With partial application we have a simpler mechanism, as we can say
addNum n m = n+m
since when addNum is applied to one argument n it returns the function adding n to its argument.
Order of arguments
It is not always possible to make a partial application, since the argument to which we want to apply the function may not be its first argument. Let’s look at the function
elem :: Char -> [Char] -> Bool
We can test whether a character ch is a whitespace character by writing
elem ch whitespace
where whitespace is the string " \t\n". We would like to write the function to test this by partially applying elem to whitespace, but cannot, because this is the secdon argument rather than the first.
One solution is to define a variant of elem which takes its arguments in the other order, as in
member xs x = elem x xs
and write the function as the partial application
member whitespace
Alternatively, we can write down this function as a lambda abstraction, like this:
The operators of the language can be partially applied, giving what are known as operator sections. Examples include
(+2)
The function which adds two to its argument.
(2+)
The function which adds two to its argument.
(>2)
The function which returns whether a number is greater than two.
(3:)
The function which puts the number 3 on the front of a list.
(++"\n")
The function which puts a newline at the end of a string.
("\n"++)
The function which puts a newline at the beginning of a string.
($ 3)
The function which applies its argument – which will have to be a function – to the integer 3.
The general rule here is that a section of the operator op will put its argument to the side which completes the application. That is,
(op x) y = y op x
(x op) y = x op y
When combined with higher-order functions like map, filter and composition, the notation is both powerful and elegant, enabling us to make a whole lot more function-level definitions. For example,
filter (>0) . map (+1)
is the function which adds one to each member of a list, and then removes those elements which are not positive.
Parentheses in Haskell
The main role of parentheses, ( …), in Haskell is to group items together so that the system interprets what you have written in the right way. Typical examples include
enclosing a pattern in a definition, as in sum (Node t1 t2) = …;
enclosing a negative literal in a function application, as in fac (-1);
enclosing a type annotation, as in foldr plus (1::Int) [1..1000];
overriding the binding power of operators, as in (2+3)*6;
grouping names in a deriving clause like deriving (Eq, Show) .
However, other uses of parentheses have an effect of building data elements or changing the meaning of an identifier.
To form a tuple, it is necessary to enclose the items in parentheses, as in (1,True); the notation 1,True on its own is meaningless.
To turn an infix operator into a prefix operator, it must be enclosed in parentheses, as in (&&).
To form an operator section, the operator and arguments are enclosed in parentheses as seen in this example: (&& True).(0 /=).(‘rem‘ 2).
The partial application and operator sections is important in Haskell programming. We have already seen that many functions can be defined as specializations of general operations like map, filter and so on. These specializations arise by passing a function to the general operation – this function is often given by a partial application, as in the examples from the pictures case study first seen in Introducing functional programming:
More examples of partial applications will be seen throughout the material to come, and can be used to simplify and clarify many of the preceding examples. Three simple examples are the text processing functions we first looked at in Example: text processing:
dropSpace = dropWhile (member whitespace)
dropWord = dropWhile (not . member whitespace)
getWord = takeWhile (not . member whitespace)
Functions in Haskell are represented in curried form, where they take their arguments one at a time. This is called currying after Haskell Curry2 who was one of the pioneers of the λ-calculus and after whom the Haskell language is named. This section explains how curried functions work, and how we can covert to and fro between curried and uncurried form.
Why are Haskell functions in curried form? A major reason is that it supports partial application, as explored in the previous section; it also gives a ‘clean’ readable form to the syntax. One reason against choosing a curried representation is its unfamiliarity to most programmers; another is discussed towards the end of the section.
Partial application can appear confusing: in some contexts functions appear to take one argument, and in others more than one. In fact, every function in Haskell takes exactly one argument. This is called the curried representation of functions.If this application yields a function, then this function may be applied to a further argument, and so on. Consider the multiplication function again.
multiply :: Int -> Int -> Int
This is shorthand for
multiply :: Int -> (Int -> Int)
and so it can therefore be applied to an integer. Doing this gives (for example)
multiply 2 :: Int -> Int
This can itself be applied to give
(multiply 2) 5 :: Int
which, since function application is left associative, can be written
multiply 2 5 :: Int
Our explanations earlier in the book are consistent with this full explanation of the system. We hid the fact that
but this did no harm to our understanding of how to use the Haskell language. It is to support this shorthand that function application is made left associative and -> is made right associative.
The syntax of application and ->
Function application is left associative so that f x y means (f x) y, notf (x y).
The function space symbol ‘->’ is right associative, so that a -> b -> c means a -> (b -> c), not(a -> b) -> c.
The arrow is not associative.
Functions f :: Int -> Int -> Int and g :: (Int -> Int) -> Int are illustrated here
The function f will yield a function from Int to Int when given a Int – an example is multiply. On the other hand, when given a function of type Int -> Int, g yields a Int. An example is
g :: (Int -> Int) -> Int
g h = (h 0) + (h 1)
The function g defined here takes a function h as argument and returns the sum of h’s values at 0 and 1, and so g succ will have the value 3.
In Haskell we have a choice of how to model functions of two or more arguments. For instance, a function to multiply two integers would normally be defined thus:
multiply :: Int -> Int -> Int
multiply x y = x*y
while an uncurried version can be given by bundling the arguments into a pair, thus:
multiplyUC :: (Int,Int) -> Int
multiplyUC (x,y) = x*y
Why do we usually opt for the curried form? There are a number of reasons.
The notation is somewhat neater; we apply a function to a single argument by juxtaposing the two, f x, and application to two arguments is done by extending this thus: g x y.
It permits partial application. In the case of multiplication we can write expressions like multiply 2, which returns a function, while this is not possible if the two arguments are bundled into a pair, as is the case for multiplyUC.
We can in any case move between the curried and uncurried representations with little difficulty, and indeed we can define two higher-order functions which convert between curried and uncurried functions.
Suppose first that we want to write a curried version of a function g, which is itself uncurried and of type (a,b) -> c.
This function expects its arguments as a pair, but its curried version, curry g, will take them separately – we therefore have to form them into a pair before applying g to them:
curry :: ((a,b) -> c) -> (a -> b -> c)
curry g x y = g (x,y)
curry multiplyUC will be exactly the same function as multiply.
Suppose now that f is a curried function, of type a -> b -> c.
The function uncurry f will expect its arguments as a pair, and these will have to be separated before f can be applied to them:
uncurry :: (a -> b -> c) -> ((a,b) -> c)
uncurry f (x,y) = f x y
uncurry multiply will be exactly the same function as multiplyUC. The functions curry and uncurry are inverse to each other.
A disadvantage of the curried representation of functions is that the inverse of a function like
unzip :: ([a,b]) -> ([a],[b])
is not zip :: [a] -> [b] -> [(a,b)] but in fact
uncurry zip :: ([a],[b]) -> [(a,b)]
(or zip’ as we called it earlier in the book) so that statements of properties of these functions, such as
prop_zip xs = uncurry zip (unzip xs) == xs
will necessarily involve the uncurried version of the binary function, rather than the curried.
Exercises
11.14 What is the effect of uncurry ($)? What is its type? Answer a similiar question for uncurry (:), uncurry (.).
11.15 [Harder] What are the effects and types of uncurry uncurry, curry uncurry.
11.16 Can you state a property relating unzip and uncurry zip, where the latter is the function applied first?
11.17 Can you define functions
curry3 :: ((a,b,c) -> d) -> (a -> b -> c -> d)
uncurry3 :: (a -> b -> c -> d) -> ((a,b,c) -> d)
which perform the analogue of curry and uncurry but for three arguments rather than two? Can you use curry and uncurry in these definitions?
which perform the analogue of curry and uncurry but for a list of arguments rather than two distinct arguments? Can you use curry and uncurry in these definitions?
This section revises the different ways that we can use to define higher-order functions, and in particular functions that return functions as results. These functions are one of the features of functional programming not shared with most other programming languages that you might be familiar with, and give Haskell particular elegance and power.
where again the function is defined directly as the composition of two other functions. The meaning of this definition is just the same as one which has explicit arguments:
rotate pic = flipV (flipH pic)
but the earlier definition is clearer to read and to modify; we see explicitly that the definition is a composition of two functions, rather than having to see it as a consequence of the way the right-hand side is defined in the latter equation.
More importantly, if we state a definition in this form, then we can apply properties of ‘.’ in analysing how rotate behaves. This means that in proofs we are able to use properties of composition, as well as being able to see examples of program transformations which will apply because of the form of composition involved. In general these remarks will apply to all higher-order, polymorphic functions, and we see examples of this in Verification and general functions below.
Let’s look at some more examples which use composition in their definitions: the simplest is this:
twice f = f.f -- (twice.1)
f is a function, and the result is f composed with itself. For this to work, it needs to have the same input and output type, so we have
twice :: (a -> a) -> (a -> a)
This states that twice takes one argument, a function of type (a -> a), and returns a result of the same type. For instance, if succ is the function to add one to an integer,
succ :: Integer -> Integer
succ n = n+1
then applying twice to it gives the example
(twice succ) 12
~> (succ.succ) 12 -- by (twice.1)
~> succ (succ 12) -- by definition of .
~> 14
We can generalize twice so that we pass a parameter giving the number of times the functional argument is to be composed with itself
iter :: Integer -> (a -> a) -> (a -> a)
iter n f
| n>0 = f . iter (n-1) f -- (iter.1)
| otherwise = id -- (iter.2)
This is a standard primitive recursion over the integer argument; in the positive case we take the composition of f with itself n-1 times and compose once more with f. In the zero case we apply f no times, so the result is a function which returns its argument unchanged, namely id.
As an example of using iter, we can define 2^n as iter n double 1, if double doubles its argument.
Local definitions allow us to define functions as a subsidiary part of a function definition. We looked earlier at the example of
addNum :: Integer -> Integer -> Integer
We can use a local definition to give the result, either using a where
addNum n = addN
where
addN m = n+m
or a let
addNum n = let
addN m = n+m
in
addN
This gives us a way of defining results which are functions by locally defining that function and returning it as the result; it has the advantage of not requiring any more advanced machinery, but the disadvantage of introducing a named definition of addN which is extraneous to the actual result.
Let’s try to define a function that takes a binary function as argument, and which returns a binary function that takes its arguments in the opposite order; let’s call it flip:
flip :: (a -> b -> c) -> (b -> a -> c)
We can use a lambda abstraction to give the result:
flip f = \x y -> f y x -- (flip.1)
This makes clear that a function like flip map takes as its first argument the list and as its second the function to be mapped; it can then be partially applied to its first argument, having the effect of applying map to its second only. This allows us to do a partial application to the second argument of a two argument function.
Partial applications give us a particularly direct way of defining some higher order functions. Taking the example we have just looked at, we can instead say
flip f x y = f y x
If we apply flip to one argument, we have a function which behaves just as described in (flip.1). Similarly, the behaviour of
addNum n = addN
where
addN m = n+m
is given by the simple definition
addNum n m = n+m
partially applied to n.
Constructors are functions too
Datatype constructors are functions, and so they can be partially applied, passed as arguments to functions or indeed returned as results. To give just one example, this expression creates a list of People from lists of names and ages:
zipWith Person ["Geraint","Bob"] [45,67]
Point-free programming
Some function-level, or ‘point-free’, definitions express what the function does with real clarity: writing flipV = map reverse precisely describes how to flip a picture in a vertical mirror. However, it is possible to take this approach too far, and write definitions which it’s very hard to understood. For instance, what does this function do:
puzzle = (.) (.)
Reading the definition tells us that it is the composition operator partially applied to itself, but still it’s not clear what the function will do. How can we work out what it does? The best way is to apply it to some arguments and see what it does:
(.) (.) x ~>(.).x
so
(.) (.) x y ~>((.).x) y ~>(.) (x y)
Applying to a third argument gives
(.) (.) x y z ~> ... ~>(.) (x y) z ~>(x y) . z
and finally
(.) (.) x y z w ~> ... ~>((x y) . z) w ~>(x y) (z w)
giving us the much more informative explanation:
puzzle x y z w = (x y) (z w)
Finally, we use to get GHCi to give its type, like this :type (.)(.) and get
(.)(.) :: (a1 -> b -> c) -> a1 -> (a -> b) -> a -> c
So there we are … To be fair, once we understand what puzzle does, it can be useful to have the original definition which explicitly uses the composition operator, because then any general laws that we discover for (.) will apply to puzzle too.
We conclude this section by exploring how partial applications and operator sections can be used to simplify and shorten definitions in a number of other examples. Often it is possible to avoid giving an explicit function definition if we can use a partial application to return a function. Revisiting the examples of Defining functions over lists we see that to double all the elements in a list we can write
doubleAll :: [Int] -> [Int]
doubleAll = map (*2)
using an operator section (*2) to replace the double function, and giving the function definition directly by partially applying map.
To filter out the even elements in a numerical list, we have to check whether the remainder on dividing by two is equal to zero. As a function we can write
(==0).(`mod` 2)
This is the composition of two operator sections: first find the remainder on dividing by two, then check if it is equal to zero. (Why can we not write (‘mod‘ 2 == 0)?) The filtering function can then be written
which takes a function f as argument, and returns (an approximation to) the two argument function which gives the area under its graph between two end points as its result.
Verification can take on a different character when we look at higher-order polymorphic functions. We can start to prove equalities between functions, rather than between values of functions, and we shall also see that we are able to prove theorems which resemble their subjects in being general and reusable, and so applicable in many contexts.
iter 2 f
= f . iter 1 f -- by (iter.1)
= f . (f . iter 0 f) -- by (iter.1)
= f . (f . id) -- by (iter.2)
= f . f -- by (compId)
= twice f -- by (twice.1)
In proving this we have used the equality between two functions
f . id = f -- (compId)
How is this proved? We examine how each side behaves on an arbitrary argument x
(f . id) x
= f (id x)
= f x
so that for any argument x the two functions have the same behaviour. As black boxes, they are therefore the same. As what interests us here is their behaviour, we say that they are equal. We call this ‘black-box’ concept of equality extensional.
Definition 2.
Principle of extensionality:
Two functions f and g are equal if they have the same value at every argument.
This is called extensionality in contrast to the idea ofintensionality in which we say two functions are the same only if they have the same definitions – we no longer think of them as black boxes; we are allowed to look inside them to see how the mechanisms work, as it were. If we are interested in the results of our programs, all that matters are the values given by functions, not how they are arrived at. We therefore use extensionality when we are reasoning about function behaviour in Haskell. If we are interested in efficiency or other performance aspects of programs, then the way in which a result is found will be significant, however. This is discussed further in Time and space behaviour.
Exercises
11.25 Using the principle of extensionality, show that function composition is associative: that is, for all f, g and h,
Our verification thus far has concentrated on first-order, monomorphic functions. Just as map, filter and fold generalize patterns of definition, we shall find that proofs about these functions generalize results we have seen already. To give some examples, it is not hard to prove that
doubleAll (xs++ys) = doubleAll xs ++ doubleAll ys
holds for all finite lists xs and ys. When doubleAll is defined as map (*2) it becomes clear that we have an example of a general result,
map f (xs++ys) = map f xs ++ map f ys -- (map++)
which is valid for any function f. We also claimed in an earlier exercise that
sum (xs++ys) = sum xs + sum ys -- (sum.3)
for all finite lists xs, ys. The function sum is given by folding in (+),
sum = foldr (+) 0
and we have, generally, if f is associative, and st is an identity for f, that is,
x `f` (y `f` z) = (x `f` y) `f` z
x `f` st = x = st `f` x
for all x, y, z then the equation
foldr f st (xs++ys) = f (foldr f st xs) (foldr f st ys) -- (foldr.3)
holds for all finite xs and ys. Obviously (+) is associative and has 0 as an identity, and so (sum.3) is a special case of (foldr.3). Now we give three proofs of examples in the same vein.
A first example concerns map and composition. Recall the definitions
map f [] = [] -- (map.1)
map f (x:xs) = f x : map f xs -- (map.2)
(f . g) x = f (g x) -- (comp.1)
It is not hard to see that we should be able to prove that
map (f . g) xs = (map f . map g) xs -- (map.3)
holds for every finite list xs.
Applying (f . g) to every member of a list should be the same as applying g to every member of the list and then applying f to every member of the result. It is proved just as easily, by structural induction. The (base) case requires the identity to be proved for the empty list.
map (f . g) [] = [] -- by (map.1)
(map f . map g) []
= map f (map g []) -- by (comp.1)
= map f [] -- by (map.1)
= [] -- by (map.1)
Again, it is enough to analyse each side of the equation.
map (f . g) (x:xs)
= (f . g) x : map (f . g) xs -- by (map.2)
= f (g x) : map (f . g) xs -- by (comp.1)
(map f . map g) (x:xs)
= map f (map g (x:xs)) -- by (comp.1)
= map f (g x : map g xs) -- by (map.2)
= f (g x) : map f (map g xs) -- by (map.2)
= f (g x) : (map f . map g) xs -- by (comp.1)
The induction hypothesis is exactly what is needed to prove the two sides equal, completing the proof of the induction step and the proof itself. ⬛
Each Haskell list type, besides containing finite lists, also contains infinite and partial lists. In Lazy programming these will be explained and it will be shown that (map.3) is true for all lists xs, and therefore that the functional equation
The proof above showed how properties of functional programs could be proved from the definitions of the functions in a straightforward way. The properties can state how the program behaves – that a sorting function returns an ordered list, for instance – or can relate one program to another. This latter idea underlies program transformation for functional languages. This section introduces an example called filter promotion which is one of the most useful of the basic functional transformations.
filter p . map f = map f . filter (p . f) -- (filter/map)
The equation says that a map followed by a filter can be replaced by a filter followed by a map. The right-hand side is potentially more efficient than the left, since the map operation will there be applied to a shorter list, consisting of just those elements with the property (p . f). An example is given by the function first defined in Partially applied operators: operator sections.
filter (0<) . map (+1)
Instead of mapping first, the function can be replaced by
and it is clear that here the transformed version is more efficient, since the test (0<=) is no more costly than (0<). The proof that
(filter p . map f) xs = (map f . filter (p . f)) xs
for finite lists xs is by structural induction. First we reiterate the definitions of map, filter and composition.
map f [] = [] -- (map.1)
map f (x:xs) = f x : map f xs -- (map.2)
filter p [] = [] -- (filter.1)
filter p (x:xs)
| p x = x : filter p xs -- (filter.2)
| otherwise = filter p xs -- (filter.3)
(f . g) x = f (g x) -- (comp.1)
The base case consists of a proof of
(filter p . map f) [] = (map f . filter (p . f)) [] -- (base)
This is true since
(filter p . map f) []
= filter p (map f []) -- by (comp.1)
= filter p [] -- by (map.1)
= [] -- by (filter.1)
and
(map f . filter (p . f)) []
= map f (filter (p . f) []) -- by (comp.1)
= map f [] -- by (filter.1)
= [] -- by (map.1)
In the induction step, a proof of
(filter p . map f) (x:xs) = (map f . filter (p . f)) (x:xs) -- (ind)
is required, using the induction hypothesis
(filter p . map f) xs = (map f . filter (p . f)) xs -- (hyp)
The proof begins with an analysis of the left-hand side of (ind).
(filter p . map f) (x:xs)
= filter p (map f (x:xs)) -- by (comp.1)
= filter p (f x : map f xs) -- by (map.2)
There are two3 cases to consider: whether p (f x) is True or False. Taking the case where p (f x) is True, we continue to examine the left-hand side of (ind), giving
= f x : filter p (map f xs) -- by (filter.2)
= f x : (filter p . map f) xs -- by (comp.1)
= f x : (map f . filter (p . f)) xs -- by (hyp)
Now we look at the right-hand side of (ind), also assuming that p (f x) is True:
(map f . filter (p . f)) (x:xs)
= map f (filter (p . f) (x:xs)) -- by (comp.1)
= map f (x: (filter (p . f) xs)) -- by (filter.2)
= f x : map f (filter (p . f) xs) -- by (map.2)
= f x : (map f . filter (p . f)) xs -- by (comp.1)
which shows that (ind) holds in the case that p (f x) is True.
A similar chain of reasoning gives the same result in the case where p (f x) is False. This establishes (ind) assuming (hyp), and so together with (base) completes the proof of the filter promotion transformation in the case of finite lists; it holds, in fact, for all lists. ⬛
We’ve already seen that QuickCheck is a very good way of checking whether particular properties hold for functions that we define. QuickCheck works by generating random test data and checking whether properties hold at these values. While generating data is not entirely straightforward for structured types like lists and algebraic types, it can be done. Generating random functions is more difficult, and isn’t supported “out of the box” by QuickCheck: for it to work we need to be able to “show” functions. We examine how to do this, and so how to use QuickCheck to test properties involving higher-order functions, in Domain-Specific Languages. In the meantime we look at how to check properties for given functions and randomly-generated lists.
Let’s take the example of the property for map and filter, (filter/map) introduced:
prop_mf p f =
\xs -> (filter p . map f) xs == (map f . filter (p . f)) xs
We can check this for specific values of p and f like this
When we introduced the Picture case study in Introducing functional programming we claimed that we could prove that flipV and flipH can be applied in either order to give the same result. Our implementation defines them thus
flipH = reverse
flipV = map reverse
and we can see informally that
reverse affects the order of the elements, while leaving the elements unchanged;
map reverse affects each of the elements, while keeping their order the same.
The second observation is a consequence of the function being a map, and so we make the more general claim that for all finite lists xs and all functions f,
map f (reverse xs) = reverse (map f xs) -- (map/reverse)
This has the consequence that
flipV (flipH xs) = flipH (flipV xs)
if we replace f in (map/reverse) by reverse. We will see in Lazy programming that we can establish (map/reverse) for all lists xs and so conclude that the functional equations hold:
map f . reverse = reverse . map f
flipV . flipH = flipH . flipV
We now prove (map/reverse) by induction over xs.
We have seen the definition of map in the previous examples; reverse is defined thus.
We have seen in this section that we can prove properties of general functions like map, filter and foldr. This means that when we define a function which uses map, say, we can call on a whole library of properties of map, including, for all finite xs and ys:
map (f . g) xs = (map f . map g) xs
(filter p . map f) xs = (map f . filter (p . f)) xs
map f (reverse xs) = reverse (map f xs)
map f (ys++zs) = map f ys ++ map f zs
We have seen that using the general functions map, filter and others allowed us to make direct definitions of new functions rather than having to define them ‘from scratch’ using recursion. In exactly the same way, these general theorems will mean that in many cases we can avoid writing an induction proof about our specific function, and instead simply use one of these theorems.
Exercises
11.31 Prove that for all ys and zs the equation
map f (ys++zs) = map f ys ++ map f zs -- (map++)
as was used in the proof of the theorem about map and reverse.
11.32 If f is associative, and st is an identity for f – these notions were defined – then prove that the equation (foldr.3):
foldr f st (xs++ys) = f (foldr f st xs) (foldr f st ys)
holds for all finite xs and ys.
11.33 Argue that the result
concat (xs ++ ys) = concat xs ++ concat ys
is a special case of (foldr.3), using
concat = foldr (++) []
as the definition of concat.
11.34 Prove that for all finite lists xs, and functions f,
concat (map (map f) xs) = map f (concat xs)
11.35 Prove that over the type Int
(0<) . (+1) = (0<=)
as is used in the theorem relating map and filter.
We have seen in this chapter how we can write functions with functions as results. This means that we can create the functions by applying operations like map, filter and foldr within our programs, and that we can indeed treat functions as ‘first-class citizens’ of our programming language. A consequence of this has been that we are able to explain the definitions of some of the Picture operations first seen in Introducing functional programming.
The main mechanisms introduced here have allowed us to create functions by applying functions or operators to fewer arguments than we expected, thus creating partial applications and operator sections. We also saw how the Haskell-type system and syntax were adapted to deal with the curried form of function definitions, by which multi-argument functions take their arguments one at a time.
We concluded by showing that we could prove general properties about general functions like map, and thus build up libraries of results about these functions which can potentially be applied whenever the general function is reused.
For technical reasons, the ‘.’ is treated as right associative in the Haskell standard prelude. ↩
In fact the first person to describe the idea was Schönfinkel, but ‘Schönfinkeling’ does not sound so snappy! ↩
We should also think about what happens when p (f x) is undefined; in this case both sides will be undefined, and so equal. ↩