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

Question

我正在尝试根据作业做这道题：

Given arbitrary foo :: [[a]] -> ([a], [a]), write down one law that the function foo satisfies, involving map on lists and pairs.

一些背景信息：我是一年级的本科生，正在学习函数式编程课程。虽然这门课程是介绍性的，但讲师提到了教学大纲中的许多内容，其中包括自由定理。因此，在尝试阅读 Wadler 的论文后，我认为 concat :: [[a]] -> [a] 与定律 map f . concat = concat . map (map f) 看起来与我的问题相关，因为我们必须有 foo xss = (concat xss, concat' xss) 其中 concat 和 concat' 是 [[a]] -> [a] 类型的任何函数。那么foo满足bimap (map f, map g) . foo = \xss -> ((fst . foo . map (map f)) xss, (snd . foo . map (map g)) xss).

这个 'law' 似乎太长了，不正确，我也不确定我的逻辑。所以我想到了使用 online free theorems generator，但我不明白 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

如果 R1 和 R2 是关系（例如，A_i 和 B_i 之间的 R_i，以及 i in {1,2}），则 lift{(,)}(R1,R2)是"lifted"关系对，介于A1 * A2和B1 * B2之间，*表示乘积（在Haskell中写成(,)） .

在生命关系中，两对(x1,x2) :: A1*A2和(y1,y2) :: B1*B2相关当且仅当x1 R1 y1和x2 R2 y2。在您的例子中，R1 和 R2 是函数 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 中我们需要使用 newtype 来定义一个仿函数实例，但我会忽略它，因为这是无关紧要的）。在这种常见情况下，自由定理有一个非常好的形式：对于每个 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).

Answer 2

与@chi 的回答相同，但仪式较少：

把函数前后的a改成b都没有关系（只要你用一个fmap-喜欢做的事）。

For any f : a -> b,

    [[a]] ------------->   [[b]]
      |    (map.map) f       |
      |                      |
     foo                    foo
      |                      |
      v                      v
    ([a],[a]) ---------> ([b],[b])
              bimap f f

commutes.

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

Law for type [[a]] -> ([a], [a])

haskell

free-theorem