module Control.Joint.Schemes.TUT where

import "adjunctions" Data.Functor.Adjunction (Adjunction (leftAdjunct))
import "distributive" Data.Distributive (Distributive (collect))
import "transformers" Control.Monad.Trans.Class (MonadTrans (lift))

import Control.Joint.Core (type (:.), type (:=))
import Control.Joint.Abilities.Interpreted (Interpreted (Primary, run))

newtype TUT t t' u a = TUT (t :. u :. t' := a)

type (<:<.>:>) = TUT

instance Interpreted (TUT t t' u) where
	type Primary (TUT t t' u) a = t :. u :. t' := a
	run :: TUT t t' u a -> Primary (TUT t t' u) a
run (TUT (t :. (u :. t')) := a
x) = (t :. (u :. t')) := a
Primary (TUT t t' u) a
x

instance (Adjunction t' t, Distributive t) => MonadTrans (TUT t t') where
	lift :: m a -> TUT t t' m a
lift = ((t :. (m :. t')) := a) -> TUT t t' m a
forall k k k (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k).
((t :. (u :. t')) := a) -> TUT t t' u a
TUT (((t :. (m :. t')) := a) -> TUT t t' m a)
-> (m a -> (t :. (m :. t')) := a) -> m a -> TUT t t' m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> t (t' a)) -> m a -> (t :. (m :. t')) := a
forall (g :: * -> *) (f :: * -> *) a b.
(Distributive g, Functor f) =>
(a -> g b) -> f a -> g (f b)
collect ((t' a -> t' a) -> a -> t (t' a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct t' a -> t' a
forall a. a -> a
id)