什么是索引单子?

问题描述

什么是索引单子以及这个 monad 的动机?

What is indexed monad and the motivation for this monad?

我读过它有助于跟踪副作用.但是类型签名和文档并没有让我去任何地方.

I have read that it helps to keep track of the side effects. But the type signature and documentation doesn't lead me to anywhere.

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

What would be an example of how it can help to keep track of side effects (or any other valid example)?

推荐答案

一如既往，人们使用的术语并不完全一致.有各种受单子启发的概念，但严格来说，这并不是完全正确的概念.术语索引 monad"monadish"和参数化的monad"(Atkey的名称))是用来表征一个这样的概念的许多术语之一.(另一个这样的概念，如果你感兴趣的话，是 Katsumata 的参数效应 monad"，由一个幺半群索引，其中 return 被中性地索引并且绑定在其索引中累积.)

As ever, the terminology people use is not entirely consistent. There's a variety of inspired-by-monads-but-strictly-speaking-isn't-quite notions. The term "indexed monad" is one of a number (including "monadish" and "parameterised monad" (Atkey's name for them)) of terms used to characterize one such notion. (Another such notion, if you're interested, is Katsumata's "parametric effect monad", indexed by a monoid, where return is indexed neutrally and bind accumulates in its index.)

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

First of all, let's check kinds.

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

即计算"的类型(或动作"，如果您愿意，但我会坚持使用计算"​​)，看起来像

That is, the type of a "computation" (or "action", if you prefer, but I'll stick with "computation"), looks like

m before after value

where before, after :: state 和 value :: *.这个想法是捕捉与具有一些可预测状态概念的外部系统安全交互的方法.一个计算的类型告诉你它运行之前 必须是什么状态，它运行 after 之后的状态是什么(就像在 * 上的常规 monad>) 计算产生什么类型的value.

where before, after :: state and value :: *. The idea is to capture the means to interact safely with an external system that has some predictable notion of state. A computation's type tells you what the state must be before it runs, what the state will be after it runs and (like with regular monads over *) what type of values the computation produces.

通常的点点滴滴都是 *-wise 就像一个 monad 和 state-wise 就像玩多米诺骨牌一样.

The usual bits and pieces are *-wise like a monad and state-wise like playing dominoes.

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 箭头"的概念这样生成的(产生计算的函数)是

The notion of "Kleisli arrow" (function which yields computation) thus generated is

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 给我们一个类别

and, as ever, the laws exactly ensure that ireturn and icomp give us a category

      ireturn `icomp` g = g
      f `icomp` ireturn = f
(f `icomp` g) `icomp` h = f `icomp` (g `icomp` h)

或者，在喜剧中伪造 C/Java/任何东西，

or, in comedy fake C/Java/whatever,

      g(); skip = g()
      skip; f() = f()
{h(); g()}; f() = h(); {g(); f()}

何必呢?为规则"建模的互动.例如，如果驱动器中没有 DVD，则无法弹出；如果驱动器中已有 DVD，则无法将 DVD 放入驱动器.所以

Why bother? To model "rules" of interaction. For example, you can't eject a dvd if there isn't one in the drive, and you can't put a dvd into the drive if there's one already in it. So

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

有了这个，我们可以定义原始"命令

With this in place, we can define the "primitive" commands

dInsert :: DVD -> DVDDrive False True ()
dInsert dvd = DInsert dvd $ DReturn ()

dEject :: DVDrive True False DVD
dEject = DEject $  dvd -> DReturn dvd

其他人用 ireturn 和 ibind 组装而成.现在，我可以写(借用 do-notation)

from which others are assembled with ireturn and ibind. Now, I can write (borrowing 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!

或者，可以直接定义自己的原始命令

Alternatively, one can define one's primitive commands directly

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 箭头是什么(什么是多米诺骨牌")，然后构建了一个合适的计算序列"概念.超过他们.

In effect, we've said what the primitive Kleisli arrows are (what one "domino" is), then built a suitable notion of "computation sequence" over them.

请注意，对于每个索引的 monad m，对角线不变"m i i 是一个 monad，但一般来说 m i j 不是.此外，值没有被索引，但计算被索引，所以索引 monad 不仅仅是为其他类别实例化 monad 的通常想法.

Note that for every indexed monad m, the "no change diagonal" m i i is a monad, but in general, m i j is not. Moreover, values are not indexed but computations are indexed, so an indexed monad is not just the usual idea of monad instantiated for some other category.

现在，再看看克莱斯利箭的类型

Now, look again at the type of a Kleisli arrow

a -> m i j b

我们知道必须处于状态 i 才能开始，并且我们预测任何延续都将从状态 j 开始.我们对这个系统了解很多！这不是一个冒险的操作！当我们将 DVD 放入驱动器时，它就进去了！dvd 驱动器在每个命令之后的状态没有任何说明.

We know we must be in state i to start, and we predict that any continuation will start from state j. We know a lot about this system! This isn't a risky operation! When we put the dvd in the drive, it goes in! The dvd drive doesn't get any say in what the state is after each command.

但在与世界互动时，通常情况并非如此.有时，您可能需要放弃一些控制权，让世界随心所欲.例如，如果您是服务器，您可能会为您的客户端提供一个选择，而您的会话状态将取决于他们的选择.服务器的提供选择"操作不决定结果状态，但服务器应该能够继续进行.这不是原始命令".从上述意义上讲，因此索引 monad 并不是对不可预测场景建模的好工具.

But that's not true in general, when interacting with the world. Sometimes you might need to give away some control and let the world do what it likes. For example, if you are a server, you might offer your client a choice, and your session state will depend on what they choose. The server's "offer choice" operation does not determine the resulting state, but the server should be able to carry on anyway. It's not a "primitive command" in the above sense, so indexed monads are not such a good tool to model the unpredictable scenario.

什么是更好的工具?

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 -> *) 而不是 *>.二、如果你看一下克莱斯利箭的类型，

Scary biscuits? Not really, for two reasons. One, it looks rather more like what a monad is, because it is a monad, but over (state -> *) rather than *. Two, if you look at the type of a Kleisli arrow,

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

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

you get the type of computations with a precondition a and postcondition b, just like in Good Old Hoare Logic. Assertions in program logics have taken under half a century to cross the Curry-Howard correspondence and become Haskell types. The type of returnIx says "you can achieve any postcondition which holds, just by doing nothing", which is the Hoare Logic rule for "skip". The corresponding composition is the Hoare Logic rule for ";".

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

Let's finish by looking at the type of bindIx, putting all the quantifiers in.

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.通过释放我们对之后"的控制状态，我们可以对不可预测的计算进行建模.

These foralls have opposite polarity. We choose initial state i, and a computation which can start at i, with postcondition a. The world chooses any intermediate state j it likes, but it must give us the evidence that postcondition b holds, and from any such state, we can carry on to make b hold. So, in sequence, we can achieve condition b from state i. By releasing our grip on the "after" states, we can model unpredictable computations.

IxMonad 和 MonadIx 都很有用.交互式计算在状态变化方面的模型有效性，分别是可预测的和不可预测的.可预测性在您可以获得时很有价值，但不可预测性有时是生活中的事实.那么，希望这个答案给出了索引 monad 是什么的一些指示，预测它们什么时候开始有用，什么时候停止.

Both IxMonad and MonadIx are useful. Both model validity of interactive computations with respect to changing state, predictable and unpredictable, respectively. Predictability is valuable when you can get it, but unpredictability is sometimes a fact of life. Hopefully, then, this answer gives some indication of what indexed monads are, predicting both when they start to be useful and when they stop.

这篇关于什么是索引单子?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，WP2