Absurdity and negation in type theory

In Section 5.4, IV, we saw how implication can be coded in type theory (in particular, in λP). We recall: by coding the implication A ⇒ B as the function type A → B, we mimic the behaviour of ‘implication’, including its introduction and elimination rule, in type theory. So we also have minimal propositional logic in λC, since λP is part of λC.

In order to get more than minimal propositional logic, we have to be able to handle more connectives, such as negation (‘¬’), conjunction (‘∧’) and disjunction (‘∨’). This cannot be done in λP, but in λC there exist very elegant ways to code the respective notions, as we presently show.

We start with negation. It is natural to consider the negation ¬A as the implication A ⇒ ⊥, where ⊥ is the ‘absurdity’, also called contradiction. So we interpret ¬A as ‘A implies absurdity’. But for this we first need a coding of the absurdity itself. (In Exercises 3.5 and 6.1 (a) we already mentioned codings of ⊥ in λ2 and λC, which we shall justify below.)

I. Absurdity

A characteristic property of the proposition ‘absurdity’, or ⊥, is the following:

If ⊥ is true, then every proposition is true.

In natural deduction this property is known under the name ⊥-elimination.

An example to start with

Logic, a fundamental part of many sciences, can be fruitfully expressed and used in an appropriate type-theory-with-definitions such as λD. We have demonstrated this extensively in Chapter 11. Our conclusion is that a flag-style approach, which is still fully formal, is very similar to the common informal style of deduction which is standard for reasoning in both logic and mathematics. The type theory λD can be fruitfully exploited for expressing the logical system of natural deduction in a feasible and practical manner.

In the present chapter, we turn to mathematics. The deductive framework of logic is essential for doing mathematics, since it embodies the principles of reasoning, but mathematics itself is much more than logic (or reasoning) alone.

In order to explore these matters, we start with some illustrative examples, showing the possibilities and the problems connected with doing mathematics in type theory. Our purpose is to investigate whether (or rather: to show how) λD ‘works’ in mathematical practice.

It will turn out that a formal translation of a mathematical text into the λD-format may demand more effort than expected. This is due, of course, to the very precise nature of the ‘formal language’ λD, requiring all aspects to be spelled out, sometimes even to an annoying degree of detail; although the flag style alleviates the burden to some extent.

Useful applications of λD

The type theory λD provides a system in which mathematical definitions, statements and proofs can be completely spelled out in a very structured way that is still close to ordinary mathematical practice. This enables and facilitates the formalisation of mathematics and the checking of its correctness. Below, we summarise the main features of type theory, and in particular λD, as a system for formalising mathematics.

Formalisation of mathematics via type theory In λD-like type theory, a mathematical notion can be defined precisely in full detail and the definition can be reasoned with in a logically sound way. The type system enforces a very high level of precision, which gives additional insight into mathematical and logical constructs. Nevertheless, formalising mathematics in λD is still very close to what is standard in mathematics.

Checking of mathematics The high level of precision of type theory greatly improves the level of correctness of the formalised mathematics: incomplete proofs, or proofs using illegal logical steps, are not accepted and a definition has to be syntactically correct. The soundness of course still depends on the axioms that one has assumed: if the axioms do not correspond to what one wants to formalise, or if they are inconsistent, the derived results are still useless. This already applies to informal mathematics, so the formalisation in type theory is separate from the question of whether the axioms are sound.

Formalising a proof of Bézout's Lemma

In Section 8.7, we considered a well-known theorem from number theory, and we have given a mathematical proof of it in Section 8.8. We now revisit this theorem and its proof, which are reproduced below, and translate it into the formal λD-format.

A thorough inspection of what we need for the formalisation of the proof in its entirety will take up the space of a full chapter: the present one. It acts as a final exercise, showing several important aspects of λD.

In the process, we will encounter various questions and problems. We'll try to foresee some of these questions and solve them before we start the actual proof. Other problems we solve ‘on the fly’. On some occasions, we come across situations of missing foreknowledge that is either too laborious or too uninspiring to be dealt with in this book; in those cases we resort to only summarising what is lacking. Hence, we decide neither to fill every gap, nor to always supply the relevant details.

The mentioned theorem reads as follows:

