foldr1的融合法？

Question

因为foldr我们有融合法:如果f是严格的f a = b,和

f (g x y) = h x (f y)对所有人来说x, y,那么f . foldr g a = foldr h b.

如何发现/得出类似的法律foldr1？(它显然甚至不能采取相同的形式 - 考虑双方采取行动的情况[x].)

Answer 1

您可以使用自由定理来推导融合定律等语句.该自动生成的自由定理做这个工作对你来说,它会自动导出,如果你输入下面的语句foldr1或类型(a -> a -> a) -> [a] -> a.

如果f严格而且f (p x y) = q (f x) (f y))对所有人x而且y你有f (foldr1 p z) = foldr1 q (map f z)).也就是说,与你的声明形成鲜明对比的是你在右侧foldr获得了额外的补充map f.

还要注意,自由定理foldr比你的融合定律略微更普遍,因此看起来非常类似于法则foldr1.即你有严格的功能g和f是否g (p x y) = q (f x) (g y))所有x和y再g (foldr p z v) = foldr q (g z) (map f v)).