Coexponentials in the Kleisli category of Cont r.

coexp.hs

{-# LANGUAGE TypeFamilies, TypeOperators #-}

-- re: http://www.reddit.com/r/haskell/comments/qwklh/coexponentials/

import Data.Category
import Data.Category.Limit
import Data.Category.CartesianClosed
import Data.Void

newtype KleisliContOp r b a = KCO (a -> (b -> r) -> r)

kcoId :: Obj (KleisliContOp r) a
kcoId = KCO (flip ($))


instance Category (KleisliContOp r) where
  src _ = kcoId
  tgt _ = kcoId
  
  KCO ab . KCO bc = KCO $ \a cr -> ab a (\b -> bc b cr)


instance HasTerminalObject (KleisliContOp r) where
  type TerminalObject (KleisliContOp r) = Void
  terminalObject = kcoId
  terminate _ = KCO $ \v _ -> absurd v


type instance BinaryProduct (KleisliContOp r) x y = Either x y

instance HasBinaryProducts (KleisliContOp r) where
  proj1 _ _ = KCO $ \x f -> f (Left x)
  proj2 _ _ = KCO $ \y f -> f (Right y)
  
  KCO xa &&& KCO ya = KCO $ \e ar -> either (\x -> xa x ar) (\y -> ya y ar) e


type instance Exponential (KleisliContOp r) y z = (z, y -> r)

instance CartesianClosed (KleisliContOp r) where
  -- z -> (Either (z, y -> r) y -> r) -> r
  apply _ _ = KCO $ \z k -> k (Left (z, \y -> k (Right y)))
  -- (Either z y, y -> r) -> (z -> r) -> r
  tuple _ _ = KCO $ \(e, yr) zr -> either zr yr e
  -- (z2 -> (z1 -> r) -> r) -> (y1 -> (y2 -> r) -> r) -> (z2, y2 -> r) -> ((z1, y1 -> r) -> r) -> r
  KCO z ^^^ KCO y = KCO $ \(z2, y2r) k -> z z2 (\z1 -> k (z1, \y1 -> y y1 y2r))

from: https://www.reddit.com/r/haskell/comments/qwklh/coexponentials/

exclude :: (a -> Cont r (Either b c)) -> (CoExp r a c -> Cont r b)
exclude f = tuple . (f ^^^ id)