什么是索引monad？

Question

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

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

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

Answer 1

与以往一样,人们使用的术语并不完全一致.有各种各样的灵感来自单子 - 但严格来说 - 不是相当的概念.术语"索引monad"是用于表征一个这样的概念的术语中的一个(包括"monadish"和"参数化monad"(Atkey的名称)).(如果你感兴趣的话,另一个这样的概念是Katsumata的"参数效应monad",由一个幺半群索引,其中返回被中性索引并且绑定在其索引中累积.)

首先,让我们检查种类.

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

也就是说,"计算"的类型(或"动作",如果你愿意,但我会坚持"计算"),看起来像

m before after value

在哪里before, after :: state和value :: *.我们的想法是捕获与具有一些可预测的状态概念的外部系统安全交互的方法.计算的类型告诉你before它运行状态必须是什么,它运行的状态是after什么(和常规monad一样*)value计算产生什么类型的s.

通常的点点*滴滴就像单子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()
{g(); h()}; 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注释)

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说,"你可以实现持有,只是什么都不做任何后置条件",这是"跳过"的霍尔逻辑规则.相应的组合是";"的Hoare Logic规则.

让我们通过查看bindIx所有量词的类型来完成.

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

这些forall具有相反的极性.我们选择初始状态i,并且可以从i后置条件开始计算a.世界选择j它喜欢的任何中间状态,但它必须向我们提供后置条件b所持有的证据,并且从任何这样的状态,我们可以继续b保持.所以,按顺序,我们可以b从国家实现条件i.通过释放我们对"后"状态的控制,我们可以模拟不可预测的计算.

这两个IxMonad和MonadIx是有用的.交互式计算的模型有效性分别相对于改变状态,可预测和不可预测.可预测性在获得它时是有价值的,但不可预测性有时是生活中的事实.那么,希望这个答案可以说明索引monad是什么,预测它们何时开始有用以及何时停止.

Answer 2

我知道至少有三种方法来定义索引monad.

我将这些选项称为索引 monadàlaX,其中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àlaAtkey.实际上,我从lens代码库中获得了很多里程.

麦克布莱德

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

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

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

然后我们可以把McBride的定义写下来

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

这感觉与Atkey的不同,但它感觉更像是一个普通的Monad,而不是建立一个monad (m :: * -> *),我们建立它(m :: (k -> *) -> (k -> *).

有趣的是,你可以通过使用聪明的数据类型从McBride's恢复Atkey的索引monad样式,McBride以其独特的风格选择说你应该读作"关键".

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的索引monad显然是monad,它只是一个不同的functor类别的monad.它endofunctors工作过的函子类别从(k -> *)到(k -> *),而不是仿函数从类别*到*.

一个有趣的练习是弄清楚如何为索引的comonads进行McBride到Atkey的转换.我个人在McBride的论文中使用数据类型'At'作为"关键"构造.我实际上走到了ICFP 2013的鲍勃·阿斯基(Bob Atkey)那里,并提到我把他翻过来让他变成了"外套".他似乎明显不安.这条线在我的头脑中发挥得更好.=)

果园

最后,第三个被广泛引用的"索引monad"名称的索赔人归因于Dominic Orchard,他在那里使用类型级别的monoid来粉碎索引.我只是链接到这个话题,而不是详细介绍构造:

http://www.cl.cam.ac.uk/~dao29/ixmonad/ixmonad-fita14.pdf

Answer 3

作为一个简单的场景,假设你有一个状态monad.状态类型是一个复杂的大型,但所有这些状态可以分为两组:红色和蓝色状态.只有当前状态为蓝色状态时,此monad中的某些操作才有意义.其中,有些将保持状态blue(blueToBlue),而其他将使状态为red(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

被触发A型错误,因为所述第二折射率blueToRed(Red)从所述第一折射率不同blueToBlue(Blue).

作为另一个例子,使用索引monad,你可以允许状态monad改变其状态的类型,例如你可以拥有

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,例如,状态monad,而是monad概念的一种泛化,具有额外的类型参数.

而"标准"monadic值具有类型Monad m => m a索引monad中的值将是IndexedMonad m => m i j a其中i和j是索引类型,因此这i是在monadic计算开始时和计算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允许编码某些依赖类型系统,以更精确地管理副作用.