Monads indexed by categories

CatMonad.hs

{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}

module CatMonad where

import Control.Category as C
import Data.Kind

class CatMonad (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) where
  type Id m :: c x x
  type Cat m (f :: c x y) (g :: c y z) :: c x z

  xpure :: a -> m (Id m) a

  xbind :: m f a -> (a -> m g b) -> m (Cat m f g) b

data Edge x y = E

newtype IWriter cat i j (q :: Edge i j) a = IWriter { runIWriter :: (a, cat i j) }

instance Category cat => CatMonad (IWriter cat) where
  type Id (IWriter cat) = E
  type Cat (IWriter cat) _ _ = E

  xpure a = IWriter (a, C.id)
  xbind (IWriter (a, f)) k =
    let IWriter (b, g) = k a in
    IWriter (b, f C.>>> g)