← back

Equational reasoning in Haskell

17 February 2017

Discussion notes, week 6, cse130

How do we know if a program is correct?

Tests? Tests only cover the errors that you, the programmer, can think of --- and because we're all human, this doesn't work when you have programs of any reasonable complexity. And of course,

Program testing can be used to show the presence of bugs, but never to show their absence! - Dijkstra, EWD249

No, to be able to say that a program is correct, as in it behaves properly for all inputs, we must give a formal proof.

One of the main benefits of functional programming is that it makes these proofs easy, as functional programs are simply mathematical equations that you can manipulate algebraically. The algebraic style of programming is a convenient tool for reasoning and proof, but an even better way to write programs --- systematically by calculation, which makes it easy to convince yourself that each step you take is sound. If each small piece is individually correct, then their composition must be also!

Basics

You'll need the following combinators

-- composition
(.) :: (b -> c) -> (a -> b) -> (a -> c)

-- application
($) :: (a -> b) -> a -> b

-- identity
id :: forall a. a -> a

flip :: (a -> b -> c) -> (b -> a -> c)

curry   :: ((a,b) -> c) -> (a -> b -> c)
uncurry :: (a -> b -> c) -> ((a,b) -> c)

Laws

Fold-map fusion law

Show that

foldr g b ◦ map f = foldr h b

where h = λx y. g (f x) y

Map distributes over composition (map fusion)

Given

map f [] = []
map f (x:xs) = f x : map f xs

Show that

map (g ◦ f) = map f ◦ map g

Properties

Homomorphisms

Prove

fmap f . pure = pure . f

[AlgProg rule 1.7]

uncurry zip . (\x -> ([f x], [g x])) = pure . (\x -> (f x, g x))

Involutivity

Given:

reverse [] = []
reverse (x:xs) = reverse xs ++ [x]

Show that reverse is involutive

reverse ◦ reverse = id

Similarly, show that flip is involutive, by parametricity (using types only)

flip ◦ flip = id

Exercises

  1. [Danielsson] Show that
((reverse ◦ map (λx.x − y)) ◦ (map (λx.y + x) ◦ reverse)) = id
  1. Show that for all pairs p,
(fst p, snd p) = p

When does this property fail to hold in ML? In Haskell?

Point-free programming

In Haskell, an idiomatic way to write functions is by composition with other functions,

Note

This material is related to the Type Tetris question on homework 3.

References