Haskell:函数应用程序在列表连接上分布是真的吗?

不,这显然不是事实:

f [_] = []
f l = l

然后

f ([1] ++ [2]) = f [1,2] = [1,2]

但是

f [1] ++ f [2] = [] ++ [] = []

我确信确实存在这个问题的函数形成了一个有趣的类,但一般函数可以对列表结构做任何事情,从而阻止这种不变量。

在看了 forall xs ys. length (xs ++ ys) = length xs + length ys 来自哈斯克尔音乐学院(第164页)。

在我看来,函数应用程序分布在列表连接上。

很明显,事实并非如此。例如:

reverse ([1..3] ++ [4..6]) /= reverse [1..3] ++ reverse [4..6]

你引用的例子是一个特殊情况,称为 幺半态射 :a函数 f :: m -> n 这样:

1. m 和 n 是具有二进制运算的幺半群 <> 和身份 mempty ;
2. f mempty = mempty
3. f (m <> m') == f m <> f m'

所以 length :: [a] -> Int 是幺半态射,发送 [] 到 0 和 ++ 到 + :

length [] = 0
length (xs ++ ys) = length xs + length ys