Tutorial - Completed (Week 2)

1. Write a Haskell function mySum that sums all elements in a list of numbers. Feel free to use the following template:

   mySum :: [Int] -> Int
   mySum []     = ???
   mySum (n:ns) = ???
   

2. Write a Haskell function myProduct that multiplies all elements in a list of numbers.

3. You probably used copypaste to solve the previous question, didn't you? No reason to be ashamed, we've all done it! But let's try not to.

   Find a generalisation myBinop that applies a given binary operator f with unit element z to a list of numbers. We will then be able to define myProduct and mySum using myBinop.

   myBinop :: (Int -> Int -> Int) -> Int -> ([Int] -> Int)
   myBinop f z [] = ???
   myBinop f z (n:ns) = ???
   
   mySum :: [Int] -> Int
   mySum ns = myBinop (+) 0 ns
   
   myProduct :: [Int] -> Int
   myProduct ns = myBinop (*) 1 ns
   

4. We just reinvented a wheel. The fold functions are general-purpose library functions that completely subsume myBinop. Try to implement mySum and myProduct using foldr instead of myBinop.

   The linked library documentation references a lot of concepts that we don't assume familiarity with, so don't worry if you don't fully understand it. Perhaps start by looking at the examples.

mySum :: [Int] -> Int
mySum [] = 0
mySum (n:ns) = n + mySum ns

myProduct :: [Int] -> Int
myProduct [] = 1
myProduct (n:ns) = n*myProduct ns

myBinop :: (Int -> Int -> Int) -> Int -> ([Int] -> Int)
myBinop f z [] = z
myBinop f z (n:ns) = n `f` myBinop f z ns

mySum2 :: [Int] -> Int
mySum2 = myBinop (+) 0

myProduct2 :: [Int] -> Int
myProduct2 = myBinop (*) 1

mySum3 :: [Int] -> Int
mySum3 = foldr (+) 0

myProduct3 :: [Int] -> Int
myProduct3 = foldr (*) 1

Consider the (++) operator in Haskell.

(++) :: [a] -> [a] -> [a]
[]     ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)

1. State the formal properties of left identity, right identity and associativity for (++).
2. Try to prove these properties. In some cases, you may need to perform induction on the structure of lists. The base case of the induction will be for the empty list, and the inductive case will be to show your property for a list (x:xs), assuming the property for the list xs (this assumption is called the inductive hypothesis).

[] ++ ys == ys -- left identity
xs ++ [] == xs -- right identity
(xs ++ (ys ++ zs)) == ((xs ++ ys) ++ zs) -- associativity

xs' ++ [] == xs'

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

LHS == (x:xs') ++ [] 
    == x:(xs' ++ []) -- Equation 2
    == (x:xs')       -- Inductive Hypothesis
    == RHS

(xs' ++ ys) ++ zs == xs' ++ (ys ++ zs)

((x:xs') ++ ys) ++ zs == (x:xs') ++ (ys ++ zs)

LHS == ((x:xs') ++ ys) ++ zs 
    == (x:(xs' ++ ys)) ++ zs -- Equation 2
    == x:((xs' ++ ys) ++ zs) -- Equation 2
    == x:(xs' ++ (ys ++ zs)) -- Inductive Hypothesis
    == (x:xs') ++ (ys ++ zs) -- Equation 2 (symmetrically)
    == RHS

Red-black trees are binary search trees where each node in the tree is coloured either red or black. In C, red-black trees could, for example, be encoded with the following user-defined data type:

typedef struct redBlackNode* link;

struct redBlackNode { 
  Item item; // Item type defined elsewhere
  link left, right; 
  int  isRed; // 1 if node is red, 0 if black
};

and in Haskell (again, we assume the Item type is defined elsewhere)

data RBColour
  = Red
  | Black

data RBTree
  = RBLeaf
  | RBNode RBColour Item RBTree RBTree 

1. The user defined Haskell data type characterises a set of terms as RBTree. List the inference rules to define the same set. Assume there already exists a judgement \(x\ \mathbf{Item}\) which is derivable for all \(x\) in the Item type.
2. In a proper red-black tree, we can never have a red parent node with a red child, although it is possible to have black nodes with black children. Moreover, the root node cannot be red. Therefore, not all terms of type RBTree are real red-black trees. Define inference rules for a property \(t\ \mathbf{OK}\), such that \(\mathbf{OK}\) is derivable if the term \(t\) represents a proper red-black tree.