%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 _ = "<>" \end{code} %endif