In this chapter we increase the level of generality that can be achieved in Haskell, by considering functions that are generic over a range of parameterised types such as lists, trees and input/output actions. In particular, we introduce functors, applicatives and monads, which variously capture generic notions of mapping, function application and effectful programming.

Functors

All three new concepts introduced in this chapter are examples of the idea of abstracting out a common programming pattern as a definition. We begin by reviewing this idea using the following two simple functions:

Both functions are defined in the same manner, with the empty list being mapped to itself, and a non-empty list to some function applied to the head of the list and the result of recursively processing the tail. The only important difference is the function that is applied to each integer in the list: in the first case it is the increment function (+1), and in the second the squaring function (^2). Abstracting out this pattern gives the familiar library function map,

using which our two examples can then be defined more compactly by simply providing the function to be applied to each integer:

More generally, the idea of mapping a function over each element of a data structure isn't specific to the type of lists, but can be abstracted further to a wide range of parameterised types. The class of types that support such a mapping function are called functors. In Haskell, this concept is captured by the following class declaration in the standard prelude:

That is, for a parameterised type f to be an instance of the class Functor, it must support a function fmap of the specified type.

What is this book?

Haskell is a purely functional language that allows programmers to rapidly develop software that is clear, concise and correct. The book is aimed at a broad spectrum of readers who are interested in learning the language, including professional programmers, university students and high-school students. However, no programming experience is required or assumed, and all concepts are explained from first principles with the aid of carefully chosen examples and exercises.Most of the material in the book should be accessible to anyone over the age of around sixteen with a reasonable aptitude for scientific ideas.

How is it structured?

The book is divided into two parts. Part I introduces the basic concepts of pure programming in Haskell and is structured around the core features of the language, such as types, functions, list comprehensions, recursion and higher-order functions. Part II covers impure programming and a range of more advanced topics, such as monads, parsing, foldable types, lazy evaluation and reasoning about programs. The book contains many extended programming examples, and each chapter includes suggestions for further reading and a series of exercises. The appendices provide solutions to selected exercises, and a summary of some of the most commonly used definitions from the Haskell standard prelude.

What is its approach?

The book aims to teach the key concepts of Haskell in a clean and simple manner. As this is a textbook rather than a reference manual we do not attempt to cover all aspects of the language and its libraries, and we sometimes choose to define functions from first principles rather than using library functions. As the book progresses the level of generality that is used is gradually increased. For example, in the beginning most of the functions that are used are specialised to simple types, and later on we see how many functions can be generalised to larger classes of types by exploiting particular features of Haskell.

How should it be read?

The basic material in part I can potentially be worked through fairly quickly, particularly for those with some prior programming experience, but additional time and effort may be required to absorb some of material in part II.

In this final chapter we show how the reasoning techniques introduced in the previous chapter can be used to calculate compilers. We start by showing how a semantics for a language can be transformed into a compiler in a series of steps, and then show how the steps can be combined to allow a compiler to be calculated directly from a statement of its correctness.

Introduction

The ability to calculate compilers has been a key objective in the field of program transformation since its earliest days. Starting from a high-level semantics for a source language, the aim is to transform the semantics into a compiler that translates source programs into a lower-level target language, together with a virtual machine that executes the resulting target programs.

There are two main advantages of such an approach. Firstly, the compiler, target language and virtual machine are systematically derived during the transformation process, rather than having to be manually defined by the user. And secondly, the resulting compiler and virtual machine do not usually require subsequent proofs of correctness, as they are correct by construction.

In chapter 16 we presented a compiler for arithmetic expressions, and proved its correctness. In this chapter we show how the compiler can be calculated directly from a statement of its correctness. We develop our approach in two stages, first introducing the basic ideas using a series of transformation steps, and then showing how the separate steps can be combined into a single step. For simplicity, we restrict our attention to arithmetic expressions, but the same techniques can also be used to calculate compilers for more sophisticated languages.

Syntax and semantics

