纯净的独特性
对于任何Applicative实例，一旦<*>写入，pure是唯一确定的。假设您有pure1和pure2，两者都遵守法律。然后
pure2 f <*> pure1 y = pure1 ($ y) <*> pure2 f -- interchange for pure1
pure2 id <*> pure1 y = pure1 ($ y) <*> pure2 id -- specialize f to id
pure1 y = pure1 ($ y) <*> pure2 id -- identity for pure2
pure1 y = fmap ($ y) (pure2 id) -- applicative/fmap law for pure1
pure1 y = pure2 ($ y) <*> pure2 id -- applicative/fmap law for pure2
pure1 y = pure2 y -- homomorphism law
但以fmap这种方式使用法律感觉就像是在作弊。有没有办法在不诉诸参数的情况下避免这种情况？
回答
当前文档中给出的法律确实依赖于参数连接到fmap.
没有参数化，我们就失去了这种联系，因为我们甚至无法证明 的唯一性fmap，而且确实存在系统 F 的模型/扩展，其中fmap不是唯一的。
打破参数性的一个简单示例是添加 type-case（类型上的模式匹配），这允许您定义以下内容twist，检查其参数的类型并翻转它找到的任何布尔值：
twist :: forall a. a -> a
twist @Bool = not
twist @(a -> b) = f -> (x -> twist @b (f (twist @a x)))
twist @a = id -- default case
它具有多态恒等式的类型，但它是not恒等函数。
然后，您可以定义以下“扭曲身份”函子，其中pure适用twist于其参数：
newtype I a = I { runI :: a }
pure :: a -> I a
pure = I . twist
(<*>) :: I (a -> b) -> I a -> I b -- The usual, no twist
(<*>) (I f) (I x) = I (f x)
的一个关键属性twist是twist . twist = id。这允许它在组合使用嵌入的值时与自身抵消pure，从而保证的四个定律Control.Applicative。（Coq 中的证明草图）
这个扭曲的函子也产生了不同的定义fmap，如u -> pure f <*> u。展开定义：
fmap :: (a -> b) -> I a -> I b
fmap f (I x) = I (twist (f (twist x)))
这与 duplode 的答案并不矛盾，后者将幺半群恒等唯一性的通常论证转化为幺半群函子的设置，但它破坏了它的方法。问题是该视图假设您已经有一个给定的函子并且幺半群结构与其兼容。特别是，法律fmap f u = pure f <*> u隐含于定义pure为x -> fmap (const x) funit（以及(<*>)相应地）。如果您fmap首先没有解决问题，那么这个论点就会失效，因此您没有任何可依赖的连贯法则。
回答
让我们切换到 applicative 的幺半群函子表示：
funit :: F ()
fzip :: (F a, F b) -> F (a, b)
fzip (funit, v) ~ v
fzip (u, funit) ~ u
fzip (u, fzip (v, w)) ~ fzip (fzip (u, v), w)
如果我们专门研究aand bto ()（并忽略元组同构），定律会告诉我们这一点funit并fzip指定一个幺半群。因为幺半群的身份是唯一的，所以funit是唯一的。对于通常的Applicative类，pure然后可以恢复为...
pure a = fmap (const a) funit
......这也是独一无二的。虽然原则上尝试将这种推理扩展到至少一些不完全参数化的函子是有意义的，但这样做可能需要在很多地方做出妥协：
-
()作为一个对象，定义funit和陈述幺半群函子定律的可用性； -
用于定义的 map 函数的唯一性
pure（另请参见Li-yao Xia 的回答），或者，如果不这样做，以某种方式唯一指定fmap . const类似物的明智方法； -
函数类型作为对象的可用性，为了用 来说明
Aplicative规律(<*>)。