8

我正在尝试从我的作业中做这个问题：

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

一些背景：我是一年级本科生，正在学习函数式编程课程。虽然这门课程是介绍性的，但讲师在教学大纲中提到了许多内容，其中包括自由定理。因此，在尝试阅读 Wadler 的论文后，我认为concat :: [[a]] -> [a]法律map 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正确推导出函数的定律？

4

2 回答 2

5

如果R1和R2是关系（例如，R_i在A_i和之间B_i，与i in {1,2}），那么lift{(,)}(R1,R2)是“提升”的关系对，在A1 * A2和之间B1 * B2，与*表示乘积（用(,)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)

甚至，无点风格：

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上面的两个 s 实际上是在不同的类型上实例化的，因此要使类型与其余的一致。

在您的特定情况下，因为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)。

于 2019-12-15T22:45:27.303 回答
2

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

a在函数之前或之后将 s 更改为s都没有关系b，你得到相同的东西（只要你使用类似fmap的东西来做）。

对于任何 f : a -> b,

    [[a]] -------------> [[b]]
      | (map.map) f |
      | |
     富富
      | |
      vv
    ([a],[a]) ---------> ([b],[b])
              双映射 ff

通勤。
于 2019-12-18T07:50:33.663 回答