Type-level monoid-like operations for generalizing indexed monads?
tl;dr: it looks like you're looking for monads indexed by categories.
Compilable gist: https://gist.github.com/Lysxia/04039e4ca6f7a3740281e4e3583ae971
IMonadHoare
is not equivalent to IMonadTF
(aka. graded monad, see effect-monad).
In particular, with IMonadTF
(graded monads) you can bind any two computations, their indices get appended together, whereas with IMonadHoare
(indexed monads) you can only bind computations with matching indices. Therefore you can't easily encode an arbitrary IMonadHoare
, such as IWriter
, as an IMonadTF
because there is no meaning to bind
when the indices don't match.
This kind of "partially defined composition" for IMonadHoare
is reminiscent of categories, and indeed we can generalize both IMonadHoare
and IMonadTF
with monads indexed by arrows of a category, instead of pairs of indices or elements of a monoid. Indeed, we can see examples of categories in both classes:
- Pairs
(i, j)
can be seen as arrows of a category in whichi
andj
are objects (so there is exactly one arrow betweeni
andj
, the pair(i, j)
, although it doesn't really matter what it is, only that there is exactly one); - Monoids are categories.
Here's the class of monads indexed by a category c :: k -> k -> Type
; this class includes the definition of the category c
, via the associated types Id
and Cat
that correspond to your Empty
and Append
. It looks actually pretty much the same as IMonadTF
, except that you have a category c :: k -> k -> Type
instead of a monoid idx :: Type
.
{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
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
Here's the category of pairs I mentioned earlier. Between every object i
and j
(in some set/type k
), there is one arrow E
(the name doesn't matter, only that there is only one). It can also be visualized as the complete graph with vertices in k
.
data Edge (i :: k) (j :: k) = E
We can now define IWriter
as a CatMonad
. It's a bit finicky, you have to put i
and j
explicitly or they get quantified in the wrong place for the CatMonad
instance head. Otherwise there isn't much trouble. Nothing really depends on E
,
it's merely a placeholder for its type, which contains the indices that matter i
and j
.
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)