haskell - 为什么 fmap 必须映射 List 的每个元素？

Question

看过书Learn you a Haskell For Great Good ，以及非常有用的 wiki 书籍文章 Haskell Category Theory这帮助我克服了常见的类别错误 of confusing category objects with the programming objects ，我还有以下问题:

为什么一定要fmap映射列表的每个元素？

我喜欢它，我只是想了解这在理论上是如何合理的。 (或者也许更容易证明使用 HoTT 的合理性？)

在 Scala 表示法中，List是一个仿函数，它接受任何类型并将其映射到所有列表类型集合中的一个类型，例如它映射类型 Int到类型 List[Int]并将函数映射到 Int例如

Int.successor: Int => Int至Functor[List].fmap(successor) : List[Int] => List[Int]

Int.toString: Int => String至Functor[List].fmap(toString): List[Int] => List[String]

现在 List[X] 的每个实例是具有 empty function 的幺半群( mempty 在 Haskell 中)和 combine function ( mappend 在 Haskell 中)。我的猜测是，人们可以使用 List 是 Monoids 这一事实来证明 map必须映射列表的所有元素。我的感觉是，如果添加 pure function from Applicative ，这给了我们一个列表，其中只有一个其他类型的元素。例如 Applicative[List[Int]].pure(1) == List(1) .由于 map(succ)在这些元素上为我们提供了下一个元素的单例列表，这涵盖了所有这些子集。然后我想 combine所有这些单例上的函数为我们提供了列表的所有其他元素。不知何故，我认为这限制了 map 的工作方式。

另一个暗示性的论点是 map必须在列表之间映射函数。由于 List[Int] 中的每个元素是 Int 类型，如果一个映射到 List[String]必须映射其中的每个元素，否则将不是正确的类型。

因此，这两个论点似乎都指向了正确的方向。但我想知道剩下的路需要什么。

反例？

为什么这不是反例 map 函数？

def map[X,Y](f: X=>Y)(l: List[X]): List[Y] = l match {
  case Nil => Nil
  case head::tail=> List(f(head))
}

似乎遵守规则

val l1 = List(3,2,1)
val l2 = List(2,10,100)

val plus2 = (x: Int) => x+ 2
val plus5 = (x: Int) => x+5

map(plus2)(List()) == List()
map(plus2)(l1) == List(5)
map(plus5)(l1) == List(8)

map(plus2 compose plus5)(l1) == List(10)
(map(plus2)_ compose map(plus5)_)(l1) == List(10)

啊。但它不符合身份证法。

def id[X](x: X): X = x

map(id[Int] _)(l1) == List(3)
id(l1) == List(3,2,1)

Answer 1

这依赖于称为“参数性”的理论结果，该结果首先由雷诺兹定义，然后由瓦德勒(以及其他人)开发。也许关于这个主题最著名的论文是 "Theorems for free!"由瓦德勒。

关键思想是，仅从函数的多态类型，我们可以得到一些关于函数语义的信息。例如:

foo :: a -> a

仅从这种类型，我们可以看出，如果 foo终止，它是恒等函数。直观地说， foo无法区分不同 a s 因为在 Haskell 中我们没有例如Java的 instanceof它可以检查实际的运行时类型。相似地，

bar :: a -> b -> a

必须返回第一个参数。和 baz :: a -> a -> a必须返回第一个或第二个。和 quz :: a -> (a -> a) -> a必须将函数应用于第一个参数的固定次数。你现在可能明白了。

可以从类型推断出的一般属性非常复杂，但幸运的是它可以计算出 mechanically .在范畴论中，这与 natural transformation 的概念有关。 .

对于 map类型，我们得到以下可怕的属性:

forall t1,t2 in TYPES, f :: t1 -> t2.
 forall t3,t4 in TYPES, g :: t3 -> t4.
  forall p :: t1 -> t3.
   forall q :: t2 -> t4.
    (forall x :: t1. g (p x) = q (f x))
    ==> (forall y :: [t1].
          map_{t3}_{t4} g (map2_{t1}_{t3} p y) =
          map2_{t2}_{t4} q (map_{t1}_{t2} f y))

以上， map是众所周知的 map 函数，而 map2是任何类型为 (a -> b) -> [a] -> [b] 的任意函数.

现在，进一步假设 map2满足仿函数定律，特别是 map2 id = id .然后我们可以选择 p = id和 t3 = t1 .我们得到

forall t1,t2 in TYPES, f :: t1 -> t2.
 forall t4 in TYPES, g :: t1 -> t4.
   forall q :: t2 -> t4.
    (forall x :: t1. g x = q (f x))
    ==> (forall y :: [t1].
          map_{t1}_{t4} g (map2_{t1}_{t1} id y) =
          map2_{t2}_{t4} q (map_{t1}_{t2} f y))

在 map2 上应用仿函数定律:

forall t1,t2 in TYPES, f :: t1 -> t2.
 forall t4 in TYPES, g :: t1 -> t4.
   forall q :: t2 -> t4.
    (forall x :: t1. g x = q (f x))
    ==> (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t2}_{t4} q (map_{t1}_{t2} f y))

现在，让我们选择 t2 = t1和 f = id :

forall t1 in TYPES.
 forall t4 in TYPES, g :: t1 -> t4.
   forall q :: t1 -> t4.
    (forall x :: t1. g x = q x)
    ==> (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t1}_{t4} q (map_{t1}_{t1} id y))

由 map 的仿函数定律:

forall t1, t4 in TYPES.
   forall g :: t1 -> t4, q :: t1 -> t4.
    g = q
    ==> (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t1}_{t4} q y)

意思是

forall t1, t4 in TYPES.
 forall g :: t1 -> t4.
    (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t1}_{t4} g y)

意思是

forall t1, t4 in TYPES.
          map_{t1}_{t4} = map2_{t1}_{t4}

加起来:

如果 map2是任何具有多态类型的函数 (a -> b) -> [a] -> [b] , 并且满足第一仿函数定律 map2 id = id ，然后 map2必须等同于标准 map功能。

另见 related blog post by Edward Kmett .

请注意，在 Scala 中，仅当您不使用 x.isInstanceOf[] 时，上述内容才成立。和其他反射工具，它们可以破坏参数化。