Open Zemyla opened 8 years ago
Did you mean something like this
newtype WrappedAdj :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
WrapAdj :: u a -> WrappedAdj f u a
deriving Functor
instance Adjunction f u => Distributive (WrappedAdj f u) where
distribute :: Functor g => g (WrappedAdj f u a) -> WrappedAdj f u (g a)
distribute = distributeRep
instance Adjunction f u => Representable (WrappedAdj f u) where
type Rep (WrappedAdj f u) = f ()
index :: WrappedAdj f u a -> (f () -> a)
index (WrapAdj ua) = indexAdjunction ua
tabulate :: (f () -> a) -> WrappedAdj f u a
tabulate f = WrapAdj (tabulateAdjunction f)
data (:!) r b = b :! Rep r deriving (Functor)
newtype Arr r b = Arr (r b) deriving newtype (Functor, Representable)
instance Representable r => Distributive (Arr r) where
distribute :: Functor f => f (Arr r a) -> Arr r (f a)
distribute = distributeRep
instance Representable r => Adjunction ((:!) r) (Arr r) where
unit :: a -> Arr r (r :! a)
unit = Arr . tabulate . (:!)
counit :: r :! Arr r a -> a
counit (xs :! rep) = xs `index` rep
There is an explicit isomorphism for this:
And there should be a newtype wrapper, for instance named
Adj
, that works likeCo
in Data.Functor.Rep, and provides instances for Comonad, instances for Applicative and Monad whenRep u
is a Monoid, etc. Also, there would be an Adjunction betweenAdj f
andCo u
, so thatCo u
has an Adjunction whenever u does.