什么是索引monad？
什么是索引monad和这个monad的动机？
我已经读过，它有助于跟踪副作用。 但型号签名和文件不会导致我到任何地方。
什么样的方式可以帮助跟踪副作用（或其他有效的例子）？
一如既往，人们使用的术语并不完全一致。 有各种各样的monads灵感，但严格说来，不是完全的概念。 术语“索引monad”是用来表征一个这样的概念的术语（包括“monadish”和“参数化的monad”（Atkey的名字））中的一个。 （如果你感兴趣的话，另一个这样的概念是Katsumata的“参数效应monad”，由一个幺半群索引，其中return是中立的，并且绑定积累在它的索引中。
首先，我们来检查种类。
IxMonad (m :: state -> state -> * -> *) 也就是说，“计算”（或“行动”，如果你喜欢，但我会坚持“计算”）的types，看起来像
m before after value
before, after :: state和value :: * 。 这个想法是捕捉手段与一个有一些可预测的国家概念的外部系统进行安全的交互。 一个计算的types告诉你before运行before状态必须是什么状态，运行after的状态是什么（和在*上的常规单子一样）计算产生的是什么types的value 。
通常的点点滴滴就像一个monad和state–就像玩多米诺骨牌一样。
ireturn :: a -> miia -- returning a pure value preserves state ibind :: mija -> -- we can go from i to j and get an a, thence (a -> mjkb) -- we can go from j to k and get ab, therefore -> mikb -- we can indeed go from i to k and get ab
由此产生的“Kleisli箭头”（产生计算的函数）的概念是
a -> mijb -- values a in, b out; state transition i to j
我们得到一个构图
icomp :: IxMonad m => (b -> mjkc) -> (a -> mijb) -> a -> mikc icomp fg = \ a -> ibind (ga) 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，则无法popupDVD，如果已经有DVD，则无法将DVD放入驱动器。 所以
data DVDDrive :: Bool -> Bool -> * -> * where -- Bool is "drive full?" DReturn :: a -> DVDDrive iia DInsert :: DVD -> -- you have a DVD DVDDrive True ka -> -- you know how to continue full DVDDrive False ka -- so you can insert from empty DEject :: (DVD -> -- once you receive a DVD DVDDrive False ka) -> -- you know how to continue empty DVDDrive True ka -- 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 = ka ibind (DInsert dvd j) k = DInsert dvd (ibind jk) 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 not）
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 ciia (:?) :: cija -> (a -> CommandIxMonad cjkb) -> CommandIxMonad cikb instance IxMonad (CommandIxMonad c) where ireturn = CReturn ibind (CReturn a) k = ka ibind (c :? j) k = c :? \ a -> ibind (ja) k
实际上，我们已经说过原始的Kleisli箭是什么（多米诺骨牌是什么），然后在它们上面build立了一个合适的“计算序列”的概念。
请注意，对于每个索引monad m ，“不变对angular线” mii是monad，但是一般来说， mij不是。 而且，值并没有编入索引，但是计算被编入索引，因此索引monad不仅仅是为其他类别实例化monad的通常想法。
现在，再看一下Kleisli箭头的types
a -> mijb
我们知道我们必须在状态i开始，并且我们预测任何延续将从状态j开始。 我们对这个系统了解很多！ 这不是一个危险的操作！ 当我们把DVD放在驱动器里时，它就进入了！ DVD驱动器在每个命令之后的状态都没有任何说法。
但是，当与世界互动时，这是不正确的。 有时你可能需要放弃一些控制，让世界做它喜欢的事情。 例如，如果你是一个服务器，你可能会为你的客户提供一个select，你的会话状态将取决于他们select什么。 服务器的“提供select”操作不能确定结果状态，但服务器应该能够继续进行。 在上述意义上，这不是一个“原始命令”，因此索引monad并不是模拟不可预测场景的好工具。
什么是更好的工具？
type f :-> g = forall state. f state -> g state class MonadIx (m :: (state -> *) -> (state -> *)) where returnIx :: x :-> mx flipBindIx :: (a :-> mb) -> (ma :-> mb) -- tidier than bindIx
可怕的cookies？ 不是真的，有两个原因。 其一，它看起来更像一个单子，因为它是一个单子，但是超过(state -> *)而不是* 。 二，如果你看一下Kleisli箭头的types，
a :-> mb = forall state. a state -> mb state
你得到的前提条件为 a和后置条件b的计算types，就像Good Good Hoare Logic中的一样。 程序逻辑中的断言在半个世纪之内穿过了Curry-Howard的对应关系，变成了Haskelltypes。 returnIx的types表示“你可以通过什么也不能做到任何后置条件”，这就是“跳过”的Hoare逻辑规则。 相应的组成是“;”的霍尔逻辑规则。
让我们看看bindIx的types，把所有的量词bindIx去。
bindIx :: forall i. mai -> (forall j. aj -> mbj) -> mbi
这些东西有相反的极性。 我们select初始状态i ，并且可以从i开始，具有后置条件a 。 世界select任何它所喜欢的中间状态，但它必须给出我们后置条件b所持有的证据，并且从这样的状态中，我们可以继续使b成立。 所以，按顺序，我们可以从状态i实现条件b 。 通过释放我们对“之后”状态的掌握，我们可以模拟不可预测的计算。
IxMonad和MonadIx都很有用。 交互式计算在改变状态方面的模型有效性，可预测性和不可预测性。 可以预见的东西很有价值，但是不可预测性有时也是生活中的事实。 那么希望这个答案给出了一些指标单子的指示，预测它们何时开始有用以及何时停止。
至less有三种方法来定义我知道的索引monad。
我将这些选项称为索引monadàla X ，其中X范围在计算机科学家Bob Atkey，Conor McBride和Dominic Orchard上，因此我倾向于这样想。 这些结构中的部分通过类别理论有更长远的辉煌的历史和更好的解释，但是我首先了解了这些结构与这些名称相关联，我试图让这个答案变得太深奥。
Atkey
Bob Atkey的索引monad的风格是使用2个额外的参数来处理monad的索引。
有了它，你可以得到其他答案中的定义：
class IMonad m where ireturn :: a -> miia ibind :: mija -> (a -> mjkb) -> mikb
我们也可以定义索引comonadsàla Atkey。 我实际上在lens代码库中获得了很多里程。
麦克布莱德
下一个monad的forms是conor McBride的定义从他的文章“Kleisli箭头的无耻的财富” 。 他改为使用索引的单个参数。 这使得索引monad定义有一个相当聪明的形状。
如果我们使用参数定义一个自然变换如下
type a ~> b = forall i. ai -> bi
那么我们可以写下McBride的定义
class IMonad m where ireturn :: a ~> ma ibind :: (a ~> mb) -> (ma ~> mb)
这个感觉和Atkey完全不同，但是它更像是一个普通的Monad，而不是在(m :: * -> *)上构build一个monad，我们把它build立在(m :: (k -> *) -> (k -> *) 。
有趣的是，你可以通过巧妙的数据types实际上恢复Atkey从McBride's中获得索引monad的风格，McBride以他独特的风格select说你应该读作“at key”。
data (:=) :: aij 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演示文稿的function。
另一方面，Atkey的performance还不够强大，无法恢复McBride版本的所有用途。 权力已被严格获得。
另一个好处是，麦克布莱德的索引monad显然是一个monad，它只是一个不同functor类别的monad。 它从(k -> *)到(k -> *)的函子类别上的endofunctors而不是从*到*的函子类别上工作。
一个有趣的练习是搞清楚如何做索引共同体的McBride到Atkey转换。 我个人在McBride的论文中使用了一个数据types“At”作为“关键”的构build。 我实际上是在ICFP 2013上走到了Bob Atkey，并提到我把他变成了“大衣”。 他似乎明显的不安。 这条线在我的脑海中performance得更好。 =）
果园
最后，第三个被称为“索引单子”的索赔人是Dominic Orchard，他使用types级别的monoid将索引粉碎。 我没有完成这个build筑的细节，而是简单地链接到这个话题上：
作为一个简单的场景，假设你有一个状态monad。 状态types是一个复杂的大型状态，但所有这些状态都可以分成两组：红色和蓝色状态。 只有在当前状态是蓝色状态的情况下，这个monad中的一些操作才有意义。 其中一些将保持蓝色（ blueToBlue ），而另一些将使状态变成红色（ blueToRed ）。 在一个普通的monad中，我们可以写
blueToRed :: State S () blueToBlue :: State S () foo :: State S () foo = do blueToRed blueToBlue
触发运行时错误，因为第二个动作需要蓝色状态。 我们想要防止这种静态。 索引monad实现了这个目标：
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会触发types错误。
作为另一个例子，对索引monad，你可以允许state monad改变它的状态types，例如你可以拥有
data State old new a = State (old -> (new, a))
你可以使用上面的build立一个静态types的异构堆栈的状态。 操作将有types
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 ()types的动作被静态地保证为文件访问自由。 相反， IO ... FilesAccessed ()types的操作可以访问文件。 拥有索引monad意味着您不必为受限IO构build单独的types，这将需要复制两个IOtypes中的每个非文件相关函数。
一个索引monad不是一个特定的monad，比如说像状态monad，而是一个带有额外types参数的monad概念的概括。
而“标准”一元值具有typesMonad m => ma ，索引monad中的值将是IndexedMonad m => mija其中， i和j是索引types，因此i是IndexedMonad m => mija的索引types计算和j在计算结束。 在某种程度上，你可以把i看作一种inputtypes，把j看作输出types。
以State为例，有状态计算State sa在整个计算过程中维护一个types为s的状态，并返回typesa a的结果。 索引版本IndexedState ija是一种状态计算，在计算过程中状态可以更改为不同的types。 初始状态具有typesi和状态，并且计算的结束具有typesj 。
在正常的monad上使用索引monad很less必要，但在某些情况下可以使用它来编码更严格的静态保证。
看看如何在依赖types中使用索引（例如，在agda中）可能很重要。 这可以解释索引如何帮助一般，然后将这个经验转化为单子。
索引允许在types的特定实例之间build立关系。 那么你可以推断一些价值观来确定这种关系是否成立。
例如（在agda中），你可以指定一些自然数与_<_相关，types告诉它们是哪个数字。 那么你可以要求某个函数被给予一个certificatem < n ，因为只有当函数正常工作 – 而且没有提供这样的见证程序将不会编译。
作为另一个例子，如果给予您select的语言足够的毅力和编译器支持，您可以编码该函数假定某个列表已sorting。
索引monad允许对某些依赖types的系统进行编码，以更精确地pipe理副作用。
