Type-level monoid-like operations for generalizing indexed monads?

Question

To motivate this question, let's first recall a bog-standard Hoare-Dijkstra-style indexed monad, and the example instance of an indexed writer monad.

For an indexed monad, we just require type alignment on (i)binds:

class IMonadHoare m where
    ireturn :: a -> m i i a
    ibind :: m i j a -> (a -> m j k b) -> m i k b

and then just to show that this is usable, let's implement an indexed writer monad:

import Prelude hiding (id, (.))
import Control.Category

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

instance (Category cat) => IMonadHoare (IWriter cat) where
    ireturn x = IWriter (x, id)

    ibind (IWriter (x, f)) k = IWriter $
        let (y, g) = runIWriter (k x)
        in (y, g . f)

And it really is a writer-like monad, since we can implement the usual methods:

itell :: (Category cat) => cat i j -> IWriter cat i j ()
itell f = IWriter ((), f)

ilisten :: (Category cat) => IWriter cat i j a -> IWriter cat i j (a, cat i j)
ilisten w = IWriter $
    let (x, f) = runIWriter w
    in ((x, f), f)

ipass :: (Category cat) => IWriter cat i j (a, cat i j -> cat i j) -> IWriter cat i j a
ipass w = IWriter $
    let ((x, censor), f) = runIWriter w
    in (x, censor f)

OK, so far so good. But now I'd like to generalize this to other kinds (heh) of indices. I thought it would work to simply add associated type families for the type-level monoid operations, like so:

