Haskell:常见的Corecursive谬误

Question

所以今晚我正在考虑一个图形距离算法,并在我开车时想到了这个:

module GraphDistance where
import Data.Map

distance :: (Ord a) => a -> Map a [a] -> Map a Int
distance a m = m' 
  where m' = mapWithKey d m
        d a' as = if a == a' then 0 else 1 + minimum (Prelude.map (m'!) as)

起初,我为自己感到骄傲,因为它看起来很优雅.但后来我意识到它不起作用 - 核心运行可能会陷入循环中.

我不得不编码来说服自己:

ghci> distance 1 $ fromList [(0,[1]),(1,[0,2]),(2,[1,3]),(3,[2])]
fromList [(0,1),(1,0),(2,^CInterrupted.

但现在我觉得我已经考虑过了.

在处理我可以阅读的核心数据时是否有常见错误和反模式的列表,所以我可以训练我的大脑进行核心思考？经验训练我很好地思考非核心数据,但如果可以的话,我想从别人的错误中吸取教训.

Answer 1

好吧,在处理corecursive数据时,实际上只有一个基本错误,那就是不小心使用递归!

Corecursion意味着在某种意义上数据是以递增方式生成的.你的图形距离函数在这里是有启发性的,因为它似乎应该工作,所以想想增量部分应该在哪里:起点是从节点到自身的距离0,否则比自己的最小距离大一个近邻.因此,我们希望每个距离值都是递增的,这意味着我们需要它们本身适当地是自动的.

然后,由于(+)和minimum:的组合发生了问题的递归,当找到最小值时,1总是会小于1 + n,而不需要担心什么n是...但是没有办法比较Ints而不计算整个值.

简而言之,该算法希望能够仅根据需要比较(1 +)应用的次数0; 也就是说,它需要使用"零"和"后继"定义的惰性自然数.

看吧:

data Nat = Z | S Nat

natToInt :: Nat -> Int
natToInt Z = 0
natToInt (S n) = 1 + natToInt n

instance Show Nat where show = show . natToInt

instance Eq Nat where
    Z == Z = True
    (S n1) == (S n2) = n1 == n2
    _ == _ = False

    Z /= Z = False
    (S n1) /= (S n2) = n1 /= n2
    _ /= _ = True


instance Ord Nat where
    compare Z Z = EQ
    compare Z (S _) = LT
    compare (S _) Z = GT
    compare (S n1) (S n2) = compare n1 n2

然后在GHCi中:

> distance 1 $ fromList [(0,[1]),(1,[0,2]),(2,[1,3]),(3,[2])]
fromList [(0,1),(1,0),(2,1),(3,2)]

证明您的算法有效^[0] ; 你的实现是不正确的.

现在,作为一个细微的变化,让我们将您的算法应用于不同的图形:

> distance 1 $ fromList [(0,[1]),(1,[0]),(2,[3]),(3,[2])]

......我们期待这件事做什么？节点1到节点2或3的距离是多少？

在GHCi中运行它有明显的结果:

fromList [(0,1),(1,0),(2,^CInterrupted.

然而,该算法在该图上正确工作.你能看到问题吗？为什么它挂在GHCi？

总之,您需要清楚地区分两种不能自由混合的形式:

• 懒惰的,可能是无限的数据,是生成的
• 有限数据,递归消耗

两种形式都可以以结构无关的方式进行转换(例如,map两者都适用于有限列表和无限列表).Codata可以通过核心递归算法逐步消耗; 数据可以递归生成,受递归算法的限制.

你不能做的是递归地消费codata(例如,左折叠无限列表)或者生成数据(由于懒惰而在Haskell中很少见).

[0]:实际上,它会在某些输入上失败(例如,某些断开连接的图形),但这是一个不同的问题.