Cont.hs

-- | The continuation promonad: @'Cont' r a b@ is a continuation transformer @(b '~>' r) -> (a '~>' r)@.
-- It is strong for the tensor but only premonoidal, as the order of effects matters.
module Proarrow.Promonad.Cont where

import Data.Kind (Type)
import Prelude (($))

import Proarrow.Category.Instance.Kleisli (KLEISLI (..), Kleisli (..))
import Proarrow.Category.Monoidal (MonoidalProfunctor (..), Tensor)
import Proarrow.Category.Monoidal.Closed (Closed (..), curry, uncurry)
import Proarrow.Category.Monoidal.StarAutonomous (ExpSA, StarAutonomous (..), applySA, currySA, expSA)
import Proarrow.Category.Monoidal.Strength (Strong (..))
import Proarrow.Colimit.BinaryCoproduct (Coprod (..), HasBinaryCoproducts (..), HasCoproducts)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..))
import Proarrow.Profunctor.Representable (Representable (..))

-- | An arrow from @a@ to @b@ is a mapping of continuations @(b '~>' r) -> (a '~>' r)@.
data Cont r a b where
  Cont :: (Ob a, Ob b) => {runCont :: (b ~> r) -> (a ~> r)} -> Cont r a b

instance (CategoryOf k) => Profunctor (Cont (r :: k)) where
  dimap l r (Cont f) = Cont ((. l) . f . (. r)) \\ l \\ r
  r \\ Cont{} = r
instance (CategoryOf k) => Promonad (Cont (r :: k)) where
  id = Cont id
  Cont f . Cont g = Cont (g . f)

-- | At @Type@ the continuation promonad is the continuation /monad/: @(b -> r) -> (a -> r)@ is
-- @a -> (b -> r) -> r@ by flipping the arguments, so @'Cont' r '%' b@ is the double-negation
-- @(b -> r) -> r@. This gives @'KLEISLI' ('Cont' r)@ its initial object and coproducts, which
-- hold for the Kleisli category of a monad but not of an arbitrary promonad.
instance Representable (Cont (r :: Type)) where
  type Cont r % b = (b -> r) -> r
  index (Cont f) a k = f k a
  tabulate g = Cont \k a -> g a k
  repMap f c k = c (k . f)

instance Strong Tensor (Cont (r :: Type)) where
  act (Cont yrxy) = Cont \byr -> uncurry (yrxy . curry byr)

-- Not costrong

-- | Only premonoidal not monoidal.
instance MonoidalProfunctor (Cont (r :: Type)) where
  one = Cont id
  Cont f ** Cont g = Cont \k (x1, y1) -> f (\x2 -> g (\y2 -> k (x2, y2)) y1) x1

instance (HasCoproducts k) => MonoidalProfunctor (Coprod (Cont (r :: k))) where
  one = Coprod (Cont id)
  Coprod (Cont @af @bf f) ** Coprod (Cont @ag @bg g) =
    withObCoprod @k @af @ag $
      withObCoprod @k @bf @bg $
        Coprod (Cont (\k -> f (k . lft @_ @bf @bg) ||| g (k . rgt @_ @bf @bg)))

instance StarAutonomous (KLEISLI (Cont (r :: Type))) where
  type Dual @(KLEISLI (Cont r)) (KL a) = KL (a ~~> r)
  withObDual r = r
  dual (Kleisli (Cont f)) = Kleisli (Cont \k br -> k (f br))
  dualInv (Kleisli (Cont f)) = Kleisli (Cont \k b -> f (\g -> g b) k)
  linDist (Kleisli (Cont f)) = Kleisli (Cont \k a -> k (\(b, c) -> f (\g -> g c) (a, b)))
  linDistInv (Kleisli (Cont f)) = Kleisli (Cont \k (a, b) -> k (\c -> f (\g -> g (b, c)) a))
instance Closed (KLEISLI (Cont (r :: Type))) where
  type a ~~> b = ExpSA a b
  withObExp r = r
  curry = currySA
  apply = applySA
  (^^^) = expSA

-- Not CompactClosed, needs ((a -> r, b -> r) -> r) -> ((a, b) -> r) -> r