module Pandora.Pattern.Functor.Covariant where

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

infixl 4 <$>, -<$>-, <$, $>
infixl 3 <$$>, -<<$$>-, -<$$>>-
infixl 2 <$$$>
infixl 1 <$$$$>

infixl 1 <&>
infixl 2 <&&>
infixl 3 <&&&>
infixl 4 <&&&&>

infixr 7 .#.., .#..., .#....

{- |
> When providing a new instance, you should ensure it satisfies:
> * Identity morphism: comap identity ≡ identity
> * Interpreted of morphisms: comap (f . g) ≡ comap f . comap g
-}

class Covariant (t :: * -> *) where
	{-# MINIMAL (<$>) #-}
	-- | Infix version of 'comap'
	(<$>) :: (a -> b) -> t a -> t b

	-- | Prefix version of '<$>'
	comap :: (a -> b) -> t a -> t b
	comap a -> b
f t a
x = a -> b
f (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t a
x
	-- | Replace all locations in the input with the same value
	(<$) :: a -> t b -> t a
	a
x <$ t b
z = (\b
_-> a
x) (b -> a) -> t b -> t a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t b
z
	-- | Flipped version of '<$'
	($>) :: t a -> b -> t b
	t a
x $> b
v = b
v b -> t a -> t b
forall (t :: * -> *) a b. Covariant t => a -> t b -> t a
<$ t a
x
	-- | Discards the result of evaluation
	void :: t a -> t ()
	void t a
x = () () -> t a -> t ()
forall (t :: * -> *) a b. Covariant t => a -> t b -> t a
<$ t a
x
	-- | Computing a value from a structure of values
	loeb :: t (a <:= t) -> t a
	loeb t (a <:= t)
tt = let fix :: (t -> t) -> t
fix t -> t
f = let x :: t
x = t -> t
f t
x in t
x in (t a -> t a) -> t a
forall t. (t -> t) -> t
fix (\t a
f -> (\a <:= t
g -> a <:= t
g t a
f) ((a <:= t) -> a) -> t (a <:= t) -> t a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t (a <:= t)
tt)
	-- | Flipped infix version of 'comap'
	(<&>) :: t a -> (a -> b) -> t b
	t a
x <&> a -> b
f = a -> b
f (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t a
x

	-- | Infix versions of `comap` with various nesting levels
	(<$$>) :: Covariant u => (a -> b) -> t :. u := a -> t :. u := b
	a -> b
f <$$> (t :. u) := a
x = ((a -> b
f (a -> b) -> u a -> u b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (u a -> u b) -> ((t :. u) := a) -> (t :. u) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (t :. u) := a
x
	(<$$$>) :: (Covariant u, Covariant v)
		=> (a -> b) -> t :. u :. v := a -> t :. u :. v := b
	a -> b
f <$$$> (t :. (u :. v)) := a
x = (((a -> b
f (a -> b) -> v a -> v b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (v a -> v b) -> u (v a) -> u (v b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (u (v a) -> u (v b))
-> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (t :. (u :. v)) := a
x
	(<$$$$>) :: (Covariant u, Covariant v, Covariant w)
		=> (a -> b) -> t :. u :. v :. w := a -> t :. u :. v :. w := b
	a -> b
f <$$$$> (t :. (u :. (v :. w))) := a
x = ((((a -> b
f (a -> b) -> w a -> w b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (w a -> w b) -> v (w a) -> v (w b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (v (w a) -> v (w b)) -> u (v (w a)) -> u (v (w b))
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (u (v (w a)) -> u (v (w b)))
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (t :. (u :. (v :. w))) := a
x

	-- | Infix flipped versions of `comap` with various nesting levels
	(<&&>) :: Covariant u => t :. u := a -> (a -> b) -> t :. u := b
	(t :. u) := a
x <&&> a -> b
f = a -> b
f (a -> b) -> ((t :. u) := a) -> (t :. u) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> (t :. u) := a
x
	(<&&&>) :: (Covariant u, Covariant v)
		=> t :. u :. v := a -> (a -> b) -> t :. u :. v := b
	(t :. (u :. v)) := a
x <&&&> a -> b
f = a -> b
f (a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b.
(Covariant t, Covariant u, Covariant v) =>
(a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
<$$$> (t :. (u :. v)) := a
x
	(<&&&&>) :: (Covariant u, Covariant v, Covariant w)
		=> t :. u :. v :. w := a -> (a -> b) -> t :. u :. v :. w := b
	(t :. (u :. (v :. w))) := a
x <&&&&> a -> b
f = a -> b
f (a -> b)
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) (w :: * -> *) a b.
(Covariant t, Covariant u, Covariant v, Covariant w) =>
(a -> b)
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
<$$$$> (t :. (u :. (v :. w))) := a
x

	(.#..) :: (t ~ v a, Category v)
		=> v c d -> v a :. v b := c -> v a :. v b := d
	v c d
f .#.. (v a :. v b) := c
g = (v c d
f v c d -> v b c -> v b d
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
.) (v b c -> v b d) -> ((v a :. v b) := c) -> (v a :. v b) := d
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (v a :. v b) := c
g

	(.#...) :: (t ~ v a, t ~ v b, Category v, Covariant (v a), Covariant (v b))
		=> v d e -> v a :. v b :. v c := d -> v a :. v b :. v c := e
	v d e
f .#... (v a :. (v b :. v c)) := d
g = (v d e
f v d e -> v c d -> v c e
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
.) (v c d -> v c e)
-> ((v a :. (v b :. v c)) := d) -> (v a :. (v b :. v c)) := e
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> (v a :. (v b :. v c)) := d
g

	(.#....) :: (t ~ v a, t ~ v b, t ~ v c, Category v, Covariant (v a), Covariant (v b), Covariant (v c))
		=> v e f -> v a :. v b :. v c :. v d := e -> v a :. v b :. v c :. v d := f
	v e f
f .#.... (v a :. (v b :. (v c :. v d))) := e
g = (v e f
f v e f -> v d e -> v d f
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
.) (v d e -> v d f)
-> ((v a :. (v b :. (v c :. v d))) := e)
-> (v a :. (v b :. (v c :. v d))) := f
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b.
(Covariant t, Covariant u, Covariant v) =>
(a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
<$$$> (v a :. (v b :. (v c :. v d))) := e
g

	(<$$) :: Covariant u => b -> t :. u := a -> t :. u := b
	b
x <$$ (t :. u) := a
s = (\a
_-> b
x) (a -> b) -> ((t :. u) := a) -> (t :. u) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> (t :. u) := a
s

	(<$$$) :: (Covariant u, Covariant v) => b -> t :. u :. v := a -> t :. u :. v := b
	b
x <$$$ (t :. (u :. v)) := a
s = (\a
_-> b
x) (a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b.
(Covariant t, Covariant u, Covariant v) =>
(a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
<$$$> (t :. (u :. v)) := a
s

	(<$$$$) :: (Covariant u, Covariant v, Covariant w) => b -> t :. u :. v :. w := a -> t :. u :. v :. w := b
	b
x <$$$$ (t :. (u :. (v :. w))) := a
s = (\a
_-> b
x) (a -> b)
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) (w :: * -> *) a b.
(Covariant t, Covariant u, Covariant v, Covariant w) =>
(a -> b)
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
<$$$$> (t :. (u :. (v :. w))) := a
s

	($$>) :: Covariant u => t :. u := a -> b -> t :. u := b
	(t :. u) := a
s $$> b
x = (\a
_-> b
x) (a -> b) -> ((t :. u) := a) -> (t :. u) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> (t :. u) := a
s

	($$$>) :: (Covariant u, Covariant v) => t :. u :. v := a -> b -> t :. u :. v := b
	(t :. (u :. v)) := a
s $$$> b
x = (\a
_-> b
x) (a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b.
(Covariant t, Covariant u, Covariant v) =>
(a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
<$$$> (t :. (u :. v)) := a
s

	($$$$>) :: (Covariant u, Covariant v, Covariant w) => t :. u :. v :. w := a -> b -> t :. u :. v :. w := b
	(t :. (u :. (v :. w))) := a
s $$$$> b
x = (\a
_-> b
x) (a -> b)
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) (w :: * -> *) a b.
(Covariant t, Covariant u, Covariant v, Covariant w) =>
(a -> b)
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
<$$$$> (t :. (u :. (v :. w))) := a
s

class (Category source, Category target) => Covariant_ t source target where
	(-<$>-) :: source a b -> target (t a) (t b)
	
(-<$$>-) :: forall t u category a b 
	. (Covariant_ u category category, Covariant_ t category category) 
	=> category a b -> category (t (u a)) (t (u b))
-<$$>- :: category a b -> category (t (u a)) (t (u b))
(-<$$>-) category a b
s = (category (u a) (u b) -> category (t (u a)) (t (u b))
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
(-<$>-) (category a b -> category (u a) (u b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
(-<$>-) @u @category @category category a b
s))

(-<<$$>-) :: forall t u source target a b 
	. (Covariant_ u source source, Covariant_ t source target) 
	=> source a b -> target (t (u a)) (t (u b))
-<<$$>- :: source a b -> target (t (u a)) (t (u b))
(-<<$$>-) source a b
s = (source (u a) (u b) -> target (t (u a)) (t (u b))
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
(-<$>-) (source a b -> source (u a) (u b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
(-<$>-) @u @source @source source a b
s))

(-<$$>>-) :: forall t u source target a b 
	. (Covariant_ u source target, Covariant_ t target target) 
	=> source a b -> target (t (u a)) (t (u b))
-<$$>>- :: source a b -> target (t (u a)) (t (u b))
(-<$$>>-) source a b
s = (target (u a) (u b) -> target (t (u a)) (t (u b))
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
(-<$>-) (source a b -> target (u a) (u b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
(-<$>-) @u @source @target source a b
s))

-- TODO: Figure out how to work with hidden type variables
-- to put intermediate category `between`
(-<$$$>-) :: forall t u v source target a b
	. (Covariant_ u source source, Covariant_ t source target, Covariant_ v target target) 
	=> source a b -> target (v (t (u a))) (v (t (u b)))
-<$$$>- :: source a b -> target (v (t (u a))) (v (t (u b)))
(-<$$$>-) source a b
s = (target (t (u a)) (t (u b)) -> target (v (t (u a))) (v (t (u b)))
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
(-<$>-) (source (u a) (u b) -> target (t (u a)) (t (u b))
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
(-<$>-) @t @source @target (source a b -> source (u a) (u b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
(-<$>-) @u @source @source source a b
s)))