CBV denotational semantics for categorical terms (from Declarative Continuations and Categorical Duality by Filinski)

CBV.hs

{-# LANGUAGE MultiParamTypeClasses, KindSignatures #-}
module CBV where
  
import Control.Functor
import Control.Category
import Control.Category.Object
import Control.Category.Associative
import Control.Category.Braided
import Control.Category.Cartesian
import Control.Category.Cartesian.Closed
import Control.Category.Monoidal
import Control.Category.Distributive
import Data.Void


type Ans = ()
newtype CBV a b = M ((b -> Ans) -> a -> Ans)
data CoCBV (hom :: * -> * -> *) b a = Co (b -> Ans) a


instance Category CBV where
  id = M $ \k v -> k v
  (M f) . (M g) = M $ \k v -> g (\t -> f k t) v


instance HasTerminalObject CBV () where
  terminate = M $ \k _ -> k ()
instance HasInitialObject CBV Void where
  initiate = M $ \_ v -> case v of { otherwise -> error "Empty choice" }

instance PreCartesian CBV (,) where
  fst = M $ \k (a, b) -> k a
  snd = M $ \k (a, b) -> k b
  M f &&& M g = M $ \k v -> f (\s -> g (\t -> k (s, t)) v) v
instance PreCoCartesian CBV Either where
  inl = M $ \k v -> k (Left v)
  inr = M $ \k v -> k (Right v)
  M f ||| M g = M $ \k v -> case v of { Left t -> f k t; Right t -> g k t } 

instance HasIdentity CBV (,) ()
instance Monoidal CBV (,) () where
  idl = M $ \k ((), r) -> k r
  idr = M $ \k (l, ()) -> k l
instance HasIdentity CBV Either Void
instance Comonoidal CBV Either Void where
  coidl = M $ \k v -> k (Right v)
  coidr = M $ \k v -> k (Left v)

instance CCC CBV (,) CBV () where
  apply = M $ \k (M f, v) -> f k v
  curry (M f) = M $ \k a -> k (M $ \b c -> f b (a, c))
  uncurry (M f) = M $ \k (a, b) -> f (\(M g) -> g k b) a
instance CoCCC CBV Either CoCBV Void where
  coapply = M $ \k v -> k (Left (Co (\t -> k (Right t)) v))
  cocurry (M f) = M $ \k (Co c a) -> f (either k c) a
  uncocurry (M f) = M $ \k v -> f (\s -> k (Left s)) (Co (\t -> k (Right t)) v)

instance Distributive CBV (,) Either where
  distribute = M $ \k (a, v) -> case v of { Left r -> k (Left (a, r)); Right s -> k (Right (a, s)) }



instance PFunctor (,) CBV CBV where
  first = first'
instance QFunctor (,) CBV CBV where
  second = second'
instance Bifunctor (,) CBV CBV CBV where
  bimap = bimapPreCartesian
instance Braided CBV (,) where
  braid = braidPreCartesian
instance Symmetric CBV (,)
instance Associative CBV (,) where
  associate = associatePreCartesian
instance Coassociative CBV (,) where
  coassociate = coassociatePreCartesian

instance PFunctor Either CBV CBV where
  first = first'
instance QFunctor Either CBV CBV where
  second = second'
instance Bifunctor Either CBV CBV CBV where
  bimap = bimapPreCoCartesian
instance Braided CBV Either where
  braid = braidPreCoCartesian
instance Symmetric CBV Either
instance Associative CBV Either where
  associate = associatePreCoCartesian
instance Coassociative CBV Either where
  coassociate = coassociatePreCoCartesian

CBV1.hs

{-# LANGUAGE MultiParamTypeClasses, KindSignatures #-}
module CBV where

import Control.Functor
import Control.Category
import Control.Category.Object
import Control.Category.Associative
import Control.Category.Braided
import Control.Category.Cartesian
import Control.Category.Cartesian.Closed
import Control.Category.Monoidal
import Control.Category.Distributive
import Data.Void

import Prelude hiding ((.), id, fst, snd)
import Control.Applicative

type Ans = ()
newtype CBV a b = M ((b -> Ans) -> a -> Ans)
data CoCBV (hom :: * -> * -> *) b a = Co (b -> Ans) a

arr :: (a -> b) -> CBV a b
arr f = f <$> id

instance Functor (CBV a) where
  fmap f (M g) = M $ \k -> g (k . f)
instance Applicative (CBV a) where
  pure x = M $ \k _ -> k x
  (M f) <*> (M x) = M $ \k v -> x (\a -> f (\ab -> k (ab a)) v) v
instance Monad (CBV a) where
  return = pure
  (M m) >>= f = M $ \k v -> m (\a -> let (M g) = f a in g k v) v

instance Category CBV where
  id = M $ id
  (M f) . (M g) = M $ g . f


instance HasTerminalObject CBV () where
  terminate = pure ()
instance HasInitialObject CBV Void where
  initiate = M $ \_ v -> case v of { otherwise -> error "Empty choice" }

instance PreCartesian CBV (,) where
  fst = arr fst
  snd = arr snd
  f &&& g = (,) <$> f <*> g
instance PreCoCartesian CBV Either where
  inl = arr Left
  inr = arr Right
  M f ||| M g = M $ either <$> f <*> g

instance HasIdentity CBV (,) ()
instance Monoidal CBV (,) () where
  idl = snd
  idr = fst
instance HasIdentity CBV Either Void
instance Comonoidal CBV Either Void where
  coidl = inr
  coidr = inl

instance CCC CBV (,) CBV () where
  apply = M $ \k (M f, v) -> f k v
  curry (M f) = M $ \k a -> k (M $ \b c -> f b (a, c))
  uncurry (M f) = M $ \k (a, b) -> f (\(M g) -> g k b) a
instance CoCCC CBV Either CoCBV Void where
  coapply = M $ \k -> k . Left . Co (k . Right)
  cocurry (M f) = M $ \k (Co c a) -> f (either k c) a
  uncocurry (M f) = M $ \k -> f (k . Left) . Co (k . Right)

instance Distributive CBV (,) Either where
  distribute = M $ \k (a, v) -> either (k . Left . (,) a) (k . Right . (,) a) v



instance PFunctor (,) CBV CBV where
  first = first'
instance QFunctor (,) CBV CBV where
  second = second'
instance Bifunctor (,) CBV CBV CBV where
  bimap = bimapPreCartesian
instance Braided CBV (,) where
  braid = braidPreCartesian
instance Symmetric CBV (,)
instance Associative CBV (,) where
  associate = associatePreCartesian
instance Coassociative CBV (,) where
  coassociate = coassociatePreCartesian

instance PFunctor Either CBV CBV where
  first = first'
instance QFunctor Either CBV CBV where
  second = second'
instance Bifunctor Either CBV CBV CBV where
  bimap = bimapPreCoCartesian
instance Braided CBV Either where
  braid = braidPreCoCartesian
instance Symmetric CBV Either
instance Associative CBV Either where
  associate = associatePreCoCartesian
instance Coassociative CBV Either where
  coassociate = coassociatePreCoCartesian