{-# LANGUAGE AllowAmbiguousTypes #-}

module Pandora.Pattern.Functor.Covariant where

import Pandora.Pattern.Betwixt (Betwixt)
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 target t u a b
	. (Covariant source (Betwixt source target) u, Covariant (Betwixt source target) 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 = (Betwixt source target (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 -> Betwixt source target (u a) (u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) @source @(Betwixt source target) @u source a b
s))

(<-|-|-|-) :: forall source target t u v a b
	. (Covariant source (Betwixt source (Betwixt source target)) v, Covariant (Betwixt source (Betwixt source target)) (Betwixt (Betwixt source target) target) u, Covariant (Betwixt (Betwixt source target) target) 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 = (Betwixt (Betwixt source target) target (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)
(<-|-) @(Betwixt (Betwixt source target) target) @target (Betwixt source (Betwixt source target) (v a) (v b)
-> Betwixt (Betwixt source target) target (u (v a)) (u (v b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) @(Betwixt source (Betwixt source target)) @(Betwixt (Betwixt source target) target) @u (source a b -> Betwixt source (Betwixt source target) (v a) (v b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) @source @(Betwixt source (Betwixt source target)) @v source a b
s)))

(<$>) :: Covariant source target t => source a b -> target (t a) (t b)
<$> :: source a b -> target (t a) (t b)
(<$>) = source a b -> target (t a) (t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-)

(<$$>) :: (Covariant source (Betwixt source target) u, Covariant (Betwixt source target) 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 -> target (t (u a)) (t (u b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
(<-|-|-)

(<$$$>) :: forall source target t u v a b
	. (Covariant source (Betwixt source (Betwixt source target)) v, Covariant (Betwixt source (Betwixt source target)) (Betwixt (Betwixt source target) target) u, Covariant (Betwixt (Betwixt source target) target) 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 = source a b -> target (t (u (v a))) (t (u (v b)))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) (v :: * -> *) a b.
(Covariant source (Betwixt source (Betwixt source target)) v,
 Covariant
   (Betwixt source (Betwixt source target))
   (Betwixt (Betwixt source target) target)
   u,
 Covariant (Betwixt (Betwixt source target) target) target t) =>
source a b -> target (t (u (v a))) (t (u (v b)))
(<-|-|-|-) source a b
s