*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!

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)
```

Show that

```
foldr g b ◦ map f = foldr h b
where h = λx y. g (f x) y
```

Given

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

Show that

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

Prove

`fmap f . pure = pure . f`

[AlgProg rule 1.7]

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

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`

- [Danielsson] Show that

`((reverse ◦ map (λx.x − y)) ◦ (map (λx.y + x) ◦ reverse)) = id`

- Show that for all pairs
`p`

,

`(fst p, snd p) = p`

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

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

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

- Danielsson et al, Fast and Loose Reasoning is Morally Correct
- Bird and Wadler, Introduction to Functional Programming, 1st ed.
- Bird and de Moor, Algebra of Programming
- Bird, A program to solve Sudoku
- Hutton, A tutorial on the universality and expressiveness of fold
- Hutton, The countdown problem