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)
foldr g b ◦ map f = foldr h b where h = λx y. g (f x) y
map f  =  map f (x:xs) = f x : map f xs
map (g ◦ f) = map f ◦ map g
fmap f . pure = pure . f
[AlgProg rule 1.7]
uncurry zip . (\x -> ([f x], [g x])) = pure . (\x -> (f x, g x))
reverse  =  reverse (x:xs) = reverse xs ++ [x]
reverse is involutive
reverse ◦ reverse = id
Similarly, show that
flip is involutive, by parametricity (using types only)
flip ◦ flip = id
((reverse ◦ map (λx.x − y)) ◦ (map (λx.y + x) ◦ reverse)) = id
(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.