Haskell:函数应用程序是否通过列表串联进行分配?

CMC*_*kai 1 haskell functional-programming proof

读完这个问题后:功能证明(Haskell)

在查看forall xs ys. length (xs ++ ys) = length xs + length ys了Haskell音乐学院的归纳证明之后(第164页).

在我看来,函数应用程序分布在列表串联上.

因此,更普遍的法律可能就是这样forall f xs ys. f (xs ++ ys) = f xs ++ f ys.

但是,如何证明/反驳这样的谓词呢?

- 编辑 -

我写了一个错字:forall f xs ys. f (xs ++ ys) = f xs + f ys它与上一个问题和Haskell SoM使用的内容相匹配.话虽如此,由于这个错字,它不再是"分配"财产.然而,@ leftaroundabout为我原来的错字问题做出了正确答案.至于我的预期问题,法律仍然不正确,因为功能不需要保留结构价值.将f可能给依赖于它应用到列表的长度完全不同的答案.

lef*_*out 8

不,这一般显然不正确:

f [_] = []
f l = l
Run Code Online (Sandbox Code Playgroud)

然后

f ([1] ++ [2]) = f [1,2] = [1,2]
Run Code Online (Sandbox Code Playgroud)

f [1] ++ f [2] = [] ++ [] = []
Run Code Online (Sandbox Code Playgroud)

我确定有这个问题的函数构成了一个有趣的类,但是一般函数可以对列表的结构做很多事情,这会阻止这样的不变量.

  • 为了记录,这些函数被称为[同态](https://ncatlab.org/nlab/show/homomorphism)(在这种情况下是岩浆同态). (4认同)