```{- |
Description : Successor Functor
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)

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

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

-}
```