看过书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)
最佳答案
这依赖于称为“参数性”的理论结果,该结果首先由雷诺兹定义,然后由瓦德勒(以及其他人)开发。也许关于这个主题最著名的论文是 "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[]
时,上述内容才成立。和其他反射工具,它们可以破坏参数化。
关于haskell - 为什么 fmap 必须映射 List 的每个元素?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36715851/