%include Haskell.fmt
%format `bind` = "\bind "
%format === = "\equiv"
%format len (a) = "\mid\!\!{"a"}\!\!\mid"
%if False
\begin{code}
import Test.QuickCheck
import Control.Monad (liftM2)
\end{code}
%endif

\begin{question}{Monads and QuickCheck}{25}

\subquestion
Instead of defining a monad by |bind| (|>>=|) and |return|, we can also define it in
terms of |map| (hereafter called |mmap| to avoid confusion with |map| from the |Prelude|), |join|, and |return|.
\begin{code}
mmap  :: Monad m => (a -> b) -> m a -> m b
join  :: Monad m => m (m a) -> m a
\end{code}
Define |mmap| and |join| in terms of |(>>=)| and |return|, and define (|>>=|) in terms of 
|mmap|, |join|, and |return|.

\answer{
\begin{code}
mmap f xs    = xs   >>=  (return . f)
join xss     = xss  >>=  id
xs `bind` f  = join (mmap f xs)
\end{code}}

\subquestion
A |Snoc|-list is an alternative representation of a (normal) list: a non-empty |Snoc|-list consists of
the last element of the list, and the rest.
\begin{code}
data Snoc a = Nil | Snoc a :< a deriving (Show, Eq)
\end{code}
Define |listToSnoc|, such that |listToSnoc [1..5]| returns
\begin{spec}
((((Nil :< 1) :< 2) :< 3) :< 4) :< 5
\end{spec}
Use higher-order functions if possible.

\answer{
\begin{code}
listToSnoc :: [a] -> Snoc a
listToSnoc = foldl (:<) Nil
\end{code}}

\subquestion
Define the operator |(<++) :: Snoc a -> Snoc a -> Snoc a|
for concatenating two |Snoc|-lists.

\answer{
\begin{code}
(<++) :: Snoc a -> Snoc a -> Snoc a
xs   <++  Nil        = xs
xs   <++  (ys :< a)  = (xs <++ ys) :< a
\end{code}
}

\subquestion
Make |Snoc| an instance of the |Monad| type class such that the 
three monad laws are satisfied. Give a definition for  
the member functions (|>>=|) and |return|.

\answer{
\begin{code}
instance Monad Snoc where
   return a         = Nil :< a
   Nil       >>= _  = Nil
   (s :< a)  >>= f  = (s >>= f) <++ (f a)
\end{code}}

\subquestion
Give the type and the result of the function |test|.
\begin{code}
test = do  x <- listToSnoc [1..5]
           return (x*x)
\end{code}

\answer{
The type of |test| is |Snoc Int|, or, more precise, |(Enum a, Num a) => Snoc a|.
Evaluating |test| results in |((((Nil :< 1) :< 4) :< 9) :< 16) :< 25|.}

\subquestion
Prove that the first two monad laws hold for a |Snoc|-list. Use equational reasoning.
\begin{center}
\begin{tabular}{rclr}
|(return x) >>= f| &|===|& |f x|   & \quad\quad (left-identity) \\
|m >>= return|     &|===|& |m|     &            (right-identity)
\end{tabular}
\end{center}

\answer{
For the following proofs, we use that |Nil <++ xs = xs| 
(follows from its definition).

Left-identity law:
\begin{spec}
return x >>= f
   = (Nil :< x) >>= f           -- definition |return|
   = (Nil >>= f) <++ (f x)      -- definition |>>=|
   = Nil <++ f x                -- definition |>>=|
   = f x                        -- definition |<++|
\end{spec}

Right-identity law: proof by induction on the length of m

case 1: |len m = 0|, then |m = Nil|.
\begin{spec}
m >>= return
   = Nil >>= return           -- definition |m|
   = Nil                      -- definition |>>=|
   = m                        -- definition |m|
\end{spec}

case 2: |len m > 0|, then |m = s <: x| \quad I.H.: |(s >>= return) = s|

\begin{spec}
m >>= return
   = (s :< x) >>= return               -- definition |m|
   = (s >>= return) <++ (return x)     -- definition |>>=|
   = s <++ (Nil :< x)                  -- I.H.
   = (s <++ Nil) :< x                  -- definition |<++|
   = s :< x                            -- definition |<++|
   = m                                 -- definition |m|
\end{spec}}

\subquestion
Give a |QuickCheck| property to check that also the third monad law holds.
\begin{center}
\begin{tabular}{rclr}
   |(m >>= f) >>= g| &|===|& |m >>= (\x -> f x >>= g)| & \quad\quad (associativity) \\
\end{tabular}
\end{center}
Indicate precisely how this property can be validated by the |QuickCheck| system, and make sure
that |QuickCheck| is able to generate random |Snoc|-lists (with an appropriate distribution of test cases).

\answer{
To generate random |Snoc|-lists, we slightly modify the instance declaration
for |Arbitrary [a]|.
\begin{code}
instance Arbitrary a => Arbitrary (Snoc a) where
   arbitrary = frequency 
      [  (1,  return Nil)
      ,  (4,  liftM2 (:<) arbitrary arbitrary)
      ]
\end{code}
The third monad law can be checked by:
\begin{code}
associativity :: Snoc Int -> (Int -> Snoc Int) -> (Int -> Snoc Int) -> Bool
associativity m f g =
   ((m >>= f) >>= g)   ==   (m >>= (\x -> f x >>= g))
\end{code}
Do not forget to give the type signature as this is required by the 
|QuickCheck| system. To check the property, we call
|quickCheck associativity| from ghci.
}

\end{question}


%if False
\begin{code}
instance Show (a -> b) where show _ = "<<function>>"
\end{code}
%endif