正确收紧ArrowLoop法

Question

根据Control.Arrow文件,对于许多monad(>>=操作严格的那些),instance MonadFix m => ArrowLoop (Kleisli m)不符合课堂loop (f >>> first h) = loop f >>> h要求的权利紧缩法()ArrowLoop.为什么会这样？

Answer 1

这是一个具有多个不同角度的多方面问题,它可以追溯到Haskell中的值递归(mfix/ mdo).请参阅此处获取背景信息.我将在这里详细讨论正确的紧缩问题.

右键紧固mfix

这是正确紧缩的财产mfix:

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

这是图片形式:

虚线表示"打结"的位置.这基本上与问题中提到的法律相同,除非它以mfix值和递归的形式表达.如本作品的第3.1节所示,对于具有严格绑定运算符的monad,您始终可以编写一个表达式来区分此等式的左侧与右侧,从而使此属性失败.(请参阅下面的Haskell中的实际示例.)

当通过Kleadli构造从monad中创建箭头时mfix,相应的loop运算符以相同的方式失败相应的属性.

领域理论和近似

在域理论术语中,不匹配将始终是近似值.

也就是说,左手边的位置总是比右手边少.(更准确地说,lhs将低于rhs,在PCPOs领域,我们用于Haskell语义的典型域.)在实践中,这意味着右侧将更频繁地终止,并且在这是一个问题.再次,见第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-notation 进行此示例的渲染,这可能更容易阅读.)

示例monad

该单子的典型例子不符合这一规律包括Maybe,List,IO,或其他任何这是基于代数类型与多个构造单子.该单子的典型例子不符合这一规律是State和Environment单子.有关总结这些结果的表,请参见第4.10节.

纯正缩小

请注意,右上角的"弱"形式,其中g上述等式中的函数是纯粹的,遵循价值递归定律:

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

这与以前的法律相同,g = return . h.那是g无法发挥任何效果的.在这种情况下,没有办法像你期望的那样区分左手边和右手边.结果确实来自价值递归公理.(有关证明,请参阅第2.6.3节.)本案例中的图片如下所示:

这个属性来自滑动属性,它是值递归的dinaturality版本,并且已知许多感兴趣的monad满足:第2.4节.

对mdo-notation的影响

该法律的失败对GHC中如何设计mdo符号有影响.翻译包括所谓的"分割"步骤,以避免右缩法的失败.有些人认为有点争议,因为GHC会自动选择细分市场,主要是采用正确的法律.如果需要显式控制,GHC提供rec关键字以将决定留给用户.

使用mdo-notation和explicit 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-notation 自动执行的分段.

如果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情况下满足了正确的法律.