类型 [[a]] -> ([a], [a]) 的法则

Question

我试图从我的作业中回答这个问题：

给定任意foo :: [[a]] -> ([a], [a])，写出函数foo满足的一条定律，涉及map到列表和对。

一些背景：我是一名学习函数式编程课程的一年级本科生。虽然这门课程比较入门，但讲师在教学大纲中提到了很多东西，其中包括自由定理。因此，在尝试阅读 Wadler 的论文后，我认为concat :: [[a]] -> [a]with the lawmap f . concat = concat . map (map f)看起来与我的问题相关，因为我们必须具有foo xss = (concat xss, concat' xss)whereconcat和concat'are 类型的任何函数[[a]] -> [a]。然后foo满足bimap (map f, map g) . foo = \xss -> ((fst . foo . map (map f)) xss, (snd . foo . map (map g)) xss)。

这个“法律”似乎太长了，不正确，我也不确定我的逻辑。所以我想使用在线免费定理生成器，但我不明白是什么lift{(,)}意思：

forall t1,t2 in TYPES, g :: t1 -> t2.
 forall x :: [[t1]].
  (f x, f (map (map g) x)) in lift{(,)}(map g,map g)

lift{(,)}(map g,map g)
  = {((x1, x2), (y1, y2)) | (map g x1 = y1) && (map g x2 = y2)}

我应该如何理解这个输出？我应该如何foo正确推导出函数的规律？

Answer 1

如果R1andR2是关系（比如，R_i在A_iand之间B_i，with i in {1,2}），那么lift{(,)}(R1,R2)是“提升”的关系对， betweenA1 * A2和B1 * B2， with*表示乘积（用(,)Haskell编写）。

在生命关系中，两对(x1,x2) :: A1*A2和(y1,y2) :: B1*B2相关当且仅当x1 R1 y1和x2 R2 y2。在你的情况下，R1andR2是 functions map g, map g，所以提升也成为一个函数：y1 = map g x1 && y2 = map g x2。

因此，生成的

(f x, f (map (map g) x)) in lift{(,)}(map g,map g)

方法：

fst (f (map (map g) x)) = map g (fst (f x))
AND
snd (f (map (map g) x)) = map g (snd (f x))

或者，换句话说：

f (map (map g) x) = (map g (fst (f x)), map g (snd (f x)))

我会写成，使用Control.Arrow：

f (map (map g) x) = (map g *** map g) (f x)

甚至，在 pointfree 风格：

f . map (map g) = (map g *** map g) . f

这并不奇怪，因为你f可以写成

f :: F a -> G a
where F a = [[a]]
      G a = ([a], [a])

和F,G是函子（在 Haskell 中，我们需要使用 anewtype来定义函子实例，但我将省略它，因为它无关紧要）。在这种常见情况下，自由定理有一个非常好的形式：对于每个g,

f . fmap_of_F g = fmap_of_G g . f

这是一种非常好的形式，称为自然性（f可以解释为合适类别中的自然变换）。注意，f上面的两个实际上是在不同的类型上实例化的，所以要使类型与其余的一致。

在您的特定情况下，因为F a = [[a]]，它是[]函子与自身的组合，因此我们（不出所料）得到fmap_of_F g = fmap_of_[] (fmap_of_[] g) = map (map g).

相反，G a = ([a],[a])是函子[]和H a = (a,a)（从技术上讲，与乘积函子组成的对角函子）的组合。我们有fmap_of_H h = (h *** h) = (\x -> (h x, h x))，从中fmap_of_G g = fmap_of_H (fmap_of_[] g) = (map g *** map g).