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

Question

阅读了这本书,了解了一本Haskell For Great Good,以及非常有用的维基书籍Haskell分类理论帮助我克服了将类别对象与编程对象混淆的常见类别错误,我仍然有以下问题:

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

我喜欢它,我只想理解这在理论上是如何合理的.(或者更容易证明使用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函数(mempty在Haskell中)和combine函数(mappend在Haskell中)的monoid .我的猜测是,人们可以使用列表是Monoids的事实,以表明map必须映射列表的所有元素.我的感觉是,如果添加了pureApplicative的函数,这给了我们一个只包含其他类型元素的列表.例如Applicative[List[Int]].pure(1) == List(1).因为map(succ)在这些元素上给我们带有下一个元素的单例列表,所以这涵盖了所有这些子集.然后我想combine所有这些单身人士的功能都会给我们列出所有其他元素.不知怎的,我想这限制了地图的工作方式.

另一个暗示性的论点是map必须在列表之间映射函数.由于a中的每个元素List[Int]都是Int类型,并且如果一个映射到List[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)

啊.但它不符合id法.

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

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

Answer 1

这依赖于称为"参数化"的理论结果,首先由雷诺兹定义,然后由瓦德勒(以及其他人)开发.也许关于这个主题的最着名的论文是"免费的定理!" 由瓦德勒.

其核心思想是,从多态类型的函数的唯一,我们可以得到关于函数的语义的一些信息.例如:

foo :: a -> a

仅从这种类型,我们可以看到,如果foo终止,它就是身份功能.直观地说,foo无法区分不同的as,因为在Haskell中我们没有例如instanceof可以检查实际运行时类型的Java .同样的,

bar :: a -> b -> a

必须返回第一个参数.并且baz :: a -> a -> a必须返回第一个或第二个.并且quz :: a -> (a -> a) -> 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].

现在,进一步假设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函数.

另请参阅Edward Kmett撰写的相关博客文章.

请注意,在Scala中,只有在不使用x.isInstanceOf[]和其他可能破坏参数的反射工具时,上述情况才会成立.