什么是函数的右/左反？

Question

Benjamin Pierce在他的"软件基础"一书中指出了这一点

该函数split是正确的逆combine

这里split是unzip和combine是zip.我想知道函数的"正逆"是什么意思,如果还有一个左逆zip.

Answer 1

r是fif f . r是身份函数(其中.表示组成)的右反.

l是fif l . f是身份函数的左逆.

在这里,他正在滥用命名,因为函数combine不作为输入对列表,而是分别考虑每个列表.

之所以split是逆的combine,而不是完全逆,是因为combine如果它们的大小不同,该函数会丢弃其输入列表之一的元素.从这个意义上说,split失去了combine无法生产的信息.

也就是说,如果你从:

l1 = [1]
l2 = [2; 3; 4]

然后:

combine l1 l2 = [(1, 2)]

和:

split (combine l1 l2) = ([1], [2])

由于只是放弃了元素并且不存在split,combine所以没有办法成为左逆.combine34

另一方面,对于任何对的列表lp:

let (l1, l2) := split lp in combine l1 l2
= lp

((combine . split) lp = lp如果combine把一对作为输入,你可以写它)