{-# LANGUAGE AllowAmbiguousTypes #-}

module Pandora.Pattern.Functor.Covariant where

import Pandora.Pattern.Semigroupoid (Semigroupoid)

infixl 4 <$>
infixl 3 <$$>
infixl 4 <$$$>

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

class (Semigroupoid source, Semigroupoid target) => Covariant source target t where
	(<$>) :: source a b -> target (t a) (t b)

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

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

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