module Filled where
import Prelude hiding (Functor(..), Monad(..))
— a great read on functors, monads, and applicatives: https://adit.io/posts/2013-04-17-functors,_applicatives,_and_monads_in_pictures.html
— from lecture notes:
class Functor f where
fmap :: (a -> b) -> f a -> f b
{-
Functor laws:
Identity: fmap id x == id x
Composition: fmap (f . g) x == fmap f (fmap g x)
-}
class Monad m where
— >>= is pronounced ‘bind’
(>>=) :: m a -> (a -> m b) -> m b
return :: a -> m a
{-
Monad Laws:
Left identity: return a >>= k = k a
Right identity: m >>= return = m
Associativity: m >>= (\x -> k x >>= h) = (m >>= k) >>= h
-}
———————————————
—- TREES —-
———————————————
data Tree a = Tip a | Branch (Tree a) (Tree a)
deriving Show
instance Functor Tree where
fmap f (Tip v) = Tip (f v) — fmap.1
fmap f (Branch left right) = Branch (fmap f left) (fmap f right) — fmap.2
{-
Functor laws:
Identity: fmap id x == id x
Proof:
Base case:
fmap id (Tip x)
={ fmap.1 }
Tip (id x)
={ id }
Tip x
={ id }
id (Tip x)
Induction step: Assume for some left, right : Branch a, the property holds
fmap id (Branch left right)
={ fmap.2 }
Branch (fmap id left) (fmap id right)
={ Ind Hyp }
Branch (id left) (id right)
={ id }
Branch (left) (right)
={ id }
id $ Branch (left) (right)
Composition: fmap (f . g) x == fmap f (fmap g x)
Proof:
Base case:
fmap (f . g) (Tip x)
={ fmap.1 }
Tip ((f . g) x)
={ . }
Tip (f (g x))
={ fmap.1 }
fmap f (Tip (g x))
={ fmap.1 }
fmap f (fmap g x)
Induction step: Assume for some left, right : Tree a, the property holds
fmap (f . g) (Branch left right)
={ fmap.2 }
Branch (fmap (f . g) left) (fmap (f . g) right)
={ Ind Hyp }
Branch (fmap f (fmap g left)) (fmap f (fmap g right))
={ fmap.2 }
fmap f (Branch (fmap g left) (fmap g right))
={ fmap.2 }
fmap f (fmap g (Branch left right))
-}
instance Monad Tree where
(>>=) (Tip v) f = f v — >>=.1
(>>=) (Branch left right) f = Branch (left >>= f) (right >>= f) — >>=.2
return v = Tip v — return
{-
Monad Laws:
Left identity: return a >>= k = k a
Proof:
return a >>= k — return
= (Tip a) >>= k — >>=.1
= k a
Right identity: m >>= return = m
Proof by induction:
Base case: m = Tip x
(Tip x) >>= return
={ >>=.1 }
return x
={ return }
Tip x
Induction step: Assume property holds for left, right :: Tree a
(Branch left right) >>= return
={ >>=.2 }
Branch (left >>= return) (right >>= return)
={ ind. hyp. }
Branch left right
Associativity: m >>= (\x -> k x >>= h) = (m >>= k) >>= h
Proof by induction:
Base case: m = Tip a
(Tip a) >>= (\x -> k x >>= h)
={ >>=.1 }
(\x -> k x >>= h) a
={ lambda application }
k a >>= h
={ >>=.1 }
((Tip a) >>= k) >>= h
Induction step: Branch left right, assuming the property holds for the left and right
(Branch left right) >>= (\x -> k x >>= h)
={ >>=.2 }
Branch (left >>= (\x -> k x >>= h)) (right >>= (\x -> k x >>= h))
={ ind hyp }
Branch ((left >>= k) >>= h) ((right >>= k) >>= h)
={ >>=.2 }
(Branch (left >>= k) (right >>= k)) >>= h
={ >>=.2 }
((Branch left right) >>= k) >>= h
-}
———————————————
—- GTREE —-
———————————————
data GTree a = Leaf a | GNode [GTree a]
deriving Show
instance Functor GTree where
fmap f (Leaf v) = Leaf (f v)
fmap f (GNode ts) = GNode (map (fmap f) ts)
— for the sake of showing the same process without using `map`
— fmap f (GNode []) = GNode []
— fmap f (GNode (t:ts)) = GNode (fmap f t : fts)
— where
— GNode fts = fmap f (GNode ts)
instance Monad GTree where
(>>=) (Leaf v) f = f v
(>>=) (GNode ts) f = GNode (map (>>= f) ts)
return v = Leaf v
———————————————
—- ROSES —-
———————————————
data Rose a = Rose a [Rose a]
deriving Show
instance Functor Rose where
fmap f (Rose v rs) = Rose (f v) (map (fmap f) rs)
instance Monad Rose where
(>>=) (Rose v rs) f = Rose fv (frs ++ map (>>= f) rs)
where Rose fv frs = f v
return v = Rose v []