索引单子（Indexed Monad）高阶编码工作原理相关问题咨询

需提前启用以下GHC扩展：

• RankNTypes
• KindSignatures
• ExistentialQuantification
• GADTs
• FlexibleInstances

1. 基于MonadIx实现索引状态单子 #

以下是可直接运行的索引状态单子定义与MonadIx实例：

-- 自然变换别名
type f :-> g = forall i. f i -> g i

-- 高阶索引状态单子定义：当前状态为s，执行后返回f o类型的结果与新状态o
newtype IxState f s = IxState { unIxState :: forall r. s -> (forall o. f o -> o -> r) -> r }

instance MonadIx IxState where
  returnIx :: f :-> IxState f
  returnIx fx = IxState $ \s k -> k fx s
  flipBindIx :: (f :-> IxState g) -> (IxState f :-> IxState g)
  flipBindIx f m = IxState $ \s k ->
    unIxState m s $ \fx o -> unIxState (f fx) o k

-- 通用常量谓词：忽略状态索引，保存返回值a
newtype K a i = K a

-- 基础状态操作
get :: IxState ((~) s) s
get = IxState $ \s k -> k Refl s
put :: o -> IxState (K ()) s
put o = IxState $ \_ k -> k (K ()) o

-- 执行索引状态计算，返回结果与最终状态
runIxState :: IxState (K a) i -> i -> (a, o)
runIxState m i = unIxState m i $ \(K a) o -> (a, o)

2. 从MonadIx恢复IxMonad能力 #

通过包装类型可以将任意MonadIx实例转换为符合Atkey定义的IxMonad实例，完整可编译实现如下：

newtype AtkeyAdapter m i j a = AtkeyAdapter (m (K a) j)

instance MonadIx m => IxMonad (AtkeyAdapter m) where
  ireturn :: a -> AtkeyAdapter m i i a
  ireturn a = AtkeyAdapter $ returnIx (K a)
  ibind :: AtkeyAdapter m i j a -> (a -> AtkeyAdapter m j k b) -> AtkeyAdapter m i k b
  ibind (AtkeyAdapter m) f = AtkeyAdapter $ flipBindIx (\(K a) -> let AtkeyAdapter m' = f a in m') m

3. 两种索引单子的映射关系 #

判断成立，MonadIx的表达能力严格强于Atkey式IxMonad，映射关系如下：

• 正向映射：任意IxMonad m => m i o a可以编码为MonadIx m' => m' (K a) o，其中m'是对原IxMonad的高阶包装，仅需要将原双状态索引的转移逻辑适配为对状态谓词f的操作即可
• 反向映射不存在：MonadIx支持对任意状态谓词f :: state -> *的操作，而Atkey的IxMonad只能描述固定起点和终点状态的转移，无法表示依赖谓词的动态状态约束，因此无法从IxMonad恢复MonadIx的全部能力

4. 带状态约束的操作表示 #

你提到的约束输入状态形态的操作，在MonadIx中可以通过自定义GADT形式的状态谓词实现。例如从(a, i)状态中取出首元素a，同时将状态变为i的操作可以实现为：

-- 自定义状态谓词：仅当输入状态为(a,i)时匹配，返回值为a
data ExtractA a i where
  ExtractA :: a -> ExtractA a i

extractHead :: IxState (ExtractA a) (a, i)
extractHead = IxState $ \(a, s) k -> k (ExtractA a) s

使用时直接对extractHead做bindIx操作即可获得取出的a，同时状态自动转移到i，完全实现和Atkey式IxMonad等价的状态约束能力。

内容的提问来源于stack exchange，提问作者SEC