monad?.hs

{-# LANGUAGE NoImplicitPrelude #-}

module Simpler where

import Prelude (($), Eq, Show)

import Control.Monad
import Data.Foldable
import Data.Monoid

data List a = Nil | Cons a (List a) deriving (Eq, Show)

instance Monoid (List a) where
    mempty = Nil

    Nil         `mappend` xs  = xs
    xs          `mappend` Nil = xs
    (Cons x xs) `mappend` ys  = Cons x (xs `mappend` ys)

instance Functor List where
    fmap _ Nil         = Nil
    fmap f (Cons x xs) = Cons (f x) (fmap f xs)

instance Foldable List where
    foldr _ z Nil         = z
    foldr f z (Cons x xs) = x `f` foldr f z xs

instance Monad List where
    return x = Cons x Nil

    m >>= f = foldr (<>) mempty $ fmap f m

{-
Left Identity
return a >>= f = f a

return a >>= f
    = Cons a Nil >>= f                                  -- Monad return
    = foldr (<>) mempty $ fmap f (Cons a Nil)           -- Monad >>=
    = foldr (<>) mempty $ Cons (f a) (fmap f Nil)       -- Functor fmap.2
    = foldr (<>) mempty $ Cons (f a) Nil                -- Functor fmap.1
    = (f a) <> foldr (<>) mempty Nil                    -- Foldable foldr.2
    = (f a) <> mempty                                   -- Foldable foldr.1
    = (f a) <> Nil                                      -- Monoid mempty
    = f a                                               -- Monoid mappend.2

Right Identity
m >>= return = m

We can prove this by induction on m

Base case m = Nil
We want: Nil >>= return = Nil

Nil >>= return
    = foldr (<>) mempty $ fmap return Nil               -- Monad >>=
    = foldr (<>) mempty Nil                             -- Functor fmap.1
    = mempty                                            -- Foldable foldr.1
    = Nil                                               -- Monoid mempty

Inductive Case m = Cons x xs
Assume xs >>= return = xs

    foldr (<>) mempty $ fmap return xs

We want: (Cons x xs) >>= return = Cons x xs

(Cons x xs) >>= return
    = foldr (<>) mempty $ fmap return (Cons x xs)            -- Monad >>=
    = foldr (<>) mempty $ Cons (return x) (fmap return xs)   -- Functor fmap.2
    = foldr (<>) mempty $ Cons (Cons x Nil) (fmap return xs) -- Monad return
    = (Cons x Nil) <> foldr (<>) mempty (fmap return xs)     -- Foldable foldr.2
    = Cons x (Nil <> foldr (<>) mempty (fmap return xs))     -- Monoid mappend.3
    = Cons x (foldr (<>) mempty (fmap return xs))            -- Monoid mappend.1
    = Cons x xs                                              -- Ind. Hypot.

Associativity
(m >>= f) >>= g = m >>= (\x -> f x >>= g)

Case m = Nil
(Nil >>= f) >>= g = Nil >>= (\x -> f x >>= g)

Left side
(Nil >>= f) >>= g
    = (foldr (<>) mempty $ fmap f Nil) >>= g            -- Monad >>=
    = (foldr (<>) mempty Nil) >>= g                     -- Functor fmap.1
    = mempty >>= g                                      -- Foldable foldr.1
    = Nil >>= g                                         -- Monoid mempty
    = foldr (<>) mempty $ fmap g Nil                    -- Monad >>=
    = foldr (<>) mempty Nil                             -- Functor fmap.1
    = mempty                                            -- Foldable foldr.1
    = Nil                                               -- Monoid mempty

Right side
Nil >>= (\x -> f x >>= g)
    = foldr (<>) mempty $ fmap (\x -> f x >>= g) Nil    -- Monad >>=
    = foldr (<>) mempty Nil                             -- Functor fmap.1
    = mempty                                            -- Foldable foldr.1
    = Nil                                               -- Monoid mempty

Inductive Case
Assume (xs >>= f) >>= g = xs >>= (\y -> f y >>= g)

    (xs >>= f) >>= g
        = (foldr (<>) mempty $ fmap f xs) >>= g

    xs >>= (\y -> f y >>= g)
        = foldr (<>) mempty $ fmap (\y -> f y >>= g) xs

Show ((Cons x xs) >>= f) >>= g = (Cons x xs) >>= (\y -> f y >>= g)

((Cons x xs) >>= f) >>= g
    = (foldr (<>) mempty $ fmap f (Cons x xs)) >>= g                                -- Monad >>=
    = (foldr (<>) mempty $ Cons (f x) (fmap f xs)) >>= g                            -- Functor fmap.2
    = ((f x) <> foldr (<>) mempty (fmap f xs)) >>= g                                -- Foldable foldr.2
    = ((f x) <> (xs >>= f)) >>= g                                                   -- Monad >>=
    ???

(Cons x xs) >>= (\y -> f y >>= g)
    = foldr (<>) mempty $ fmap (\y -> f y >>= g) (Cons x xs)                        -- Monad >>=
    = foldr (<>) mempty $ Cons ((\y -> f y >>= g) x) (fmap (\y -> f y >>= g) xs)    -- Functor fmap.2
    = foldr (<>) mempty $ Cons (f x >>= g) (fmap (\y -> f y >>= g) xs)              -- Subtitution
    = (f x >>= g) <> foldr (<>) mempty $ fmap (\y -> f y >>= g) xs                  -- Foldable foldr.2
    = (f x >>= g) <> (xs >>= (\y -> f y >>= g))                                     -- Monad >>=
    = (f x >>= g) <> ((xs >>= f) >>= g)                                             -- Ind. Hypot.
    ???

-}