{-# LANGUAGE TypeFamilies, PolyKinds, MultiParamTypeClasses, FunctionalDependencies #-}

import Data.Kind

class IMonadTF idx (m :: idx -> Type -> Type) | m -> idx where
    type Empty m :: idx
    type Append m (i :: idx) (j :: idx) :: idx

    ireturn :: a -> m (Empty m) a
    ibind :: m i a -> (a -> m j b) -> m (Append m i j) b

So, does this work? Well, you can use it to define something where Empty/Append is non-indexed, like so:

{-# LANGUAGE DataKinds, TypeOperators #-}

import GHC.TypeLists

newtype Counter (n :: Nat) a = Counter{ runCounter :: a }

instance IMonadTF Nat Counter where
    type Empty Counter = 0
    type Append Counter n m = n + m

    ireturn = Counter
    ibind (Counter x) k = Counter . runCounter $ k x

tick :: Counter 1 ()
tick = Counter ()

But now can we recreate our IWriter example? Unfortunately, I haven't been able to.

First of all, we can't even declare Empty:

data IWriter cat (ij :: (Type, Type)) a where
    IWriter :: { runIWriter :: (a, cat i j) } -> IWriter cat '(i, j) a

instance (Category cat) => IMonadTF (Type, Type) (IWriter cat) where
    type Empty (IWriter cat) = '(i, i)

This, of course, fails because the type variable i is not in scope.

Let's change Empty into a Constraint instead, and recreate the Counter instance just to validate it:

class IMonadConstraint idx (m :: idx -> Type -> Type) | m -> idx where
    type IsEmpty m (i :: idx) :: Constraint
    type Append m (i :: idx) (j :: idx) :: idx

    ireturn :: (IsEmpty m i) => a -> m i a
    ibind :: m i a -> (a -> m j b) -> m (Append m i j) b

newtype Counter (n :: Nat) a = Counter{ runCounter :: a }

instance IMonadConstraint Nat Counter where
    type IsEmpty Counter n = n ~ 0
    type Append Counter n m = n + m

    ireturn = Counter
    ibind (Counter x) k = Counter . runCounter $ k x

tick :: Counter 1 ()
tick = Counter ()

Now we can at least write down the definition of IsEmpty (Writer cat), but in the code below, ireturn still doesn't typecheck. It is as if the defintion of IsEmpty isn't used to solve constraints:

instance (Category cat) => IMonadConstraint (Type, Type) (IWriter cat) where
    type IsEmpty (IWriter cat) '(i, j) = i ~ j

    ireturn x = IWriter (x, id)

Could not deduce i ~ '(j0, j0) from the context IsEmpty (IWriter cat) i

Similarly, we can try to enforce the alignment in the middle by adding a constraint for appending:

class IMonadConstraint2 idx (m :: idx -> Type -> Type) | m -> idx where
    type IsAppend m (i :: idx) (j :: idx) :: Constraint
    type Append m (i :: idx) (j :: idx) :: idx

    ireturn :: (IsEmpty m i) => a -> m i a    ibind :: (IsAppend m i j) => m i a -> (a -> m j b) -> m (Append m i j) b

But then that fails for IWriter in a similar way:

instance (Category cat) => IMonadConstraint2 (Type, Type) (IWriter cat) where
    type IsAppend (IWriter cat) '(i, j) '(j', k) = j ~ j'
    type Append (IWriter cat) '(i, j) '(j', k) = '(i, k)

    ibind (IWriter (x, w)) k = IWriter $
        let (y, w') = runIWriter (k x)
        in (y, w' . w)

Could not deduce j ~ '(j1, j0) from the context IsAppend (IWriter cat) i j

Is it because IsEmpty and IsAppend defined "pointwise"?

Answer 1

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:

1. Pairs (i, j) can be seen as arrows of a category in which i and j are objects (so there is exactly one arrow between i and j, the pair (i, j), although it doesn't really matter what it is, only that there is exactly one);
2. 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)

Answer 2

(There is no reason to put a tuple into IWriter; I'm just going to use this

data IWriter (cat :: idx -> idx -> Type) (p :: (idx, idx)) (a :: Type) where
  IWriter :: a -> cat i j -> IWriter cat '(i, j) a

)

You've write

ireturn x = IWriter x id

for all version of the class. However, IWriter x id :: forall i. IWriter cat (i, i) a, while you need IWriter cat m a (where cat, m and a are arguments to ireturn). (,) _ _ is not m, period. You cannot write a constraint that proves this, either, because then i needs to be an argument to ireturn, but it's a typeclass method, so that can't be allowed. That aside, the correct IMonad is really the last one (IMonadConstraint, both 1 and 2, together).

class IMonad (m :: idx -> Type -> Type) | m -> idx where
  type IsEmpty m (i :: idx) :: Constraint
  type IsAppend m (i :: idx) (j :: idx) :: Constraint
  type Append m (i :: idx) (j :: idx) :: idx
  ireturn :: IsEmpty m i => a -> m i a
  ibind :: IsAppend m i j => m i a -> (a -> m j b) -> m (Append m i j) b

You need to assert an axiom:

data IsTup (p :: (i, j)) where IsTup :: IsTup '(x, y)
isTup :: forall p. IsTup p
isTup = unsafeCoerce IsTup

The statement forall (p :: (i, j)). exists (x :: i) (y :: j). p ~ '(x, y) is neither provable nor disprovable in Haskell, so we can take it as an axiom like this, if we need it. It seems "true" enough.

instance Category cat => IMonad (IWriter cat) where
  type IsEmpty (IWriter cat) '(i, j) = i ~ j
  type IsAppend (IWriter cat) '(_, i) '(j, _) = i ~ j
  type Append (IWriter cat) '(i, _) '(_, j) = '(i, j)
  ireturn :: forall i a. IsEmpty (IWriter cat) i => a -> IWriter cat i a
  ireturn x | IsTup <- isTup @i = IWriter x id
  ibind (IWriter x w) f | IWriter y w' <- f x = IWriter y (w >>> w')
  -- IWriter :: forall cat p a. forall i j. p ~ '(i, j) => a -> cat i j -> IWriter cat p a
  -- IsTup   :: forall     p  . forall x y. p ~ '(x, y) =>                 IsTup       p
  -- in ibind, the two matches on IWriter prove that the two type-level tuple
  -- arguments are actually tuples
  -- in ireturn, you need to split that behavior out into it's own type IsTup,
  -- make forall p. IsTup p an axiom, and use it to show that the argument i
  -- is also really a tuple