fmap 的自由定理

如何解决fmap 的自由定理

考虑以下包装器：

newtype F a = Wrap { unwrap :: Int }

我想反驳（作为围绕 this interesting post 的练习）存在一个合法的 Functor F 实例，它允许我们将 Int -> Int 类型的函数应用于实际内容，并且~忽略~所有其他函数（即fmap nonIntInt = id）。

我相信这应该通过 fmap 的自由定理来完成（我读过 here）： 对于给定的 f、g、h 和 k，使得 g . f = k . h：$map g . fmap f = fmap k . $map h，其中 $map 是 给定构造函数的>自然贴图。

什么定义了自然地图？我认为它是 flip const 的简单 F 是否正确？

据我所知：$map f 是我们在范畴论中表示为 Ff 的东西。因此，在绝对意义上，我们只是希望下图中的线之间有一些东西可以通勤：

然而，我不知道用什么来代替 ???（也就是说，我们应用什么函子来得到这样的图以及我们如何表示这个几乎-fmap ？）。

那么，对于F，一般来说什么是自然地图？ fmap 的自由定理的正确图表是什么？

---

我要去哪里？

考虑：

f = const 42
g = id

h    = const ()
k () = 42

很容易看出 f . g 是 h . k。然而，不存在的 fmap 只会执行 f，而不是 k，从而产生不同的结果。如果我对自然性的直觉是正确的，那么这样的证明就行了。这就是我想弄清楚的。

@leftaroundabout 提出了一个更简单的证明：与 fmap show . fmap (+1) 不同，fmap $ show . (+1) 改变了内容。这是一个很好的证明，但我仍然想将自由定理作为练习。

解决方法

所以我们正在娱乐一个函数 m :: forall a b . (a->b) -> F a -> F b 使得（除其他外）

m (1 +)    (Wrap x) = (Wrap (1+x))
m (show)   (Wrap x) = (Wrap x)

这里有两个相关的问题。

1. 一个乖巧的fmap能做到这一点吗？
2. 参数函数可以做到这一点吗？

这两个问题的答案都是“否”。

行为良好的 fmap 不能这样做，因为 fmap 必须遵守 Functor 的公理。我们的环境是否参数化无关紧要。 Functor 的公理表示，对于所有函数 a 和 b，fmap (a . b) = fmap a . fmap b 必须成立，而这对于 a = show 和 b = (1 +) 失败。所以m不可能是一个乖巧的fmap。

参数函数不能这样做，因为参数定理就是这样说的。当将类型视为术语之间的关系时，相关函数将相关参数用于相关结果。很容易看出 m 参数化失败，但查看 m': forall a b. (a -> b) -> (Int -> Int) 稍微容易一些（两者可以简单地相互转换）。 (1 +) 与 show 相关，因为 m' 的参数是多态的，因此参数的不同值可以通过 any 关系相关联。函数是关系，并且存在一个将 (1 +) 发送到 show 的函数。但是m'的结果类型没有类型变量，所以对应的是常量关系（它的值只和自己相关）。由于包括 m' 在内的每个值都与自身相关，因此所有参数函数 m :: forall a b. (a -> b) -> (Int -> Int) 必须服从 m f = m g，即它们必须忽略它们的第一个参数。这在直觉上很明显，因为没有什么可应用的。

事实上，通过观察行为良好的 fmap 必须是参数化的，可以从第二个陈述中推断出第一个陈述。因此，即使该语言允许非参数化，fmap 也不能对其进行任何非平凡的使用。