索引单子的高阶编码是如何工作的？

定义索引 monad a la Atkey的常用方法是：

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

另一种方法可以在McBride的工作中找到（他也在这里讨论过）：

type f :-> g = forall i. f i -> g i

class MonadIx (m :: (state -> *) -> (state -> *)) where
  returnIx    :: f :-> m f
  flipBindIx  :: (f :-> m g) -> (m f :-> m g)

的类型与flipBindIx同构bindIx :: forall i. m f i -> (forall j. f j -> m g j) -> m g i。而正常的 Haskell monad 表征m :: * -> *（和“正常”索引的 monad 表征m :: state -> state -> * -> *），MonadIx表征 monads m :: (state -> *) -> state -> *。这就是为什么我称后者为“高阶”（但如果有更好的名字，请告诉我）。

虽然这在一定程度上有意义，并且我可以看到两种编码之间的某些结构相似性，但我在一些事情上遇到了困难。以下是一些似乎相关的问题：

• 最根本的是，我只是不明白如何使用MonadIx编写一个简单的索引状态 monad —— 一个IxMonad看起来就像常规状态 monad 的，具有更通用的类型。

• 相关地，在之前链接的 SO 问题中，Kmett 讨论了一种IxMonad从MonadIx. 然而，该技术并未完全展示（而且我无法再编译相关代码）。

• MonadIx比 强IxMonad。这表明应该存在从 anyIxMonad m => m i o a到 some MonadIx m => m f（或 is m f i？）的映射，但不是相反，对吗？那是什么映射？

• 最后，参数化在 的定义中比比皆是MonadIx。但是IxMonad动作可以自由地对传入状态的形状提出要求，如m :: IxMonad m (a, i) i a。这些动作看起来如何MonadIx？