module Pandora.Pattern.Functor.Covariant where

import Pandora.Pattern.Semigroupoid (Semigroupoid)

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

-- TODO: use -<$>- instead of comap here
{- |
> 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 (Semigroupoid source, Semigroupoid 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 category a b
	. (Covariant t category category, Covariant u category category, Covariant v category category) 
	=> category a b -> category (t (u (v a))) (t (u (v b)))
-<$$$>- :: category a b -> category (t (u (v a))) (t (u (v b)))
(-<$$$>-) category a b
s = (category (u (v a)) (u (v b))
-> category (t (u (v a))) (t (u (v b)))
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
(-<$>-) @t @category @category (category (v a) (v b) -> category (u (v a)) (u (v 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 -> category (v a) (v b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
(-<$>-) @v @category @category category a b
s)))

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