module Pandora.Pattern.Functor.Distributive where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.Functor.Covariant (Covariant)

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

> When providing a new instance, you should ensure it satisfies:
> * 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
x -> t a
x)

	-- | 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 = (u :. v) := a
x ((u :. v) := a) -> (v a -> t (v b)) -> (t :. (u :. v)) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- (v a -> (a -> t b) -> t (v b)
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- a -> t b
f)
	(>>>>-) :: (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 = (u :. (v :. w)) := a
x ((u :. (v :. w)) := a)
-> ((:.) v w a -> t (v (w b))) -> (t :. (u :. (v :. w))) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- ((:.) v w a -> (w a -> t (w b)) -> t (v (w b))
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- (w a -> (a -> t b) -> t (w b)
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- a -> t b
f))
	(>>>>>-) :: (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 = (u :. (v :. (w :. j))) := a
x ((u :. (v :. (w :. j))) := a)
-> ((:.) v (w :. j) a -> t (v (w (j b))))
-> (t :. (u :. (v :. (w :. j)))) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- ((:.) v (w :. j) a -> ((:.) w j a -> t (w (j b))) -> t (v (w (j b)))
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- ((:.) w j a -> (j a -> t (j b)) -> t (w (j b))
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- (j a -> (a -> t b) -> t (j b)
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- a -> t b
f)))