module Spec where
import Types

import qualified Prelude
import Prelude hiding ((>>=),return)
import Data.Monoid

-- a) 
--   fmap return  :: Monad2 m => m a          -> m (m a)
--   join         :: Monad2 m => m (m (m a))  -> m (m a)

units :: Monad2 m => [m a -> m a]
units = [ join . return
        , id
        , join . (fmap return :: Monad2 m => m a -> m (m a))
        ]

assoc :: Monad2 m => [m (m (m a)) -> m a]
assoc = [ join . fmap join 
        , join . (join :: Monad2 m => m (m (m a)) -> m (m a))
        ]


-- b)

z :: Monoid w => w
z = mempty

instance Monoid w => Monad2 ((,) w) where
    return a           = (z        , a)
    join (w, (w', a))  = (w <> w'  , a)

assocProof :: Monoid w => (w, (w, (w, a))) -> [(w, a)]
assocProof (w1, (w2, (w3, a))) = 
    [ (join . fmap join) (w1, (w2, (w3, a)))
    , -- Def. |(.)|
      join   (fmap join  (w1, (w2, (w3, a))))
    , -- Def. |fmap|
      join (w1,    join       (w2, (w3, a)))
    , -- Def. |join|
      join (w1,               (w2 <> w3, a))
    , -- Def. |join|
      (w1 <> (w2 <> w3), a)
    , -- Monoid law (assoc. |(<>)|)
      ((w1 <> w2) <> w3, a)
    , -- Def. |join|
      join (w1 <> w2,              (w3, a))
    , -- Def. |join|
      join (join    (w1, (w2,      (w3, a))))
    , -- Def. |(.)|
      (join . join) (w1, (w2,      (w3, a)))
    ]

unitProof :: Monoid w => (w, a) -> [(w, a)]
unitProof (w, a) = 
    [ (join . return) (w, a)
    , -- Def. |(.)|
      join (return (w, a))
    , -- Def. |return|
      join (z, (w, a))
    , -- Def. |join|
      (z <> w, a)
    , -- Monoid law
      (w, a)
    , -- Def. |id|. Left part of the law done.
      id (w, a)
    , -- Def. |id|. Right part proof starting.
      (w, a)
    , -- Monoid law
      (w <> z, a)
    , -- Def. |join|
      join (w, (z, a))
    , -- Def. |return|
      join (w, return a)
    , -- Def. |fmap|
      join (fmap return (w, a))
    , -- Def. |(.)|
      (join . fmap return) (w, a)
    ]