什么是索引化Monad？

Question

什么是索引化Monad？

haskellmonads

103

什么是索引化Monad，以及引入这种monad的动机是什么？

我看到有人说它有助于跟踪副作用。但是类型签名和文档并没有指导我怎样使用。

有没有关于如何使用该monad来跟踪副作用（或者其他有效的例子）的示例？

- Sibi

5个回答

50

我知道至少有三种定义带索引单子的方法。

我将这些选项称为“基于Bob Atkey、Conor McBride和Dominic Orchard的索引单子”，因为这是我想到他们的方式。这些构造的某些部分具有更悠久的历史，并通过范畴论提供了更好的解释，但我最初是通过这些名字学习到它们的，并且我试图让这个答案不太深奥。

Atkey

Bob Atkey的索引单子风格是使用两个额外的参数来处理单子的索引。

这样，您就可以得到其他答案中提到的定义：

class IMonad m where
  ireturn  ::  a -> m i i a
  ibind    ::  m i j a -> (a -> m j k b) -> m i k b

我们还可以按照Atkey的方式定义索引余单子。我实际上从这些在lens代码库中获得了很多收益。

麦克布莱德

下一种形式的索引单子是Conor McBride在他的论文"Kleisli Arrows of Outrageous Fortune"中定义的。他使用单个参数来表示索引。这使得索引单子的定义具有相当巧妙的形式。

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

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 - > *）的函子范畴上工作，而不是从*到*的函子范畴上。

一个有趣的练习是找出如何将McBride转换为Indexed comonads Atkey版本。我个人使用一个名为“At”的数据类型来构建McBride论文中的“at key”构造。我实际上走到了Bob Atkey面前，在2013年ICFP会议上提到我把他变成了“Coat”。他似乎非常不安。这句话在我的脑海中表现得更好。=)

Orchard

最后，第三个更不常见的声称为“indexed monad”的是Dominic Orchard，他使用类型级单子来组合索引。而不是通过构造细节，我只会简单地链接到这个演讲：

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

- Edward Kmett

1

我的理解是，Orchard的单子与Atkey的单子是等价的。因为我们可以通过取Endomorphism幺半群从前者到达后者，通过在状态转换中使用CPS编码幺半群附加操作来倒退。 - András Kovács

这对我来说听起来很合理。 - Edward Kmett

话虽如此，根据他在ICFP 2013对我说的一些话，我相信Orchard打算让他的类型族表现得像一个真正的幺半群，而不是一个任意的范畴，其中一些箭头无法连接，因此故事可能比这更复杂，因为Atkey的构造使您可以轻松地限制某些Kleisli操作与其他操作的连接 - 在很多方面，这正是它和McBride版本的关键所在。 - Edward Kmett

2

对“仔细阅读ibind”进行扩展：引入类型别名Atkey m i j a = m (a := j) i。将其用作Atkey定义中的m，可以恢复我们搜索的两个签名：ireturnAtkin :: a -> m (a := i) i和ibindAtkin :: m (a := j) i -> (a -> m (b := k) j) -> m (b := k) i。第一个通过组合获得：ireturn . V。第二个通过（1）通过模式匹配构建函数forall j. (a := j) j -> m (b := k) j，然后将恢复的a传递给ibindAtkin的第二个参数来实现。 - WorldSEnder

24

作为一个简单的场景，假设你有一个状态单子。状态类型是一个复杂的大型状态，但所有这些状态可以分成两组：红色和蓝色状态。这个单子里的一些操作只有在当前状态是蓝色状态时才有意义。其中一些将保持蓝色状态（blueToBlue），而其他一些将使状态变为红色（blueToRed）。在常规单子中，我们可以编写以下代码。

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 单子，不允许文件访问。您可以使用例如：

openFile :: IO any FilesAccessed ()
newIORef :: a -> IO any any (IORef a)
-- no operation of type :: IO any NoAccess _

