纯净的独特性

如何解决纯净的独特性

对于任何 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 不是唯一的。

打破参数化的一个简单示例是添加类型大小写（类型的模式匹配），这允许您定义以下 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 嵌入的值时与自身抵消，从而保证 the four laws of Control.Applicative。 (Proof sketch in 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)

如果我们将 a 和 b 特化为 ()（并查看元组同构），定律告诉我们funit 和 fzip 指定了一个幺半群。由于幺半群的身份是唯一的，funit 是唯一的。对于通常的 Applicative 类，pure 然后可以恢复为...

pure a = fmap (const a) funit

... 这也是独一无二的。虽然原则上尝试将这种推理扩展到至少一些不完全参数化的函子是有意义的，但这样做可能需要在很多地方做出妥协：

• () 作为对象的可用性，用于定义 funit 并说明幺半群函子定律；

• 用于定义 pure 的 map 函数的唯一性（另见 Li-yao Xia's answer），或者，如果不这样做，以某种方式唯一指定 fmap . const 类似物的明智方法；

• 函数类型作为对象的可用性，为了说明 Aplicative 方面的 (<*>) 定律。