{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DerivingVia #-}

-- | Indexed applicative functors and monads: see 'Apply', 'Bind', 'Cobind'.

module Data.Functor.Indexed (module Data.Functor.Indexed, pure, copure) where

import Prelude (Functor (fmap), pure, (<$>), Foldable, Traversable, Eq, Ord)
import qualified Control.Applicative as Base
import Control.Category
import qualified Control.Monad as Base
import Control.Comonad (copure)
import qualified Control.Comonad as Base
import Data.Function (flip)
import Data.Kind (Type)

infixl 4 <*>, *>, <*, <**>
-- | Functors into which binary (and thus @n@-ary) functions can be lifted
--
-- Laws:
--
-- * @('.') '<$>' u '<*>' v '<*>' w = u '<*>' (v '<*>' w)@
--
-- Relations of methods:
--
-- * @'liftA2' f x y = f '<$>' x '<*>' y@
-- * @('<*>') = 'liftA2' 'id'@
-- * @('*>') = 'liftA2' ('pure' 'id')@
-- * @('<*') = 'liftA2' ('id' 'pure')@
class (∀ i j . Functor (p i j)) => Apply p where
    {-# MINIMAL (<*>) | liftA2 #-}

    (<*>) :: p i j (a -> b) -> p j k a -> p i k b
    (<*>) = ((a -> b) -> a -> b) -> p i j (a -> b) -> p j k a -> p i k b
forall k (p :: k -> k -> * -> *) a b c (i :: k) (j :: k) (k :: k).
Apply p =>
(a -> b -> c) -> p i j a -> p j k b -> p i k c
liftA2 (a -> b) -> a -> b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

    (*>) :: p i j a -> p j k b -> p i k b
    (*>) = (a -> b -> b) -> p i j a -> p j k b -> p i k b
forall k (p :: k -> k -> * -> *) a b c (i :: k) (j :: k) (k :: k).
Apply p =>
(a -> b -> c) -> p i j a -> p j k b -> p i k c
liftA2 ((b -> b) -> a -> b -> b
forall (f :: * -> *) a. Applicative f => a -> f a
pure b -> b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)

    (<*) :: p i j a -> p j k b -> p i k a
    (<*) = (a -> b -> a) -> p i j a -> p j k b -> p i k a
forall k (p :: k -> k -> * -> *) a b c (i :: k) (j :: k) (k :: k).
Apply p =>
(a -> b -> c) -> p i j a -> p j k b -> p i k c
liftA2 a -> b -> a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

    liftA2 :: (a -> b -> c) -> p i j a -> p j k b -> p i k c
    liftA2 f :: a -> b -> c
f x :: p i j a
x y :: p j k b
y = a -> b -> c
f (a -> b -> c) -> p i j a -> p i j (b -> c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> p i j a
x p i j (b -> c) -> p j k b -> p i k c
forall k (p :: k -> k -> * -> *) (i :: k) (j :: k) a b (k :: k).
Apply p =>
p i j (a -> b) -> p j k a -> p i k b
<*> p j k b
y

(<**>) :: Apply p => p i j a -> p j k (a -> b) -> p i k b
<**> :: p i j a -> p j k (a -> b) -> p i k b
(<**>) = (a -> (a -> b) -> b) -> p i j a -> p j k (a -> b) -> p i k b
forall k (p :: k -> k -> * -> *) a b c (i :: k) (j :: k) (k :: k).
Apply p =>
(a -> b -> c) -> p i j a -> p j k b -> p i k c
liftA2 (((a -> b) -> a -> b) -> a -> (a -> b) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> b) -> a -> b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)

infixl 1 >>=
-- | Functors of which nested levels can be combined
--
-- Laws in terms of 'join':
--
-- * @'join' '.' 'fmap' 'join' = 'join' '.' 'join'@
--
-- Laws in terms of '>>=':
--
-- * @('>>=' f) '.' ('>>=' g) = ('>>=' ('>>=' f) '.' g)@
--
-- Relation of 'join' and '>>=':
--
-- * @'join' = ('>>=' 'id')@
-- * @('>>=' f) = 'join' '.' 'fmap' 'f'@
class Apply m => Bind m where
    {-# MINIMAL join | (>>=) #-}

    join :: m i j (m j k a) -> m i k a
    join = (m i j (m j k a) -> (m j k a -> m j k a) -> m i k a
forall k (m :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Bind m =>
m i j a -> (a -> m j k b) -> m i k b
>>= m j k a -> m j k a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)

    (>>=) :: m i j a -> (a -> m j k b) -> m i k b
    x :: m i j a
x >>= f :: a -> m j k b
f = m i j (m j k b) -> m i k b
forall k (m :: k -> k -> * -> *) (i :: k) (j :: k) (k :: k) a.
Bind m =>
m i j (m j k a) -> m i k a
join (a -> m j k b
f (a -> m j k b) -> m i j a -> m i j (m j k b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m i j a
x)

apIxMonad :: (Bind m, ∀ k . Base.Applicative (m k k)) => m i j (a -> b) -> m j k a -> m i k b
apIxMonad :: m i j (a -> b) -> m j k a -> m i k b
apIxMonad fm :: m i j (a -> b)
fm xm :: m j k a
xm = [a -> b
f a
x | a -> b
f <- m i j (a -> b)
fm, a
x <- m j k a
xm] where
    return :: a -> m k k a
return = a -> m k k a
forall (f :: * -> *) a. Applicative f => a -> f a
Base.pure

infixr 1 <<=
-- | Dual of 'Bind'
--
-- Laws in terms of 'cut':
--
-- * @'cut' '.' 'cut' = 'fmap' 'cut' '.' 'cut'@
--
-- Laws in terms of '<<=':
--
-- * @(f '<<=') '.' (g '<<=') = (f '.' (g '<<=') '<<=')@
--
-- Relation of 'cut' and '<<=':
--
-- * @'cut' = ('id' '<<=')@
-- * @(f '<<=') = 'fmap' f . 'cut'@
class (∀ i j . Functor (ɯ i j)) => Cobind ɯ where
    {-# MINIMAL cut | (<<=) #-}

    cut :: ɯ i k a -> ɯ i j (ɯ j k a)
    cut = (ɯ j k a -> ɯ j k a) -> ɯ i k a -> ɯ i j (ɯ j k a)
forall k (ɯ :: k -> k -> * -> *) (j :: k) (k :: k) a b (i :: k).
Cobind ɯ =>
(ɯ j k a -> b) -> ɯ i k a -> ɯ i j b
(<<=) ɯ j k a -> ɯ j k a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

    (<<=) :: (ɯ j k a -> b) -> ɯ i k a -> ɯ i j b
    (<<=) f :: ɯ j k a -> b
f = (ɯ j k a -> b) -> ɯ i j (ɯ j k a) -> ɯ i j b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ɯ j k a -> b
f (ɯ i j (ɯ j k a) -> ɯ i j b)
-> (ɯ i k a -> ɯ i j (ɯ j k a)) -> ɯ i k a -> ɯ i j b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ɯ i k a -> ɯ i j (ɯ j k a)
forall k (ɯ :: k -> k -> * -> *) (i :: k) (k :: k) a (j :: k).
Cobind ɯ =>
ɯ i k a -> ɯ i j (ɯ j k a)
cut

infixl 1 =>>
(=>>) :: Cobind ɯ => ɯ i k a -> (ɯ j k a -> b) -> ɯ i j b
=>> :: ɯ i k a -> (ɯ j k a -> b) -> ɯ i j b
(=>>) = ((ɯ j k a -> b) -> ɯ i k a -> ɯ i j b)
-> ɯ i k a -> (ɯ j k a -> b) -> ɯ i j b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ɯ j k a -> b) -> ɯ i k a -> ɯ i j b
forall k (ɯ :: k -> k -> * -> *) (j :: k) (k :: k) a b (i :: k).
Cobind ɯ =>
(ɯ j k a -> b) -> ɯ i k a -> ɯ i j b
(<<=)

infixr 1 =>=, =<=

(=>=) :: Cobind ɯ => (ɯ j k a -> b) -> (ɯ i j b -> c) -> ɯ i k a -> c
f :: ɯ j k a -> b
f =>= :: (ɯ j k a -> b) -> (ɯ i j b -> c) -> ɯ i k a -> c
=>= g :: ɯ i j b -> c
g = ɯ i j b -> c
g (ɯ i j b -> c) -> (ɯ i k a -> ɯ i j b) -> ɯ i k a -> c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (ɯ j k a -> b
f (ɯ j k a -> b) -> ɯ i k a -> ɯ i j b
forall k (ɯ :: k -> k -> * -> *) (j :: k) (k :: k) a b (i :: k).
Cobind ɯ =>
(ɯ j k a -> b) -> ɯ i k a -> ɯ i j b
<<=)

(=<=) :: Cobind ɯ => (ɯ i j b -> c) -> (ɯ j k a -> b) -> ɯ i k a -> c
=<= :: (ɯ i j b -> c) -> (ɯ j k a -> b) -> ɯ i k a -> c
(=<=) = ((ɯ j k a -> b) -> (ɯ i j b -> c) -> ɯ i k a -> c)
-> (ɯ i j b -> c) -> (ɯ j k a -> b) -> ɯ i k a -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ɯ j k a -> b) -> (ɯ i j b -> c) -> ɯ i k a -> c
forall k (ɯ :: k -> k -> * -> *) (j :: k) (k :: k) a b (i :: k) c.
Cobind ɯ =>
(ɯ j k a -> b) -> (ɯ i j b -> c) -> ɯ i k a -> c
(=>=)

newtype IxWrap f i j a = IxWrap { IxWrap f i j a -> f a
unIxWrap :: f a }
  deriving (a -> IxWrap f i j b -> IxWrap f i j a
(a -> b) -> IxWrap f i j a -> IxWrap f i j b
(forall a b. (a -> b) -> IxWrap f i j a -> IxWrap f i j b)
-> (forall a b. a -> IxWrap f i j b -> IxWrap f i j a)
-> Functor (IxWrap f i j)
forall a b. a -> IxWrap f i j b -> IxWrap f i j a
forall a b. (a -> b) -> IxWrap f i j a -> IxWrap f i j b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (f :: * -> *) k (i :: k) k (j :: k) a b.
Functor f =>
a -> IxWrap f i j b -> IxWrap f i j a
forall (f :: * -> *) k (i :: k) k (j :: k) a b.
Functor f =>
(a -> b) -> IxWrap f i j a -> IxWrap f i j b
<$ :: a -> IxWrap f i j b -> IxWrap f i j a
$c<$ :: forall (f :: * -> *) k (i :: k) k (j :: k) a b.
Functor f =>
a -> IxWrap f i j b -> IxWrap f i j a
fmap :: (a -> b) -> IxWrap f i j a -> IxWrap f i j b
$cfmap :: forall (f :: * -> *) k (i :: k) k (j :: k) a b.
Functor f =>
(a -> b) -> IxWrap f i j a -> IxWrap f i j b
Functor)

deriving via (p :: Type -> Type) instance Base.Applicative p => Base.Applicative (IxWrap p i j)
deriving via (m :: Type -> Type) instance Base.Monad m => Base.Monad (IxWrap m i j)
instance Base.Comonad ɯ => Base.Comonad (IxWrap ɯ i j) where
    cut :: IxWrap ɯ i j a -> IxWrap ɯ i j (IxWrap ɯ i j a)
cut (IxWrap ɯ :: ɯ a
ɯ) = ɯ (IxWrap ɯ i j a) -> IxWrap ɯ i j (IxWrap ɯ i j a)
forall k k k (f :: k -> *) (i :: k) (j :: k) (a :: k).
f a -> IxWrap f i j a
IxWrap (ɯ a -> IxWrap ɯ i j a
forall k k k (f :: k -> *) (i :: k) (j :: k) (a :: k).
f a -> IxWrap f i j a
IxWrap (ɯ a -> IxWrap ɯ i j a) -> ɯ (ɯ a) -> ɯ (IxWrap ɯ i j a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ɯ a -> ɯ (ɯ a)
forall (ɯ :: * -> *) a. Comonad ɯ => ɯ a -> ɯ (ɯ a)
Base.cut ɯ a
ɯ)
    copure :: IxWrap ɯ i j a -> a
copure (IxWrap ɯ :: ɯ a
ɯ) = ɯ a -> a
forall (ɯ :: * -> *) a. Comonad ɯ => ɯ a -> a
copure ɯ a
ɯ

instance Base.Applicative p => Apply (IxWrap p) where
    IxWrap f :: p (a -> b)
f <*> :: IxWrap p i j (a -> b) -> IxWrap p j k a -> IxWrap p i k b
<*> IxWrap x :: p a
x = p b -> IxWrap p i k b
forall k k k (f :: k -> *) (i :: k) (j :: k) (a :: k).
f a -> IxWrap f i j a
IxWrap (p (a -> b)
f p (a -> b) -> p a -> p b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
Base.<*> p a
x)

instance Base.Monad m => Bind (IxWrap m) where
    join :: IxWrap m i j (IxWrap m j k a) -> IxWrap m i k a
join = m a -> IxWrap m i k a
forall k k k (f :: k -> *) (i :: k) (j :: k) (a :: k).
f a -> IxWrap f i j a
IxWrap (m a -> IxWrap m i k a)
-> (IxWrap m i j (IxWrap m j k a) -> m a)
-> IxWrap m i j (IxWrap m j k a)
-> IxWrap m i k a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. m (m a) -> m a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
Base.join (m (m a) -> m a)
-> (IxWrap m i j (IxWrap m j k a) -> m (m a))
-> IxWrap m i j (IxWrap m j k a)
-> m a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (IxWrap m j k a -> m a) -> m (IxWrap m j k a) -> m (m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IxWrap m j k a -> m a
forall k (f :: k -> *) k (i :: k) k (j :: k) (a :: k).
IxWrap f i j a -> f a
unIxWrap (m (IxWrap m j k a) -> m (m a))
-> (IxWrap m i j (IxWrap m j k a) -> m (IxWrap m j k a))
-> IxWrap m i j (IxWrap m j k a)
-> m (m a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IxWrap m i j (IxWrap m j k a) -> m (IxWrap m j k a)
forall k (f :: k -> *) k (i :: k) k (j :: k) (a :: k).
IxWrap f i j a -> f a
unIxWrap

instance Base.Comonad ɯ => Cobind (IxWrap ɯ) where
    cut :: IxWrap ɯ i k a -> IxWrap ɯ i j (IxWrap ɯ j k a)
cut = ɯ (IxWrap ɯ j k a) -> IxWrap ɯ i j (IxWrap ɯ j k a)
forall k k k (f :: k -> *) (i :: k) (j :: k) (a :: k).
f a -> IxWrap f i j a
IxWrap (ɯ (IxWrap ɯ j k a) -> IxWrap ɯ i j (IxWrap ɯ j k a))
-> (IxWrap ɯ i k a -> ɯ (IxWrap ɯ j k a))
-> IxWrap ɯ i k a
-> IxWrap ɯ i j (IxWrap ɯ j k a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (ɯ a -> IxWrap ɯ j k a) -> ɯ (ɯ a) -> ɯ (IxWrap ɯ j k a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ɯ a -> IxWrap ɯ j k a
forall k k k (f :: k -> *) (i :: k) (j :: k) (a :: k).
f a -> IxWrap f i j a
IxWrap (ɯ (ɯ a) -> ɯ (IxWrap ɯ j k a))
-> (IxWrap ɯ i k a -> ɯ (ɯ a))
-> IxWrap ɯ i k a
-> ɯ (IxWrap ɯ j k a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ɯ a -> ɯ (ɯ a)
forall (ɯ :: * -> *) a. Comonad ɯ => ɯ a -> ɯ (ɯ a)
Base.cut (ɯ a -> ɯ (ɯ a))
-> (IxWrap ɯ i k a -> ɯ a) -> IxWrap ɯ i k a -> ɯ (ɯ a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IxWrap ɯ i k a -> ɯ a
forall k (f :: k -> *) k (i :: k) k (j :: k) (a :: k).
IxWrap f i j a -> f a
unIxWrap

infixr 1 >=>, <=<, =<<

(>=>) :: Bind m => (a -> m i j b) -> (b -> m j k c) -> a -> m i k c
f :: a -> m i j b
f >=> :: (a -> m i j b) -> (b -> m j k c) -> a -> m i k c
>=> g :: b -> m j k c
g = (m i j b -> (b -> m j k c) -> m i k c
forall k (m :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Bind m =>
m i j a -> (a -> m j k b) -> m i k b
>>= b -> m j k c
g) (m i j b -> m i k c) -> (a -> m i j b) -> a -> m i k c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> m i j b
f

(<=<) :: Bind m => (b -> m j k c) -> (a -> m i j b) -> a -> m i k c
<=< :: (b -> m j k c) -> (a -> m i j b) -> a -> m i k c
(<=<) = ((a -> m i j b) -> (b -> m j k c) -> a -> m i k c)
-> (b -> m j k c) -> (a -> m i j b) -> a -> m i k c
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> m i j b) -> (b -> m j k c) -> a -> m i k c
forall k (m :: k -> k -> * -> *) a (i :: k) (j :: k) b (k :: k) c.
Bind m =>
(a -> m i j b) -> (b -> m j k c) -> a -> m i k c
(>=>)

(=<<) :: Bind m => (a -> m j k b) -> m i j a -> m i k b
=<< :: (a -> m j k b) -> m i j a -> m i k b
(=<<) = (m i j a -> (a -> m j k b) -> m i k b)
-> (a -> m j k b) -> m i j a -> m i k b
forall a b c. (a -> b -> c) -> b -> a -> c
flip m i j a -> (a -> m j k b) -> m i k b
forall k (m :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Bind m =>
m i j a -> (a -> m j k b) -> m i k b
(>>=)