{- | Description : Successor Functor Copyright : © Joachim Breitner, 2017 License : MIT Maintainer : mail@joachim-breitner.de A value of type @'Succs' a@ represents a step in a graph with nodes of type @a@, or in other words, a node plus the list of its successors. The 'Applicative' instance for @'Succs' a@ is such that the node represented by @a '<*>' b@ is the application of the node of @a@ applied to the node of @b@, and (more importantly) the successors modeled by @a '<*>' b@ are the node of @a@ applied to the succesors of @b@ in addition to the succesors of @a@ applied to the node of @b@. This way, at most one step is taken. >>> (++) <$> Succs "0" ["1","2"] <*> Succs "A" ["B","C"] Succs "0A" ["1A","2A","0B", "0C"] >>> skip x = Succs [x] [[]] >>> getSuccs $ (concat <$> traverse skip "Hello") ["ello","Hllo","Helo","Helo","Hell"] This applicative functor can be useful to define shrink functions for QuickCheck, using the helper > shrinkSuccs x = Succs x (shrink x) as explained in a <http://stackoverflow.com/a/41944525/946226 StackExchange answer.> -} module Control.Applicative.Successors where data Succs a = Succs a [a] deriving (Int -> Succs a -> ShowS [Succs a] -> ShowS Succs a -> String (Int -> Succs a -> ShowS) -> (Succs a -> String) -> ([Succs a] -> ShowS) -> Show (Succs a) forall a. Show a => Int -> Succs a -> ShowS forall a. Show a => [Succs a] -> ShowS forall a. Show a => Succs a -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Succs a] -> ShowS $cshowList :: forall a. Show a => [Succs a] -> ShowS show :: Succs a -> String $cshow :: forall a. Show a => Succs a -> String showsPrec :: Int -> Succs a -> ShowS $cshowsPrec :: forall a. Show a => Int -> Succs a -> ShowS Show, Succs a -> Succs a -> Bool (Succs a -> Succs a -> Bool) -> (Succs a -> Succs a -> Bool) -> Eq (Succs a) forall a. Eq a => Succs a -> Succs a -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Succs a -> Succs a -> Bool $c/= :: forall a. Eq a => Succs a -> Succs a -> Bool == :: Succs a -> Succs a -> Bool $c== :: forall a. Eq a => Succs a -> Succs a -> Bool Eq) instance Functor Succs where fmap :: (a -> b) -> Succs a -> Succs b fmap a -> b f (Succs a o [a] s) = b -> [b] -> Succs b forall a. a -> [a] -> Succs a Succs (a -> b f a o) ((a -> b) -> [a] -> [b] forall a b. (a -> b) -> [a] -> [b] map a -> b f [a] s) instance Applicative Succs where pure :: a -> Succs a pure a x = a -> [a] -> Succs a forall a. a -> [a] -> Succs a Succs a x [] Succs a -> b f [a -> b] fs <*> :: Succs (a -> b) -> Succs a -> Succs b <*> Succs a x [a] xs = b -> [b] -> Succs b forall a. a -> [a] -> Succs a Succs (a -> b f a x) (((a -> b) -> b) -> [a -> b] -> [b] forall a b. (a -> b) -> [a] -> [b] map ((a -> b) -> a -> b forall a b. (a -> b) -> a -> b $ a x) [a -> b] fs [b] -> [b] -> [b] forall a. [a] -> [a] -> [a] ++ (a -> b) -> [a] -> [b] forall a b. (a -> b) -> [a] -> [b] map a -> b f [a] xs) instance Monad Succs where Succs a x [a] xs >>= :: Succs a -> (a -> Succs b) -> Succs b >>= a -> Succs b f = b -> [b] -> Succs b forall a. a -> [a] -> Succs a Succs b y ((a -> b) -> [a] -> [b] forall a b. (a -> b) -> [a] -> [b] map (Succs b -> b forall t. Succs t -> t getCurrent (Succs b -> b) -> (a -> Succs b) -> a -> b forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Succs b f) [a] xs [b] -> [b] -> [b] forall a. [a] -> [a] -> [a] ++ [b] ys) where Succs b y [b] ys = a -> Succs b f a x -- | Returns the represented node -- -- Properties: -- -- prop> getCurrent (pure x) == x -- prop> getCurrent (f <*> x) == (getCurrent f) (getCurrent x) -- prop> getCurrent (x >>= k) == getCurrent (k (getCurrent x)) getCurrent :: Succs t -> t getCurrent :: Succs t -> t getCurrent (Succs t x [t] _) = t x -- | Returns the represented successors -- -- prop> getSuccs (pure x) == [] -- prop> getSuccs (f <*> x) == map ($ getCurrent x) (getSuccs f) ++ map (getCurrent f) (getSuccs x) -- prop> getSuccs (x >>= k) == map (getCurrent . k) (getSuccs x) ++ getSuccs k (getCurrent x) getSuccs :: Succs t -> [t] getSuccs :: Succs t -> [t] getSuccs (Succs t _ [t] xs) = [t] xs {- The Applicative laws: pure id <*> Succs x xs = Succs id [] <*> Succs x xs = Succs (id x) (map ($ x) [] ++ map id xs) = Succs x xs pure (.) <*> Succs u us <*> Succs v vs <*> Succs w ws = Succs (.) [] <*> Succs u us <*> Succs v vs <*> Succs w ws = Succs (u .) (map (.) us) <*> Succs v vs <*> Succs w ws = Succs (u . v) (map ($v) (map (.) us) ++ map (u .) vs) <*> Succs w ws = Succs (u . v) (map (($v).(.)) us ++ map (u .) vs) <*> Succs w ws = Succs ((u . v) w) (map ($w) (map (($v).(.)) us ++ map (u .) vs) ++ map (u.v) ws) = Succs ((u . v) w) (map (($w).($v).(.)) us ++ map (($w).(u.)) vs ++ map (u.v) ws) = Succs (u (v w)) (map (\u -> u (v w)) us ++ map (\v -> u (v w)) vs ++ map (\w -> u (v w)) ws) = Succs (u (v w)) (map ($(v w)) us ++ map u (map ($w) vs ++ map v ws)) = Succs u us <*> Succs (v w) (map ($w) vs ++ map v ws) = Succs u us <*> (Succs v vs <*> Succs w ws) pure f <*> pure x = Succs f [] <*> Succs x [] = Succs (f x) [] = pure (f x) Succs u us <*> pure y = Succs u us <*> Succs y [] = Succs (u y) (map ($y) us) = Succs (($y) u) (map ($y) us) = Succs ($y) [] <*> Succs u us = pure ($ y) <*> u The Monad laws: return a >>= k = Succs a [] >>= k = let Succs y ys = k a in Succs y (map (getCurrent . k) [] ++ ys) = let Succs y ys = k a in Succs y ys = k a Succs x xs >>= return = let Succs y ys = return x in Succs y (map (getCurrent . return) xs ++ ys) = let Succs y ys = Succs x [] in Succs y (map (getCurrent . return) xs ++ ys) = Succs x (map (getCurrent . return) xs ++ []) = Succs x xs Lemma: getCurrent (s >>= k) = getCurrent (k (getCurrent s)) Proof: getCurrent (Succs x xs >>= k) = getCurrent (let Succs y ys = k x in Succs y …) = let Succs y ys = k x in y = getCurrent (k x) = getCurrent (k (getCurrent (Succs x xs))) Succs x xs >>= (\x -> k x >>= h) = let Succs z zs = (\x -> k x >>= h) x in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs) = let Succs z zs = k x >>= h in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs) = let Succs z zs = k x >>= h in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs) = let Succs z zs = k x >>= h in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs) = let Succs z zs = (let Succs y ys = k x in Succs y ys >>= h) in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs) = let Succs z zs = (let Succs y ys = k x in let Succs z zs = h y in Succs z (map (getCurrent . h) ys ++ zs)) in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs) = let Succs y ys = k x in let Succs z zs = h y in let Succs z zs = Succs z (map (getCurrent . h) ys ++ zs) in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs) = let Succs y ys = k x in let Succs z zs = h y in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ map (getCurrent . h) ys ++ zs) = let Succs y ys = k x in let Succs z zs = h y in Succs z (map (\x -> getCurrent (k x >>= h)) xs ++ map (getCurrent . h) ys ++ zs) = let Succs y ys = k x in let Succs z zs = h y in Succs z (map (\x -> getCurrent (h (getCurrent (k x)))) xs ++ map (getCurrent . h) ys ++ zs) = let Succs y ys = k x in let Succs z zs = h y in Succs z (map (getCurrent . h . getCurrent . k) xs ++ map (getCurrent . h) ys ++ zs) = let Succs y ys = k x in let Succs z zs = h y in Succs z (map (getCurrent . h) (map (getCurrent . k) xs ++ ys) ++ zs) = let Succs y ys = k x in Succs y (map (getCurrent . k) xs ++ ys) >>= h = (let Succs y ys = k x in Succs y (map (getCurrent . k) xs ++ ys)) >>= h = (Succs x xs >>= k) >>= h Lemma: (<*>) = ap Proof: Succs f fs <*> Succs x xs = Succs (f x) (map ($ x) fs ++ map f xs) = let Succs y ys = Succs (f x) (map f xs) in Succs y (map ($ x) fs ++ ys) = let Succs y ys = Succs (f x) (map (\x -> f x) xs) in Succs y (map ($ x) fs ++ ys) = let Succs y ys = Succs (f x) (map (getCurrent . (\x -> pure (f x)) xs)) in Succs y (map ($ x) fs ++ ys) = let Succs y ys = let Succs z zs = pure (f x) in Succs z (map (getCurrent . (\x -> pure (f x)) xs ++ zs)) in Succs y (map ($ x) fs ++ ys) = let Succs y ys = Succs x xs >>= \x -> pure (f x) in Succs y (map ($ x) fs ++ ys) = let Succs y ys = Succs x xs >>= \x -> pure (f x) in Succs y (map (\f -> getCurrent ((\x -> pure (f x)) (getCurrent (Succs x xs)))) fs ++ ys) = let Succs y ys = Succs x xs >>= \x -> pure (f x) in Succs y (map (\f -> getCurrent (Succs x xs >>= (\x -> pure (f x)))) fs ++ ys) = let Succs y ys = Succs x xs >>= \x -> pure (f x) in Succs y (map (getCurrent . (\f -> Succs x xs >>= (\x -> pure (f x)))) fs ++ ys) = Succs f fs >>= (\f -> Succs x xs >>= (\x -> pure (f x))) = Succs f fs `ap` Succs x xs -}