haskell - 什么是索引单子(monad)？

Question

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

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

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

Answer 1

与以往一样，人们使用的术语并不完全一致。有各种受单子(monad)启发的概念，但严格地说，这并不是完全正确的概念。术语“索引 monad”是用于表征这样一个概念的许多术语(包括“monadish”和“参数化 monad”(Atkey 的名称))之一。 (另一个这样的概念，如果你感兴趣，是 Katsumata 的“参数效应 monad”，由一个幺半群索引，其中 return 被中性地索引并且 bind 在其索引中累积。)
首先，让我们检查一下种类。

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

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

m before after value

哪里 before, after :: state和 value :: * .这个想法是捕捉与具有一些可预测状态概念的外部系统安全交互的方法。计算的类型告诉您状态必须是什么 before它运行，状态将是什么 after它运行(就像在 * 上的常规 monad 一样)什么类型的 value s 计算产生。
通常的点点滴滴是 * - 像单子(monad)一样明智和 state - 聪明的喜欢玩多米诺骨牌。

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 放入驱动器。所以

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 驱动器在每个命令之后的状态没有任何说明。
但在与世界互动时，通常情况并非如此。有时，您可能需要放弃一些控制权，让世界随心所欲。例如，如果您是服务器，您可能会为您的客户端提供一个选择，而您的 session 状态将取决于他们的选择。服务器的“提供选择”操作并不能确定结果状态，但无论如何服务器应该能够继续进行。它不是上述意义上的“原始命令”，因此索引 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

可怕的 cookies ？不是真的，有两个原因。一，它看起来更像一个 monad，因为它是一个 monad，但在 (state -> *)而不是 * .二、如果你看看克莱斯利箭的类型，

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

这些 forall s 具有相反的极性。我们选择初始状态 i ，以及可以从 i 开始的计算, 后置条件 a .世界选择任何中间状态 j它喜欢，但它必须给我们证明后置条件 b持有，并且从任何这样的状态，我们可以继续使 b拿着。因此，按顺序，我们可以达到条件 b来自 State i .通过释放对“之后”状态的控制，我们可以对不可预测的计算进行建模。
两者 IxMonad和 MonadIx有用。交互式计算在状态变化方面的模型有效性，分别是可预测的和不可预测的。可预测性在您可以获得时很有值(value)，但不可预测性有时是生活中的事实。那么，希望这个答案给出了索引 monad 是什么的一些指示，预测它们何时开始有用以及何时停止。