haskell - 右紧 ArrowLoop 定律

Question

根据 Control.Arrow 文档，对于许多 monads(那些 >>= 操作是严格的)instance MonadFix m => ArrowLoop (Kleisli m)不满足 loop (f >>> first h) = loop f >>> h 所要求的右紧律 ( ArrowLoop )类(class)。为什么呢？

Answer 1

这是一个多方面的问题，有几个不同的角度，它可以追溯到 Haskell 中的值递归 ( mfix/mdo )。见 here背景信息。我将在这里详细讨论右紧缩问题。

mfix 的右拧紧

这是 mfix 的右拧紧属性:

mfix (λ(x, y). f x >>= λz. g z >>= λw. return (z, w))
    = mfix f >>= λz. g z >>= λw. return (z, w)

这是图片形式:



虚线显示“打结”发生的位置。这与问题中提到的定律基本相同，只是用 mfix 表示。和值递归。如 Section 3.1 of this work所示，对于带有严格绑定(bind)运算符的 monad，您总是可以编写一个表达式来区分此等式的左侧和右侧，从而使此属性失败。 (有关 Haskell 中的实际示例，请参见下文。)

当一个箭头是通过 Kleisli 构造从一个带有 mfix 的 monad 创建时，对应 loop运算符以相同的方式使相应的属性失败。

领域理论和近似

在域理论术语中，失配将始终是近似值。

也就是说，左侧总是比右侧更不明确。 (更准确地说，在 PCPO 的域中，lhs 将低于 rhs，这是我们用于 Haskell 语义的典型域。)实际上，这意味着右侧将更频繁地终止，并且在以下情况下是首选这是一个问题。同样，请参见 this 的第 3.1 节详情。

在实践中

这听起来可能很抽象，在某种意义上确实如此。更直观地，左侧有机会对自 g 以来产生的递归值进行操作。位于“循环”内，因此能够干扰定点计算。这是一个实际的 Haskell 程序来说明:

import Control.Monad.Fix

f :: [Int] -> IO [Int]
f xs = return (1:xs)

g :: [Int] -> IO Int
g [x] = return x
g _   = return 1

lhs = mfix (\(x, y) -> f x >>= \z -> g z >>= \w -> return (z, w))
rhs = mfix f >>= \z -> g z >>= \w -> return (z, w)

如果您评估 lhs它永远不会终止，而 rhs将按预期为您提供 1 的无限列表:

*Main> :t lhs
lhs :: IO ([Int], Int)
*Main> lhs >>= \(xs, y) -> return (take 5 xs, y)
^CInterrupted.
*Main> rhs >>= \(xs, y) -> return (take 5 xs, y)
([1,1,1,1,1],1)

我在第一种情况下中断了计算，因为它是非终止的。虽然这是一个人为的例子，但它是说明这一点的最简单方法。 (请参阅下面使用 mdo - 表示法呈现的此示例，这可能更易于阅读。)

示例 monad

的 monad 的典型例子不要满足这个规律包括 Maybe , List , IO ，或任何其他基于具有多个构造函数的代数类型的 monad。 的 monad 的典型例子做 满足这个规律的是 State和 Environment单子(monad)。见 Section 4.10用于总结这些结果的表格。

纯右收缩

注意右紧缩的“较弱”形式，其中函数 g上面的等式是纯的，遵循值递归定律:

mfix (λ(x, y). f x >>= λz. return (z, h z))
  = mfix f >>= λz. return (z, h z)

这与之前的定律相同， g = return . h .即 g不能执行任何效果。在这种情况下，无法像您预期的那样区分左侧和右侧。结果确实来自值递归公理。 (见 Section 2.6.3 证明。)本例中的图片如下所示:



这个属性来自滑动属性，这是值递归的非自然性的一个版本，并且被许多感兴趣的 monad 满足: Section 2.4 .

对 mdo 符号的影响

该法律的失败对 mdo notation 的影响是在 GHC 中设计的。翻译包括所谓的“分割”步骤，正是为了避免右收缩定律的失败。有些人认为这有点争议，因为 GHC 会自动选择段，基本上是应用右紧法。如果需要显式控制，GHC 提供 rec keyword将决定权留给用户。

使用 mdo -符号和显式 do rec ，上面的例子呈现
如下:

{-# LANGUAGE RecursiveDo #-}

f :: [Int] -> IO [Int]
f xs = return (1:xs)

g :: [Int] -> IO Int
g [x] = return x
g _   = return 1


lhs :: IO ([Int], Int)
lhs = do rec x <- f x
             w <- g x
         return (x, w)

rhs :: IO ([Int], Int)
rhs = mdo x <- f x
          w <- g x
          return (x, w)

人们可能会天真地期望 lhs和 rhs上面应该是一样的，但是由于右收缩律的失败，它们不是。和以前一样， lhs卡住了，而 rhs成功产生值:

*Main> lhs >>= \(x, y) -> return (take 5 x, y)
^CInterrupted.
*Main> rhs >>= \(x, y) -> return (take 5 x, y)
([1,1,1,1,1],1)

目视检查代码，我们看到递归只是针对函数 f ，这证明了由 mdo 自动执行的分段是合理的-符号。

如果 rec符号是首选，程序员需要把它放在最少的块中以确保终止。例如，上述 lhs 的表达式应该写成这样:

lhs :: IO ([Int], Int)
lhs = do rec x <- f x
         w <- g x
         return (x, w)

mdo -notation 负责解决这个问题，并将递归放置在最小块上，而无需用户干预。

Kleisli Arrows 失败

绕了这么长的一段路之后，现在让我们回到最初关于箭头对应定律的问题。类似于 mfix在这种情况下，我们也可以为 Kleisli 箭头构建一个失败的例子。事实上，上面的例子或多或少是直接翻译的:

{-# LANGUAGE Arrows #-}
import Control.Arrow

f :: Kleisli IO ([Int], [Int]) ([Int], [Int])
f = proc (_, ys) -> returnA -< (ys, 1:ys)

g :: Kleisli IO [Int] Int
g = proc xs -> case xs of
                 [x] -> returnA -< x
                 _   -> returnA -< 1

lhs, rhs :: Kleisli IO [Int] Int
lhs = loop (f >>> first g)
rhs = loop f >>> g

就像 mfix 的情况一样， 我们有:

*Main> runKleisli rhs []
1
*Main> runKleisli lhs []
^CInterrupted.

mfix右旋失败IO-monad 也阻止了 Kleisli IO箭头来自满足 ArrowLoop 中的右紧律实例。