    {-# LANGUAGE DeriveFunctor, GADTs, RankNTypes #-}
    -----------------------------------------------------------------------------
    -- |
    -- Module     : Control.Selective.Rigid.Freer
    -- Copyright  : (c) Andrey Mokhov 2018-2024
    -- License    : MIT (see the file LICENSE)
    -- Maintainer : andrey.mokhov@gmail.com
    -- Stability  : experimental
    --
    -- This is a library for /selective applicative functors/, or just
    -- /selective functors/ for short, an abstraction between applicative functors
    -- and monads, introduced in this paper: https://dl.acm.org/doi/10.1145/3341694.
    --
    -- This module defines /freer rigid selective functors/. Rigid selective
    -- functors are those that satisfy the property @\<*\> = apS@. Compared to the
    -- "free" construction from "Control.Selective.Rigid.Free", this "freer"
    -- construction does not require the underlying base data type to be a functor.
    --
    -----------------------------------------------------------------------------
    module Control.Selective.Rigid.Freer (
        -- * Free rigid selective functors
        Select (..), liftSelect,

        -- * Static analysis
        getPure, getEffects, getNecessaryEffect, runSelect, foldSelect
        ) where

    import Control.Selective.Trans.Except
    import Control.Selective
    import Data.Bifunctor
    import Data.Function
    import Data.Functor

    -- Inspired by free applicative functors by Capriotti and Kaposi.
    -- See: https://arxiv.org/pdf/1403.0749.pdf

    -- Note: In the current implementation, 'fmap' and 'select' cost O(N), where N
    -- is the number of effects. It is possible to improve this to O(1) by using the
    -- idea developed for free applicative functors by Dave Menendez, see this blog
    -- post: https://www.eyrie.org/~zednenem/2013/05/27/freeapp.
    -- An example implementation can be found here:
    -- http://hackage.haskell.org/package/free/docs/Control-Applicative-Free-Fast.html

    -- | Free rigid selective functors.
    data Select f a where
        Pure   :: a -> Select f a
        Select :: Select f (Either (x -> a) a) -> f x -> Select f a

    -- TODO: Prove that this is a lawful 'Functor'.
    instance Functor (Select f) where
        fmap :: forall a b. (a -> b) -> Select f a -> Select f b
    fmap a -> b
    f (Pure a
    a)     = b -> Select f b
    forall a (f :: * -> *). a -> Select f a
    Pure (a -> b
    f a
    a)
        fmap a -> b
    f (Select Select f (Either (x -> a) a)
    x f x
    y) = Select f (Either (x -> b) b) -> f x -> Select f b
    forall (f :: * -> *) x a.
    Select f (Either (x -> a) a) -> f x -> Select f a
    Select (((x -> a) -> x -> b)
    -> (a -> b) -> Either (x -> a) a -> Either (x -> b) b
    forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
    forall (p :: * -> * -> *) a b c d.
    Bifunctor p =>
    (a -> b) -> (c -> d) -> p a c -> p b d
    bimap (a -> b
    f(a -> b) -> (x -> a) -> x -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .) a -> b
    f (Either (x -> a) a -> Either (x -> b) b)
    -> Select f (Either (x -> a) a) -> Select f (Either (x -> b) b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Select f (Either (x -> a) a)
    x) f x
    y -- O(N)

    -- TODO: Prove that this is a lawful 'Applicative'.
    instance Applicative (Select f) where
        pure :: forall a. a -> Select f a
    pure  = a -> Select f a
    forall a (f :: * -> *). a -> Select f a
    Pure
        <*> :: forall a b. Select f (a -> b) -> Select f a -> Select f b
    (<*>) = Select f (a -> b) -> Select f a -> Select f b
    forall (f :: * -> *) a b. Selective f => f (a -> b) -> f a -> f b
    apS -- Rigid selective functors

    -- TODO: Prove that this is a lawful 'Selective'.
    instance Selective (Select f) where
        select :: forall a b.
    Select f (Either a b) -> Select f (a -> b) -> Select f b
    select = (Either a b -> Either ((a -> b) -> b) b)
    -> Select f (Either a b) -> Select f (a -> b) -> Select f b
    forall a b c (f :: * -> *).
    (a -> Either (b -> c) c) -> Select f a -> Select f b -> Select f c
    selectBy ((a -> (a -> b) -> b) -> Either a b -> Either ((a -> b) -> b) b
    forall a b c. (a -> b) -> Either a c -> Either b c
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first a -> (a -> b) -> b
    forall a b. a -> (a -> b) -> b
    (&))
          where
            selectBy :: (a -> Either (b -> c) c) -> Select f a -> Select f b -> Select f c
            selectBy :: forall a b c (f :: * -> *).
    (a -> Either (b -> c) c) -> Select f a -> Select f b -> Select f c
    selectBy a -> Either (b -> c) c
    f Select f a
    x (Pure b
    y)     = ((b -> c) -> c) -> (c -> c) -> Either (b -> c) c -> c
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either ((b -> c) -> b -> c
    forall a b. (a -> b) -> a -> b
    $b
    y) c -> c
    forall a. a -> a
    id (Either (b -> c) c -> c) -> (a -> Either (b -> c) c) -> a -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Either (b -> c) c
    f (a -> c) -> Select f a -> Select f c
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Select f a
    x
            selectBy a -> Either (b -> c) c
    f Select f a
    x (Select Select f (Either (x -> b) b)
    y f x
    z) = Select f (Either (x -> c) c) -> f x -> Select f c
    forall (f :: * -> *) x a.
    Select f (Either (x -> a) a) -> f x -> Select f a
    Select ((a
     -> Either
          (Either (x -> b) b -> Either (x -> c) c) (Either (x -> c) c))
    -> Select f a
    -> Select f (Either (x -> b) b)
    -> Select f (Either (x -> c) c)
    forall a b c (f :: * -> *).
    (a -> Either (b -> c) c) -> Select f a -> Select f b -> Select f c
    selectBy a
    -> Either
         (Either (x -> b) b -> Either (x -> c) c) (Either (x -> c) c)
    g Select f a
    x Select f (Either (x -> b) b)
    y) f x
    z -- O(N)
              where
                g :: a
    -> Either
         (Either (x -> b) b -> Either (x -> c) c) (Either (x -> c) c)
    g a
    a = case a -> Either (b -> c) c
    f a
    a of Right c
    c -> Either (x -> c) c
    -> Either
         (Either (x -> b) b -> Either (x -> c) c) (Either (x -> c) c)
    forall a b. b -> Either a b
    Right (c -> Either (x -> c) c
    forall a b. b -> Either a b
    Right c
    c)
                                  Left b -> c
    bc -> (Either (x -> b) b -> Either (x -> c) c)
    -> Either
         (Either (x -> b) b -> Either (x -> c) c) (Either (x -> c) c)
    forall a b. a -> Either a b
    Left  (((x -> b) -> x -> c)
    -> (b -> c) -> Either (x -> b) b -> Either (x -> c) c
    forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
    forall (p :: * -> * -> *) a b c d.
    Bifunctor p =>
    (a -> b) -> (c -> d) -> p a c -> p b d
    bimap (b -> c
    bc(b -> c) -> (x -> b) -> x -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .) b -> c
    bc)

    -- | Lift a functor into a free selective computation.
    liftSelect :: f a -> Select f a
    liftSelect :: forall (f :: * -> *) a. f a -> Select f a
    liftSelect = Select f (Either (a -> a) a) -> f a -> Select f a
    forall (f :: * -> *) x a.
    Select f (Either (x -> a) a) -> f x -> Select f a
    Select (Either (a -> a) a -> Select f (Either (a -> a) a)
    forall a (f :: * -> *). a -> Select f a
    Pure ((a -> a) -> Either (a -> a) a
    forall a b. a -> Either a b
    Left a -> a
    forall a. a -> a
    id))

    -- | Given a natural transformation from @f@ to @g@, this gives a canonical
    -- natural transformation from @Select f@ to @g@.
    runSelect :: Selective g => (forall x. f x -> g x) -> Select f a -> g a
    runSelect :: forall (g :: * -> *) (f :: * -> *) a.
    Selective g =>
    (forall x. f x -> g x) -> Select f a -> g a
    runSelect forall x. f x -> g x
    _ (Pure a
    a)     = a -> g a
    forall a. a -> g a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    a
    runSelect forall x. f x -> g x
    t (Select Select f (Either (x -> a) a)
    x f x
    y) = g (Either (x -> a) a) -> g ((x -> a) -> a) -> g a
    forall a b. g (Either a b) -> g (a -> b) -> g b
    forall (f :: * -> *) a b.
    Selective f =>
    f (Either a b) -> f (a -> b) -> f b
    select ((forall x. f x -> g x)
    -> Select f (Either (x -> a) a) -> g (Either (x -> a) a)
    forall (g :: * -> *) (f :: * -> *) a.
    Selective g =>
    (forall x. f x -> g x) -> Select f a -> g a
    runSelect f x -> g x
    forall x. f x -> g x
    t Select f (Either (x -> a) a)
    x) (x -> (x -> a) -> a
    forall a b. a -> (a -> b) -> b
    (&) (x -> (x -> a) -> a) -> g x -> g ((x -> a) -> a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f x -> g x
    forall x. f x -> g x
    t f x
    y)

    -- | Concatenate all effects of a free selective computation.
    foldSelect :: Monoid m => (forall x. f x -> m) -> Select f a -> m
    foldSelect :: forall m (f :: * -> *) a.
    Monoid m =>
    (forall x. f x -> m) -> Select f a -> m
    foldSelect forall x. f x -> m
    f = Over m a -> m
    forall m a. Over m a -> m
    getOver (Over m a -> m) -> (Select f a -> Over m a) -> Select f a -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (forall x. f x -> Over m x) -> Select f a -> Over m a
    forall (g :: * -> *) (f :: * -> *) a.
    Selective g =>
    (forall x. f x -> g x) -> Select f a -> g a
    runSelect (m -> Over m x
    forall m a. m -> Over m a
    Over (m -> Over m x) -> (f x -> m) -> f x -> Over m x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f x -> m
    forall x. f x -> m
    f)

    -- | Extract the resulting value if there are no necessary effects.
    getPure :: Select f a -> Maybe a
    getPure :: forall (f :: * -> *) a. Select f a -> Maybe a
    getPure = (forall x. f x -> Maybe x) -> Select f a -> Maybe a
    forall (g :: * -> *) (f :: * -> *) a.
    Selective g =>
    (forall x. f x -> g x) -> Select f a -> g a
    runSelect (Maybe x -> f x -> Maybe x
    forall a b. a -> b -> a
    const Maybe x
    forall a. Maybe a
    Nothing)

    -- | Collect all possible effects in the order they appear in a free selective
    -- computation.
    getEffects :: Functor f => Select f a -> [f ()]
    getEffects :: forall (f :: * -> *) a. Functor f => Select f a -> [f ()]
    getEffects = (forall x. f x -> [f ()]) -> Select f a -> [f ()]
    forall m (f :: * -> *) a.
    Monoid m =>
    (forall x. f x -> m) -> Select f a -> m
    foldSelect (f () -> [f ()]
    forall a. a -> [a]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (f () -> [f ()]) -> (f x -> f ()) -> f x -> [f ()]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f x -> f ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void)

    -- | Extract the necessary effect from a free selective computation. Note: there
    -- can be at most one effect that is statically guaranteed to be necessary.
    getNecessaryEffect :: Functor f => Select f a -> Maybe (f ())
    getNecessaryEffect :: forall (f :: * -> *) a. Functor f => Select f a -> Maybe (f ())
    getNecessaryEffect = Either (f ()) a -> Maybe (f ())
    forall a b. Either a b -> Maybe a
    leftToMaybe (Either (f ()) a -> Maybe (f ()))
    -> (Select f a -> Either (f ()) a) -> Select f a -> Maybe (f ())
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Except (f ()) a -> Either (f ()) a
    forall e a. Except e a -> Either e a
    runExcept (Except (f ()) a -> Either (f ()) a)
    -> (Select f a -> Except (f ()) a) -> Select f a -> Either (f ()) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (forall x. f x -> ExceptT (f ()) Identity x)
    -> Select f a -> Except (f ()) a
    forall (g :: * -> *) (f :: * -> *) a.
    Selective g =>
    (forall x. f x -> g x) -> Select f a -> g a
    runSelect (f () -> ExceptT (f ()) Identity x
    forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
    throwE (f () -> ExceptT (f ()) Identity x)
    -> (f x -> f ()) -> f x -> ExceptT (f ()) Identity x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f x -> f ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void)

    leftToMaybe :: Either a b -> Maybe a
    leftToMaybe :: forall a b. Either a b -> Maybe a
    leftToMaybe (Left a
    a) = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    a
    leftToMaybe Either a b
    _        = Maybe a
    forall a. Maybe a
    Nothing