content: {-# LANGUAGE Rank2Types #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE Safe #-}
  
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  Control.Applicative.Free
  -- Copyright   :  (C) 2012-2013 Edward Kmett
  -- License     :  BSD-style (see the file LICENSE)
  --
  -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
  -- Stability   :  provisional
  -- Portability :  GADTs, Rank2Types
  --
  -- 'Applicative' functors for free
  ----------------------------------------------------------------------------
  module Control.Applicative.Free
    (
    -- | Compared to the free monad, they are less expressive. However, they are also more
    -- flexible to inspect and interpret, as the number of ways in which
    -- the values can be nested is more limited.
    --
    -- See <http://arxiv.org/abs/1403.0749 Free Applicative Functors>,
    -- by Paolo Capriotti and Ambrus Kaposi, for some applications.
  
      Ap(..)
    , runAp
    , runAp_
    , liftAp
    , iterAp
    , hoistAp
    , retractAp
  
    -- * Examples
    -- $examples
    ) where
  
  import Control.Applicative
  import Control.Comonad (Comonad(..))
  import Data.Functor.Apply
  import Data.Foldable
  import Data.Semigroup.Foldable
  import Data.Functor.Classes
  
  import Prelude hiding (null)
  
  -- | The free 'Applicative' for a 'Functor' @f@.
  data Ap f a where
    Pure :: a -> Ap f a
    Ap   :: f a -> Ap f (a -> b) -> Ap f b
  
  -- | Given a natural transformation from @f@ to @g@, this gives a canonical monoidal natural transformation from @'Ap' f@ to @g@.
  --
  -- prop> runAp t == retractApp . hoistApp t
  runAp :: Applicative g => (forall x. f x -> g x) -> Ap f a -> g a
  runAp _ (Pure x) = pure x
  runAp u (Ap f x) = flip id <$> u f <*> runAp u x
  
  -- | Perform a monoidal analysis over free applicative value.
  --
  -- Example:
  --
  -- @
  -- count :: Ap f a -> Int
  -- count = getSum . runAp_ (\\_ -> Sum 1)
  -- @
  runAp_ :: Monoid m => (forall a. f a -> m) -> Ap f b -> m
  runAp_ f = getConst . runAp (Const . f)
  
  instance Functor (Ap f) where
    fmap f (Pure a)   = Pure (f a)
    fmap f (Ap x y)   = Ap x ((f .) <$> y)
  
  instance Apply (Ap f) where
    Pure f <.> y = fmap f y
    Ap x y <.> z = Ap x (flip <$> y <.> z)
  
  instance Applicative (Ap f) where
    pure = Pure
    Pure f <*> y = fmap f y
    Ap x y <*> z = Ap x (flip <$> y <*> z)
  
  instance Comonad f => Comonad (Ap f) where
    extract (Pure a) = a
    extract (Ap x y) = extract y (extract x)
    duplicate (Pure a) = Pure (Pure a)
    duplicate (Ap x y) = Ap (duplicate x) (extend (flip Ap) y)
  
  -- | @foldMap f == foldMap f . 'runAp' 'Data.Foldable.toList'@
  instance Foldable f => Foldable (Ap f) where
    foldMap f (Pure a) = f a
    foldMap f (Ap x y) = foldMap (\a -> foldMap (\g -> f (g a)) y) x
  
    null (Pure _) = False
    null (Ap x y) = null x || null y
  
    length = go 1
      where
        -- This type annotation is required to do polymorphic recursion
        go :: Foldable t => Int -> Ap t a -> Int
        go n (Pure _) = n
        go n (Ap x y) = case n * length x of
          0  -> 0
          n' -> go n' y
  
  -- | @foldMap f == foldMap f . 'runAp' 'toNonEmpty'@
  instance Foldable1 f => Foldable1 (Ap f) where
    foldMap1 f (Pure a) = f a
    foldMap1 f (Ap x y) = foldMap1 (\a -> foldMap1 (\g -> f (g a)) y) x
  
  
  {- $note_eq1
  
  This comment section is an internal documentation, but written in proper
  Haddock markup. It is to allow rendering them to ease reading this rather long document.
  
  === About the definition of @Eq1 (Ap f)@ instance
  
  The @Eq1 (Ap f)@ instance below has a complex definition. This comment
  explains why it is defined like that.
  
  The discussion given here also applies to @Ord1 (Ap f)@ instance with a little change.
  
  ==== General discussion about @Eq1@ type class
  
  Currently, there isn't a law on the @Eq1@ type class, but the following
  properties can be expected.
  
  * If @Eq (f ())@, and @Functor f@ holds, @Eq1 f@ satisfies
  
      > liftEq (\_ _ -> True) x y == (() <$ x) == (() <$ y)
  
  * If @Foldable f@ holds, @Eq1 f@ satisfies:
  
      * @boringEq x y@ implies @length (toList x) == length (toList y)@
  
      * @liftEq eq x y == liftEq (\_ _ -> True) && all (\(a,b) -> eq a b)) (zip (toList x) (toList y))@
  
  Let's define the commonly used function @liftEq (\\_ _ -> True)@ as @boringEq@.
  
  > boringEq :: Eq1 f => f a -> f b -> Bool
  > boringEq = liftEq (\_ _ -> True)
  
  Changing the constant @True@ to the constant @False@ in the definition of
  @boringEq@, let @emptyEq@ function be defined as:
  
  > emptyEq :: Eq1 f => f a -> f b -> Bool
  > emptyEq = liftEq (\_ _ -> False)
  
  From the above properties expectated on a @Eq1@ instance, @emptyEq@ satisfies the following.
  
  > emptyEq x y = boringEq x y && null (zip (toList x) (toList y))
  
  ==== About @instance (Eq1 (Ap f))@
  
  If we're to define @Eq1 (Ap f)@ satisfying these properties as expected, @Eq (Ap f ())@ will determine
  how @liftEq@ should behave. It's not unreasonable to define equality between @Ap f ()@ as below.
  
  > boringEqAp (Pure _) (Pure _) = True
  > boringEqAp (Ap x1 y1) (Ap x2 y2) = boringEq x1 x2 && boringEqAp y1 y2
  >    {-  = ((() <$ x1) == (() <$ x2)) && (y1 == y2)  -}
  > boringEqAp _ _ = False
  
  Its type can be more general than equality between @Ap f ()@:
  
  > boringEqAp :: Eq1 f => Ap f a -> Ap f b -> Bool
  
  Using @boringEqAp@, the specification of @liftEq@ will be:
  
  > liftEq eq x y = boringEqAp x y && and (zipWith eq (toList x) (toList y))
  
  Then unfold @toList@ to remove the dependency to @Foldable@.
  
  > liftEq eq (Pure a1) (Pure a2)
  >   = boringEqAp (Pure a1) (Pure a2) && all (\(a,b) -> eq a b)) (zip (toList (Pure x)) (toList Pure y))
  >   = True && all (\(a,b) -> eq a b) (zip [a1] [a2])
  >   = eq a1 a2
  > liftEq eq (Ap x1 y1) (Ap x2 y2)
  >   = boringEqAp (Ap x1 y1) (Ap x2 y2) && all (\(b1, b2) -> eq b1 b2) (zip (toList (Ap x1 y1)) (toList (Ap x2 y2)))
  >   = boringEq x1 y1 && boringEqAp y1 y2 && all (\(b1, b2) -> eq b1 b2) (zip (toList x1 <**> toList y1) (toList x2 <**> toList y2))
  >   = boringEq x1 y1 && boringEqAp y1 y2 && all (\(b1, b2) -> eq b1 b2) (zip (as1 <**> gs1) (as2 <**> gs2))
  >        where as1 = toList x1
  >              as2 = toList x2
  >              gs1 = toList y1
  >              gs2 = toList y2
  >   = boringEq x1 y1 && boringEqAp y1 y2 && all (\(a1, a2) -> all (\(g1, g2) -> eq (g1 a1) (g2 a2)) (zip gs1 gs2)) (zip as1 as2)
  
  If @zip as1 as2@ is /not/ empty, the following transformation is valid.
  
  > (...) | not (null (zip as1 as2))
  >   = boringEq x1 x2 && boringEqAp y1 y2 && all (\(a1, a2) -> all (\(g1, g2) -> eq (g1 a1) (g2 a2)) (zip gs1 gs2)) (zip as1 as2)
  >   = boringEq x1 x2 && all (\(a1, a2) -> boringEqAp y1 y2 && all (\(g1, g2) -> eq (g1 a1) (g2 a2)) (zip gs1 gs2)) (zip as1 as2)
  > --                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  >   = boringEq x1 x2 && all (\(a1, a2) -> liftEq (\g1 g2 -> eq (g1 a1) (g2 a2)) y1 y2) (zip as1 as2)
  >   = liftEq (\a1 a2 -> liftEq (\g1 g2 -> eq (g1 a1) (g2 a2)) y1 y2)) x1 x2
  
  Because, generally, the following transformation is valid if @xs@ is a nonempty list.
  
  > cond && all p xs = all (\x -> cond && p x) xs -- Only when xs is not empty!
  
  If @zip as1 as2@ is empty, @all (...) (zip as1 as2)@ is vacuously true, so the following transformation is valid.
  
  > (...) | null (zip as1 as2)
  >   = boringEq x1 x2 && boringEqAp y1 y2 && all (\(a1, a2) -> all (\(g1, g2) -> eq (g1 a1) (g2 a2)) (zip gs1 gs2)) (zip as1 as2)
  >   = boringEq x1 x2 && boringEqAp y1 y2
  
  Combining two cases:
  
  > liftEq eq (Ap x1 y1) (Ap x2 y2)
  >   = null (zip as1 as2) && boringEq x1 x2 && boringEqAp y1 y2
  >       || not (null (zip as1 as2)) && liftEq (\a1 a2 -> liftEq (\g1 g2 -> eq (g1 a1) (g2 a2)) y1 y2)) x1 x2
  >   = null (zip as1 as2) && boringEq x1 x2 && boringEqAp y1 y2
  >       || liftEq (\a1 a2 -> liftEq (\g1 g2 -> eq (g1 a1) (g2 a2)) y1 y2)) x1 x2
  >   = emptyEq x1 x2 && boringEqAp y1 y2
  >       || liftEq (\a1 a2 -> liftEq (\g1 g2 -> eq (g1 a1) (g2 a2)) y1 y2)) x1 x2
  
  The property about @emptyEq@ is used in the last equation.
  
  Hence it's defined as this source code.
  
  -}
  
  -- | Specialized 'boringEq' for @Ap f@.
  boringEqAp :: Eq1 f => Ap f a -> Ap f b -> Bool
  boringEqAp (Pure _) (Pure _) = True
  boringEqAp (Ap x1 y1) (Ap x2 y2) = boringEq x1 x2 && boringEqAp y1 y2
  boringEqAp _ _ = False
  
  -- | Implementaion of 'liftEq' for @Ap f@.
  liftEqAp :: Eq1 f => (a -> b -> Bool) -> Ap f a -> Ap f b -> Bool
  liftEqAp eq (Pure a1) (Pure a2) = eq a1 a2
  liftEqAp eq (Ap x1 y1) (Ap x2 y2)
      -- This branching is necessary and not just an optimization.
      -- See the above comment for more
    | emptyEq x1 x2 = boringEqAp y1 y2
    | otherwise =
        liftEq (\a1 a2 -> liftEqAp (\g1 g2 -> eq (g1 a1) (g2 a2)) y1 y2) x1 x2
  liftEqAp _ _ _ = False
  
  -- | @boringEq fa fb@ tests if @fa@ and @fb@ are equal ignoring any difference between
  --   their content (the values of their last parameters @a@ and @b@.)
  --
  --   It is named \'boring\' because the type parameters @a@ and @b@ are
  --   treated as if they are the most boring type @()@.
  boringEq :: Eq1 f => f a -> f b -> Bool
  boringEq = liftEq (\_ _ -> True)
  
  -- | @emptyEq fa fb@ tests if @fa@ and @fb@ are equal /and/ they don't have any content
  --   (the values of their last parameters @a@ and @b@.)
  --
  --   It is named \'empty\' because it only tests for values without any content,
  --   like an empty list or @Nothing@.
  --
  --   If @f@ is also @Foldable@, @emptyEq fa fb@ would be equivalent to
  --   @null fa && null fb && liftEq eq@ for any @eq :: a -> b -> Bool@.
  --
  --   (It depends on each instance of @Eq1@. Since @Eq1@ does not have
  --   any laws currently, this is not a hard guarantee. But all instances in "base", "transformers",
  --   "containers", "array", and "free" satisfy it.)
  --
  --   Note that @emptyEq@ is not a equivalence relation, since it's possible @emptyEq x x == False@.
  emptyEq :: Eq1 f => f a -> f b -> Bool
  emptyEq = liftEq (\_ _ -> False)
  
  instance Eq1 f => Eq1 (Ap f) where
    liftEq = liftEqAp
  
  instance (Eq1 f, Eq a) => Eq (Ap f a) where
    (==) = eq1
  
  -- | Specialized 'boringCompare' for @Ap f@.
  boringCompareAp :: Ord1 f => Ap f a -> Ap f b -> Ordering
  boringCompareAp (Pure _) (Pure _) = EQ
  boringCompareAp (Pure _) (Ap _ _) = LT
  boringCompareAp (Ap x1 y1) (Ap x2 y2) = boringCompare x1 x2 `mappend` boringCompareAp y1 y2
  boringCompareAp (Ap _ _) (Pure _) = GT
  
  -- | Implementation of 'liftCompare' for @Ap f@
  liftCompareAp :: Ord1 f => (a -> b -> Ordering) -> Ap f a -> Ap f b -> Ordering
  liftCompareAp cmp (Pure a1) (Pure a2) = cmp a1 a2
  liftCompareAp _   (Pure _) (Ap _ _) = LT
  liftCompareAp cmp (Ap x1 y1) (Ap x2 y2)
      -- This branching is necessary and not just an optimization.
      -- See the above comment for more
    | emptyEq x1 x2 = boringCompareAp y1 y2
    | otherwise     = liftCompare (\a1 a2 -> liftCompareAp (\g1 g2 -> cmp (g1 a1) (g2 a2)) y1 y2) x1 x2
  liftCompareAp _   (Ap _ _) (Pure _) = GT
  
  -- | @boringCompare fa fb@ compares @fa@ and @fb@ ignoring any difference between
  --   their content (the values of their last parameters @a@ and @b@.)
  --
  --   It is named \'boring\' because the type parameters @a@ and @b@ are
  --   treated as if they are the most boring type @()@.
  boringCompare :: Ord1 f => f a -> f b -> Ordering
  boringCompare = liftCompare (\_ _ -> EQ)
  
  instance Ord1 f => Ord1 (Ap f) where
    liftCompare = liftCompareAp
  
  instance (Ord1 f, Ord a) => Ord (Ap f a) where
    compare = compare1
  
  -- | A version of 'lift' that can be used with just a 'Functor' for @f@.
  liftAp :: f a -> Ap f a
  liftAp x = Ap x (Pure id)
  {-# INLINE liftAp #-}
  
  -- | Tear down a free 'Applicative' using iteration.
  iterAp :: Functor g => (g a -> a) -> Ap g a -> a
  iterAp algebra = go
    where go (Pure a) = a
          go (Ap underlying apply) = algebra (go . (apply <*>) . pure <$> underlying)
  
  -- | Given a natural transformation from @f@ to @g@ this gives a monoidal natural transformation from @Ap f@ to @Ap g@.
  hoistAp :: (forall a. f a -> g a) -> Ap f b -> Ap g b
  hoistAp _ (Pure a) = Pure a
  hoistAp f (Ap x y) = Ap (f x) (hoistAp f y)
  
  -- | Interprets the free applicative functor over f using the semantics for
  --   `pure` and `<*>` given by the Applicative instance for f.
  --
  --   prop> retractApp == runAp id
  retractAp :: Applicative f => Ap f a -> f a
  retractAp (Pure a) = pure a
  retractAp (Ap x y) = x <**> retractAp y
  
  {- $examples
  
  <examples/ValidationForm.hs Validation form>
  
  -}
  