-- Fortgeschrittene Funktionale Programmierung, 
--   LMU, TCS, Wintersemester 2015/16
--   Steffen Jost, Alexander Isenko
--
-- Übungsblatt 06a. 25.11.2015
--
-- Thema: Monaden-Gesetze, Erste Schritte mit Monaden und Do-Notation
--
-- Hier machen wir ein paar erste Schritte mit Monaden.
-- Wer das alles schon kennt und bereits von woanders her 
-- mit der Do-Notation vertraut ist, sollte stattessen 
-- die B-Version dieses Übungsblattes machen: 
-- einen applikativen Parser bauen.
-- 
-- Gehen Sie diese Datei durch und bearbeiten Sie 
-- alle Vorkommen von undefined bzw. die mit -- !!! TODO !!!
-- markierten Stellen. Testen Sie Ihre Lösungen mit GHCi!


---- A6-1 Monaden Gesetze nachweisen
-- 
--
-- a)
-- Auf Folie 04-42 fehlt der Beweis für die Assoziativität
-- Maybe-Instanz für die Typklasse Monad. 
-- Führen Sie den Beweis aus!
-- (Geht ganz analog zu den anderen beiden Beweisen, d.h.
--  Definitionen ausfalten und umformen.
--  Bei Abgabe: Bitte zusätzlich kurze Begründung für jeden Schritt angeben!)
{-
Zu Zeigen: 
  Ausdruck
    m >>= (\x-> ((f x) >>= g))
  ist gleich zu
    (m >>= f) >>= g
-}  

-- !!! TODO !!!


-- b)
{- Beweisen Sie, dass folgende Definition 
  
    instance Monad [] where
      return x = [x]                   -- (Mo1)
      xs >>= f = concat (map f xs)     -- (Mo2)
  
  das Monaden-Gesetz "Links-Identität" einhält!  
 
  Folgende Definition sind dabei eventuell nützlich:

    concat :: [[a]] -> [a]
    concat []       = []               -- (CcN)
    concat (xs:xss) = xs ++ concat xss -- (CcC)

    (++) :: [a] -> [a] -> [a]
    (++) xs     [] = xs                -- (ANr)
    (++) []     ys = ys                -- (ANl)
    (++) (x:xs) ys = x : (xs ++ ys)    -- (ACl)

    map :: (a -> b) -> [a] -> [b]
    map _   []   =                     -- (MpN)
    map f (x:xs) = (f x) : (map f xs)  -- (MpC)
-}

-- !!! TODO !!!




---- A6-2 Either-Monade und Do-Notation
--
-- In der vorletzten Vorlesung am 12.11. haben wir gesehen
-- wie der Datentyp Either der Standardbibliothek zum 
-- Funktor gemacht werden kann. 
--
-- Machen Sie diesen Datentyp nun zu einer Monade!
-- Um Namenskonflikten aus dem Weg zu gehen,
-- definieren wir Either einfach noch mal neu:

data Entweder a b = Eines a | Anderes b
  deriving (Show, Eq)

-- Die Idee ist dabei die gleiche wie bei Maybe,
-- nur das "Nothing" hier noch einen Wert tragen kann.

instance Functor (Entweder a) where
  fmap f (Anderes x) = Anderes $ f x
  fmap _ (Eines x) = Eines x -- Because x@(Either a b) is not (Either a c), even if we can prove that x is Left.

instance Applicative (Entweder a) where
  pure = Anderes
  (Anderes f) <*> (Anderes x) = Anderes $ f x
  (Eines x) <*> _ = Eines x -- ditto
  _ <*> (Eines x) = Eines x

instance Monad (Entweder a) where
  (Anderes a) >>= f = f a
  (Eines x) >>= _ = Eines x -- ditto

-- Applicative Tests:
-- (*) <$> (Anderes 3) <*> (Anderes 4)
-- (*) <$> (Eines   3) <*> (Anderes 4)
-- (*) <$> (Anderes 3) <*> (Eines 4)

  
-- b)
-- Verallgemeinern Sie folgende gewöhnlichen Funktionsdefinition,
-- welche Kenntnis des Typs Entweder voraussetzen.
-- Schreiben Sie jeweils eine generische Fassung,
-- welche nur die Monaden-Instanz oder, wenn möglich, 
-- nur Applicative voraussetzt:

-- b1) Beispiel:
multEnt :: (Num b) => (Entweder a b) -> (Entweder a b) -> (Entweder a b)
multEnt (Anderes x) (Anderes y) = Anderes (x * y)
multEnt (Anderes _) other       = other
multEnt other       _           = other


multEnt_M :: (Num b, Monad m) => m b -> m b -> m b
multEnt_M = multEnt_A -- The monad-applicative proposal was implemented ;-)

multEnt_A :: (Num b, Applicative f) => f b -> f b -> f b
multEnt_A a b = (*) <$> a <*> b


-- b2)
foo :: (Entweder a (b->c)) -> (Entweder a b) -> (Entweder a c)
foo (Anderes f) (Anderes x) = Anderes $ f x
foo (Eines a) _ = Eines a
foo _ (Eines a) = Eines a

foo_M :: (Monad m) => (m (b->c)) -> (m b) -> (m c)
foo_M = foo_A

foo_A :: (Applicative m) => (m (b->c)) -> (m b) -> (m c)
foo_A f x = ($) <$> f <*> x


-- b3)
ifM :: (Entweder a Bool) -> (Entweder a b) -> (Entweder a b) -> (Entweder a b)
ifM (Anderes True)  x _ = x
ifM (Anderes False) _ y = y
ifM (Eines a)       _ _ = Eines a

ifM_M :: (Monad m) => m Bool -> m b -> m b -> m b
ifM_M = ifM_A
ifM_A :: (Applicative f) => f Bool -> f b -> f b -> f b
ifM_A b x y = bool <$> x <*> y <*> b



bool :: a -> a -> Bool -> a
-- ^ This should really be in Prelude (Data.Bool at least)
bool x _ True = x
bool _ x False = x



---- A6-3 Do - Notation
--
-- Implementieren Sie folgende Funktion unter Verwendung der Do-Notation:
-- Hinweis: Einfach den Typen folgen, alles andere kommt von allein!
  
filterM :: Monad m => (a -> m Bool) -> [a] -> m [a]
filterM p = foldr trav (return [])
  where
    trav x xs = bool (x :) id <$> p x <*> xs -- Applicative is cooler than do notation ;-)

    trav' x xs = do -- But if I must …
      include <- p x
      xs' <- xs
      return $ case include of
        True -> x : xs'
        False -> xs'

-- Beispiele zum Testen:
silly1 :: Int -> Maybe Bool
silly1 0 = Nothing
silly1 x = Just $ even x

silly2 :: Int -> [Bool]
silly2 0 = []
silly2 x | even x    = [False,True,True,False]
         | otherwise = [False,False]

-- > filterM silly [1..10]
-- Just [2,4,6,8,10]
  
-- > filterM silly $ [1..10]++[1,0,1]
-- Nothing