We start in the same manner as the compiler correctness example from the previous chapter, with two definitions that respectively capture the syntax (form) and semantics (meaning) of a simple language of arithmetic expressions built up from integer values using an addition operator:

In this appendix we present model solutions to selected exercises for each chapter. If solutions are being tested out using GHCi, note that some functions may need to be renamed to avoid clashing with built-in functions from the standard prelude. For example, product could be renamed to myproduct.

Introduction

Exercise 1

or

There are a number of other possible answers.

Exercise 2

Exercise 3

For example:

First steps

Exercise 2

Exercise 3

Exercise 4

or

Types and classes

Exercise 1

Exercise 2

There are a number of other possible answers for bools, nums and add.

In this chapter we introduce lazy evaluation, the mechanism used to evaluate expressions in Haskell. We start by reviewing the notion of evaluation, then consider evaluation strategies and their properties, discuss infinite structures and modular programming, and conclude with a special form of function application that can improve the space performance of programs.

Introduction

As we have seen throughout this book, the basic method of computation in Haskell is the application of functions to arguments. For example, suppose that we define a function that increments an integer:

Then the expression inc (2*3) can be evaluated as follows:

Alternatively, the same final result can also be obtained by performing the first two function applications in the opposite order:

The fact that changing the order in which functions are applied does not affect the final result is not specific to simple examples such as the above, but is an important general property of function application in Haskell. More formally, in Haskell any two different ways of evaluating the same expression will always produce the same final value, provided that they both terminate. We will return to the issue of termination later on in this chapter.

We also note that the above property does not hold for most imperative programming languages, in which the basic method of computation is changing stored values. For example, consider the imperative expressionn + (n = 1)that adds the current value of the variable n to the result of changing its value to one. Assuming that n initially has the value zero, this expression can be evaluated by first performing the left-hand side of the addition

or alternatively, by first performing the right-hand side:

In this chapter we take our first proper steps with Haskell. We start by introducing the GHC system and the standard prelude, then explain the notation for function application, develop our first Haskell script, and conclude by discussing a number of syntactic conventions concerning scripts.

Glasgow Haskell Compiler

As we saw in the previous chapter, small Haskell programs can be executed by hand. In practice, however, we usually require a system that can execute programs automatically. In this book we use the Glasgow Haskell Compiler, a state-of-the-art, open source implementation of Haskell.

The system has two main components: a batch compiler called GHCi, and an interactive interpreter called GHCi. We will primarily use the interpreter in this book, as its interactive nature makes it well suited for teaching and prototyping purposes, and its performance is sufficient for most of our applications. However, if greater performance or a stand-alone executable version of a Haskell program is required, the compiler itself can be used. For example, we will use the compiler in extended programming examples in chapters 9 and 11.

Installing and starting

The Glasgow Haskell Compiler is freely available for a range of operating systems from the Haskell home page, http://www.haskell.org. For first time users we recommend downloading the Haskell Platform, which provides a convenient means to install the system and a collection of commonly used libraries. More advanced users may prefer to install the system and libraries manually.

Once installed, the interactive GHCi system can be started from the terminal command prompt, such as $, by simply typing ghci:

All being well, a welcome message will then be displayed:

The GHCi prompt > indicates that the system is now waiting for the user to enter an expression to be evaluated. For example, it can be used as a calculator to evaluate simple numeric expressions:

Following normal mathematical convention, in Haskell exponentiation is assumed to have higher priority than multiplication and division, which in turn have higher priority than addition and subtraction.

In this chapter we introduce a range of mechanisms for defining functions in Haskell. We start with conditional expressions and guarded equations, then introduce the simple but powerful idea of pattern matching, and conclude with the concepts of lambda expressions and operator sections.

New from old

Perhaps the most straightforward way to define new functions is simply by combining one or more existing functions. For example, a few library functions that can be defined in this way are shown below.

• Decide if an integer is even:

• Split a list at the nth element:

• Reciprocation:

