All types from the kan-extensions package are special cases of Procompose, Rift and Ran from the profunctors package.

Rift.hs

{-# LANGUAGE StandaloneKindSignatures, GADTs, DataKinds, PolyKinds, RankNTypes, TypeOperators #-}
module Rift where

import Data.Bifunctor.Clown
import Data.Bifunctor.Joker
import Data.Profunctor
import Data.Profunctor.Cayley
import Data.Profunctor.Composition
import Data.Profunctor.Ran
import Data.Kind (Type)
import Data.Functor.Identity
import Data.Functor.Contravariant

type RiftF :: (k1 -> k2 -> Type) -> (k2 -> Type) -> (k1 -> Type)
type RiftF p f = CoJoker (Rift p (Joker f))
type Ran' j f = RiftF (Star j) f
type Yoneda f = Ran' Identity f
type Codensity m = Ran' m m
type CoT w m = RiftF (Cayley w (Star m)) m
type Curried j f = RiftF (Cayley j (->)) f

type ComposeF :: (k1 -> k2 -> Type) -> (k1 -> Type) -> (k2 -> Type)
type ComposeF p f = CoJoker (Procompose p (Joker f))
type Lan j f = ComposeF (Costar j) f
type Coyoneda f = Lan Identity f
type Density w = Lan w w
type Day f1 f2 = Lan K2 (F2 f1 f2)


riftLaw :: (Procompose p q :-> r) -> q :-> Rift p r
riftLaw n q = Rift $ \p -> n (Procompose p q)

runRiftF :: RiftF p f a -> p a b -> f b
runRiftF = (runJoker .) . runRift . runCoJoker

riftFLaw :: (forall x y. p x y -> g x -> f y) -> g a -> RiftF p f a
riftFLaw n = CoJoker . riftLaw (\(Procompose p g) -> Joker . n p . runJoker $ g) . Joker

runRan' :: Ran' j f a -> (a -> j b) -> f b
runRan' r = runRiftF r . Star

ran'Law :: Functor g => (forall x. g (j x) -> f x) -> g a -> Ran' j f a
ran'Law n = riftFLaw (\(Star j) -> n . fmap j)

runYoneda :: Yoneda f a -> (a -> b) -> f b
runYoneda y = runRan' y . (Identity .)

yonedaLaw :: Functor f => f a -> Yoneda f a
yonedaLaw = ran'Law (fmap runIdentity)

runCoT :: Functor w => CoT w m a -> w (a -> m r) -> m r
runCoT r = runRiftF r . Cayley . fmap Star

coTLaw :: Functor w => (forall x y. w (x -> m y) -> g x -> m y) -> g a -> CoT w m a
coTLaw n = riftFLaw (\(Cayley w) -> n (runStar <$> w))

runCurried :: Curried j f a -> j (a -> r) -> f r
runCurried r = runRiftF r . Cayley

curriedLaw :: (forall x y. j (y -> x) -> g y -> f x) -> g a -> Curried j f a
curriedLaw n = riftFLaw (n . runCayley)


composeRiftLaw :: (q :-> Rift p r) -> Procompose p q :-> r
composeRiftLaw n (Procompose p q) = runRift (n q) p

composeF :: p a b -> f a -> ComposeF p f b
composeF p = CoJoker . Procompose p . Joker

composeFLaw :: (forall x y. p x y -> f x -> g y) -> ComposeF p f a -> g a
composeFLaw n = runJoker . composeRiftLaw (\f -> Rift $ \p -> Joker . n p . runJoker $ f) . runCoJoker

lan :: (j a -> b) -> f a -> Lan j f b
lan = composeF . Costar

lanLaw :: Functor g => (forall x. f x -> g (j x)) -> Lan j f a -> g a
lanLaw n = composeFLaw (\(Costar j) -> fmap j . n)

coyoneda :: (a -> b) -> f a -> Coyoneda f b
coyoneda = lan . (. runIdentity)

coyonedaLaw :: Functor f => Coyoneda f a -> f a
coyonedaLaw = lanLaw (fmap Identity)

day :: f1 a1 -> f2 a2 -> (a1 -> a2 -> b) -> Day f1 f2 b
day f1 f2 ab = lan (uncurry ab . unK2) (F2 f1 f2)

dayLaw :: Functor g => (forall x1 x2. f1 x1 -> f2 x2 -> g (x1, x2)) -> Day f1 f2 a -> g a
dayLaw n = lanLaw (\(F2 f1 f2) -> uncurry K2 <$> n f1 f2)


type RanC :: (k1 -> k2 -> Type) -> (k1 -> Type) -> (k2 -> Type)
type RanC p f = CoClown (Ran p (Clown f))
type ContraRan j f = RanC (Costar j) f
type ContraYoneda f = ContraRan Identity f

type ComposeC :: (k1 -> k2 -> Type) -> (k2 -> Type) -> (k1 -> Type)
type ComposeC p f = CoClown (Procompose (Clown f) p)
type ContraLan j f = ComposeC (Star j) f
type ContraCoyoneda f = ContraLan Identity f
type ContraDay f1 f2 = ContraLan K2 (F2 f1 f2)


ranLaw :: (Procompose p q :-> r) -> p :-> Ran q r
ranLaw n p = Ran $ \q -> n (Procompose p q)

runRanF :: RanC p f b -> p a b -> f a
runRanF = (runClown .) . runRan . runCoClown

ranFLaw :: (forall x y. p x y -> g y -> f x) -> g a -> RanC p f a
ranFLaw n = CoClown . ranLaw (\(Procompose g p) -> Clown . n p . runClown $ g) . Clown

runContraRan :: ContraRan j f b -> (j a -> b) -> f a
runContraRan r = runRanF r . Costar

contraRanLaw :: Contravariant g => (forall x. g (j x) -> f x) -> g a -> ContraRan j f a
contraRanLaw n = ranFLaw (\(Costar j) -> n . contramap j)

runContraYoneda :: ContraYoneda f a -> (r -> a) -> f r
runContraYoneda r = runContraRan r . (. runIdentity)

contraYonedaLaw :: Contravariant f => f a -> ContraYoneda f a
contraYonedaLaw = contraRanLaw (contramap Identity)


composeRanLaw :: p :-> Ran q r -> (Procompose p q :-> r)
composeRanLaw n (Procompose p q) = runRan (n p) q

composeC :: p a b -> f b -> ComposeC p f a
composeC p = CoClown . flip Procompose p . Clown

composeCLaw :: (forall x y. p x y -> f y -> g x) -> ComposeC p f a -> g a
composeCLaw n = runClown . composeRanLaw (\f -> Ran $ \p -> Clown . n p . runClown $ f) . runCoClown

contraLan :: (a -> j b) -> f b -> ContraLan j f a
contraLan = composeC . Star

contraLanLaw :: Contravariant g => (forall x. f x -> g (j x)) -> ContraLan j f a -> g a
contraLanLaw n = composeCLaw (\(Star j) -> contramap j . n)

contraCoyoneda :: (a -> b) -> f b -> ContraCoyoneda f a
contraCoyoneda = contraLan . (Identity .)

contraCoyonedaLaw :: Contravariant f => ContraCoyoneda f a -> f a
contraCoyonedaLaw = contraLanLaw (contramap runIdentity)

contraDay :: f1 b1 -> f2 b2 -> (a -> (b1, b2)) -> ContraDay f1 f2 a
contraDay f1 f2 ab = contraLan (uncurry K2 . ab) (F2 f1 f2)

contraDayLaw :: Contravariant g => (forall x1 x2. f1 x1 -> f2 x2 -> g (x1, x2)) -> ContraDay f1 f2 a -> g a
contraDayLaw n = contraLanLaw (\(F2 f1 f2) -> unK2 >$< n f1 f2)


type K2 :: ((Type, Type) -> Type)
data K2 ab where
  K2 :: a -> b -> K2 '(a, b)
unK2 :: K2 '(a, b) -> (a, b)
unK2 (K2 a b) = (a, b)

type F2 :: (Type -> Type) -> (Type -> Type) -> ((Type, Type) -> Type)
data F2 f g a where
  F2 :: f b -> g c -> F2 f g '(b, c)

newtype CoJoker p b = CoJoker { runCoJoker :: p () b }
newtype CoClown p a = CoClown { runCoClown :: p a () }