* Overview

** Sheet 3

Good Haskell solutions. 
- Take care when using patterns. 
- Evaluation order!
- Sensible function names.
- Hoogle: search using type signature.


Proofs were OK, but there are a few things that could be improved.
- Induction proof without using the induction hypothesis 
       -> no need for induction OR there is an error! 


** Recursion on lists practice

   
** Folds


** Difference lists


** Uncluttering Haskell code



* Sheet 3 - Exercise 1

(a)

 G |- P(0)   G |- Forall n:Nat. P(n) -> P(n+1)
==============================================
 G |- Forall n:Nat. P(n)

Can simplify the rule to obtain a new one (All-I):

 G |- P(0)   G |- P(n) -> P(n+1)
================================= where n not free in G
 G |- Forall n:Nat. P(n)

And further simplify with Imp-I:

 G |- P(0)   G,P(n) |- P(n+1)
================================= where n not free in G
 G |- Forall n:Nat. P(n)

(b)

First we state and prove a Lemma that relates the function aux to
fibLouis:

Lemma 1: Forall n:Nat. aux n = (fibLouis n, fibLouis (n+1))
-----
Proof:
  Let P(n) := (aux n = (fibLouis n, fibLouis (n+1)))
  We show Forall n:Nat. P(n) by induction.

  Base Case: Show P(0).

	aux 0 = (0,1)                    -- aux.1
	      = (fibLouis 0, fibLouis 1)  -- fibLouis.1, fibLouis.2
    
  Step Case: Let n:Nat be arbitrary. Assume P(n). Show P(n+1).

      aux (n+1)
    = next (aux n)                                           -- aux.2
    = next (fibLouis n, fibLouis (n+1))                      -- P(n)
    = (fibLouis (n+1), fibLouis n + fibLouis (n+1))          -- next.1
    = (fibLouis (n+1), fibLouis (n+2-1) + fibLouis (n+2-2))  -- arith
    = (fibLouis (n+1), fibLouis (n+2))                       -- rev. fibLouis.3

    Note that in the first step, we actually have to check the condition that
    the argument of "aux (n+1)" really isn't equal to 0, because otherwise
    the case aux.1 would apply. This is OK, as n+1 > 0. Furthermore for the
    last step, we have to check that the left-hand side of fibLouis.3, really
    is greater than 1. This is OK, as n+2 > 1.

qed.


With the help of lemma 1, the proof of the proposition is simple.


Proposition: Forall n:Nat. fibEva n = fibLouis n
------- 

Proof: Let n:Nat be arbitrary.

    fibEva n = fst (aux n)                       -- fibEva.1
             = fst (fibLouis n, fibLouis (n+1))  -- Lemma 1
             = fibLouis n                        -- Definition of fst
                                                    (see Prelude.hs)
qed.


Note that no induction was needed for the proof of the proposition
with Lemma 1. Whenever you do a "proof by induction" without using the
induction hypothesis, you should be suspicious! Either your proof is
incorrect, or you do not actually need induction. In either case, you
should change your proof.

* Sheet 3 - Exercise 3

(a) 

> prime :: Int -> Bool
> prime n = [1,n] == [x | x<-[1..n], n `mod` x == 0]

(b)

> primes :: Int -> [Int]
> primes n = filter prime [2..n]

or

> primes' n = [p | p<-[2..n], prime p]


(c)

> firstPrimes n = take n (filter prime [2..])

Exercise: sieve of Eratosthenes


* Recursion on lists
  Implement the following functions:

| splitAt :: Int -> [a] -> ([a], [a])    | splitAt 3 "FOO,BAR" = ("FOO",",BAR")         |
| takeWhile :: (a -> Bool) -> [a] -> [a] | takeWhile (<4) [1..10] = [1,2,3]             |
| intersperse :: a -> [a] -> [a]         | intersperse ',' "123" ="1,2,3"               |
| intercalate :: [a] -> [ [a] ]-> [a]    | intercalate ", " ["Haskell", "C#", "Java"] = |
|                                        | "Haskell, C#, Java"                          |
| pow :: [a] -> [ [a] ]                  | pow [1,2,3] =                                |
|                                        | [[1,2,3],[1,2],[1,3],[1],[2,3],[2],[3],[]]   |


* Folds: Warmup exercise 4

Recall that the function foldr is defined as
  foldr :: (a -> b -> b) -> b -> [a] -> b
  foldr f z []     =  z
  foldr f z (x:xs) =  f x (foldr f z xs)

(a)

foldr (\x y-> 1+y) 0 [1,2,3] =
1 + (foldr (\x y-> 1+y) 0 [2,3]) =
1 + (1 + (foldr (\x y-> 1+y) 0 [3])) =
1 + (1 + (1 + (foldr (\x y-> 1+y) 0 []))) =
1 + (1 + (1 + 0)) =
1 + (1 + 1) =
1 + 2 =
3

The function
  foldr (\_ y-> 1+y) 0
has type [a] -> Int and returns the length of the given list.

(b)

Claim: foldr (:) [] is the identity function on lists.

Proof:
  Let P(xs) := foldr (:) [] xs = xs
  We prove by induction over lists that Forall xs::[a]. P(xs) holds.

Base case: Show P([]).
   foldr (:) [] [] = []         -- foldr.1

