Nucleus of a profunctor

nucleus.hs

{-# LANGUAGE
    PolyKinds
  , RankNTypes
  , TypeFamilies
  , TypeOperators
  , TypeApplications
  , FlexibleInstances
  , ScopedTypeVariables
  , AllowAmbiguousTypes
  , MultiParamTypeClasses
  , StandaloneKindSignatures
  #-}

import Data.Functor.Contravariant
import qualified Data.Functor.Contravariant.Rep as Co
import Data.Functor.Rep
import Data.Profunctor
import Data.Kind (Type)

type C2F :: (a_op -> b -> Type) -> (a_op -> Type) -> (b -> Type)
type F2C :: (a_op -> b -> Type) -> (b -> Type) -> (a_op -> Type)
newtype C2F p f b = C2F { unC2F :: forall a. f a -> p a b }
newtype F2C p f a = F2C { unF2C :: forall b. f b -> p a b }

instance Profunctor p => Functor (C2F p f) where
  fmap f (C2F n) = C2F (rmap f . n)
instance Profunctor p => Contravariant (F2C p f) where
  contramap f (F2C n) = F2C (lmap f . n)

type f ~> g = forall a. f a -> g a

mapC2F :: (g ~> f) -> C2F p f ~> C2F p g
mapC2F f (C2F n) = C2F (n . f)
mapF2C :: (g ~> f) -> F2C p f ~> F2C p g
mapF2C f (F2C n) = F2C (n . f)

-- Adjunction between C2F and F2C
adjunctF :: (g ~> F2C p f) -> (f ~> C2F p g)
adjunctF n fb = C2F $ (`unF2C` fb) . n
adjunctC :: (g ~> C2F p f) -> (f ~> F2C p g)
adjunctC n fa = F2C $ \gb -> unC2F (n gb) fa
unitF :: forall p f. f ~> C2F p (F2C p f)
unitF = adjunctF id
unitC :: forall p f. f ~> F2C p (C2F p f)
unitC = adjunctC id

class (Profunctor p, Functor f) => IsInNucleusF p f where
  isInNucleusF :: C2F p (F2C p f) ~> f

class (Profunctor p, Contravariant f) => IsInNucleusC p f where
  isInNucleusC :: F2C p (C2F p f) ~> f

defaultFmap :: forall p f a b. IsInNucleusF p f => (a -> b) -> f a -> f b
defaultFmap f = isInNucleusF @p . fmap f . unitF @p

defaultContramap :: forall p f a b. IsInNucleusC p f => (a -> b) -> f b -> f a
defaultContramap f = isInNucleusC @p . contramap f . unitC @p

instance Profunctor p => IsInNucleusF p (C2F p f) where
  isInNucleusF (C2F n) = C2F $ \fa -> n (unitC fa)

instance Profunctor p => IsInNucleusC p (F2C p f) where
  isInNucleusC (F2C n) = F2C $ \fb -> n (unitF fb)

instance Representable f => IsInNucleusF (->) f where
  isInNucleusF (C2F n) = tabulate (n (F2C index))

instance Co.Representable f => IsInNucleusC (->) f where
  isInNucleusC (F2C n) = Co.tabulate (n (C2F Co.index))

-- NucleusF p = C2F p (NucleusC p) = FixH (C2F p :.: F2C p)
newtype NucleusF p b = NucleusF (forall a. NucleusC p a -> p a b)
instance Profunctor p => Functor (NucleusF p) where
  fmap f (NucleusF g) = NucleusF $ \h -> rmap f (g h)
instance Profunctor p => IsInNucleusF p (NucleusF p) where
  isInNucleusF (C2F n) = NucleusF $ \(NucleusC h) -> n (F2C h)

-- NucleusC p = F2C p (NucleusF p) = FixH (F2C p :.: C2F p)
newtype NucleusC p a = NucleusC (forall b. NucleusF p b -> p a b)
instance Profunctor p => Contravariant (NucleusC p) where
  contramap f (NucleusC g) = NucleusC $ \h -> lmap f (g h)
instance Profunctor p => IsInNucleusC p (NucleusC p) where
  isInNucleusC (F2C n) = NucleusC $ \(NucleusF h) -> n (C2F h)