Some concepts I had for COMP3141 exam questions.

3141_exam_questions.md

In the exercises and assignments, you may have made use of the >> operator. If not, here is its implementation:

(>>) :: (Monad m) => m t -> m u -> m u
a >> b = a >>= (\_ -> b)

It behaves identically to >>=, except that it discards the result of the first monadic operation.

1. Prove by careful equational reasoning that >> is associative, i.e. (a >> b) >> c == a >> (b >> c).

2. Give an example to explain why >>= must be left-associative.

---

1. The hard part is the monad law step:

   (a >> b) >> c = (a >>= (\_ -> b)) >> c                   -- definition
                 = (a >>= (\_ -> b)) >>= (\_ -> c)          -- definition
                 = a >>= (\x -> (\_ -> b) x >>= (\_ -> c))  -- monad law: associativity
                 = a >>= (\_ -> b >>= (\_ -> c))            -- simplification: \x -> (\_ -> b) x == \_ -> b
                 = a >>= (\_ -> b >> c)                     -- definition
                 = a >> (b >> c)                            -- definition

2. Because right-associativity would potentially cause type errors in seemingly valid use cases:

   (["hi", "cs3141"] >>= words) >>= reverse == "ih1413sc"
   ["hi", "cs3141"] >>= (words >>= reverse) == ???

A function g :: [a] -> b is said to be a fold if there exists a function f :: a -> b -> b and value x :: b such that f satisfies

g     [] = x          -- fold prop. 1
g (y:ys) = f y (g ys) -- fold prop. 2

Use structural induction to prove the following universality theorem: if g satisfies the fold equations for some f and x, then g = foldr f x.

---

We use structural induction on ys :: [a] to show that g ys = foldr f x ys.

In the base case ys = [], by the first fold property and the definition of foldr, we have g [] = foldr f x [].

In the inductive case, write ys = y:ys' and assume as an inductive hypothesis that g ys' = foldr f x ys'. Then

g ys = g (y:ys')           -- def. of xs
     = f y (g ys')         -- fold prop. 2
     = f y (foldr f x ys') -- hypothesis
     = foldr f x (y:ys')   -- def. of foldr
     = foldr f x ys        -- def. of xs

Thus, g = foldr f x for all input lists ys :: [a].

---

It is trivial to see that foldr f x is a fold, so we have proved the universal property of fold: this is the unique fold.

Consider the following extension of the Monad typeclass, which we shall call MonoidalMonad:

class (Monad m) => MonoidalMonad m where
  nil :: m t
  (<+>) :: m t -> m t -> m t

In addition to the usual monad laws, a monoidal monad instance is subject to some additional rules:

-- rule 1
nil <+> a = a

-- rule 2
a <+> nil = a

-- rule 3
a <+> (b <+> c) = (a <+> b) <+> c

-- rule 4
nil >>= m = nil

-- rule 5
(a <+> b) >>= m = (a >>= m) <+> (b >>= m)

1. Implement a lawful MonoidalMonad instance for lists. (1 mark)

   instance MonoidalMonad [] where
     nil     = {- your implementation here -}
     x <+> y = {- your implementation here -}

2. Here is a potential MonoidalMonad instance for Maybe:

   instance MonoidalMonad Maybe where
     nil = Nothing
     Nothing <+> y = y
     x <+> _ = x

   Construct a counterexample where one of the monoidal monad laws does not hold. (3 marks)

3. Explain why the previous part implies that no lawful MonoidalMonad instance for Maybe exists. (2 marks)

---

1. The implementation is quite straightforward:

   instance MonoidalMonad [] where
     nil = []
     (<+>) = (++)

2. Rule 5 has a counterexample. If we let

   a = Just False
   b = Just True
   
   m False = Nothing
   m True  = Just True

   then (a <+> b) >>= m evaluates to Nothing, while (a >>= m) <+> (b >>= m) evaluates to Just True.

3. There are only a few possible instances that type check, and it's not hard to see that all of them either fail one of the simpler laws or fail rule 5 similarly as the given instance.

Let F be some type with a Functor instance. For this instance to be lawful, we are usually required to prove that both functor laws hold:

-- fmap-id
fmap id = id
-- fmap-comp
fmap (f . g) = fmap f . fmap g

Due to a deep concept called parametricity, the type signature of fmap gives us a so-called free theorem that it automatically satisfies, regardless of whether the instance is lawful or not:

-- fmap-free
f . g = f' . g' ==> nmapF f . fmap g = fmap f' . nmapF g

In this theorem, the function nmapF is the natural map for F. In COMP3141, we don't need to define what exactly that means, but you can assume that nmapF satisfies

-- nmapF-id
nmapF id = id

Finally, assume that F's implementation of fmap satisfies the first functor law, fmap-id.

1. Under these assumptions, prove by equational reasoning that nmapF = fmap. (3 marks)
2. Why does part 1 imply that fmap is the only function of its type which satisfies fmap-id? (1 mark)
3. Using everything established so far, prove by equational reasoning that fmap must also satisfy fmap-comp. (2 marks)

(This shows that any Functor instance which satisfies the first law automatically satisfies the second law!)

---

1. For any function h,

   fmap h = id . fmapF h       -- definition of id
          = nmapF id . fmap h  -- nmapF-id
          = fmap id . nmapF h  -- fmap-free[f = f' = id, g = g' = h]
          = id . nmapF h       -- fmap-id
          = nmapF h            -- definition of id

   so nmapF = fmap.
2. If fmap' also satisfies fmap' id = id, then by part 1, fmap' = nmapF = fmap.
3. For any functions f and g,

   fmap f . fmap g = nmapF f . fmap g        -- part 1
                   = fmap id . nmapF (f . g) -- fmap-free[f' = id, g' = f . g]
                   = id . nmapF (f . g)      -- fmap-id
                   = nmapF (f . g)           -- definition of id
                   = fmap (f . g)            -- part 1