module Pandora.Pattern.Functor.Distributive where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Core.Morphism ((%))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Category (identity, (.))

{- |
> Let f :: Distributive g => (a -> g b)

> When providing a new instance, you should ensure it satisfies the two laws:
> * Identity morphism: distribute . distribute ≡ identity
> * Interchange collection: collect f ≡ distribute . comap f
-}

infixl 5 >>-, >>>-, >>>>-, >>>>>-

class Covariant t => Distributive t where
	{-# MINIMAL (>>-) #-}
	-- | Infix and flipped version of 'collect'
	(>>-) :: Covariant u => u a -> (a -> t b) -> t :. u := b

	-- | Prefix version of '>>-'
	collect :: Covariant u => (a -> t b) -> u a -> t :. u := b
	collect a -> t b
f u a
t = u a
t u a -> (a -> t b) -> (t :. u) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- a -> t b
f
	-- | The dual of 'sequence'
	distribute :: Covariant u => u :. t := a -> t :. u := a
	distribute (u :. t) := a
t = (u :. t) := a
t ((u :. t) := a) -> (t a -> t a) -> (t :. u) := a
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- t a -> t a
forall (m :: * -> * -> *) a. Category m => m a a
identity

	-- | Infix versions of `collect` with various nesting levels
	(>>>-) :: (Covariant u, Covariant v)
		=> u :. v := a -> (a -> t b) -> t :. u :. v := b
	(u :. v) := a
x >>>- a -> t b
f = ((v a -> t (v b)) -> ((u :. v) := a) -> (t :. (u :. v)) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
(a -> t b) -> u a -> (t :. u) := b
collect ((v a -> t (v b)) -> ((u :. v) := a) -> (t :. (u :. v)) := b)
-> ((a -> t b) -> v a -> t (v b))
-> (a -> t b)
-> ((u :. v) := a)
-> (t :. (u :. v)) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> t b) -> v a -> t (v b)
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
(a -> t b) -> u a -> (t :. u) := b
collect) a -> t b
f (u :. v) := a
x
	(>>>>-) :: (Covariant u, Covariant v, Covariant w)
		=> u :. v :. w := a -> (a -> t b) -> t :. u :. v :. w := b
	(u :. (v :. w)) := a
x >>>>- a -> t b
f = ((v (w a) -> t (v (w b)))
-> ((u :. (v :. w)) := a) -> (t :. (u :. (v :. w))) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
(a -> t b) -> u a -> (t :. u) := b
collect ((v (w a) -> t (v (w b)))
 -> ((u :. (v :. w)) := a) -> (t :. (u :. (v :. w))) := b)
-> ((a -> t b) -> v (w a) -> t (v (w b)))
-> (a -> t b)
-> ((u :. (v :. w)) := a)
-> (t :. (u :. (v :. w))) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (w a -> t (w b)) -> v (w a) -> t (v (w b))
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
(a -> t b) -> u a -> (t :. u) := b
collect ((w a -> t (w b)) -> v (w a) -> t (v (w b)))
-> ((a -> t b) -> w a -> t (w b))
-> (a -> t b)
-> v (w a)
-> t (v (w b))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> t b) -> w a -> t (w b)
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
(a -> t b) -> u a -> (t :. u) := b
collect) a -> t b
f (u :. (v :. w)) := a
x
	(>>>>>-) :: (Covariant u, Covariant v, Covariant w, Covariant j)
		=> u :. v :. w :. j := a -> (a -> t b) -> t :. u :. v :. w :. j := b
	(u :. (v :. (w :. j))) := a
x >>>>>- a -> t b
f = ((v (w (j a)) -> t (v (w (j b))))
-> ((u :. (v :. (w :. j))) := a)
-> (t :. (u :. (v :. (w :. j)))) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
(a -> t b) -> u a -> (t :. u) := b
collect ((v (w (j a)) -> t (v (w (j b))))
 -> ((u :. (v :. (w :. j))) := a)
 -> (t :. (u :. (v :. (w :. j)))) := b)
-> ((a -> t b) -> v (w (j a)) -> t (v (w (j b))))
-> (a -> t b)
-> ((u :. (v :. (w :. j))) := a)
-> (t :. (u :. (v :. (w :. j)))) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (w (j a) -> t (w (j b))) -> v (w (j a)) -> t (v (w (j b)))
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
(a -> t b) -> u a -> (t :. u) := b
collect ((w (j a) -> t (w (j b))) -> v (w (j a)) -> t (v (w (j b))))
-> ((a -> t b) -> w (j a) -> t (w (j b)))
-> (a -> t b)
-> v (w (j a))
-> t (v (w (j b)))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (j a -> t (j b)) -> w (j a) -> t (w (j b))
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
(a -> t b) -> u a -> (t :. u) := b
collect ((j a -> t (j b)) -> w (j a) -> t (w (j b)))
-> ((a -> t b) -> j a -> t (j b))
-> (a -> t b)
-> w (j a)
-> t (w (j b))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> t b) -> j a -> t (j b)
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
(a -> t b) -> u a -> (t :. u) := b
collect) a -> t b
f (u :. (v :. (w :. j))) := a
x

instance Distributive ((->) e) where
	u a
g >>- :: u a -> (a -> e -> b) -> ((->) e :. u) := b
>>- a -> e -> b
f = \e
e -> (a -> e -> b
f (a -> e -> b) -> e -> a -> b
forall a b c. (a -> b -> c) -> b -> a -> c
% e
e) (a -> b) -> u a -> u b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> u a
g