module Pandora.Pattern.Functor.Traversable where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.Category (identity, (.))
import Pandora.Pattern.Functor.Covariant (Covariant)
import Pandora.Pattern.Functor.Applicative (Applicative)
import Pandora.Pattern.Functor.Pointable (Pointable)

{- |
> Let f :: (Applicative t, Applicative g) => t a -> u a
> Let p :: (Pointable t, Pointable g) => t a -> u a

> When providing a new instance, you should ensure it satisfies the four laws:
> * Numeratority of traversing: g . traverse f ≡ traverse (g . f)
> * Numeratority of sequencing: f . sequence = sequence . comap f
> * Preserving point: p (point x) ≡ point x
> * Preserving apply: f (x <*> y) ≡ f x <*> f y
-}

infixl 3 ->>, ->>>, ->>>>, ->>>>>

class Covariant t => Traversable t where
	{-# MINIMAL (->>) #-}
	-- | Infix version of 'traverse'
	(->>) :: (Pointable u, Applicative u) => t a -> (a -> u b) -> u :. t := b

	-- | Prefix version of '->>'
	traverse :: (Pointable u, Applicative u) => (a -> u b) -> t a -> u :. t := b
	traverse a -> u b
f t a
t = t a
t t a -> (a -> u b) -> (u :. t) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f
	-- | The dual of 'distribute'
	sequence :: (Pointable u, Applicative u) => t :. u := a -> u :. t := a
	sequence (t :. u) := a
t = (t :. u) := a
t ((t :. u) := a) -> (u a -> u a) -> (u :. t) := a
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> u a -> u a
forall (m :: * -> * -> *) a. Category m => m a a
identity

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