{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Controlflow.Effect.Adaptable where

import Pandora.Core.Functor (type (>), type (>>>), type (<))
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Category (Category (identity))
import Pandora.Pattern.Functor.Covariant (Covariant)
import Pandora.Pattern.Functor.Monoidal (Monoidal)
import Pandora.Pattern.Transformer (Liftable (lift))
import Pandora.Paradigm.Algebraic.Exponential (type (-->))
import Pandora.Paradigm.Algebraic.Product ((:*:))
import Pandora.Paradigm.Algebraic (Pointable, extract, point)
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly)
import Pandora.Paradigm.Controlflow.Effect.Transformer (Monadic, wrap, (:>))

class Adaptable u m t where
	{-# MINIMAL adapt #-}
	adapt :: m < t a < u a

instance Category m => Adaptable t m t where
	adapt :: (m < t a) < t a
adapt = forall a. Category m => m a a
forall (m :: * -> * -> *) a. Category m => m a a
identity @m

class Effectful m v t u where
	effect :: m (v a) (t :> u >>> a)

instance (Pointable u, Monadic m t) => Effectful m t t u where
	effect :: m (t a) ((t :> u) >>> a)
effect = m (t a) ((t :> u) >>> a)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a.
(Monadic m t, Pointable u) =>
(m < t a) < (:>) t u a
wrap

instance (Covariant m m u, Liftable m ((:>) t)) => Effectful m u t u where
	effect :: m (u a) ((t :> u) >>> a)
effect = m (u a) ((t :> u) >>> a)
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift

instance {-# OVERLAPS #-} (Semigroupoid m, Effectful m u t u, Adaptable u m v) => Effectful m v t u where
	effect :: m (v a) ((t :> u) >>> a)
effect = forall a. Effectful m u t u => m (u a) ((t :> u) >>> a)
forall k (m :: k -> * -> *) (v :: * -> k) (t :: * -> *)
       (u :: * -> *) a.
Effectful m v t u =>
m (v a) ((t :> u) >>> a)
effect @m @u @t @u m (u a) ((t :> u) >>> a)
-> m (v a) (u a) -> m (v a) ((t :> u) >>> a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a. Adaptable u m v => (m < v a) < u a
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt @u @m @v

instance Effectful m v t u => Adaptable (t :> u) m v where
	adapt :: (m < v a) < (:>) t u a
adapt = forall a. Effectful m v t u => (m < v a) < (:>) t u a
forall k (m :: k -> * -> *) (v :: * -> k) (t :: * -> *)
       (u :: * -> *) a.
Effectful m v t u =>
m (v a) ((t :> u) >>> a)
effect @m @v @t @u