{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Controlflow.Effect.Transformer.Comonadic (Comonadic (..), (:<) (..)) where

import Pandora.Core.Functor (type (~>))
import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Applicative (Applicative ((<*>)))
import Pandora.Pattern.Functor.Alternative (Alternative ((<+>)))
import Pandora.Pattern.Functor.Distributive (Distributive ((>>-)))
import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
import Pandora.Pattern.Functor.Bindable (Bindable ((>>=)))
import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable (hoist))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Schematic, Interpreted (Primary, run, unite))

class Interpreted t => Comonadic t where
	{-# MINIMAL bring #-}
	bring :: Extractable u => t :< u ~> t

infixr 3 :<
newtype (:<) t u a = TC { (:<) t u a -> Schematic Comonad t u a
tc :: Schematic Comonad t u a }

instance Covariant (Schematic Comonad t u) => Covariant (t :< u) where
	a -> b
f <$> :: (a -> b) -> (:<) t u a -> (:<) t u b
<$> TC Schematic Comonad t u a
x = Schematic Comonad t u b -> (:<) t u b
forall (t :: * -> *) (u :: * -> *) a.
Schematic Comonad t u a -> (:<) t u a
TC (Schematic Comonad t u b -> (:<) t u b)
-> Schematic Comonad t u b -> (:<) t u b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a -> b
f (a -> b) -> Schematic Comonad t u a -> Schematic Comonad t u b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Schematic Comonad t u a
x

instance Pointable (Schematic Comonad t u) => Pointable (t :< u) where
	point :: a |-> (t :< u)
point = Schematic Comonad t u a -> (:<) t u a
forall (t :: * -> *) (u :: * -> *) a.
Schematic Comonad t u a -> (:<) t u a
TC (Schematic Comonad t u a -> (:<) t u a)
-> (a -> Schematic Comonad t u a) -> a |-> (t :< u)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Schematic Comonad t u a
forall (t :: * -> *) a. Pointable t => a |-> t
point

instance Extractable (Schematic Comonad t u) => Extractable (t :< u) where
	extract :: a <-| (t :< u)
extract = a <-| Schematic Comonad t u
forall (t :: * -> *) a. Extractable t => a <-| t
extract (a <-| Schematic Comonad t u)
-> ((:<) t u a -> Schematic Comonad t u a) -> a <-| (t :< u)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (:<) t u a -> Schematic Comonad t u a
forall (t :: * -> *) (u :: * -> *) a.
(:<) t u a -> Schematic Comonad t u a
tc

instance Applicative (Schematic Comonad t u) => Applicative (t :< u) where
	TC Schematic Comonad t u (a -> b)
f <*> :: (:<) t u (a -> b) -> (:<) t u a -> (:<) t u b
<*> TC Schematic Comonad t u a
x = Schematic Comonad t u b -> (:<) t u b
forall (t :: * -> *) (u :: * -> *) a.
Schematic Comonad t u a -> (:<) t u a
TC (Schematic Comonad t u b -> (:<) t u b)
-> Schematic Comonad t u b -> (:<) t u b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Schematic Comonad t u (a -> b)
f Schematic Comonad t u (a -> b)
-> Schematic Comonad t u a -> Schematic Comonad t u b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> Schematic Comonad t u a
x

instance Alternative (Schematic Comonad t u) => Alternative (t :< u) where
	TC Schematic Comonad t u a
x <+> :: (:<) t u a -> (:<) t u a -> (:<) t u a
<+> TC Schematic Comonad t u a
y = Schematic Comonad t u a -> (:<) t u a
forall (t :: * -> *) (u :: * -> *) a.
Schematic Comonad t u a -> (:<) t u a
TC (Schematic Comonad t u a -> (:<) t u a)
-> Schematic Comonad t u a -> (:<) t u a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Schematic Comonad t u a
x Schematic Comonad t u a
-> Schematic Comonad t u a -> Schematic Comonad t u a
forall (t :: * -> *) a. Alternative t => t a -> t a -> t a
<+> Schematic Comonad t u a
y

instance Traversable (Schematic Comonad t u) => Traversable (t :< u) where
	TC Schematic Comonad t u a
x ->> :: (:<) t u a -> (a -> u b) -> (u :. (t :< u)) := b
->> a -> u b
f = Schematic Comonad t u b -> (:<) t u b
forall (t :: * -> *) (u :: * -> *) a.
Schematic Comonad t u a -> (:<) t u a
TC (Schematic Comonad t u b -> (:<) t u b)
-> u (Schematic Comonad t u b) -> (u :. (t :< u)) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (Schematic Comonad t u a
x Schematic Comonad t u a
-> (a -> u b) -> u (Schematic Comonad t u b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f)

instance Distributive (Schematic Comonad t u) => Distributive (t :< u) where
	u a
x >>- :: u a -> (a -> (:<) t u b) -> ((t :< u) :. u) := b
>>- a -> (:<) t u b
f = Schematic Comonad t u (u b) -> ((t :< u) :. u) := b
forall (t :: * -> *) (u :: * -> *) a.
Schematic Comonad t u a -> (:<) t u a
TC (Schematic Comonad t u (u b) -> ((t :< u) :. u) := b)
-> Schematic Comonad t u (u b) -> ((t :< u) :. u) := b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ u a
x u a
-> (a -> Schematic Comonad t u b) -> Schematic Comonad t u (u b)
forall (t :: * -> *) (u :: * -> *) a b.
(Distributive t, Covariant u) =>
u a -> (a -> t b) -> (t :. u) := b
>>- (:<) t u b -> Schematic Comonad t u b
forall (t :: * -> *) (u :: * -> *) a.
(:<) t u a -> Schematic Comonad t u a
tc ((:<) t u b -> Schematic Comonad t u b)
-> (a -> (:<) t u b) -> a -> Schematic Comonad t u b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> (:<) t u b
f

instance Bindable (Schematic Comonad t u) => Bindable (t :< u) where
	TC Schematic Comonad t u a
x >>= :: (:<) t u a -> (a -> (:<) t u b) -> (:<) t u b
>>= a -> (:<) t u b
f = Schematic Comonad t u b -> (:<) t u b
forall (t :: * -> *) (u :: * -> *) a.
Schematic Comonad t u a -> (:<) t u a
TC (Schematic Comonad t u b -> (:<) t u b)
-> Schematic Comonad t u b -> (:<) t u b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Schematic Comonad t u a
x Schematic Comonad t u a
-> (a -> Schematic Comonad t u b) -> Schematic Comonad t u b
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= (:<) t u b -> Schematic Comonad t u b
forall (t :: * -> *) (u :: * -> *) a.
(:<) t u a -> Schematic Comonad t u a
tc ((:<) t u b -> Schematic Comonad t u b)
-> (a -> (:<) t u b) -> a -> Schematic Comonad t u b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> (:<) t u b
f

instance Extendable (Schematic Comonad t u) => Extendable (t :< u) where
	TC Schematic Comonad t u a
x =>> :: (:<) t u a -> ((:<) t u a -> b) -> (:<) t u b
=>> (:<) t u a -> b
f = Schematic Comonad t u b -> (:<) t u b
forall (t :: * -> *) (u :: * -> *) a.
Schematic Comonad t u a -> (:<) t u a
TC (Schematic Comonad t u b -> (:<) t u b)
-> Schematic Comonad t u b -> (:<) t u b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Schematic Comonad t u a
x Schematic Comonad t u a
-> (Schematic Comonad t u a -> b) -> Schematic Comonad t u b
forall (t :: * -> *) a b. Extendable t => t a -> (t a -> b) -> t b
=>> (:<) t u a -> b
f ((:<) t u a -> b)
-> (Schematic Comonad t u a -> (:<) t u a)
-> Schematic Comonad t u a
-> b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Schematic Comonad t u a -> (:<) t u a
forall (t :: * -> *) (u :: * -> *) a.
Schematic Comonad t u a -> (:<) t u a
TC

instance (Extractable (t :< u), Extendable (t :< u)) => Comonad (t :< u) where

instance Lowerable (Schematic Comonad t) => Lowerable ((:<) t) where
	lower :: (t :< u) ~> u
lower (TC Schematic Comonad t u a
x) = Schematic Comonad t u a -> u a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower Schematic Comonad t u a
x

instance Hoistable (Schematic Comonad t) => Hoistable ((:<) t) where
	hoist :: (u ~> v) -> (t :< u) ~> (t :< v)
hoist u ~> v
f (TC Schematic Comonad t u a
x) = Schematic Comonad t v a -> (:<) t v a
forall (t :: * -> *) (u :: * -> *) a.
Schematic Comonad t u a -> (:<) t u a
TC (Schematic Comonad t v a -> (:<) t v a)
-> Schematic Comonad t v a -> (:<) t v a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (u ~> v) -> Schematic Comonad t u a -> Schematic Comonad t v a
forall k (t :: (* -> *) -> k -> *) (u :: * -> *) (v :: * -> *).
(Hoistable t, Covariant u) =>
(u ~> v) -> t u ~> t v
hoist u ~> v
f Schematic Comonad t u a
x

instance (Interpreted (Schematic Comonad t u)) => Interpreted (t :< u) where
	type Primary (t :< u) a = Primary (Schematic Comonad t u) a
	run :: (:<) t u a -> Primary (t :< u) a
run ~(TC Schematic Comonad t u a
x) = Schematic Comonad t u a -> Primary (Schematic Comonad t u) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Schematic Comonad t u a
x
	unite :: Primary (t :< u) a -> (:<) t u a
unite = Schematic Comonad t u a -> (:<) t u a
forall (t :: * -> *) (u :: * -> *) a.
Schematic Comonad t u a -> (:<) t u a
TC (Schematic Comonad t u a -> (:<) t u a)
-> (Primary (Schematic Comonad t u) a -> Schematic Comonad t u a)
-> Primary (Schematic Comonad t u) a
-> (:<) t u a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Primary (Schematic Comonad t u) a -> Schematic Comonad t u a
forall (t :: * -> *) a. Interpreted t => Primary t a -> t a
unite