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

问题描述 投票：11回答：1

阅读了本书Learn you a Haskell For Great Good，以及帮助我​​克服常见类别错误Haskell Category Theory的非常有用的维基书籍文章of confusing category objects with the programming objects，我仍然有以下问题：

为什么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 function（Haskell中的mempty）和combine function（Haskell中的mappend）的幺半群。我的猜测是，人们可以使用列表是Monoids的事实，以表明map必须映射列表的所有元素。我的感觉是，如果添加pure function from Applicative，这给了我们一个列表，只有一个其他类型的元素。例如Applicative[List[Int]].pure(1) == List(1)。由于这些元素上的map(succ)为我们提供了包含下一个元素的单例列表，因此这涵盖了所有这些子集。然后我想所有那些单身人士的combine函数给了我们列表中的所有其他元素。不知怎的，我想这限制了地图的工作方式。

另一个有争议的论点是，map必须在列表之间映射函数。由于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)
haskell functor scalaz category-theory scala-cats
1个回答
11
投票

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

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

foo :: a -> a

仅从这种类型，我们可以看到，如果foo终止，它就是身份函数。直觉上，foo无法区分不同的as，因为在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是众所周知的地图函数，而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[]和其他可能破坏参数的反射工具时，上述情况才会成立。

最新问题
© www.soinside.com 2019 - 2024. All rights reserved.