'Theorem (“Bézout's Lemma”, restricted version)

Let m, n ∈ ℕ+ be coprime. Then ∃x,y∈ℤ(mx + ny = 1).’

Remark 15.1.1The lemma has been attributed to the French mathematician É. Bézout (1730–1783), although it already appeared in earlier work of others.

The present book is a completely rewritten version of the second edition of my Introduction to Functional Programming using Haskell (Prentice Hall). The main changes are: a reorganisation of some introductory material to reflect the needs of a one or two term lecture course; a fresh set of case studies; and a collection of over 100 exercises that now actually contain answers. As before, no knowledge of computers or programming is assumed, so the material is suitable as a first course in computing.

Every author has his or her own drum to beat when writing a textbook, and the present one is no different. While there are now numerous books, tutorials, articles and blogs devoted to Haskell, few of them emphasise what seems to me the main reason why functional programming is the best thing since sliced bread: the ability to think mathematically about functional programs. And the mathematics involved is neither new nor difficult. Any student who has come to grips with, say, high-school trigonometry and has applied simple trigonometric laws and identities to simplify expressions involving sines and cosines (a typical example: express sin 3α in terms of sin α) will quickly appreciate that a similar activity is being proposed for programming problems. And the payoff is there at the terminal: faster computations.

In a nutshell:

1. • Functional programming is a method of program construction that emphasises functions and their application rather than commands and their execution.

2. • Functional programming uses simple mathematical notation that allows problems to be described clearly and concisely.

3. • Functional programming has a simple mathematical basis that supports equational reasoning about the properties of programs.

Our aim in this book is to illustrate these three key points, using a specific functional language called Haskell.

Functions and types

We will use the Haskell notation

to assert that f is a function taking arguments of type X and returning results of type Y. For example,

Float is the type of floating-point numbers, things like 3.14159, and Int is the type of limited-precision integers, integers n that lie in a restricted range such as −229 ≤ n < 229. The restriction is lifted with the type Integer, which is the type of unlimited-precision integers. As we will see in Chapter 3, numbers in Haskell come in many flavours.

In mathematics one usually writes f(x) to denote the application of the function f to the argument x.

Lists are the workhorses of functional programming. They can be used to fetch and carry data from one function to another; they can be taken apart, rearranged and combined with other lists to make new lists. Lists of numbers can be summed and multiplied; lists of characters can be read and printed; and so on. The list of useful operations on lists is a long one. This chapter describes some of the operations that occur most frequently, though one particularly important class will be introduced only in Chapter 6.

List notation

As we have seen, the type [a] denotes lists of elements of type a. The empty list is denoted by []. We can have lists over any type but we cannot mix different types in the same list. As examples,

List notation, such as [1,2,3], is in fact an abbreviation for a more basic form

1:2:3:[]

The operator (:) :: a → [a] → [a], pronounced ‘cons’, is a constructor for lists. It associates to the right so there is no need for parentheses in the above expression. It has no associated definition, which is why it is a constructor. In other words, there are no rules for simplifying an expression such as 1:2:[].

The question of efficiency has been an ever-present undercurrent in recent discussions, and the time has come to bring this important subject to the surface. The best way to achieve efficiency is, of course, to find a decent algorithm for the problem. That leads us into the larger topic of Algorithm Design, which is not the primary focus of this book. Nevertheless we will touch on some fundamental ideas later on. In the present chapter we concentrate on a more basic question: functional programming allows us to construct elegant expressions and definitions, but do we know what it costs to evaluate them? Alan Perlis, a US computer scientist, once inverted Oscar Wilde's definition of a cynic to assert that a functional programmer was someone who knew the value of everything and the cost of nothing.

Lazy evaluation

We said in Chapter 2 that, under lazy evaluation, an expression such as

where sqr x = x*x, is reduced to its simplest possible form by applying reduction steps from the outside in. That means the definition of the function sqr is installed first, and its argument is evaluated only when needed. The following evaluation sequence follows this prescription, but is not lazy evaluation:

The ellipsis in the penultimate line hides no fewer than four evaluations of 3+4 and two of 7⋆7.