这样，类型为IO ... NoAccess ()的操作在静态上得到了保证，不会访问文件。相反，类型为IO ... FilesAccessed ()的操作可以访问文件。使用索引化单子意味着您不必为受限制的IO构建单独的类型，这将需要在两种IO类型中重复每个非文件相关的函数。

- chi

19

一个索引化的单子并不像状态单子一样是一个具体的单子，而是单子概念的一种泛化形式，具有额外的类型参数。

与“标准”单子值具有类型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。

在正常单子上使用索引化单子很少是必要的，但在某些情况下可用于编码更严格的静态保证。

- shang

5

可能需要看一下如何在依赖类型中使用索引（例如在Agda中）是很重要的。这可以解释索引如何在一般情况下有所帮助，然后将这种经验转化为单子。

索引允许建立类型的特定实例之间的关系。然后您可以推理出某些值来确定该关系是否成立。

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

另一个例子是，通过足够的毅力和编译器对所选语言的支持，您可以编码函数假定某个列表已排序。

索引单子允许编码部分依赖类型系统所做的事情，以更精确地管理副作用。

- Sassa NF

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- pigworker · Accepted Answer

术语并不是完全一致的。有许多受到单子启发但严格来说不太一样的概念。"索引单子"（indexed monad）是其中之一，还有其他一些术语，比如"单子般的"（monadish）和"参数化单子"（Atkey 给它们起的名字），用来描述这种概念。如果您感兴趣，另一种类似的概念是 Katsumata 的 "参数效应单子"（parametric effect monad），以单子为索引，其中返回值是中性的，而 bind 在其索引中累积。

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

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

也就是说，一个“计算”（或者如果你愿意的话，可以叫它“动作”，不过我会继续使用“计算”这个词），的类型看起来像是

m before after value

其中 before, after :: state 且 value :: *。该想法是捕捉与具有某些可预测状态的外部系统安全交互的方法。计算的类型告诉您运行之前状态必须是什么，运行后状态将是什么以及（就像常规 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，则无法再插入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箭头（一个“骨牌”）是什么，然后在其上构建了一个合适的“计算序列”的概念。

请注意，对于每个索引单子m，"无变化对角线" m i i 是一个单子，但一般情况下，m i j 不是单子。此外，值不是索引的，而是计算被索引的，因此索引单子不仅仅是为某些其他类别实例化的单子的通常想法。

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

a -> m i j b

我们知道必须处于状态i才能开始，并且我们预测任何继续都将从状态j开始。我们对这个系统了解很多！这不是一项冒险的操作！当我们把DVD放入驱动器时，它会进去！DVD驱动器在每个命令后不会发表任何声明。

但是，在与世界互动时通常情况下并非如此。有时您可能需要放弃一些控制权，让世界做它想做的事情。例如，如果你是一个服务器，你可能会给客户端提供选择，你的会话状态将取决于他们的选择。服务器的“提供选择”操作并不确定结果状态，但服务器应该能够继续进行。它不是上述意义上的“原始命令”，因此索引单子不是建模不可预测情况的好工具。

什么是更好的工具？

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

吓人的饼干？并不是，有两个原因。首先，它看起来更像单子的样子，因为它就是一个单子，但是作用于(state -> *)而不是*。其次，如果你看一下Kleisli箭头的类型。

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

通过一个前提条件a和后置条件b，你可以获得计算类型，就像在Good Old Hoare Logic中一样。程序逻辑中的断言花费了不到半个世纪的时间来跨越Curry-Howard对应关系，并成为Haskell类型。 returnIx的类型表明：“只需什么都不做即可实现任何保持的后置条件”，这是“skip”的Hoare Logic规则。相应的组合是“；”的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成立。因此，按顺序，我们可以从状态i实现条件b。通过释放对“之后”状态的掌握，我们可以建模不可预测的计算。

IxMonad和MonadIx都很有用。它们分别模拟与更改状态相关的交互式计算的有效性，包括可预测和不可预测的情况。如果可以预测，预测性是非常有价值的，但不可预测性有时也是生活的事实。希望这个答案能够预示什么是索引单子，以及它们何时开始有用，何时停止。