为什么fmap必须映射列表的每个元素？

Question

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

• Int.extinent:Int=>Int到函式[List].fmap（extinente):List[Int]=>List[Int]
• Int.toString:Int=>String到函式[List].fmap（toString）:List[Int]=>List[String]

现在，list[X]的每个实例都是一个monoid，具有empty函数（在Haskell中为mempty)和combine函数（在Haskell中为mappend)。我的猜测是，可以使用列表是单ID这一事实来说明map必须映射列表的所有元素。我在这里的感觉是，如果从Applicative中添加pure函数，就会得到一个列表，其中只有一个其他类型的元素。例如application[List[Int]].pure(1)==List(1)。由于这些元素上的map(succ)为我们提供了包含下一个元素的单例列表，因此它涵盖了所有这些子集。那么，我想所有这些单例的combine函数将为我们提供列表的所有其他元素。不知何故，我想这限制了地图的工作方式。

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

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

反例？

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

这依赖于一个叫做“参数性”的理论结果，首先由雷诺定义，然后由Wadler（和其他人）发展。也许关于这个主题最著名的论文是“免费的定理！”Wadler的。

其核心思想是只从函数的多态类型中获取函数的语义信息。例如：

foo :: a -> a

仅从这个类型中，我们可以看到，如果foo终止，它就是标识函数。直观地说，foo不能区分不同的A，因为在Haskell中我们没有例如Java的instanceof，它可以检查实际的运行时类型。同样，

bar :: a -> b -> a

可以从一个类型中推断出的一般性质是相当复杂的，但幸运的是，它可以机械地计算出来。在范畴理论中，这与自然转化的概念有关。

对于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]类型的任意函数。

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))

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))

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}