----------------------------------------------------------------------

Module:         COMP2003 Advanced Functional Programming
School:         Computer Science, University of Nottingham
Lecturer:       Graham Hutton
Level:          2
Semester:       Spring
Year:           24-25

----------------------------------------------------------------------

QUESTION 1:

a) return x = \s -> (x,s)

   st >>= f = \s -> let (x,s') = st s in f x s'

   That is, return converts a value into a state transformer that
   simply returns that value without modifying the state.

   That is, >>= provides a means of sequencing state transformers:
   st >>= f applies the state transformer st to an initial state s,
   then applies the function f to the resulting value x to give a
   second state transformer (f x), which is then applied to the
   modified state s' to give the final result value.

b) fresh = \n -> (n, n+1)

c) label (Leaf x)   = do n <- fresh
                         return (Leaf n)
   label (Node l r) = do l' <- label l
                         r' <- label r
                         return (Node l' r')

d) label (Leaf x)   = fresh >>= \n ->
                      return (Leaf n)
   label (Node l r) = label l >>= \l' ->
                      label r >>= \r' ->
                      return (Node l' r')

e) return x >>= f    =  f x                             (1)

   mx >>= return     =  mx                              (2)

   (mx >>= f) >>= g  =  mx >>= (\x -> (f x >>= g))      (3)

   Equation (1) states that if we return a value x and then feed
   this value into a function f, this should give the same result
   as simply applying f to x.  Dually, (2) states that if we feed
   the result of a computation mx into the function return, this
   should give the same result as simply performing mx.  Together,
   these equations express --- modulo the fact that the second
   argument to >>= involves a binding operation --- that return is
   the left and right identity for >>=.  Equation (3) expresses
   (again modulo binding) that >>= is associative.

----------------------------------------------------------------------

QUESTION 2:

a) P(Leaf)    forall l,x,r. [P(l) ^ P(r) => P(Node l x r)]
   -------------------------------------------------------
                       forall t. P(t)

   Suppose that we want to prove some property, p, say holds for
   all (finite) trees.  Then the principle of induction states
   that it is sufficient to show that p holds for Leaf, called
   the base case, and that p is preserved by Node, called the
   inductive case.  More precisely, in the inductive case one
   is required is show that if the property p holds for any
   trees l and r, then it also holds for Node l x r.

b) Definition:

     leaves :: Tree a -> Int
     leaves Leaf         = 1
     leaves (Node l x r) = leaves l + leaves r

   Property:

     leaves (reflect t) = leaves t

   Base case: t = Leaf

     leaves (reflect Leaf)
   =    applying reflect
     leaves Leaf

   Inductive case: t = Node l x r

     leaves (reflect (Node l x r))
   =    applying reflect
     leaves (Node (reflect r) x (reflect l))
   =    applying leaves
     leaves (reflect r) + leaves (reflect l)
   =    induction hypotheses for l and r
     leaves r + leaves l
   =    commutativity of +
     leaves l + leaves r
   =    unapplying leaves
     leaves (Node l x r)

c) Base case:

     flatten' Leaf xs
   =    specification of flatten'
     flatten Leaf ++ xs
   =    applying flatten
     [] ++ xs
   =    applying ++
     xs

   Inductive case:

     flatten' (Node l x r) xs
   =    specification of flatten'
     flatten (Node l x r) ++ xs
   =    applying flatten
     (flatten l ++ [x] ++ flatten r) ++ xs
   =    associativity of ++
     flatten l ++ ([x] ++ (flatten r ++ xs))
   =    induction hypothesis for r
     flatten l ++ ([x] ++ flatten' r xs)
   =    property of ++
     flatten l ++ (x : flatten' r xs)
   =    induction hypothesis for l
     flatten' l (x : flatten' r xs)

   In conclusion, we have defined:

     flatten' Leaf         xs = xs
     flatten' (Node l x r) xs = flatten' l (x : flatten' r xs)

d) The original function flatten uses the append operator ++,
   which takes linear time in the length of its first argument.
   As a result, the flatten function is inefficient.  In contrast,
   the function flatten' does not use the ++ operator and is hence
   more efficient, but allows the behaviour of the original function
   to be recovered by defining flatten t = flatten' t [].

e) Induction is a technique for proving that a particular property
   holds for all values of a recursively defined type.  Constructive
   induction is the use of induction to guide the construction of
   a definition that satisfies a particular property.  They are often
   two sides of the same coin, in the sense that an inductive proof
   can often be turned into a constructive induction by re-ordering
   the steps.  For example, given the definitions

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

     rev' []     ys = ys
     rev' (x:xs) ys = rev' xs (x:ys)

   we can prove by induction that rev' xs ys = rev xs ++ ys, or
   alternatively, we can construct the definition of rev' from
   this equation by using constructive induction.

----------------------------------------------------------------------

QUESTION 3:

> The following example essay illustrates the kind of points that
> students are expected to cover.  However, students are free to
> answer the question in any way that they please, provided that
> the use of the >>= operator is clearly explained.

Consider the following type of expressions that are built up from
integer values using a division operator:

   data Expr = Val Int | Div Expr Expr

Such expressions can be evaluated as follows:

   eval :: Expr -> Int
   eval (Val n)   = n
   eval (Div x y) = eval x `div` eval y

However, this function does not take account of the possibility of
division by zero, and will produce an error in this case.  To address
this, we can use the Maybe type to define a safe version of division
that returns Nothing when the second argument is zero,

   safediv :: Int -> Int -> Maybe Int
   safediv _ 0 = Nothing
   safediv n m = Just (n `div` m)

and modify our evaluator to explicitly handle the possibility of
failure when the function is called recursively:

   eval :: Expr -> Maybe Int
   eval (Val n)   = Just n
   eval (Div x y) = case eval x of
                       Nothing -> Nothing
                       Just n  -> case eval y of
                                     Nothing -> Nothing
                                     Just m  -> safediv n m

The new definition for eval resolves the division by zero issue,
but is rather verbose.  To write eval in a simpler manner, we
can observe the common pattern that occurs twice in its definition,
namely performing a case analysis on a Maybe value, mapping Nothing
to itself and Just x to some result depending on x.  Abstracting out
this pattern gives a new operator >>= that is defined as follows:

   (>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b
   mx >>= f = case mx of
                 Nothing -> Nothing
                 Just x  -> f x

Using the >>= operator and the lambda notation, we can now redefine
the function eval in a more compact manner as follows:

   eval :: Expr -> Maybe Int
   eval (Val n)   = Just n
   eval (Div x y) = eval x >>= \n ->
                    eval y >>= \m ->
                    safediv n m

The case for division states that we first evaluate x and call
its result value n, then evaluate y and call its result value m,
and finally combine the two results by applying safediv.

Using the >>= operator in the above definition ensures that the
division case only succeeds if every component in this case succeeds.
Moreover, we no longer have to worry about handling the possibility
of failure at any point in the definition, as this is handled
automatically by the definition of the >>= operator.

In conclusion, the >>= operator captures a common pattern of failure
management, and allows us to focus on the successful cases when we
are defining functions, with the detection and propagation of
failure being handled automatically by the >>= operator.

----------------------------------------------------------------------