Note the use of the class constraints in the types for even and recip above, which make precise the idea that these functions can be applied to numbers of any integral and fractional types, respectively.

Conditional expressions

Haskell provides a range of different ways to define functions that choose between a number of possible results. The simplest are conditional expressions, which use a logical expression called a condition to choose between two results of the same type. If the condition is True, then the first result is chosen, and if it is False, then the second result is chosen. For example, the library function abs that returns the absolute value of an integer can be defined as follows:

Conditional expressions may be nested, in the sense that they can contain other conditional expressions. For example, the library function signum that returns the sign of an integer can be defined as follows:

Note that unlike in some programming languages, conditional expressions in Haskell must always have an else branch, which avoids the well-known dangling else problem.

In this chapter we introduce mechanisms for declaring new types and classes in Haskell. We start with three approaches to declaring types, then consider recursive types, show how to declare classes and their instances, and conclude by developing a tautology checker and an abstract machine.

Type declarations

The simplest way of declaring a new type is to introduce a new name for an existing type, using the type mechanism of Haskell. For example, the following declaration from the standard prelude states that the type String is just a synonym for the type [Char] of lists of characters:

As in this example, the name of a new type must begin with a capital letter. Type declarations can be nested, in the sense that one such type can be declared in terms of another. For example, if we were defining a number of functions that transform coordinate positions, we might declare a position as a pair of integers, and a transformation as a function on positions:

However, type declarations cannot be recursive. For example, consider the following recursive declaration for a type of trees:

That is, a tree is a pair comprising an integer and a list of subtrees. While this declaration is perfectly reasonable, with the empty list of subtrees forming the base case for the recursion, it is not permitted in Haskell because it is recursive. If required, recursive types can be declared using the more powerful data mechanism, which will be introduced in the next section.

Type declarations can also be parameterised by other types. For example, if we were defining a number of functions that manipulate pairs of values of the same type, we could declare a synonym for such pairs:

Finally, type declarations with more than one parameter are possible too. For example, a type of lookup tables that associate keys of one type to values of another type can be declared as a list of (key,value) pairs:

Using this type, a function that returns the first value that is associated with a given key in a table can then be defined as follows:

Data declarations

A completely new type, as opposed to a synonym for an existing type, can be declared by specifying its values using the data mechanism of Haskell.

Modularity is the most important technique for controlling the complexity of programs. Programs are decomposed into separate components with precisely specified, and tightly controlled, interactions. The pathways for interaction among components determine dependencies that constrain the process by which the components are integrated, or linked, to form a complete system. Different systems may use the same components, and a single system may use multiple instances of a single component. Sharing of components amortizes the cost of their development across systems and helps limit errors by limiting coding effort.

Modularity is not limited to programming languages. In mathematics, the proof of a theorem is decomposed into a collection of definitions and lemmas. References among the lemmas determine a dependency relation that constrains their integration to form a complete proof of the main theorem. Of course, one person's theorem is another person's lemma; there is no intrinsic limit on the depth and complexity of the hierarchies of results in mathematics. Mathematical structures are themselves composed of separable parts, for example, a ring comprises a group and a monoid structure on the same underlying set. Modularity arises from the structural properties of the hypothetical and general judgments. Dependencies among components are expressed by free variables whose typing assumptions state the presumed properties of the component. Linking amounts to substitution to discharge the hypothesis.

Simple Units and Linking

Decomposing a program into units amounts to exploiting the transitivity of the hypothetical judgment (see Chapter 3). The decomposition may be described as an interaction between two parties, the client and the implementor, mediated by an agreed-upon contract, an interface. The client assumes that the implementor upholds the contract, and the implementor guarantees that the contract will be upheld. The assumption made by the client amounts to a declaration of its dependence on the implementor discharged by linking the two parties accordng to their agreed-upon contract.

The interface that mediates the interaction between a client and an implementor is a type. Linking is the implementation of the composite structural rules of substitution The type τintf is the interface type. It defines the operations provided by the implementor eimpl and relied upon by the client eclient.