We have seen a lot of laws in the previous two chapters, though perhaps the word ‘law’ is a little inappropriate because it suggests something that is given to us from on high and which does not have to be proved. At least the word has the merit of being short. All of the laws we have encountered so far assert the equality of two functional expressions, possibly under subsidiary conditions; in other words, laws have been equations or identities between functions, and calculations have been point-free calculations (see Chapter 4, and the answer to Exercise K for more on the point-free style). Given suitable laws to work with, we can then use equational reasoning to prove other laws. Equational logic is a simple but powerful tool in functional programming because it can guide us to new and more efficient definitions of the functions and other values we have constructed. Efficiency is the subject of the following chapter. This one is about another aspect of equational reasoning, proof by induction. We will also show how to shorten proofs by introducing a number of higher-order functions that capture common patterns of computations. Instead of proving properties of similar functions over and over again, we can prove more general results about these higher-order functions, and appeal to them instead.

In Haskell every well-formed expression has, by definition, a well-formed type. Each well-formed expression has, by definition, a value. Given an expression for evaluation,

1. • GHCi checks that the expression is syntactically correct, that is, it conforms to the rules of syntax laid down by Haskell.

2. • If it is, GHCi infers a type for the expression, or checks that the type supplied by the programmer is correct.

3. • Provided the expression is well-typed, GHCi evaluates the expression by reducing it to its simplest possible form to produce a value. Provided the value is printable, GHCi then prints it at the terminal.

In this chapter we continue the study of Haskell by taking a closer look at these processes.

A session with GHCi

One way of finding out whether or not an expression is well-formed is of course to use GHCi. There is a command :type expr which, provided expr is well-formed, will return its type. Here is a session with GHCi (with some of GHCi's responses abbreviated):

ghci> 3 +4)

<interactive>:1:5: parse error on input ‵)'

GHCi is complaining that on line 1 the character ')' at position 5 is unexpected; in other words, the expression is not syntactically correct.

Back in Chapter 2 we described the function putStrLn as being a Haskell command, and IO a as being the type of input–output computations that interact with the outside world and deliver values of type a. We also mentioned some syntax, called do-notation, for sequencing commands. This chapter explores what is really meant by these words, and introduces a new style of programming called monadic programming. Monadic programs provide a simple and attractive way to describe interaction with the outside world, but are also capable of much more: they provide a simple sequencing mechanism for solving a range of problems, including exception handling, destructive array updates, parsing and state-based computation. In a very real sense, a monadic style enables us to write functional programs that mimic the kind of imperative programs one finds in languages such as Python or C.

The IO monad

The type IO a is an abstract type in the sense described in the previous chapter, so we are not told how its values, which are called actions or commands, are represented. But you can think of this type as being

Thus an action is a function that takes a world and delivers a value of type a and a new world.

This chapter is devoted to an example of how to build a small library in Haskell. A library is an organised collection of types and functions made available to users for carrying out some task. The task we have chosen to discuss is pretty-printing, the idea of taking a piece of text and laying it out over a number of lines in such a way as to make the content easier to view and understand. We will ignore many of the devices for improving the readability of a piece of text, devices such as a change of colour or size of font. Instead we concentrate only on where to put the line breaks and how to indent the contents of a line. The library won't help you to lay out bits of mathematics, but it can help in presenting tree-shaped information, or in displaying lists of words as paragraphs.

Setting the scene

Let's begin with the problem of displaying conditional expressions. In this book we have used three ways of displaying such expressions:

These three layouts, which occupy one, two or three lines, respectively, are considered acceptable, but the following two are not:

The decision as to what is or is not acceptable is down to me, the author.

Numbers in Haskell are complicated because in the Haskell world there are many different kinds of number, including:

Most programs make use of numbers in one way or another, so we have to get at least a working idea of what Haskell offers us and how to convert between the different kinds. That is what the present chapter is about.

The type class Num

In Haskell all numbers are instances of the type class Num:

The class Num is a subclass of both Eq and Show. That means every number can be printed and any two numbers can be compared for equality. Any number can be added to, subtracted from or multiplied by another number. Any number can be negated. Haskell allows -x to denote negate x; this is the only prefix operator in Haskell.

The functions abs and signum return the absolute value of a number and its sign.