什么是索引单子？

Question

indexed monad 是什么以及这个 monad 的动机？

我读到它有助于跟踪副作用。但是类型签名和文档并没有把我带到任何地方。

什么是它如何帮助跟踪副作用的示例（或任何其他有效示例）？

Answer 1

与以往一样，人们使用的术语并不完全一致。有各种各样的灵感来自单子，但严格来说并不完全是概念。术语“indexed monad”是用于描述一个这样的概念的许多术语之一（包括“monadish”和“parameterized monad”（Atkey 的名字））。 （如果您感兴趣，另一个这样的概念是 Katsumata 的“参数效应单子”，由一个幺半群索引，其中 return 是中性索引的，并且 bind 在其索引中累积。）

首先，让我们检查一下种类。

IxMonad (m :: state -> state -> * -> *)

也就是说，“计算”（或“动作”，如果您愿意，但我会坚持使用“计算”​​）的类型，看起来像

m before after value

before, after :: state 和 value :: *。这个想法是捕捉与具有一些可预测状态概念的外部系统安全交互的方法。计算的类型告诉你它运行的状态必须是before，它运行的状态将是after，以及（就像* 上的常规单子一样）计算产生的values 的类型。

通常的点点滴滴是*-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，“无变化对角线”m i i 是一个 monad，但一般来说，m i j 不是。此外，值不被索引，但计算被索引，因此索引 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

可怕的饼干？不是真的，有两个原因。第一，它看起来更像是一个 monad，因为它是一个 monad，但在 (state -> *) 而不是 * 上。二，如果你看一下 Kleisli 箭头的类型，

a :-> m b   =   forall state. a state -> m b state

您会得到具有 前置条件 a 和后置条件 b 的计算类型，就像在 Good Old Hoare Logic 中一样。程序逻辑中的断言用了不到半个世纪的时间来跨越 Curry-Howard 对应关系并成为 Haskell 类型。 returnIx 的类型表示“您可以通过什么都不做来实现任何成立的后置条件”，这是“跳过”的霍尔逻辑规则。对应的组合是“;”的霍尔逻辑规则。

让我们看看bindIx的类型，把所有的量词都放进去。

bindIx :: forall i. m a i -> (forall j. a j -> m b j) -> m b i

这些foralls 极性相反。我们选择初始状态i，计算可以从i开始，后置条件a。世界选择它喜欢的任何中间状态j，但它必须给我们证明后置条件b 成立，并且从任何这样的状态，我们可以继续使b 成立。因此，按顺序，我们可以从状态i 实现条件b。通过释放对“之后”状态的控制，我们可以模拟不可预测的计算。

IxMonad 和 MonadIx 都很有用。这两种模型的交互计算的有效性分别是关于状态变化的，可预测的和不可预测的。当你能得到它时，可预测性是有价值的，但不可预测性有时是生活中的事实。那么，希望这个答案能够说明索引 monad 是什么，预测它们何时开始有用以及何时停止。

Answer 2

据我所知，定义索引 monad 的方法至少有三种。

我将这些选项称为indexed monads à 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。我实际上从那些in the lens codebase 中获得了很多里程。

麦克布莱德

索引 monad 的下一种形式是 Conor McBride 在他的论文 "Kleisli Arrows of Outrageous Fortune" 中的定义。他改为使用单个参数作为索引。这使得带索引的 monad 定义具有相当巧妙的形状。

如果我们使用如下参数定义自然变换

type a ~> b = forall i. a i -> b i 

那么我们可以把麦克布莱德的定义写成

class IMonad m where
  ireturn :: a ~> m a
  ibind :: (a ~> m b) -> (m a ~> m b)

这感觉与 Atkey 的完全不同，但感觉更像是一个普通的 Monad，而不是在 (m :: * -> *) 上构建一个 monad，我们在 (m :: (k -> *) -> (k -> *) 上构建它。

有趣的是，您实际上可以通过使用一种巧妙的数据类型从 McBride 恢复 Atkey 的索引 monad 风格，McBride 以其独特的风格选择说您应该将其读为“at key”。

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 的索引单子显然是单子，它只是不同函子类别上的单子。它适用于从(k -> *) 到(k -> *) 的函子类别的内函子，而不是从* 到* 的函子类别。

一个有趣的练习是弄清楚如何为索引 comonads 进行 McBride 到 Atkey 的转换。我个人将数据类型“At”用于 McBride 论文中的“关键”结构。实际上，我在 2013 年 ICFP 上走到 Bob Atkey 面前，提到我把他翻了个身，让他变成了一件“外套”。他似乎很不安。这条线在我脑海中表现得更好。 =)

果园

最后，第三个被称为“indexed monad”的很少被引用的声明是由于 Dominic Orchard，他使用类型级别的 monoid 将索引粉碎在一起。我不会详细介绍构建的细节，而是简单地链接到这个演讲：

https://github.com/dorchard/effect-monad/blob/master/docs/ixmonad-fita14.pdf

Answer 3

作为一个简单的场景，假设您有一个状态单子。状态类型是一个复杂的大状态，但所有这些状态都可以分为两组：红色和蓝色状态。仅当当前状态为蓝色状态时，此 monad 中的某些操作才有意义。其中，一些将状态保持为蓝色（blueToBlue），而另一些将状态设置为红色（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) 的第一个索引不同，触发了类型错误。

作为另一个例子，使用索引单子，您可以允许状态单子更改其状态的类型，例如你可以有

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 类型中复制每个与文件无关的函数。

Answer 4

索引 monad 不是特定的 monad，例如 state monad，而是带有额外类型参数的 monad 概念的一种概括。

而“标准”单子值的类型为Monad m => m a，索引单子中的值将是IndexedMonad m => m i j a，其中i 和j 是索引类型，因此i 是索引的类型一元计算的开始和计算结束时的j。在某种程度上，您可以将i 视为一种输入类型，将j 视为输出类型。

以State 为例，有状态计算State s a 在整个计算过程中保持s 类型的状态，并返回a 类型的结果。索引版本IndexedState i j a 是一种有状态计算，其中状态可以在计算期间更改为不同的类型。初始状态的类型为i，状态和计算结束的类型为j。

很少需要在普通 monad 上使用索引 monad，但在某些情况下可以使用它来编码更严格的静态保证。

Answer 5

看看索引是如何在依赖类型中使用的可能很重要（例如在agda中）。这可以解释索引一般如何提供帮助，然后将这种经验转化为 monad。

索引允许在特定类型实例之间建立关系。然后你可以推理一些值来确定这种关系是否成立。

例如（在 agda 中）您可以指定一些自然数与 _<_ 相关，并且类型告诉它们是哪些数字。然后您可以要求为某个函数提供m < n 的见证，因为只有这样该函数才能正常工作 - 如果不提​​供这样的见证，程序将无法编译。

作为另一个例子，如果你选择的语言有足够的毅力和编译器支持，你可以对函数进行编码，假设某个列表已排序。

索引 monad 允许对依赖类型系统所做的一些事情进行编码，以更精确地管理副作用。