问题描述
考虑以下包装器:
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)
这里有两个相关的问题。
- 一个乖巧的
fmap
能做到这一点吗? - 参数函数可以做到这一点吗?
这两个问题的答案都是“否”。
行为良好的 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
也不能对其进行任何非平凡的使用。