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：看起来您正在寻找按类别索引的 monad。

可编译要点：https://gist.github.com/Lysxia/04039e4ca6f7a3740281e4e3583ae971

IMonadHoare不等于IMonadTF（又名：graded monad，参见effect-monad）。

特别是，使用IMonadTF（分级单子），您可以绑定任意两个计算，它们的索引附加在一起，而使用IMonadHoare（索引单子），您只能将计算与匹配的索引绑定。因此，您无法轻松地将任意IMonadHoare，例如IWriter，编码为 an ，因为当索引不匹配时IMonadTF没有任何意义。bind

这种“部分定义的组合”让人IMonadHoare想起类别，实际上我们可以将IMonadHoare和概括IMonadTF为由类别箭头索引的单子，而不是索引对或幺半群的元素。事实上，我们可以在两个类中看到类别的示例：

1. 对(i, j)可以被视为一个类别的箭头，其中i和是对象（因此，在和之间j恰好有一个箭头，对，尽管它是什么并不重要，只重要的是只有一个）；ij(i, j)
2. 幺半群是类别。

这是按类别索引的单子类c :: k -> k -> Type；该类包括类别的定义c，通过关联类型Id和Cat对应于您的Empty和Append。它看起来实际上与 几乎相同IMonadTF，只是你有一个类别c :: k -> k -> Type而不是一个幺半群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

这是我之前提到的配对类别。在每个对象i和j（在某些 set/type 中k）之间，有一个箭头E（名称并不重要，只是只有一个）。它也可以被可视化为带有 中顶点的完整图k。

data Edge (i :: k) (j :: k) = E

我们现在可以定义IWriter为CatMonad. 这有点挑剔，您必须明确地放置i和j，否则它们会在实例头的错误位置进行量化CatMonad。不然也不会有太大的麻烦。没有什么真正依赖于E，它只是其类型的占位符，其中包含重要的索引i和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)