Step case: Let x::a and xs::[a] be arbitrary. Assume P(xs). Show P(x:xs).
 
     foldr (:) [] (x:xs)
   = (:) x (foldr (:) [] xs)      -- foldr.2
   = (:) x xs                     -- P(xs)
   = (x:xs)                       -- syntax change

* Folds: Exercises I

Implement the following functions *using foldr*.
and :: [Bool] -> Bool, or :: [Bool] -> Bool,
sum :: [Int] -> Int,   product :: [Int] -> Int
concat :: [ [a] ] -> [a]

* Folds: Exercises I

> and' = foldr (&&) True
> or' = foldr (||) False
> sum' = foldr (+) 0
> product' = foldr (*) 1
> concat' = foldr (++) []

* Folds: Exercises II

Implement the following functions:
all :: (a -> Bool) -> [a] -> Bool
exists :: (a -> Bool) -> [a] -> Bool.

* Folds: Exercises II

> all' :: (a -> Bool) -> [a] -> Bool
> all' p xs = and' (map p xs)

> all'' p = foldr (\x a -> p x && a) True

> exists' :: (a -> Bool) -> [a] -> Bool
> exists' p = or' . map p

> exists'' p = foldr (\x a -> p x || a) False



Sieve of Eratosthenes

> primes'' = sieve [2..]
>    where sieve (x:xs) = x : sieve [y | y <- xs, y `mod` x /= 0]

Powerset

> pow [] = [[]]
> pow (x:xs) = map (x:) (pow xs) ++ pow xs



Difference list uses:

Recall the naive implementation of reverse:

> rev []   = []
> rev (x:xs) = (rev xs) ++ [x] 

Efficient implementation of reverse, as seen in lecture 
w2-lists, slide 26:

> qrev xs = aux (xs, [])
> aux ([],     ys) = ys
> aux ((x:xs), ys) = aux (xs, x:ys)

Can we do this without the accumulator but a difference list instead?
First, here is the difference list implementation:

> type DList a = [a] -> [a]

> dempty :: DList a
> dempty = \ys -> ys

> dsingle :: a -> DList a
> dsingle x = \ys -> x : ys

> infixr 5 `dappend`

> dappend :: DList a -> DList a -> DList a
> dappend xs ys = \zs -> xs (ys zs)

> fromList :: [a] -> DList a
> fromList xs = \ys -> xs ++ ys

> toList :: DList a -> [a]
> toList xs = xs []

Now let us define drev, reverse based on difference lists:

> drev :: [a] -> [a]
> drev xs = toList (aux xs)
>   where aux [] = dempty
>         aux (x:xs) = (aux xs) `dappend` (dsingle x)

Let us look at the performance:

rev [1..10000] 
(3.89 secs, 4653946424 bytes)

drev [1..10000] 
(0.18 secs, 45993544 bytes)



You have now seen a large number of syntactic constructs and it may be
tempting to try and use as many of them as possible. But, that is not
always the best thing to do. Here are some constructs (and exercises
about them) to avoid, in no particular order.

You never need to compare to True, i.e., "x == True", as that means
that 'x' is already a Boolean and can be used by itself. See this
particularly silly example:

> silly x 
>   | x == True = True
>   | otherwise = False
                       
which can simply be written as:

> silly' x = x


You can do eta-contraction on functions:
(\x -> f x)
which is nothing other than
f

Similarly, but maybe less obvious, with multiple arguments,
(\x y -> f x y)
is also simply
f

Consider the order of parameters passed to functions and think about
where you can swap them if necessary.

foldr (\x y -> foo y x) ...
  where foo a b = ...

can instead be written as

foldr foo ...
  where foo b a = ...

with the ... identical to above!

Let us look at the functions "contains" and "elem" which consider an
element and a list and check containment (being an element), but use
reverse order of parameters:

> elem' :: Eq a => a -> [a] -> Bool
> elem' x []     = False
> elem' x (y:ys) = (x == y) || elem' x ys

> contains :: Eq a => [a] -> a -> Bool
> contains xs x = elem' x xs

Exercises
---------

Simplify these definitions:

map (\(x,y) -> y)


parity takes a list of Integers and transforms it into a list of 0/1s.

> parity xs = map elemPar xs
>   where elemPar x = mod x 2

The split function splits a list (and given a pair of empty lists)
into two lists of equal (+-1) length.

> split :: [a] -> ([a],[a]) -> ([a],[a])
> split zs (left, right) = foldr (\a (xs, ys) -> combine xs ys a) (left, right) zs
>   where combine xs ys x = (x:ys, xs) 
          
split [1,2,3,4,5,6] ([],[])
([1,3,5],[2,4,6])


          

Solutions:

map snd

> parity1 xs = map (\x -> mod x 2) xs
> parity2 xs = map (\x -> x `mod` 2) xs
> parity3    = map (\x -> x `mod` 2) 

> parity'    = map (`mod` 2)

Note that split' uses "flip" to reverse the order of arguments, so we
do not even need to spell them out anymore.

> split' :: [a] -> ([a],[a]) -> ([a],[a])
> split' = flip $ foldr (\a (xs, ys) -> (a:ys, xs))

split' [1,2,3,4,5,6] ([],[])
([1,3,5],[2,4,6])



As further examples see the last slide of w2-lists (slide 62) where
the difference list functions are uncluttered.