什么是索引monad？
什么是索引monad和这个monad的动机？
我已经读过，它有助于跟踪副作用。 但是型号签名和文档不会让我到任何地方。
什么是它可以如何帮助跟踪副作用（或任何其他有效的例子）的例子？
与以往一样，人们使用的术语并不完全一致。 有许多灵感来源于单子，但严格说来并不完全是概念。 术语“索引monad”是用于表征一个这样的概念的术语（包括“monadish”和“参数化monad”（Atkey的名字））中的一个。 （另一个这样的概念，如果你感兴趣的话，是Katsumata的“参数效应monad”，由一个幺半群索引，其中return是中立的，并且绑定积累在它的索引中。）
首先，让我们来检查种类。
IxMonad (m :: state -> state -> * -> *)
也就是说，“计算”的类型（或者“动作”，如果你愿意，但我会坚持“计算”），看起来像
m before after value
before, after :: state和value :: * 。 这个想法是捕捉手段与外部系统安全地进行交互，该外部系统具有可预测的状态概念。 计算的类型告诉你状态before运行before必须是什么状态，状态after运行after会是什么状态，并且（就像在常规单选符上运行* ）计算生成的是什么类型的value 。
通常的点点滴滴都* -wise像一个单子和state -wise喜欢玩多米诺骨牌。
ireturn :: a -> m i i a -- returning a pure value preserves state
ibind :: m i j a -> -- we can go from i to j and get an a, thence
(a -> m j k b) -- we can go from j to k and get a b, therefore
-> m i k b -- we can indeed go from i to k and get a b
由此产生的“Kleisli箭头”（产生计算的函数）的概念是
a -> m i j b -- values a in, b out; state transition i to j
我们得到一份作品
icomp :: IxMonad m => (b -> m j k c) -> (a -> m i j b) -> a -> m i k c
icomp f g = a -> ibind (g a) f
和以往一样，法律确切地确保了ireturn和icomp给我们一个类别
ireturn `icomp` g = g
f `icomp` ireturn = f
(f `icomp` g) `icomp` h = f `icomp` (g `icomp` h)
或者，在喜剧假C / Java /无论如何，
g(); skip = g()
skip; f() = f()
{h(); g()}; f() = h(); {g(); f()}
何必？ 模拟交互的“规则”。 例如，如果驱动器中没有DVD，则无法弹出DVD，如果已经有DVD，则无法将DVD放入驱动器。 所以
data DVDDrive :: Bool -> Bool -> * -> * where -- Bool is "drive full?"
DReturn :: a -> DVDDrive i i a
DInsert :: DVD -> -- you have a DVD
DVDDrive True k a -> -- you know how to continue full
DVDDrive False k a -- so you can insert from empty
DEject :: (DVD -> -- once you receive a DVD
DVDDrive False k a) -> -- you know how to continue empty
DVDDrive True k a -- so you can eject when full
instance IxMonad DVDDrive where -- put these methods where they need to go
ireturn = DReturn -- so this goes somewhere else
ibind (DReturn a) k = k a
ibind (DInsert dvd j) k = DInsert dvd (ibind j k)
ibind (DEject j) k = DEject j $ dvd -> ibind (j dvd) k
有了这个，我们可以定义“原始”命令
dInsert :: DVD -> DVDDrive False True ()
dInsert dvd = DInsert dvd $ DReturn ()
dEject :: DVDrive True False DVD
dEject = DEject $ dvd -> DReturn dvd
从其他人那里与ireturn和ibind聚集在一起。 现在，我可以写（借用do -notation）
discSwap :: DVD -> DVDDrive True True DVD
discSwap dvd = do dvd' <- dEject; dInsert dvd ; ireturn dvd'
但不是身体上不可能的
discSwap :: DVD -> DVDDrive True True DVD
discSwap dvd = do dInsert dvd; dEject -- ouch!
或者，可以直接定义一个原始命令
data DVDCommand :: Bool -> Bool -> * -> * where
InsertC :: DVD -> DVDCommand False True ()
EjectC :: DVDCommand True False DVD
然后实例化通用模板
data CommandIxMonad :: (state -> state -> * -> *) ->
state -> state -> * -> * where
CReturn :: a -> CommandIxMonad c i i a
(:?) :: c i j a -> (a -> CommandIxMonad c j k b) ->
CommandIxMonad c i k b
instance IxMonad (CommandIxMonad c) where
ireturn = CReturn
ibind (CReturn a) k = k a
ibind (c :? j) k = c :? a -> ibind (j a) k
实际上，我们已经说过原始的Kleisli箭是什么（多米诺骨牌是什么），然后在它们上面建立了一个合适的“计算序列”概念。
请注意，对于每个索引monad m ，“不变对角线” mii是一个单子，但一般来说， mij不是。 此外，值并没有编入索引，但计算被编入索引，因此索引monad不仅仅是monad为其他类别实例化的常用思路。
现在，再看一下Kleisli箭头的类型
a -> m i j b
我们知道我们必须处于状态i开始，并且我们预测任何延续都将从状态j开始。 我们对这个系统了解很多！ 这不是一个危险的操作！ 当我们把DVD放入驱动器时，它就进入了！ DVD驱动器在每个命令之后的状态都没有任何说法。
但是，当与世界进行交流时，情况并非如此。 有时你可能需要放弃一些控制，让世界做它喜欢的事情。 例如，如果您是服务器，您可能会为您的客户提供选择，而您的会话状态将取决于他们选择的内容。 服务器的“提供选择”操作不能确定结果状态，但服务器应该能够继续进行。 在上述意义上，它不是一个“原始命令”，因此索引monad并不是模拟不可预测场景的好工具。
什么是更好的工具？
type f :-> g = forall state. f state -> g state
class MonadIx (m :: (state -> *) -> (state -> *)) where
returnIx :: x :-> m x
flipBindIx :: (a :-> m b) -> (m a :-> m b) -- tidier than bindIx
可怕的饼干？ 不是真的，有两个原因。 其一，它看起来更像是一个单子，因为它是一个单子，但超过(state -> *)而不是* 。 二，如果你看一下Kleisli箭头的类型，
a :-> m b = forall state. a state -> m b state
你会得到带有先决条件a和后置条件b的计算类型，就像Good Good Hoare Logic中的一样。 程序逻辑中的断言在半个世纪之内穿过了Curry-Howard的对应关系并成为Haskell类型。 returnIx的类型表示“你可以通过什么都不能做到的任何后置条件来实现”，这是“跳过”的霍尔逻辑规则。 相应的组合是“;”的霍尔逻辑规则。
让我们看看bindIx的类型，将所有量词放入。
bindIx :: forall i. m a i -> (forall j. a j -> m b j) -> m b i
这些forall ■找相反的极性。 我们选择初始状态i ，并且可以从i开始，具有后置条件a 。 世界选择的任何中间状态j它喜欢，但后置条件，必须给我们证据b成立，并从任何这样的状态，我们可以继续做b保持。 所以，按顺序，我们可以从状态i获得条件b 。 通过释放我们对“之后”状态的掌握，我们可以对不可预测的计算进行建模。
IxMonad和MonadIx都很有用。 交互式计算在改变状态方面的模型有效性，分别可预测和不可预测。 可以预见的东西很有价值，但不可预测性有时也是生活中的事实。 然后，希望这个答案能够给出一些指示单子的指示，预测它们何时开始有用以及何时停止。
至少有三种方法可以定义我知道的索引monad。
我将这些选项称为索引monadàla X，其中X分布在计算机科学家Bob Atkey，Conor McBride和Dominic Orchard上，因为这是我倾向于想到的。 这些结构中的部分通过类别理论具有更长的辉煌历史和更好的解释，但我首先了解到这些名称与它们有关，并且我试图让这个答案变得太过于深奥。
Atkey
Bob Atkey的索引monad的风格是使用2个额外的参数来处理monad的索引。
有了它，你可以得到其他答案中的定义：
class IMonad m where
ireturn :: a -> m i i a
ibind :: m i j a -> (a -> m j k b) -> m i k b
我们也可以定义索引的comonadsàla Atkey。 我实际上在lens代码库中获得了很多里程。
麦克布莱德
下一个索引monad的形式是Conor McBride在他的论文“Kleisli Arrows of Outrageous Fortune”中的定义。 他改为使用索引的单个参数。 这使得索引monad定义具有相当巧妙的形状。
如果我们使用参数定义一个自然变换如下
type a ~> b = forall i. a i -> b i
那么我们可以写下McBride的定义
class IMonad m where
ireturn :: a ~> m a
ibind :: (a ~> m b) -> (m a ~> m b)
这感觉与Atkey完全不同，但它更像是一个普通的Monad，而不是在(m :: * -> *)上构建monad，我们将它构建在(m :: (k -> *) -> (k -> *) 。
有趣的是，通过使用巧妙的数据类型，你实际上可以从McBride's中恢复Atkey的索引monad风格，McBride以其独特的风格选择说你应该读作“关键”。
data (:=) :: a i j where
V :: a -> (a := i) i
现在你可以解决这个问题
ireturn :: IMonad m => (a := j) ~> m (a := j)
扩展到
ireturn :: IMonad m => (a := j) i -> m (a := j) i
只有当j = i时才能被调用，然后仔细阅读ibind可以让你回到Atkey的ibind 。 您需要传递这些（：=）数据结构，但它们恢复了Atkey演示文稿的强大功能。
另一方面，Atkey演示文稿还不够强大，无法恢复McBride版本的所有用途。 权力已被严格获得。
另一个好处是，McBride的索引monad显然是monad，它只是一个不同函数类别的monad。 它从(k -> *)到(k -> *)的函子类别上的endofunctors而不是从*到*的函子类别工作。
一个有趣的练习是弄清楚如何为索引化的comonads做McBride to Atkey转换。 我个人使用数据类型'At'作为McBride论文中的“关键”构造。 我实际上在ICFP 2013上走访了Bob Atkey，并提到我将他变成了“外套”。 他似乎明显感到不安。 这条线在我脑海中表现得更好。 =）
果园
最后，第三个被称为“索引monad”的索赔人是Dominic Orchard，他使用类型级monoid将索引粉碎到一起。 我没有详细介绍施工细节，而只是简单地链接到这个话题：
http://www.cl.cam.ac.uk/~dao29/ixmonad/ixmonad-fita14.pdf
作为一个简单的场景，假设你有一个状态monad。 状态类型是一个复杂的大型状态，但所有这些状态都可以分成两组：红色和蓝色状态。 只有当前状态为蓝色状态时，此单子中的某些操作才有意义。 其中一些将保持蓝色状态（ blueToBlue ），而另一些则会使状态blueToRed红色（ blueToRed ）。 在一个普通的monad中，我们可以写
blueToRed :: State S ()
blueToBlue :: State S ()
foo :: State S ()
foo = do blueToRed
blueToBlue
由于第二个动作需要蓝色状态，因此触发运行时错误。 我们想要防止这种静态。 索引单子实现了这个目标：
data Red
data Blue
-- assume a new indexed State monad
blueToRed :: State S Blue Red ()
blueToBlue :: State S Blue Blue ()
foo :: State S ?? ?? ()
foo = blueToRed `ibind` _ ->
blueToBlue -- type error
由于blueToRed （ Red ）的第二个索引不同于blueToBlue （ Blue ）的第一个索引， blueToBlue会触发类型错误。
作为另一个例子，对于带索引的monad，你可以允许状态monad改变其状态的类型，例如你可以拥有
data State old new a = State (old -> (new, a))
你可以使用上面的方法来构建一个静态类型的异构堆栈。 操作会有类型
push :: a -> State old (a,old) ()
pop :: State (a,new) new a
作为另一个例子，假设你想要一个不允许文件访问的限制IO monad。 你可以使用例如
openFile :: IO any FilesAccessed ()
newIORef :: a -> IO any any (IORef a)
-- no operation of type :: IO any NoAccess _
通过这种方式，具有IO ... NoAccess ()类型的动作可以静态保证为无文件访问。 相反， IO ... FilesAccessed ()类型的操作可以访问文件。 拥有索引monad意味着您不必为限制IO构建单独的类型，这将需要在两种IO类型中复制每个非文件相关的函数。