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

Question

定义索引 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？

Answer 1

\n

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

\n

\n

McBride 风格的索引单子是关于量化运行时的不确定性。如果普通 monadm a模拟一个返回 an 的计算a，那么索引 monadm a i模拟一个从 state* 开始的计算，并为某些未知的输出状态i返回 an 。您唯一可以说的是它满足谓词。a j jja

\n

^{*我在这里使用的词“状态”、“输入”和“输出”有些宽松。}

\n

这就是为什么 McBridebind拥有更高级别的类型：

\n

mcBind :: m a i -> (forall j. a j -> m b j) -> m b i\n

\n

延续forall j. a j -> m b j必须是不可知的j，超出了它在运行时通过检查a j. （对于返回多个as 的非确定性 monad，j每个 s 的值可能不同。）

\n

McBride 在Outrageous Fortune论文中的运行示例是关于文件 API 的，该 API可能会成功返回打开的文件，也可能会失败（如果文件不存在）。Hasochism论文中还有一个关于平铺窗口管理器的示例\ xe2\x80\x94 你有一个 2D 盒子，它可能由彼此相邻放置的较小盒子组成。您可以深入查看各个框并将其替换为其他框。您不知道每个单独的盒子静态有多大，但是当用另一个盒子替换一个盒子时，它们必须具有相同的大小。

\n

因此，索引状态单子 ( State i j a) 接受已知的输入状态i并产生已知的输出状态j，它根本不适合McBride 风格的索引单子。的类型mcBind是错误的，因为它丢弃了有关输出状态的信息。

\n

\n

IxMonad[T]这里应该是从任何[to] 的映射MonadIx，但不是相反，对吧？那个映射是什么？

\n

\n

恰恰相反。McBride 的索引单子比 Atkey 的索引单子更强大 \xe2\x80\x94 如果您有 的m :: (i -> *) -> i -> *实例，那么MonadIx您总是可以找到对应的n :: i -> i -> * -> *实例IxMonad。（令人惊讶的是，反之亦然。）这在 McBride 论文的第 5 节（“天使、恶魔和鲍勃”）中有详细介绍。简要地：

\n

-- McBride wittily pronounces this type "at key"\ndata (a := i) j where\n    V :: a -> (a := i) i\n\nnewtype Atkey m i j a = Atkey { getAtkey :: m (a := j) i }\n\ninstance MonadIx m => IxMonad (Atkey m) where\n    ireturn a = Atkey (returnIx (V a))\n    ibind (Atkey m) f = Atkey $ m `bindIx` (\\(V a) -> getAtkey (f a))\n

\n