为什么使用头/尾代替模式匹配会使评估终止？

Question

作为练习,我试图定义一个ruler值

ruler :: (Num a, Enum a) => [a]

这对应于标尺功能

0,1,0,2,0,1,0,3,0,1,0,2,0,1,0,4,0,1,0,2...

其中n列表的第th个元素(假设第一个元素对应n=1)是2的最大幂,它均匀分割n.为了使它更有趣,我试图实现ruler而不必进行任何可分性测试.

使用辅助函数

interleave :: [a] -> [a] -> [a]

这简单地交替了两个给定列表中的元素,我想出了这个 - 但是它不起作用:

interleave :: [a] -> [a] -> [a]
interleave  (x:xs) (y:ys) = x : y : interleave xs ys
interleave  _      _      = []

ruler :: (Num a, Enum a) => [a]
ruler = foldr1 interleave . map repeat $ [0..]

main :: IO ()
main = print (take 20 ruler)

该程序最终耗尽所有堆栈空间.

现在,奇怪的是,如果我调整interleave它的读取的定义,该程序工作正常

interleave (x:xs) ys = x : head ys : interleave xs (tail ys)

即我不再在第二个参数上使用模式匹配.为什么使用head和tail在这里ruler终止 - 毕竟,模式匹配是相当防御的(我只评估列表脊柱的第一个元素,没有？).

Answer 1

您正在将foldr严格的组合函数应用于无限列表.

简而言之,您可以在此处查看此行为:

*Main> :t const
const :: a -> b -> a
*Main> :t flip seq
flip seq :: c -> a -> c
*Main> foldr1 const [0..]
0
*Main> foldr1 (flip seq) [0..]
^CInterrupted.

正如其他答案中所解释的那样,解决方案是使interleave懒惰.

更具体地说,这是发生的事情.首先我们解决foldr1,用以下内容替换每个:外部列表interleave:

foldr1 interleave [[0..], [1...], ...]
= interleave [0...] (interleave [1...] (...))

为了取得进展,第一个interleave想要在产生第一个值之前评估第二个参数.但是第二个想要评估它的第二个参数,依此类推.

使用惰性定义interleave,在评估第二个参数之前生成第一个值.特别是,在进一步评估内容之前,interleave [1...] (...)将评估1 : ...(这有助于第一个interleave进步).

Answer 2

不同之处在于模式匹配会强制脊椎中的第一个项目,head/tail而不是.

您可以使用延迟模式来实现相同的目标:

interleave  (x:xs) ~(y:ys) = x : y : interleave xs ys

注意~:这相当于定义y和ys使用head和tail.

例如:下面的列表未定义.

fix (\ (x:xs) -> 1:x:xs)

fix固定点组合子在哪里(例如从Data.Function).相比之下,这个其他列表1永远重复:

fix (\ ~(x:xs) -> 1:x:xs)

这是因为在1列表x和之间分割之前生成了xs.

为什么强制脊椎中的第一项会触发问题？

在推理关于递归方程时,如

x = f x

它通常有助于x将值视为"接近"的值

undefined
f undefined
f (f undefined)
f (f (f undefined))
...

(通过一些指称语义和Kleene的不动点定理,可以使上述直觉变得精确.)

例如,等式

x = 1 : x

定义序列的"限制"

undefined
1 : undefined
1 : 1 : undefined
...

这显然收敛于重复列表.

当使用模式匹配来定义递归值时,等式变为例如

(y:ys) = 1:y:ys

由于模式匹配,转换为

x = case x of (y:ys) -> 1:y:ys

让我们考虑它的近似序列

undefined
case undefined of (y:ys) -> ....   = undefined
case undefined of (y:ys) -> ....   = undefined
...

在第二步,case分歧,使结果仍然undefined.序列不接近预期的"重复的"列表,但是不断undefined.

相反,使用惰性模式

x = case x of ~(y:ys) -> 1:y:ys

我们获得了序列

undefined
case undefined of ~(y:ys) -> 1:y:ys 
    = 1 : (case undefined of (y:_) -> y) : (case undefined of (_:ys) -> ys)
    = 1 : undefined : undefined      -- name this L1
case L1 of ~(y:ys) -> 1:y:ys
    = 1 : (case L1 of (y:_) -> y) : (case L1 of (_:ys) -> ys)
    = 1 : 1 : undefined : undefined  -- name this L2
case L2 of ~(y:ys) -> 1:y:ys
    = 1 : (case L2 of (y:_) -> y) : (case L2 of (_:ys) -> ys)
    = 1 : 1 : 1 : undefined : undefined

它会收敛到预期的列表.请注意,如果不case及早评估参数,那么懒惰模式是如何"向前推进"的.这就是他们懒惰的原因.以这种方式,在1执行模式匹配之前产生,使得递归定义的实体的结果不重要.