什么是索引monad？ [英] What is indexed monad?

问题描述

什么是索引monad 和这个单子的动机？

我读过它有助于跟踪副作用。但是类型签名和文档不会让我到任何地方。

这将是一个如何帮助跟踪副作用（或任何其他有效例如）？

解决方案

以前，人们使用的术语并不完全一致。有许多灵感来源于单子，但严格说来并不完全是概念。术语索引monad是用于表征一个这样的概念的术语（包括monadish和参数化monad（Atkey的名字））中的一个。 （另一个这样的概念，如果你感兴趣的话，是Katsumata的参数效应monad，由一个幺半群索引，其中return是中立的，并且绑定积累在它的索引中。）

<首先，让我们来检查种类。

  IxMonad（m :: state  - >状态 - > *  - > ; *）
  

也就是说，计算（或动作更喜欢，但我会坚持使用计算​​），看起来像

  m之前值
  

其中在:: state 和之前:: * 。这个想法是捕捉与具有一些可预测状态概念的外部系统进行安全交互的手段。计算的类型告诉你，在它运行之前，状态必须是，在运行之后状态是，就像 * 中的常规单子一样）计算产生的值的类型。

通常的元素和元素是 * - 就像monad和 state - 类似玩多米诺骨牌。

  ireturn :: a  - > m i我a  - 返回一个纯粹的值保存状态
 ibind :: m i j a  - > - 我们可以从i到j并得到a，因此
（a  - > m j k b） - 我们可以从j到k并得到b，因此
  - > mikb  - 我们确实可以从我到k并获得ab 
  

Kleisli箭头 （产生计算的函数）是

  a  - > m i j b  - 值a in，b out;我们转换到j 
  

，并且我们得到一份作文

  icomp :: IxMonad m => （b→m j k c）→> （a  - > m i j b） - > a  - > m i k c 
 icomp f g = \ 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，则无法弹出DVD，如果已经有DVD，则无法将DVD放入驱动器。所以

  data DVDDrive :: Bool  - >布尔 - > *  - > *其中 -  Bool是驱动器已满？ 
 DReturn :: a  - > DVDDrive i我a 
 DInsert :: DVD  - > - 您有DVD 
 DVDDrive True k a  - > - 你知道如何继续完整
 DVDDrive False ka  - 所以你可以插入空
 DEject ::（DVD  - >  - 一旦你收到DVD 
 DVDDrive False ka） - > - 你知道如何继续清空
 DVDDrive True ka  - 所以你可以弹出完整的
 
实例IxMonad DVDDrive其中 - 将这些方法放在需要的地方
 ireturn = DReturn  - 所以这是另一个地方$ b $ ibind（DReturn a）k = ka 
 ibind（DInsert dvd j）k = DInsert dvd（ibind jk）
 ibind（DEject j）k =项目j $ \ dvd  - > ibind（j dvd）k 
  

有了这个，我们可以定义原始 p>

  dInsert :: DVD  - > DVDDrive False True（）
 dInsert dvd = DInsert dvd $ DReturn（）
 
 dEject :: DVDrive True False DVD 
 dEject = DEject $ \ 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  - 哎！ 
  

或者，您可以直接定义一个原始命令



  data DVDCommand :: Bool  - >布尔 - > *  - > *其中
 InsertC :: DVD  - > DVDCommand False True（）
 EjectC :: DVDCommand True False DVD 
  

然后实例化generic模板



 数据CommandIxMonad ::（状态 - >状态 - > *  - > *） - > 
状态 - >状态 - > *  - > *其中
 CReturn :: a  - > CommandIxMonad c我是
（：？）:: c i j a  - > （a  - > CommandIxMonad c j k b） - > 
 CommandIxMonad cikb 
 
实例IxMonad（CommandIxMonad c）其中
 ireturn = CReturn 
 ibind（CReturn a）k = ka 
 ibind（c：？j ）k = c：？ \ a  - > ibind（ja）k 
  

实际上，我们已经说过原始的Kleisli箭是什么dominois），然后在它们上面建立了一个合适的计算顺序概念。



请注意，对于每个索引monad m ，不改变对角线 mii 是一个monad，但通常情况下， mij 不是。此外，值并没有被编入索引，但计算被编入索引，因此索引monad不仅仅是monad为其他类别实例化的通常想法。

现在，再看看Kleisli箭头的类型

  a  - > mijb 
  

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

但是，当与世界进行交互时，通常情况并非如此。有时你可能需要放弃一些控制，让世界做它喜欢的事情。例如，如果您是服务器，您可能会为您的客户提供选择，而您的会话状态将取决于他们选择的内容。服务器的提供选择操作不能确定结果状态，但服务器应该能够继续进行。它不是上述意义上的原始命令，因此索引monad并不是一种很好的工具来模拟不可预知的情况。

什么是一个更好的工具？

  type f： - > g =全部状态。 f状态 - > g状态
 
 class MonadIx（m ::（state  - > *） - >（state  - > *））其中
 returnIx :: x： - > m x 
 flipBindIx ::（a： - > m b） - > （m a： - > m b） - 比bindIx更清晰
  

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

  a： - > m b =全部状态。状态 - > mb state 
  

您可以使用前提条件获得计算类型 a 和后置条件 b ，就像Good Good Hoare Logic中的一样。程序逻辑中的断言在半个世纪之内穿过了Curry-Howard的对应关系并成为Haskell类型。 returnIx 类型表示你可以实现任何后置条件，只要不做任何事情，这就是跳过的Hoare逻辑规则。相应的组合是;的Hoare逻辑规则。

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

  bindIx :: forall i。 m a i  - > （所有j，a j  - > m b j） - > m 
  

这些 forall s的极性相反。我们选择初始状态 i ，并且可以从 i 开始，后置条件为 a 。世界选择了它所喜欢的任何中间状态 j ，但它必须为我们提供后验条件 b 成立的证据，任何这样的状态，我们都可以继续让 b 成立。所以，按顺序，我们可以从状态 i 实现条件 b 。通过释放对后状态的控制，我们可以对不可预测的计算进行建模。

c $ c>和 MonadIx 很有用。交互式计算在改变状态方面的模型有效性，分别可预测和不可预测。可以预见的东西很有价值，但不可预测性有时也是生活中的事实。然后，希望这个答案给出了一些指标monads的指示，预测它们何时开始有用以及何时停止。

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)?

解决方案

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 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.

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

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

and we get a composition

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

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)

or, in comedy fake C/Java/whatever,

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

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

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'

but not the physically impossible

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

and then instantiate the generic template

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

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.

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

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.

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.

What's a better tool?

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

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

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 ";".

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

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.

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.

这篇关于什么是索引monad？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！